Require Import Lia.
Require Import Bool.
Require Import Arith.

Module Invariants.

  (** Invariant I1: Existence does not imply permission (Ambient authority stripped) *)
  Record Capability := {
    cap_id : nat;
    is_explicit : bool;
    is_valid : bool;
  }.

  Definition check_I1 (c : Capability) : bool :=
    c.(is_explicit) && c.(is_valid).

  Theorem I1_soundness : forall c : Capability,
    check_I1 c = true -> c.(is_explicit) = true /\ c.(is_valid) = true.
  Proof.
    intros c H.
    apply andb_true_iff in H.
    exact H.
  Qed.

  (** Invariant I2: Monotonic convergence under join-semilattice properties *)
  Record State := {
    admissibility_level : nat;
  }.

  Definition join (s1 s2 : State) : State :=
    {| admissibility_level := Nat.max s1.(admissibility_level) s2.(admissibility_level) |}.

  Theorem I2_monotonicity : forall s1 s2 : State,
    s1.(admissibility_level) <= (join s1 s2).(admissibility_level).
  Proof.
    intros s1 s2.
    unfold join. simpl.
    lia.
  Qed.

  (** Invariant I3: Fixed execution bounds *)
  Parameter tau_override_ms_x100 : nat. (* 1199 = 11.99 ms *)
  Parameter stack_bound_bytes : nat.     (* 4096 B *)
  Parameter heap_alloc_allowed : bool.   (* false *)

  Axiom tau_ceiling : tau_override_ms_x100 <= 1199.
  Axiom stack_ceiling : stack_bound_bytes <= 4096.
  Axiom zero_heap : heap_alloc_allowed = false.

End Invariants.