text:
Require Import Reals Psatz.
From mathcomp Require Import ssrfun ssreflect eqtype ssrbool seq fintype choice.
From discprob.basic Require Import base sval order monad bigop_ext nify.
From discprob.prob Require Import prob countable finite stochastic_order.
From discprob.monad.idxval Require Import pival_dist pival ival_dist ival ival_pair pidist_singleton.

(*
Definition subset_couplingP {A1 A2} (Is1: pidist A1) (Is2: pidist A2) (P: A1 → A2 → Prop) :=
  ∀ (I1: ival A1), In (I1 : ival A1) Is1 →
  { I2 : { I2: ival A2 | In (I2 : ival A2) Is2 } & ival_couplingP I1 (sval I2) P }.
*)

Definition subset_couplingP {A1 A2} (Is1: pidist A1) (Is2: pidist A2) (P: A1 → A2 → Prop) : Prop :=
  ∀ (I1: ival A1), pival.In (I1 : ival A1) Is1 →
  ∃ (I2: ival A2), pival.In (I2 : ival A2) Is2 ∧ ∃ (C: ival_couplingP I1 I2 P), True.

Lemma subset_coupling_eq {A} (Is1 Is2: pidist A)
      (Ic: subset_couplingP Is1 Is2 (λ x y, x = y)): le_pidist Is1 Is2.
Proof.
  intros I1 Hin.
  specialize (Ic (lift_In_pidist I1 Hin) Hin).
  destruct Ic as (I2&Hin2&(Hcouple&_)).
  exists I2; split; auto.
  eapply ival_coupling_eq in Hcouple; done.
Qed.

Lemma singleton_coupling_eq {A} (I1 : ivdist A) (Is2: pidist A)
      (Ic: subset_couplingP (singleton I1) Is2 (λ x y, x = y)): In_pidist I1 Is2.
Proof.
  by apply In_pidist_le_singleton, subset_coupling_eq.
Qed.

Lemma subset_coupling_bind {A1 A2 B1 B2} (f1: A1 → pidist B1) (f2: A2 → pidist B2)
      Is1 Is2 P Q (Ic: subset_couplingP Is1 Is2 P):
  (∀ x y, P x y → subset_couplingP (f1 x) (f2 y) Q) →
  subset_couplingP (mbind f1 Is1) (mbind f2 Is2) Q.
Proof.
  intros Hfc.
  intros I1 Hin.
  edestruct (pival_mbind_in_inv_idxOf Is1 f1 I1) as (I1_0&h1&Hin1_0&Hh1&Heq); auto.
  specialize (Ic I1_0 Hin1_0).
  destruct Ic as (I2_0&Hin2_0&(Hcouple&_)).
  apply ival_coupling_idxOf in Hcouple.
  destruct Hcouple as ((Rel&Hfunc)&[Ic_0 Hp1 Hp2]).
  apply ClassicalEpsilon.constructive_indefinite_description in Hp1.
  destruct Hp1 as (hidx1&Hp1).
  apply ClassicalEpsilon.constructive_indefinite_description in Hp1.
  destruct Hp1 as (hidx1'&?&?&Hind1&?).

  apply ClassicalEpsilon.constructive_indefinite_description in Hp2.
  destruct Hp2 as (hidx2&Hp2).
  apply ClassicalEpsilon.constructive_indefinite_description in Hp2.
  destruct Hp2 as (hidx2'&?&?&Hind2&?).

  unshelve (edestruct (pival_mbind_in_alt2_idxOf Is2 f2 I2_0) as (Ib&Heqb&Hinb)).
  { intros i2.
    destruct (Rgt_dec (val I2_0 i2) 0) as [Hgt|Hngt]; last (exact zero_ival).
    destruct (hidx2 (coerce_supp _ _ Hgt)) as ((i0&[])&Hgt0).
    destruct (ind Ic_0 i0) as ((i1&i2')&(HP&Hsup1&Hsup2)).
    specialize (Hfc _ _ HP (h1 i1) (Hh1 _ Hsup1)).
    apply ClassicalEpsilon.constructive_indefinite_description in Hfc.
    destruct Hfc as (I2&?).
    exact I2.
  }
  - exists I2_0; split; auto; reflexivity.
  - intros.
    simpl. destruct Rgt_dec as [r|?] => //=.
    specialize (Hind2 ((coerce_supp (val I2_0) i r))).
    destruct (hidx2) as ((i0&[])&Hgt0) => //=.
    rewrite //= in Hind2.
    case_eq (ind Ic_0 i0). intros (i1&i2') (HP&Hsup1&Hsup2&HQ) Heq0.
    rewrite Heq0. rewrite Heq0 in Hind2.
    destruct ClassicalEpsilon.constructive_indefinite_description as (?&?&?); auto.
    subst. done.
  - exists Ib; split; auto.
    unshelve (eexists); last done.
    eapply ival_coupling_proper.
    * eauto.
    * eauto.
    * eapply (ival_coupling_bind _ _ _ _
          (λ x y, P (ind I1_0 x) (ind I2_0 y) ∧ val I1_0 x > 0 ∧ val I2_0 y > 0 ∧ Rel x y)).
      { exists Ic_0. exists hidx1; eauto. exists hidx2; eauto.  }
      intros x y (HP&Hgtx&Hgty&HRel).
      destruct Rgt_dec as [r|?] => //=.
    specialize (Hind2 ((coerce_supp (val I2_0) y r))).
    destruct (hidx2) as ((i0&[])&Hgt0) => //=.
    rewrite //= in Hind2.
    case_eq (ind Ic_0 i0). intros (i1&i2') (HP'&Hsup1&Hsup2&HQ) Heq0.
    rewrite Heq0. rewrite Heq0 in Hind2.
      destruct ClassicalEpsilon.constructive_indefinite_description as (?&?&Hc).
      apply ClassicalEpsilon.constructive_indefinite_description in Hc as (Hc&?).
      cut (x = i1).
      { intros.  subst. auto. }
      eapply Hfunc.
      eauto. clear -HQ Hind2. rewrite //= in Hind2. rewrite -Hind2. rewrite //= in HQ.
Qed.

Lemma subset_coupling_le {X Y} Is1 Is1' Is2 Is2' (P: X → Y → Prop) :
  le_pidist Is1' Is1 →
  le_pidist Is2 Is2' →
  subset_couplingP Is1 Is2 P →
  subset_couplingP Is1' Is2' P.
Proof.
  intros Hle1 Hle2 Hsub.
  intros I1' Hin1'.
  destruct (Hle1 _ Hin1') as (I1&Heq&Hin1).
  destruct (Hsub _ Hin1) as (I2&Hin2&Hc&_).
  destruct (Hle2 _ Hin2) as (I2'&Heq2&Hin2').
  exists I2'; split; auto.
  eexists; last by done.
  eapply ival_coupling_proper; try eassumption.
    by symmetry.
Qed.

Lemma subset_coupling_proper {X Y} Is1 Is1' Is2 Is2' (P: X → Y → Prop) :
  eq_pidist Is1 Is1' →
  eq_pidist Is2 Is2' →
  subset_couplingP Is1 Is2 P →
  subset_couplingP Is1' Is2' P.
Proof.
  intros Heq1 Heq2. eapply subset_coupling_le; eauto.
  - setoid_rewrite Heq1; reflexivity.
  - setoid_rewrite Heq2; reflexivity.
Qed.

Lemma subset_coupling_support {X Y} I1 I2 (P: X → Y → Prop) :
  subset_couplingP I1 I2 P →
  subset_couplingP I1 I2 (λ x y, P x y ∧ In_psupport x I1 ∧ In_psupport y I2).
Proof.
  intros Hsub I Hin.
  edestruct (Hsub I Hin) as (I'&Hin'&Ic&_).
  exists I'; split; first done.
  unshelve (eexists); last done.
  eapply ival_coupling_conseq; last first.
  { apply (ival_coupling_support _ _ _ Ic). }
  intros x y (Hpf&Hin1&Hin2&?); repeat split; auto.
  - exists I; auto. edestruct Hin1; eexists; eauto.
  - exists I'; auto. edestruct Hin2; eexists; eauto.
Qed.

Lemma subset_coupling_plus {A1 A2} p Hpf p' Hpf'
      (P : A1 → A2 → Prop) (Is1 Is1': pidist A1) (Is2 Is2': pidist A2) :
  p = p' →
  subset_couplingP Is1 Is2 P →
  subset_couplingP Is1' Is2' P →
  subset_couplingP (pidist_plus p Hpf Is1 Is1') (pidist_plus p' Hpf' Is2 Is2') P.
Proof.
  intros Hp Hsub Hsub'.
  subst.
  intros I (I1&I1'&Hin1&Hin1'&Heq1)%pidist_plus_in_inv.
  subst.

  edestruct (Hsub _ Hin1) as (I2&Hin&Hequiv&?).
  edestruct (Hsub' _ Hin1') as (I2'&Hin'&Hequiv'&?).
  exists (iplus (iscale p' I2) (iscale (1 - p') I2')).
  split.
  - apply pplus_in; apply pscale_in; auto.
  - unshelve (eexists); auto.
    apply ival_coupling_plus'; auto.
Qed.

author: jtassarotti

repo: coq-proba

save_path: github-repos/coq/jtassarotti-coq-proba


text:
Require Import PeanoNat.

(* Strong induction on Natural numbers with properties sending to Type. *)

Theorem strong_induction:
forall P : nat -> Prop,
(forall n : nat, (forall k : nat, (k < n -> P k)) -> P n) ->
forall n : nat, P n.
Proof.
intros P H. assert (Lem : forall n, (forall m, m <= n -> P m)).
{ induction n. intros.
  - assert (E: m = 0). inversion H0.  reflexivity. rewrite E. apply H.
    intros. exfalso. inversion H1.
  - intros. apply H. intros. apply IHn. inversion H0.
    * rewrite H2 in H1. apply Nat.lt_succ_r. apply H1.
    * assert (E: k <= m). apply Nat.lt_le_incl. apply H1.
      apply Nat.le_trans with (m:=m). apply E. apply H3. }
intro n. apply H. intros. apply Lem with (n:=n) (m:=k).
apply Nat.lt_le_incl. apply H0.
Qed.

author: ianshil


text:
From Coq Require Import Morphisms.
From ITree Require Import
     Axioms
     ITree
     ITreeFacts
     Basics.HeterogeneousRelations
     Events.State
     Events.StateFacts.

From ITree.Extra Require Import
     Secure.SecureEqHalt
     Secure.SecureEqEuttHalt
     Secure.SecureEqWcompat
     Secure.SecureEqBind
     Secure.SecureEqProgInsens
     Secure.SecureEqProgInsensFacts
     Secure.StrongBisimProper
     Secure.SecureStateHandler
.

Import Monads.
Import MonadNotation.
Local Open Scope monad_scope.

From Paco Require Import paco.

Section GeneralStateHandler.

Context (S : Type).
Context (RS : S -> S -> Prop).
Context (RS_Eq: Equivalence RS).

Context (E1 E2 : Type -> Type).

Context (handler : E1 ~> stateT S (itree E2) ).

Context (Label : Preorder).
Context (priv1 : forall A, E1 A -> L).
Context (priv2 : forall A, E2 A -> L).
Context (l : L).

Definition state_pi_eqit_secure {R1 R2 : Type} (b1 b2 : bool) (RR : R1 -> R2 -> Prop)
           (m1 : stateT S (itree E2) R1) (m2 : stateT S (itree E2) R2) :=
  forall s1 s2, RS s1 s2 -> pi_eqit_secure Label priv2 (prod_rel RS RR) b1 b2 l (m1 s1) (m2 s2).

Definition top2 {R1 R2} (r1 : R1) (r2 : R2) : Prop := True.

Definition secure_in_nonempty_context {R} (m : stateT S (itree E2) R) :=
   forall r' : R, state_pi_eqit_secure true true top2 m (ret r').

Definition secure_in_empty_context  {R} (m : stateT S (itree E2) R) :=
   state_pi_eqit_secure true true (@top2 R R) m (fun s => ITree.spin).

Lemma diverges_with_spin : forall E A P,
    diverges_with P (@ITree.spin E A).
Proof.
  intros. pcofix CIH. pfold. red. cbn. constructor.
  right; auto.
Qed.

Lemma pi_eqit_secure_silent_divergel : forall A B RR (t1 : itree E2 A) (t2 : itree E2 B),
    diverges_with (fun _ e => ~ leq (priv2 _ e) l) t1 ->
    pi_eqit_secure Label priv2 RR true true l t1 t2.
Proof.
  intros A B RR. pcofix CIH. intros.
  punfold H0. all : try apply mono_diverges_with. red in H0.
  inversion H0; use_simpobs; try rewrite H; try rewrite H3.
  - pfold. constructor; auto. right. pclearbot. eapply CIH; eauto.
  - destruct (classic_empty B0).
    + eapply paco2_mon with (r := bot2); intros; try contradiction.
      apply pi_eqit_secure_sym.
      apply pi_eqit_secure_private_halt; auto.
    + pfold. red. cbn. constructor; auto. right. pclearbot. eapply CIH; eauto.
      apply H1.
 Qed.

Lemma pi_eqit_secure_silent_diverger : forall A B RR (t1 : itree E2 A) (t2 : itree E2 B),
    diverges_with (fun _ e => ~ leq (priv2 _ e) l) t2 ->
    pi_eqit_secure Label priv2 RR true true l t1 t2.
Proof.
  intros. apply pi_eqit_secure_sym. apply pi_eqit_secure_silent_divergel; auto.
Qed.

Lemma silent_terminates_eqit_secure_ret : forall R (m : stateT S (itree E2) R), nonempty R ->
      (forall s, terminates S RS E2 s (fun B e => ~ leq (priv2 _ e) l /\ nonempty B) (m s) ) -> forall r' : R, state_pi_eqit_secure true true top2 m (ret r').
Proof.
  red. intros. specialize (H0 s1).
  cbn. induction H0.
  - pfold; constructor. split; try constructor. cbn. etransitivity; eauto. symmetry. auto.
  - pfold; constructor; auto.
    left. eapply IHterminates; auto.
  - apply pi_eqit_secure_priv_visl; auto. destruct H3. auto.
Qed.

Variant handler_respects_priv (A : Type) (e : E1 A) : Prop :=
| respect_private' (SECCHECK : ~ leq (priv1 _ e) l)
                 (RESCHECK : state_pi_eqit_secure true true top2 (handler A e) (ret tt) )
| respect_public'' (SECCHECK : leq (priv1 _ e) l)
                 (RESCHECK : state_pi_eqit_secure true true eq (handler A e) (handler A e))
.

Context (Hhandler : forall A (e : E1 A), handler_respects_priv A e).

Hint Resolve mono_diverges_with : paco.
(*
Lemma diverge_with_respectful_handler : forall (R : Type) (t : itree E1 R),
    diverges_with (fun _ e => ~ leq (priv1 _ e) l ) t ->
    forall s, diverges_with (fun _ e => ~ leq (priv2 _ e) l) (interp_state handler t s).
Proof.
  intro R. pcofix CIH. intros t Hdiv s. pinversion Hdiv; use_simpobs.
  - rewrite H. rewrite interp_state_tau. pfold. constructor. right. eapply CIH; eauto.
  - rewrite H. rewrite interp_state_vis.
    destruct (classic_empty B).
    + specialize (Hhandler _ e). destruct Hhandler; try contradiction; try contra_size.
      specialize (DIVCHECK s). eapply paco1_mon with (r:= bot1). eapply diverges_with_bind; eauto.
      intros; contradiction.
    + specialize (Hhandler _ e). destruct Hhandler; try contradiction; try contra_size.
      specialize (FINCHECK s). induction FINCHECK.
      * rewrite bind_ret_l. cbn. pfold. constructor. right. eapply CIH; eauto. apply H0.
      * rewrite bind_tau. pfold. constructor. left. eapply IHFINCHECK; eauto.
      * destruct H5. rewrite bind_vis. pfold. constructor; auto. left. eapply H4; eauto.
Qed.
*)
Lemma diverges_with_bind : forall E R S P (t : itree E R) (k : R -> itree E S),
    diverges_with P t -> diverges_with P (ITree.bind t k).
Proof.
  intros E R1 R2 P. pcofix CIH.
  intros t k Ht. punfold Ht. pfold. red.
  unfold observe. cbn. red in Ht. inv Ht.
  - cbn. constructor. right. pclearbot. eapply CIH; eauto.
  - pclearbot. cbn. constructor; auto. right. eapply CIH; eauto. apply H0.
Qed.

Lemma interp_pi_eqit_secure_state : forall (R1 R2 : Type) (RR : R1 -> R2 -> Prop) (t1 : itree E1 R1) (t2 : itree E1 R2),
    pi_eqit_secure Label priv1 RR true true l t1 t2 ->
    state_pi_eqit_secure true true RR (interp_state handler t1) (interp_state handler t2).
Proof.
  intros R1 R2 RR. ginit. gcofix CIH. intros t1 t2 Ht s1 s2 Hs. punfold Ht.
  red in Ht.
  inv Ht; intros; use_simpobs.
  - rewrite H, H0. repeat rewrite interp_state_ret. gstep. constructor.
    split; auto.
  - rewrite H, H0. repeat rewrite interp_state_tau. gstep. constructor.
    gfinal. left. pclearbot. apply CIH; auto.
  - pclearbot. rewrite H. rewrite interp_state_tau. gstep. constructor; auto.
    gfinal. left. eapply CIH; eauto. apply simpobs in H0. rewrite <- itree_eta in H0.
    rewrite H0. auto.
  - pclearbot. rewrite H0. rewrite interp_state_tau. gstep. constructor; auto.
    gfinal. left. eapply CIH; eauto. apply simpobs in H. rewrite <- itree_eta in H.
    rewrite H. auto.
  - pclearbot. rewrite H, H0.
    repeat rewrite interp_state_vis.
    specialize (Hhandler A e). inv Hhandler; try contradiction.
    eapply pi_secure_eqit_bind'; eauto.
    intros. destruct H2; destruct r1; destruct r2; cbn in *; subst.
    pfold. constructor. right. eapply CIH; eauto. apply H1.
  - rewrite H, H0. pclearbot. rewrite interp_state_tau.
    gstep. constructor; auto. rewrite interp_state_vis.
    specialize (Hhandler A e). inv Hhandler; try contradiction.
    red in RESCHECK. apply RESCHECK in Hs as He.
    remember (handler A e s1) as t3. clear Heqt3.
    cbn in He. generalize dependent t3. gcofix CIH'.
    intros t3 Ht3. pinversion Ht3; use_simpobs; subst.
    + destruct H4. cbn in *. destruct r1. cbn in *.
      rewrite H2. rewrite bind_ret_l. gstep. constructor; auto.
      gfinal. left. eapply CIH'0. eapply CIH; eauto. cbn. apply H1.
    + rewrite H2. rewrite bind_tau. gstep; constructor; auto.
      gfinal. left. eapply CIH'; eauto. symmetry in H3. use_simpobs.
      rewrite <- H3. auto.
    + rewrite H2. rewrite bind_vis. gstep. constructor; auto.
      intros. gfinal. left. eapply CIH'; eauto. symmetry in H3.
      use_simpobs. rewrite <- H3. apply H4.
 - rewrite H, H0. pclearbot. rewrite interp_state_tau.
    gstep. constructor; auto. rewrite interp_state_vis.
    specialize (Hhandler A e). inv Hhandler; try contradiction.
    red in RESCHECK. symmetry in Hs. apply RESCHECK in Hs as He.
    remember (handler A e s2) as t3. clear Heqt3.
    cbn in He. generalize dependent t3. gcofix CIH'.
    intros t3 Ht3. pinversion Ht3; use_simpobs; subst.
    + destruct H4. cbn in *. destruct r1. cbn in *.
      rewrite H2. rewrite bind_ret_l. gstep. constructor; auto.
      gfinal. left. eapply CIH'0. eapply CIH; eauto. cbn. apply H1.
      symmetry. auto.
    + rewrite H2. rewrite bind_tau. gstep; constructor; auto.
      gfinal. left. eapply CIH'; eauto. symmetry in H3. use_simpobs.
      rewrite <- H3. auto.
    + rewrite H2. rewrite bind_vis. gstep. constructor; auto.
      intros. gfinal. left. eapply CIH'; eauto. symmetry in H3.
      use_simpobs. rewrite <- H3. apply H4.
 - pclearbot. rewrite H, H0. repeat rewrite interp_state_vis.
   specialize (Hhandler A e1) as He1. specialize (Hhandler B e2) as He2.
   inv He1; inv He2; try contradiction.
   eapply pi_secure_eqit_bind' with (RR := prod_rel RS top2); eauto.
   + intros [? ?] [? ?] [? ?]. cbn in *. pstep. constructor.
     right. eapply CIH; eauto. apply H1.
   + cbn in *. apply pi_eqit_secure_RR_imp with
                   (RR1 := rcompose (prod_rel RS (@top2 A unit)) (prod_rel RS top2) ).
     { intros. inv H2. destruct REL1. destruct REL2. split; auto.
       etransitivity; eauto. }
     eapply pi_eqit_secure_trans_ret; eauto.
     apply pi_eqit_secure_sym. apply pi_eqit_secure_RR_imp with
                                   (RR1 := prod_rel RS top2).
     { intros. inv H2. split; auto. symmetry. auto.  }
     eapply RESCHECK0. reflexivity.
 - apply simpobs in H0. rewrite <- itree_eta in H0. rewrite H0.
   rewrite H. rewrite interp_state_vis.
   specialize (Hhandler A e). inv Hhandler; try contradiction.
   red in RESCHECK. apply RESCHECK in Hs as He.
    remember (handler A e s1) as t3. clear Heqt3.
    cbn in He. generalize dependent t3. gcofix CIH'.
    intros t3 Ht3. pinversion Ht3; use_simpobs; subst.
    + destruct H4. cbn in *. destruct r1. cbn in *.
      rewrite H2. rewrite bind_ret_l. gstep. constructor; auto.
      gfinal. left. eapply CIH; eauto. cbn. apply H1.
    + rewrite H2. rewrite bind_tau. gstep; constructor; auto.
      gfinal. left. eapply CIH'; eauto. symmetry in H3. use_simpobs.
      rewrite <- H3. auto.
    + rewrite H2. rewrite bind_vis. gstep. constructor; auto.
      intros. gfinal. left. eapply CIH'; eauto. symmetry in H3.
      use_simpobs. rewrite <- H3. apply H4.
 - apply simpobs in H. rewrite <- itree_eta in H. rewrite H.
   pclearbot. rewrite H0. rewrite interp_state_vis.
   specialize (Hhandler A e). inv Hhandler; try contradiction.
    red in RESCHECK. symmetry in Hs. apply RESCHECK in Hs as He.
    remember (handler A e s2) as t3. clear Heqt3.
    cbn in He. generalize dependent t3. gcofix CIH'.
    intros t3 Ht3. pinversion Ht3; use_simpobs; subst.
    + destruct H4. cbn in *. destruct r1. cbn in *.
      rewrite H2. rewrite bind_ret_l. gstep. constructor; auto.
      gfinal. left. cbn. eapply CIH; eauto. cbn. apply H1.
      symmetry. auto.
    + rewrite H2. rewrite bind_tau. gstep; constructor; auto.
      gfinal. left. eapply CIH'; eauto. symmetry in H3. use_simpobs.
      rewrite <- H3. auto.
    + rewrite H2. rewrite bind_vis. gstep. constructor; auto.
      intros. gfinal. left. eapply CIH'; eauto. symmetry in H3.
      use_simpobs. rewrite <- H3. apply H4.
Qed.

End GeneralStateHandler.

author: DeepSpec

repo: InteractionTrees


text:
From compcert Require Export Clightdefs.
Require Import VST.sepcomp.semantics.

Require Import VST.veric.juicy_base.
Require Import VST.veric.juicy_mem VST.veric.juicy_mem_lemmas VST.veric.juicy_mem_ops.
Require Import VST.veric.res_predicates.
Require Import VST.veric.extend_tc.
Require Import VST.veric.Clight_seplog.
Require Import VST.veric.Clight_assert_lemmas.
Require Import VST.veric.Clight_new.
Require Import VST.sepcomp.extspec.
Require Import VST.sepcomp.step_lemmas.
Require Import VST.veric.juicy_extspec.
Require Import VST.veric.tycontext.
Require Import VST.veric.expr2.
Require Import VST.veric.semax.
Require Import VST.veric.semax_lemmas.
Require Import VST.veric.semax_conseq.
Require Import VST.veric.Clight_lemmas.
Require Import VST.veric.Clight_initial_world.
Require Import VST.veric.semax_call.
Require Import VST.veric.semax_straight.
Require Import VST.veric.semax_loop.
Require Import VST.veric.semax_switch.
Require Import VST.veric.semax_prog.
Require Import VST.veric.semax_ext.
Require Import VST.veric.SeparationLogic.
Require Import VST.veric.expr_rel.
Require Import VST.floyd.SeparationLogicFacts.
Require Import VST.floyd.SeparationLogicAsLogic.
Require Import VST.veric.SeparationLogicSoundness.
Local Open Scope logic.
Require Import VST.veric.ghost_PCM.

Module DeepEmbeddedSoundness
       (Def: CLIGHT_SEPARATION_HOARE_LOGIC_DEF)
       (MinimumLogic: MINIMUM_CLIGHT_SEPARATION_HOARE_LOGIC with Module CSHL_Def := Def)
       (Sound: SEPARATION_HOARE_LOGIC_SOUNDNESS with Module CSHL_Def := Def)
       <: SEPARATION_HOARE_LOGIC_SOUNDNESS.

Module DeepEmbedded := DeepEmbedded (Def) (MinimumLogic).

Module CSHL_Def := DeepEmbedded.DeepEmbeddedDef.

Module CSHL_Defs := DeepEmbedded.DeepEmbeddedDefs.

Arguments CSHL_Def.semax {_} {_} _ _ _ _.

Module Conseq := GenConseq (Def) (MinimumLogic).

Module ExtrFacts := GenExtrFacts (Def) (Conseq) (MinimumLogic).

Import Conseq ExtrFacts.

Module CallF: CLIGHT_SEPARATION_HOARE_LOGIC_CALL_FORWARD with Module CSHL_Def := Def.

Module CSHL_Def := Def.

Definition semax_call_forward := @MinimumLogic.semax_call.

End CallF.

Module CallB := CallF2B (Def) (Conseq) (MinimumLogic) (CallF).

Module SetF: CLIGHT_SEPARATION_HOARE_LOGIC_SET_FORWARD with Module CSHL_Def := Def.

Module CSHL_Def := Def.

Definition semax_set_forward := @MinimumLogic.semax_set_forward.

End SetF.

Module SetB := SetF2B (Def) (Conseq) (MinimumLogic) (SetF).

Module PtrCmpF: CLIGHT_SEPARATION_HOARE_LOGIC_PTR_CMP_FORWARD with Module CSHL_Def := Def.

Module CSHL_Def := Def.

Definition semax_ptr_compare_forward := @MinimumLogic.semax_ptr_compare.

End PtrCmpF.

Module PtrCmpB := PtrCmpF2B (Def) (Conseq) (MinimumLogic) (PtrCmpF).

Module LoadF: CLIGHT_SEPARATION_HOARE_LOGIC_LOAD_FORWARD with Module CSHL_Def := Def.

Module CSHL_Def := Def.

Definition semax_load_forward := @MinimumLogic.semax_load.

End LoadF.

Module LoadB := LoadF2B (Def) (Conseq) (MinimumLogic) (LoadF).

Module CastLoadF: CLIGHT_SEPARATION_HOARE_LOGIC_CAST_LOAD_FORWARD with Module CSHL_Def := Def.

Module CSHL_Def := Def.

Definition semax_cast_load_forward := @MinimumLogic.semax_cast_load.

End CastLoadF.

Module CastLoadB := CastLoadF2B (Def) (Conseq) (MinimumLogic) (CastLoadF).

Module StoreF: CLIGHT_SEPARATION_HOARE_LOGIC_STORE_FORWARD with Module CSHL_Def := Def.

Module CSHL_Def := Def.

Definition semax_store_forward := @MinimumLogic.semax_store.

End StoreF.

Module StoreB := StoreF2B (Def) (Conseq) (MinimumLogic) (StoreF).

Module Extr : CLIGHT_SEPARATION_HOARE_LOGIC_EXTRACTION with Module CSHL_Def := Def := MinimumLogic.

Module Sset := ToSset (Def) (Conseq) (Extr) (SetB) (PtrCmpB) (LoadB) (CastLoadB).

Theorem semax_sound: forall Espec CS Delta P c Q,
  @DeepEmbedded.DeepEmbeddedDef.semax Espec CS Delta P c Q ->
  @Def.semax Espec CS Delta P c Q.
Proof.
  intros.
  induction H.
  + rewrite andp_assoc.
    apply semax_extract_prop.
    intros.
    apply MinimumLogic.semax_ifthenelse; auto.
  + eapply MinimumLogic.semax_seq; eauto.
  + apply MinimumLogic.semax_break.
  + apply MinimumLogic.semax_continue.
  + eapply MinimumLogic.semax_loop; eauto.
  + apply semax_extract_prop.
    intros.
    apply MinimumLogic.semax_switch; auto.
  + apply CallB.semax_call_backward.
  + apply MinimumLogic.semax_return.
  + apply Sset.semax_set_ptr_compare_load_cast_load_backward.
  + apply StoreB.semax_store_backward.
  + apply MinimumLogic.semax_skip.
  + rewrite <- (andp_dup FF).
    unfold FF at 1.
    apply semax_extract_prop.
    tauto.
  + apply MinimumLogic.semax_Slabel; auto.
  + rewrite <- (andp_dup FF).
    unfold FF at 1.
    apply semax_extract_prop.
    tauto.
  + eapply MinimumLogic.semax_conseq; eauto.
Qed.

Theorem semax_body_sound: forall Vspec Gspec CS f id,
  @DeepEmbedded.DeepEmbeddedDefs.semax_body Vspec Gspec CS f id ->
  @MinimumLogic.CSHL_Defs.semax_body Vspec Gspec CS f id.
Proof.
  intros.
  unfold MinimumLogic.CSHL_Defs.semax_body, CSHL_Defs.semax_body in H |- *.
  destruct id.
  destruct f0.
  intros.
  apply semax_sound.
  apply H.
Qed.

Theorem semax_func_sound: forall Espec Vspec Gspec CS ids fs,
  @DeepEmbedded.DeepEmbeddedDef.semax_func Espec Vspec Gspec CS ids fs ->
  @Def.semax_func Espec Vspec Gspec CS ids fs.
Proof.
  intros.
  induction H.
  + apply MinimumLogic.semax_func_nil.
  + apply MinimumLogic.semax_func_cons; auto.
    apply semax_body_sound; auto.
  + eapply MinimumLogic.semax_func_cons_ext; eauto.
Qed.

Theorem semax_prog_sound: forall Espec prog Vspec Gspec f,
  @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec prog Vspec Gspec f ->
  @MinimumLogic.CSHL_Defs.semax_prog Espec prog Vspec Gspec f.
Proof.
  intros.
  hnf in H |- *.
  pose proof semax_func_sound Espec Gspec f prog (prog_funct Vspec) f.
  tauto.
Qed.

Theorem semax_prog_rule :
  forall {Espec: OracleKind}{CS: compspecs},
  OK_ty = unit ->
  forall V G prog m h,
     @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec CS prog V G ->
     Genv.init_mem prog = Some m ->
     { b : block & { q : corestate &
       (Genv.find_symbol (globalenv prog) (prog_main prog) = Some b) *
       (forall jm, m_dry jm = m -> exists jm', semantics.initial_core (juicy_core_sem (cl_core_sem (globalenv prog))) h
                    jm q jm' (Vptr b Ptrofs.zero) nil) *
       forall n,
         { jm |
           m_dry jm = m /\ level jm = n /\
           (forall z, jsafeN (@OK_spec Espec) (globalenv prog) n z q jm) /\
           no_locks (m_phi jm) /\
           matchfunspecs (globalenv prog) G (m_phi jm) /\
           app_pred (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm)
     } } }%type.
Proof.
  intros.
  apply Sound.semax_prog_rule; auto.
  apply semax_prog_sound; auto.
Qed.

Theorem semax_prog_rule' :
  forall {Espec: OracleKind}{CS: compspecs},
  forall V G prog m h,
     @DeepEmbedded.DeepEmbeddedDefs.semax_prog Espec CS prog V G ->
     Genv.init_mem prog = Some m ->
     { b : block & { q : corestate &
       (Genv.find_symbol (globalenv prog) (prog_main prog) = Some b) *
       (forall jm, m_dry jm = m -> exists jm', semantics.initial_core (juicy_core_sem (cl_core_sem (globalenv prog))) h
                    jm q jm' (Vptr b Ptrofs.zero) nil) *
       forall n z,
         { jm |
           m_dry jm = m /\ level jm = n /\
           nth_error (ghost_of (m_phi jm)) 0 = Some (Some (ext_ghost z, NoneP)) /\
           jsafeN (@OK_spec Espec) (globalenv prog) n z q jm /\
           no_locks (m_phi jm) /\
           matchfunspecs (globalenv prog) G (m_phi jm) /\
           app_pred (funassert (nofunc_tycontext V G) (empty_environ (globalenv prog))) (m_phi jm)
     } } }%type.
Proof.
  intros.
  apply Sound.semax_prog_rule'; auto.
  apply semax_prog_sound; auto.
Qed.

End DeepEmbeddedSoundness.

(********************************************************)
(*                                                      *)
(*            Main Theorem of Verifiable C              *)
(*                                                      *)
(********************************************************)

Module MainTheorem: MAIN_THEOREM_STATEMENT.

Module DeepEmbedded := DeepEmbedded (VericDef) (VericMinimumSeparationLogic).

Import DeepEmbedded.

Module CSHL_Def := DeepEmbeddedDef.

Module CSHL_Defs := DeepEmbeddedDefs.

Module CSHL_MinimumLogic := DeepEmbeddedMinimumSeparationLogic.

Module CSHL_PracticalLogic := DeepEmbeddedPracticalLogic.

Module CSHL_Sound := DeepEmbeddedSoundness (VericDef) (VericMinimumSeparationLogic) (VericSound).

End MainTheorem.

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


text:
Require Import Coq.Arith.Compare_dec.

Require Import Axioms.
Require Import Sigma.
Require Import Tactics.

(* We only use ordinals up to omega+2 or so, but it's cleaner to define them under omega^2. *)

Definition ordinal : Type := nat * nat.

Definition fin (i : nat) : ordinal := (0, i).
Definition omegaplus (i : nat) : ordinal := (1, i).
Definition omega : ordinal := omegaplus 0.
Definition omegaplus1 : ordinal := omegaplus 1.

Definition succ (w : ordinal) : ordinal := (fst w, S (snd w)).

Lemma succ_fin :
  forall i, succ (fin i) = fin (S i).
Proof.
intros i.
reflexivity.
Qed.

Inductive le_ord : ordinal -> ordinal -> Prop :=
| le_ord_fst :
    forall i j k l, i < k -> le_ord (i, j) (k, l)

| le_ord_snd :
    forall i j k, j <= k -> le_ord (i, j) (i, k)
.

Definition lt_ord (a b : ordinal) := le_ord (succ a) b.

Notation "a <<= b" := (le_ord a b)
  (at level 70, right associativity) : ordinal_scope.

Notation "a << b" := (lt_ord a b)
  (at level 70, right associativity) : ordinal_scope.

Open Scope ordinal_scope.

Lemma le_fin :
  forall i j, i <= j -> fin i <<= fin j.
Proof.
intros i j Hij.
apply le_ord_snd; auto.
Qed.

Lemma lt_fin :
  forall i j, i < j -> fin i << fin j.
Proof.
intros i j Hij.
apply le_ord_snd.
cbn.
omega.
Qed.

Lemma le_ord_zero :
  forall w, fin 0 <<= w.
Proof.
intros w.
destruct w as (i, j).
destruct i as [| i].
  {
  apply le_ord_snd; omega.
  }

  {
  apply le_ord_fst.
  omega.
  }
Qed.

Lemma le_fin_omega :
  forall i j, fin i <<= omegaplus j.
Proof.
intros i j.
apply le_ord_fst.
omega.
Qed.

Lemma lt_fin_omega :
  forall i j, fin i << omegaplus j.
Proof.
intros i j.
apply le_ord_fst.
cbn.
omega.
Qed.

Lemma lt_omega_fin :
  forall w, w << omega -> existsT i, w = fin i.
Proof.
intros w Hlt.
destruct w as (i, j).
exists j.
invert Hlt; try (intros; omega).
intros Hi.
assert (i = 0) by omega; subst i.
reflexivity.
Qed.

Lemma omega_limit :
  forall w,
    w << omega
    -> succ w << omega.
Proof.
intros w Hlt.
so (lt_omega_fin _ Hlt) as (i & ->).
rewrite -> succ_fin.
apply lt_fin_omega.
Qed.

Lemma lt_ord_impl_le_ord :
  forall v w, v << w -> v <<= w.
Proof.
intros (i, j) (k, l) Hvw.
invert Hvw.
  {
  intro.
  apply le_ord_fst; auto.
  }

  {
  intros H <-.
  apply le_ord_snd.
  omega.
  }
Qed.

Lemma le_ord_refl :
  forall w, w <<= w.
Proof.
intros w.
destruct w as (i, j).
apply le_ord_snd.
auto.
Qed.

Lemma le_ord_refl' :
  forall w w', w = w' -> w <<= w'.
Proof.
intros w w' H.
subst w'.
apply le_ord_refl.
Qed.

Lemma le_ord_antisymm :
  forall v w, v <<= w -> w <<= v -> v = w.
Proof.
intros v w Hvw Hwv.
invertc Hvw.
  {
  intros i j k l Hik <- <-.
  invertc Hwv.
    {
    intro Hki.
    omega.
    }

    {
    intros Hlj ->.
    f_equal.
    omega.
    }
  }

  {
  intros i j k Hjk <- <-.
  invertc Hwv.
    {
    intros H.
    omega.
    }

    {
    intros Hkj.
    f_equal.
    omega.
    }
  }
Qed.

Lemma le_ord_trans :
  forall u v w, u <<= v -> v <<= w -> u <<= w.
Proof.
intros u v w Huv Hvw.
invertc Huv.
  {
  intros a b c d Hac <- <-.
  invertc Hvw.
    {
    intros e f Hce <-.
    apply le_ord_fst.
    omega.
    }

    {
    intros e Hde <-.
    apply le_ord_fst; auto.
    }
  }

  {
  intros a b c Hbc <- <-.
  invertc Hvw.
    {
    intros d e Had <-.
    apply le_ord_fst; auto.
    }

    {
    intros d Hcd <-.
    apply le_ord_snd.
    omega.
    }
  }
Qed.

Lemma le_ord_succ :
  forall v w, v <<= w -> succ v <<= succ w.
Proof.
intros v w H.
invertc H.
  {
  intros a b c d Hac <- <-.
  apply le_ord_fst; auto.
  }

  {
  intros a b c Hbc <- <-.
  apply le_ord_snd.
  cbn.
  omega.
  }
Qed.

Lemma lt_ord_succ :
  forall v w,
    v << w
    -> succ v << succ w.
Proof.
intros v w H.
apply le_ord_succ; auto.
Qed.

Lemma lt_ord_0_succ :
  forall w,
    fin 0 << succ w.
Proof.
intros w.
unfold lt_ord.
apply le_ord_succ.
apply le_ord_zero.
Qed.

Lemma succ_increase :
  forall w, w << succ w.
Proof.
intro w.
apply le_ord_succ.
apply le_ord_refl.
Qed.

Lemma succ_nodecrease :
  forall w, w <<= succ w.
Proof.
intro w.
apply lt_ord_impl_le_ord.
apply succ_increase.
Qed.

Lemma le_lt_ord_trans :
  forall u v w, u <<= v -> v << w -> u << w.
Proof.
unfold lt_ord.
intros u v w Huv Hvw.
eapply le_ord_trans; eauto.
apply le_ord_succ; auto.
Qed.

Lemma lt_le_ord_trans :
  forall u v w, u << v -> v <<= w -> u << w.
Proof.
unfold lt_ord.
intros u v w Huv Hvw.
eapply le_ord_trans; eauto.
Qed.

Lemma lt_ord_trans :
  forall u v w, u << v -> v << w -> u << w.
Proof.
intros u v w Huv Hvw.
eapply lt_le_ord_trans; eauto.
apply lt_ord_impl_le_ord; auto.
Qed.

Lemma lt_ord_irrefl :
  forall w, ~ w << w.
Proof.
intros w H.
unfold lt_ord in H.
destruct w as (i, j).
unfold succ in H.
cbn in H.
invert H; intros; omega.
Qed.

Lemma lt_ord_wf :
  forall w, Acc lt_ord w.
Proof.
intros w.
destruct w as (i, j).
revert j.
wfinduct i using lt_wf.
intros i IHi.
intro j.
wfinduct j using lt_wf.
intros j IHj.
apply Acc_intro.
intros (k, l) H.
invertc H.
  {
  intros Hki.
  apply IHi; auto.
  }

  {
  intros Hlj ->.
  apply IHj; auto.
  }
Qed.

Lemma eq_ord_dec :
  forall (v w : ordinal), {v = w} + {v <> w}.
Proof.
intros (a, b) (c, d).
so (eq_nat_dec a c) as [| Hneq].
2:{
  right.
  intro H.
  injection H.
  intros; contradiction.
  }
subst c.
so (eq_nat_dec b d) as [| Hneq].
2:{
  right.
  intro H.
  injection H.
  intros; contradiction.
  }
subst d.
left; reflexivity.
Qed.

Lemma lt_eq_lt_ord_dec :
  forall v w, {v << w} + {v = w} + {w << v}.
Proof.
intros (a, b) (c, d).
so (lt_eq_lt_dec a c) as [[Hac | Heq] | Hca].
  {
  left; left.
  apply le_ord_fst; auto.
  }

  {
  subst c.
  so (lt_eq_lt_dec b d) as [[Hbd | Heq] | Hdb].
    {
    left; left.
    apply le_ord_snd.
    cbn.
    omega.
    }

    {
    subst d.
    left; right.
    reflexivity.
    }

    {
    right.
    apply le_ord_snd.
    cbn.
    omega.
    }
  }

  {
  right.
  apply le_ord_fst; auto.
  }
Qed.

Lemma le_ord_dec :
  forall v w, {v <<= w} + {~ v <<= w}.
Proof.
intros v w.
so (lt_eq_lt_ord_dec v w) as [[H | H]|H].
  {
  left.
  apply lt_ord_impl_le_ord; auto.
  }

  {
  subst w.
  left.
  apply le_ord_refl.
  }

  {
  right.
  intros H'.
  apply (lt_ord_irrefl v).
  eapply le_lt_ord_trans; eauto.
  }
Qed.

Lemma lt_ord_dec :
  forall v w, {v << w} + {~ v << w}.
Proof.
intros v w.
so (lt_eq_lt_ord_dec v w) as [[H | H]|H].
  {
  left; auto.
  }

  {
  subst w.
  right.
  apply lt_ord_irrefl.
  }

  {
  right.
  intros H'.
  apply (lt_ord_irrefl v).
  eapply lt_ord_trans; eauto.
  }
Qed.

Lemma le_lt_ord_dec :
  forall v w, {v <<= w} + {w << v}.
Proof.
intros v w.
so (lt_eq_lt_ord_dec v w) as [[Hlt | Heq]|Hlt]; subst; auto using le_ord_refl, lt_ord_impl_le_ord.
Qed.

Lemma lt_ord_dec_is :
  forall v w (h : v << w),
    lt_ord_dec v w = left h.
Proof.
intros v w h.
set (X := lt_ord_dec v w).
destruct X as [h' | Hnlt].
  {
  f_equal.
  apply proof_irrelevance.
  }

  {
  contradiction.
  }
Qed.

Lemma le_ord_dec_is :
  forall v w (h : v <<= w),
    le_ord_dec v w = left h.
Proof.
intros v w h.
set (X := le_ord_dec v w).
destruct X as [h' | Hnlt].
  {
  f_equal.
  apply proof_irrelevance.
  }

  {
  contradiction.
  }
Qed.

Lemma lt_ord_dec_is_not :
  forall v w (h : ~ v << w),
    lt_ord_dec v w = right h.
Proof.
intros v w h.
set (X := lt_ord_dec v w).
destruct X as [Hlt | h'].
  {
  contradiction.
  }

  {
  f_equal.
  apply proof_irrelevance.
  }
Qed.

Lemma le_lt_eq_ord_dec :
  forall v w, v <<= w -> {v << w} + {v = w}.
Proof.
intros v w Hvw.
so (lt_eq_lt_ord_dec v w) as [[H | H]|H]; auto.
destruct (lt_ord_irrefl v).
eapply le_lt_ord_trans; eauto.
Qed.

Lemma le_ord_nlt_impl_eq :
  forall v w, v <<= w -> ~ v << w -> v = w.
Proof.
intros v w Hle Hnlt.
so (le_lt_eq_ord_dec v w Hle) as [Hlt | Heq]; auto.
contradiction.
Qed.

Lemma not_le_ord_impl_lt_ord :
  forall v w,
    ~ v <<= w -> w << v.
Proof.
intros v w Hnle.
so (lt_eq_lt_ord_dec v w) as [[H | H]|H]; auto.
  {
  destruct Hnle.
  apply lt_ord_impl_le_ord; auto.
  }

  {
  subst v.
  destruct Hnle.
  apply le_ord_refl.
  }
Qed.

Lemma not_lt_ord_impl_le_ord :
  forall v w, ~ v << w -> w <<= v.
Proof.
intros v w H.
so (le_ord_dec w v) as [| Hnle]; auto.
destruct H.
apply not_le_ord_impl_lt_ord; auto.
Qed.

Lemma not_le_ord_impl_le_ord :
  forall v w,
    ~ v <<= w -> w <<= v.
Proof.
intros v w Hnle.
apply lt_ord_impl_le_ord.
apply not_le_ord_impl_lt_ord; auto.
Qed.

Lemma le_ord_succ_cancel :
  forall v w, succ v <<= succ w -> v <<= w.
Proof.
intros v w H.
so (le_ord_dec v w) as [| Hnle]; auto.
exfalso.
apply (lt_ord_irrefl (succ w)).
eapply lt_le_ord_trans; eauto.
apply lt_ord_succ.
apply not_le_ord_impl_lt_ord; auto.
Qed.

Definition min_ord (v w : ordinal) : ordinal :=
  match le_ord_dec w v with
  | left _ => w
  | right _ => v
  end.

Definition max_ord (v w : ordinal) : ordinal :=
  match le_ord_dec v w with
  | left _ => w
  | right _ => v
  end.

Lemma min_ord_id :
  forall w, min_ord w w = w.
Proof.
intros w.
unfold min_ord.
set (X := le_ord_dec w w).
destruct X as [H | H]; auto.
Qed.

Lemma max_ord_id :
  forall w, max_ord w w = w.
Proof.
intros w.
unfold max_ord.
set (X := le_ord_dec w w).
destruct X as [H | H]; auto.
Qed.

Lemma min_ord_l :
  forall v w, v <<= w -> min_ord v w = v.
Proof.
intros v w Hwv.
unfold min_ord.
set (X := le_ord_dec w v).
destruct X as [H | H]; auto.
apply le_ord_antisymm; auto.
Qed.

Lemma max_ord_l :
  forall v w, w <<= v -> max_ord v w = v.
Proof.
intros v w Hwv.
unfold max_ord.
set (X := le_ord_dec v w).
destruct X as [H | H]; auto.
apply le_ord_antisymm; auto.
Qed.

Lemma min_ord_r :
  forall v w, w <<= v -> min_ord v w = w.
Proof.
intros v w Hvw.
unfold min_ord.
set (X := le_ord_dec w v).
destruct X as [H | H]; auto.
contradiction.
Qed.

Lemma max_ord_r :
  forall v w, v <<= w -> max_ord v w = w.
Proof.
intros v w Hvw.
unfold max_ord.
set (X := le_ord_dec v w).
destruct X as [H | H]; auto.
contradiction.
Qed.

Lemma le_ord_min_l :
  forall v w, min_ord v w <<= v.
Proof.
intros v w.
so (le_ord_dec w v) as [H | H].
  {
  rewrite -> min_ord_r; auto.
  }

  {
  rewrite -> min_ord_l; auto using le_ord_refl.
  apply not_le_ord_impl_le_ord; auto.
  }
Qed.

Lemma le_ord_max_l :
  forall v w, v <<= max_ord v w.
Proof.
intros v w.
so (le_ord_dec v w) as [H | H].
  {
  rewrite -> max_ord_r; auto.
  }

  {
  rewrite -> max_ord_l; auto using le_ord_refl.
  apply not_le_ord_impl_le_ord; auto.
  }
Qed.

Lemma le_ord_min_r :
  forall v w, min_ord v w <<= w.
Proof.
intros v w.
so (le_ord_dec v w) as [H | H].
  {
  rewrite -> min_ord_l; auto.
  }

  {
  rewrite -> min_ord_r; auto using le_ord_refl.
  apply not_le_ord_impl_le_ord; auto.
  }
Qed.

Lemma le_ord_max_r :
  forall v w, w <<= max_ord v w.
Proof.
intros v w.
so (le_ord_dec w v) as [H | H].
  {
  rewrite -> max_ord_l; auto.
  }

  {
  rewrite -> max_ord_r; auto using le_ord_refl.
  apply not_le_ord_impl_le_ord; auto.
  }
Qed.

Lemma min_ord_glb :
  forall u v w,
    w <<= u
    -> w <<= v
    -> w <<= min_ord u v.
Proof.
intros u v w Huw Hvw.
so (le_ord_dec v u) as [H | H].
  {
  rewrite -> min_ord_r; auto.
  }

  {
  rewrite -> min_ord_l; auto.
  apply not_le_ord_impl_le_ord; auto.
  }
Qed.

Lemma max_ord_lub :
  forall u v w,
    u <<= w
    -> v <<= w
    -> max_ord u v <<= w.
Proof.
intros u v w Huw Hvw.
so (le_ord_dec u v) as [H | H].
  {
  rewrite -> max_ord_r; auto.
  }

  {
  rewrite -> max_ord_l; auto.
  apply not_le_ord_impl_le_ord; auto.
  }
Qed.

Lemma min_ord_glb_l :
  forall u v w, w <<= min_ord u v -> w <<= u.
Proof.
intros u v w Hle.
eapply le_ord_trans; eauto.
apply le_ord_min_l.
Qed.

Lemma max_ord_lub_l :
  forall u v w, max_ord u v <<= w -> u <<= w.
Proof.
intros u v w Hle.
eapply le_ord_trans; eauto.
apply le_ord_max_l.
Qed.

Lemma min_ord_glb_r :
  forall u v w, w <<= min_ord u v -> w <<= v.
Proof.
intros u v w Hle.
eapply le_ord_trans; eauto.
apply le_ord_min_r.
Qed.

Lemma max_ord_lub_r :
  forall u v w, max_ord u v <<= w -> v <<= w.
Proof.
intros u v w Hle.
eapply le_ord_trans; eauto.
apply le_ord_max_r.
Qed.

Lemma succ_min_ord :
  forall v w, succ (min_ord v w) = min_ord (succ v) (succ w).
Proof.
intros v w.
so (le_ord_dec w v) as [Hvw | Hnvw].
  {
  rewrite -> !min_ord_r; auto.
  apply le_ord_succ; auto.
  }

  {
  so (not_le_ord_impl_le_ord _ _ Hnvw) as Hwv.
  rewrite -> !min_ord_l; auto.
  apply le_ord_succ; auto.
  }
Qed.

Lemma succ_max_ord :
  forall v w, succ (max_ord v w) = max_ord (succ v) (succ w).
Proof.
intros v w.
so (le_ord_dec v w) as [Hvw | Hnvw].
  {
  rewrite -> !max_ord_r; auto.
  apply le_ord_succ; auto.
  }

  {
  so (not_le_ord_impl_le_ord _ _ Hnvw) as Hwv.
  rewrite -> !max_ord_l; auto.
  apply le_ord_succ; auto.
  }
Qed.

Lemma min_ord_glb_strict :
  forall u v w,
    w << u
    -> w << v
    -> w << min_ord u v.
Proof.
intros u v w Huw Hvw.
apply min_ord_glb; auto.
Qed.

Lemma max_ord_lub_strict :
  forall u v w,
    u << w
    -> v << w
    -> max_ord u v << w.
Proof.
intros u v w Huw Hvw.
unfold lt_ord.
rewrite -> succ_max_ord.
apply max_ord_lub; auto.
Qed.

Lemma min_ord_glb_strict_l :
  forall u v w, w << min_ord u v -> w << u.
Proof.
intros u v w H.
eapply min_ord_glb_l; eauto.
Qed.

Lemma max_ord_lub_strict_l :
  forall u v w, max_ord u v << w -> u << w.
Proof.
intros u v w H.
eapply le_lt_ord_trans; eauto.
apply le_ord_max_l.
Qed.

Lemma min_ord_glb_strict_r :
  forall u v w, w << min_ord u v -> w << v.
Proof.
intros u v w H.
eapply min_ord_glb_r; eauto.
Qed.

Lemma max_ord_lub_strict_r :
  forall u v w, max_ord u v << w -> v << w.
Proof.
intros u v w H.
eapply le_lt_ord_trans; eauto.
apply le_ord_max_r.
Qed.

Lemma min_ord_comm :
  forall v w, min_ord v w = min_ord w v.
Proof.
intros v w.
so (le_ord_dec w v) as [H | H].
  {
  rewrite -> min_ord_r; auto.
  rewrite -> min_ord_l; auto.
  }

  {
  so (not_le_ord_impl_le_ord _ _ H) as H'.
  rewrite -> min_ord_l; auto.
  rewrite -> min_ord_r; auto.
  }
Qed.

Lemma max_ord_comm :
  forall v w, max_ord v w = max_ord w v.
Proof.
intros v w.
so (le_ord_dec v w) as [H | H].
  {
  rewrite -> max_ord_r; auto.
  rewrite -> max_ord_l; auto.
  }

  {
  so (not_le_ord_impl_le_ord _ _ H) as H'.
  rewrite -> max_ord_l; auto.
  rewrite -> max_ord_r; auto.
  }
Qed.

Lemma min_ord_assoc :
  forall u v w, min_ord u (min_ord v w) = min_ord (min_ord u v) w.
Proof.
intros u v w.
so (le_ord_dec w v) as [Hvw | Hnvw].
  {
  rewrite -> (min_ord_r v w); auto.
  so (le_ord_dec v u) as [Huv | Hnuv].
    {
    rewrite -> (min_ord_r u v); auto.
    rewrite -> (min_ord_r v w); auto.
    rewrite -> (min_ord_r u w); auto.
    eapply le_ord_trans; eauto.
    }

    {
    so (not_le_ord_impl_le_ord _ _ Hnuv) as Hvu.
    rewrite -> (min_ord_l u v); auto.
    }
  }

  {
  so (not_le_ord_impl_le_ord _ _ Hnvw) as Hwv.
  rewrite -> (min_ord_l v w); auto.
  so (le_ord_dec v u) as [Huv | Hnuv].
    {
    rewrite -> (min_ord_r u v); auto.
    rewrite -> min_ord_l; auto.
    }

    {
    so (not_le_ord_impl_le_ord _ _ Hnuv) as Hvu.
    rewrite -> (min_ord_l u v); auto.
    rewrite -> min_ord_l; auto.
    eapply le_ord_trans; eauto.
    }
  }
Qed.

Lemma max_ord_assoc :
  forall u v w, max_ord u (max_ord v w) = max_ord (max_ord u v) w.
Proof.
intros u v w.
so (le_ord_dec v w) as [Hvw | Hnvw].
  {
  rewrite -> (max_ord_r v w); auto.
  so (le_ord_dec u v) as [Huv | Hnuv].
    {
    rewrite -> (max_ord_r u v); auto.
    rewrite -> (max_ord_r v w); auto.
    rewrite -> (max_ord_r u w); auto.
    eapply le_ord_trans; eauto.
    }

    {
    so (not_le_ord_impl_le_ord _ _ Hnuv) as Hvu.
    rewrite -> (max_ord_l u v); auto.
    }
  }

  {
  so (not_le_ord_impl_le_ord _ _ Hnvw) as Hwv.
  rewrite -> (max_ord_l v w); auto.
  so (le_ord_dec u v) as [Huv | Hnuv].
    {
    rewrite -> (max_ord_r u v); auto.
    rewrite -> max_ord_l; auto.
    }

    {
    so (not_le_ord_impl_le_ord _ _ Hnuv) as Hvu.
    rewrite -> (max_ord_l u v); auto.
    rewrite -> max_ord_l; auto.
    eapply le_ord_trans; eauto.
    }
  }
Qed.

Lemma min_ord_mono :
  forall v v' w w',
    v <<= v'
    -> w <<= w'
    -> min_ord v w <<= min_ord v' w'.
Proof.
intros v v' w w' Hv Hw.
so (le_lt_ord_dec w v) as [Hvw | Hwv].
  {
  rewrite -> (min_ord_r v w); auto.
  apply min_ord_glb; eauto using le_ord_trans.
  }

  {
  so (lt_ord_impl_le_ord _ _ Hwv) as Hwv'.
  rewrite -> (min_ord_l v w); auto.
  apply min_ord_glb; eauto using le_ord_trans.
  }
Qed.

Lemma max_ord_mono :
  forall v v' w w',
    v <<= v'
    -> w <<= w'
    -> max_ord v w <<= max_ord v' w'.
Proof.
intros v v' w w' Hv Hw.
so (le_lt_ord_dec v' w') as [Hvw | Hwv].
  {
  rewrite -> (max_ord_r v' w'); auto.
  apply max_ord_lub; eauto using le_ord_trans.
  }

  {
  so (lt_ord_impl_le_ord _ _ Hwv) as Hwv'.
  rewrite -> (max_ord_l v' w'); auto.
  apply max_ord_lub; eauto using le_ord_trans.
  }
Qed.

Definition limitord w : Prop
  :=
  fin 0 << w
  /\
  forall v, v << w -> succ v << w.

Lemma limitord_lub :
  forall w v,
    limitord w
    -> (forall u, u << w -> u <<= v)
    -> w <<= v.
Proof.
intros w v Hlimit Hv.
so (le_ord_dec w v) as [| Hnle]; auto.
destruct (lt_ord_irrefl v).
so (not_le_ord_impl_lt_ord _ _ Hnle) as Hlt.
so (Hlimit ander _ Hlt) as Hlt'.
so (Hv _ Hlt') as Hle.
eapply le_lt_ord_trans; eauto.
Qed.

Lemma ordinal_trichot :
  forall w,
    { w = fin 0 } + { exists v, w = succ v } + { limitord w }.
Proof.
intros w.
destruct w as (i, j).
destruct j as [| j].
  {
  destruct i as [| j].
    {
    left; left.
    reflexivity.
    }

    {
    right.
    split.
      {
      apply le_ord_fst.
      cbn.
      omega.
      }

      {
      intros v Hv.
      destruct v as (k, l).
      unfold lt_ord in Hv.
      invertc Hv.
        {
        intro H; apply le_ord_fst; auto.
        }

        {
        intros; omega.
        }
      }
    }
  }

  {
  left; right.
  exists (i, j).
  reflexivity.
  }
Qed.

author: kcrary

repo: istari

save_path: github-repos/coq/kcrary-istari


text:
(*
 * Copyright (c) Meta Platforms, Inc. and affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

From stdpp Require Import base strings gmap stringmap fin_maps.

From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import iprop own wsat.
From iris.algebra.lib Require Import gmap_view.

From shack Require Import lang progdef subtype ok typing.
From shack Require Import eval heap modality interp soundness.

From shack.reflect Require Import lang progdef subtype.

Definition arraykey := UnionT IntT BoolT.

(* TODO: we don't have void atm so I'm using null ;) *)

(* Definition of class ROBox<+T as arraykey>:
 * class ROBox<+T> {
 *   private T $data;
 *   function get(): T { $ret = $this->data; return $ret; }
 *)
Definition Get := {|
  methodargs := ∅;
  methodrettype := GenT 0;
  methodbody := GetC "$ret" ThisE "$data";
  methodret := VarE "$ret";
  methodvisibility := Public;
|}.

Definition ROBox := {|
  superclass := None;
  generics := [Covariant];
  constraints := [(GenT 0, arraykey)];
  classfields := {["$data" := (Private, GenT 0)]};
  classmethods := {["get" := Get]};
|}.

(* Definition of class Box<T>:
 * class Box<T> {
 *   public T $data;
 *   function set(T $data) : void { $this->data = $data; }
 *   function get(): T { $ret = $this->data; return $ret; }
 * }
 *)
Definition BoxSet := {|
  methodargs := {["$data" := GenT 0 ]};
  methodrettype := NullT;
  methodbody := SetC ThisE "$data" (VarE "$data");
  methodret := NullE;
  methodvisibility := Public;
|}.

Definition Box := {|
  superclass := None;
  generics := [Invariant];
  constraints := [];
  classfields := {["$data" := (Public, GenT 0)]};
  classmethods := {["set" := BoxSet; "get" := Get]};
|}.

(* Definition of class IntBoxS:
 * class IntBoxS extends Box<int> {
 * function set(int $data) : void { $this->data = $data + 1; }
 *)

Definition σ : list lang_ty := [IntT].

Definition IntBoxSSet := {|
  methodargs := {["$data" := IntT ]};
  methodrettype := NullT;
  methodbody := SetC ThisE "$data" (BinOpE PlusO (VarE "$data") (IntE 1%Z));
  methodret := NullE;
  methodvisibility := Public;
|}.

Definition IntBoxS := {|
  superclass := Some ("Box", σ);
  generics := [];
  constraints := [];
  classfields := ∅;
  classmethods := {["set" := IntBoxSSet]};
|}.

(* Main program:
 * function main(): bool {
 *   $robox = new ROBox(43);
 *   $init = $robox->get();
 *   $box = new IntBoxS($init);
 *   $tmp = $box->get();
 *   $tmp = $tmp + 20;
 *   $_ = $box->set($tmp - 10);
 *   $tmp = $box->data;
 *   return ($tmp == 43);
 * }
 *)
Definition ProgramBody :=
   SeqC (NewC "$robox" "ROBox" (Some [IntT]) {["$data" := IntE 32]})
  (SeqC (CallC "$init" (VarE "$robox") "get" ∅)
  (SeqC (NewC "$box" "IntBoxS" None {["$data" := VarE "$init"]})
  (SeqC (CallC "$tmp" (VarE "$box") "get" ∅)
  (SeqC (LetC "$tmp" (BinOpE PlusO (VarE "$tmp") (IntE 20)))
  (SeqC (CallC "$_" (VarE "$box") "set"
           {["$data" := BinOpE MinusO (VarE "$tmp") (IntE 10)]})
        (GetC "$tmp" (VarE "$box") "$data")
  ))))).

Definition EntryPoint := {|
  methodargs := ∅;
  methodrettype := BoolT;
  methodbody := ProgramBody;
  methodret := BinOpE EqO (VarE "$tmp") (IntE 43);
  methodvisibility := Public;
|}.

Definition Main := {|
  superclass := None;
  generics := [];
  constraints := [];
  classfields := ∅;
  classmethods := {["entry_point" := EntryPoint]};
 |}.

Definition pdefs0 : stringmap classDef :=
  {[ "ROBox" := ROBox; "Box" := Box; "IntBoxS" := IntBoxS; "Main" := Main ]}.

Local Instance PDC : ProgDefContext := { pdefs := pdefs0 }.

Lemma pacc : ∀ c, Acc (λ x y, extends y x) c.
Proof.
  apply check_acc_defs_correct with (n := 100).
  by exact (I <: True).
Qed.

Local Instance PDA : ProgDefAcc  := { pacc := pacc }.

(* Invalid constraint, so we can prove anything trivially *)
Local Instance SDTCC : SDTClassConstraints := {
  Δsdt := λ _, [(IntT, BoolT) ];
  Δsdt_m := λ _ _, [(IntT, BoolT) ];
}.

Local Instance SDTCS : SDTClassSpec.
Proof.
  split.
  - move => ???; rewrite list_lookup_singleton_Some => [[? <-]]; by constructor.
  - move => ????; rewrite list_lookup_singleton_Some => [[? <-]]; by constructor.
  - move => ?????; rewrite list_lookup_singleton_Some => [[? <-]]; by constructor.
  - move => ??????; rewrite list_lookup_singleton_Some => [[? <-]]; by constructor.
  - move => ???; rewrite list_lookup_singleton_Some => [[? <-]]; by constructor.
  - move => ????; rewrite list_lookup_singleton_Some => [[? <-]]; by constructor.
Qed.

Local Instance SDTCVS : SDTClassVarianceSpec.
Proof.
  split.
  move => ????????.
  move => ??.
  rewrite list_lookup_singleton_Some.
  case => ? <- /=.
  apply SubConstraint.
  by set_solver.
Qed.

Lemma wfσ : Forall wf_ty σ.
Proof.
  apply Forall_lookup => x ? hx.
  apply list_lookup_singleton_Some in hx as [-> <-].
  by constructor.
Qed.

Lemma σbounded : Forall (bounded (length (generics IntBoxS))) σ.
Proof.
  apply Forall_lookup => x ? hx.
  apply list_lookup_singleton_Some in hx as [-> <-].
  by constructor.
Qed.

Lemma has_method_get0: has_method "get" "ROBox" "ROBox" Get.
Proof. by repeat econstructor; eauto. Qed.

Lemma has_method_get1: has_method "get" "IntBoxS" "Box" (subst_mdef σ Get).
Proof. by repeat econstructor; eauto. Qed.

Lemma has_method_set: has_method "set" "IntBoxS" "IntBoxS" IntBoxSSet.
Proof. by repeat econstructor; eauto. Qed.

Lemma has_fields_ROBox : has_fields "ROBox" {[ "$data" := (Private, GenT 0, "ROBox") ]}.
Proof.
  move => f vis fty orig; split => h.
  - inv h.
    + rewrite /pdefs /= lookup_insert in H.
      simplify_eq.
      rewrite /ROBox /= lookup_singleton_Some in H0.
      by destruct H0 as [<- <-].
    + by rewrite /pdefs /= lookup_insert in H; simplify_eq.
  - rewrite lookup_singleton_Some in h.
    destruct h as [<- [= <- <- <-]].
    change Private with (Private, GenT 0).1.
    by econstructor.
Qed.

Lemma has_fields_Box : has_fields "Box" {[ "$data" := (Public, GenT 0, "Box") ]}.
Proof.
  move => f vis fty orig; split => h.
  - inv h.
    + rewrite /pdefs /= lookup_insert_ne // lookup_insert in H.
      simplify_eq.
      rewrite /Box /= lookup_singleton_Some in H0.
      by destruct H0 as [<- <-].
    + by rewrite /pdefs /= lookup_insert_ne // lookup_insert in H; simplify_eq.
  - rewrite lookup_singleton_Some in h.
    destruct h as [<- [= <- <- <-]].
    change Public with (Public, GenT 0).1.
    by econstructor.
Qed.

Lemma has_fields_IntBoxS : has_fields "IntBoxS" {[ "$data" := (Public, IntT, "Box") ]}.
Proof.
  move => f vis fty orig; split => h.
  - inv h.
    + rewrite /pdefs /= lookup_insert_ne // lookup_insert_ne // lookup_insert in H; by simplify_eq.
    + rewrite /pdefs /= lookup_insert_ne // lookup_insert_ne // lookup_insert in H; simplify_eq.
      apply lookup_singleton_Some.
      rewrite /IntBoxS /= in H1 H0.
      injection H1; intros; subst; clear H1.
      inv H2.
      * rewrite /pdefs /= lookup_insert_ne // lookup_insert in H; simplify_eq.
        rewrite /Box /= lookup_singleton_Some in H1.
        by destruct H1 as [<- <-].
      * by rewrite /pdefs /= lookup_insert_ne // lookup_insert in H; simplify_eq.
  - rewrite lookup_singleton_Some in h.
    destruct h as [<- [= <- <- <-]].
    change IntT with (subst_ty σ (GenT 0)).
    eapply InheritsField => //.
    change Public with (Public, GenT 0).1.
    econstructor; first done.
    by rewrite /Box /=.
Qed.

Lemma has_fields_Main : has_fields "Main" ∅.
Proof.
  move => f vis fty orig; split => h; last by rewrite lookup_empty in h.
  inv h.
  - rewrite lookup_insert_ne // lookup_insert_ne // in H.
    rewrite lookup_insert_ne // lookup_insert in H.
    by simplify_eq.
  - rewrite lookup_insert_ne // lookup_insert_ne // in H.
    rewrite lookup_insert_ne // lookup_insert in H.
    by simplify_eq.
Qed.

Definition final_le le new_loc1 new_loc2 : local_env :=
   <["$_":=NullV]>
  (<["$tmp":=IntV 43]>
  (<["$box":=LocV new_loc1]>
  (<["$init":= IntV 32]>
  (<["$robox":= LocV new_loc2]> le)))).

Definition final_heap (h: heap) new_loc1 new_loc2 :=
   <[new_loc1 := ("IntBoxS", {["$data" := IntV 43]})]>
  (<[new_loc2 := ("ROBox", {["$data" := IntV 32]})]> h).

Lemma Main_eval st:
 ∀ new_loc1 new_loc2,
 st.2 !! new_loc1 = None →
 st.2 !! new_loc2 = None →
 new_loc1 <> new_loc2 →
 cmd_eval "Main" st ProgramBody (final_le st.1 new_loc1 new_loc2, final_heap st.2 new_loc1 new_loc2) 8.
Proof.
  case: st => le h /= new_loc1 new_loc2 hnew1 hnew2 hnew.
  rewrite /ProgramBody.
  change 8 with (1 + (2 + (1 + (2 + (0 + (1 + 1)))))).
  eapply SeqEv.
  { apply NewEv; first by apply hnew2.
    rewrite /map_args option_guard_True /=; first by rewrite omap_singleton.
    by apply map_Forall_singleton.
  }
  eapply SeqEv.
  { eapply CallEv => /=.
    - by rewrite lookup_insert.
    - rewrite /map_args option_guard_True; first done.
      by apply map_Forall_empty.
    - by rewrite lookup_insert.
    - by apply has_method_get0.
    - done.
    - by rewrite /Get /= !dom_empty_L.
    - by rewrite omap_empty.
    - eapply GetEv.
      + by constructor.
      + by rewrite lookup_insert.
      + by rewrite lookup_insert.
      + by apply (HasField _ _ ROBox (Private, GenT 0)).
      + done.
    - by rewrite /Get /= lookup_insert.
  }
  eapply SeqEv.
  { apply NewEv.
    - rewrite lookup_insert_ne; first by exact hnew1.
      done.
    - rewrite /map_args option_guard_True /=; first by rewrite omap_singleton.
      apply map_Forall_singleton => /=.
      by rewrite lookup_insert.
  }
  eapply SeqEv.
  { eapply CallEv => /=.
    - by rewrite lookup_insert.
    - rewrite /map_args option_guard_True; first done.
      by apply map_Forall_empty.
    - by rewrite lookup_insert.
    - by apply has_method_get1.
    - done.
    - by rewrite /Get /= fmap_empty !dom_empty_L.
    - by rewrite omap_empty.
    - eapply GetEv.
      + by constructor.
      + by rewrite lookup_insert.
      + by rewrite lookup_insert.
      + eapply InheritsField => //.
        by apply (HasField _ _ Box (Public, GenT 0)).
      + done.
    - by rewrite /Get /= lookup_insert.
  }
  eapply SeqEv.
  { (* Let *)
    eapply LetEv => /=.
    by rewrite lookup_insert.
  }
  eapply SeqEv.
  { eapply CallEv => /=.
    - rewrite lookup_insert_ne //.
      by rewrite lookup_insert_ne // lookup_insert.
    - rewrite /map_args option_guard_True; first done.
      apply map_Forall_singleton => /=.
      by rewrite lookup_insert.
    - by rewrite lookup_insert.
    - by apply has_method_set.
    - done.
    - by rewrite /IntBoxSSet /= !dom_singleton_L.
    - by rewrite omap_singleton /= lookup_insert.
    - rewrite /IntBoxSSet /=.
      eapply SetEv.
      + by constructor.
      + by constructor.
      + by rewrite lookup_insert.
      + done.
      + eapply InheritsField => //.
        by apply (HasField _ _ Box (Public, GenT 0)).
      + done.
    - by rewrite /IntBoxSSet /=.
  }
  rewrite lookup_insert.
  replace (final_le le new_loc1 new_loc2) with
    ( <["$tmp" := IntV 43]>
     (<["$_":=NullV]>
     (<["$tmp":=IntV (32 + 20)]>
     (<["$tmp":=IntV 32]>
     (<["$box":=LocV new_loc1]>
     (<["$init":= IntV 32]>
     (<["$robox":= LocV new_loc2]> le))))))); last first.
  { rewrite /final_le.
    destruct le as [vthis lenv] => /=.
    rewrite /local_env_insert /=.
    f_equal.
    rewrite insert_commute //.
    f_equal.
    by rewrite !insert_insert.
  }
  replace (final_heap h new_loc1 new_loc2) with
    ( <[new_loc1:=("IntBoxS", {["$data" := IntV (33 + 20 - 10); "$data" := IntV 32]})]>
     (<[new_loc1:=("IntBoxS", {["$data" := IntV 32]})]>
     (<[new_loc2:=("ROBox", {["$data" := IntV 32]})]> h))); last first.
  { rewrite /final_heap.
    by rewrite !insert_insert.
  }
  eapply GetEv.
  - do 3 (rewrite /= lookup_insert_ne //).
    by rewrite lookup_insert.
  - by rewrite lookup_insert.
  - by rewrite lookup_insert.
  - eapply InheritsField => //.
    by apply (HasField _ _ Box (Public, GenT 0)).
  - done.
Qed.

Definition final_lty lty : local_tys :=
   <["$tmp"   := IntT]>
  (<["$_"     := NullT]>
  (<["$box"   := ClassT true "IntBoxS" []]>
  (<["$init"  := IntT]>
  (<["$robox" := ClassT true "ROBox" [IntT]]> lty)))).

Definition MainC := [(ThisT, ClassT false "Main" (gen_targs 0))].

Lemma Main_ty n lty :
  bounded_lty n lty →
  cmd_has_ty "Main" MainC Plain n lty ProgramBody (final_lty lty).
Proof.
  move => hb.
  rewrite /final_lty /ProgramBody.
  eapply SeqTy.
  { eapply NewTy.
    + reflexivity.
    + econstructor => //.
      rewrite Forall_lookup => k ty; rewrite list_lookup_singleton_Some.
      case => _ <-; by constructor.
    + constructor.
      by rewrite Forall_singleton.
    + econstructor => //.
      * move => i ty.
        rewrite list_lookup_singleton_Some => [[? <-]].
        by constructor.
      * rewrite /ROBox /= => i [??] h.
        apply list_lookup_singleton_Some in h as [? heq].
        case: heq => <- <- /=.
        by eauto.
    + by apply has_fields_ROBox.
    + by set_solver.
    + move => f fty arg.
      rewrite !lookup_singleton_Some.
      case => <- <- [_ <-].
      by constructor.
  }
  eapply SeqTy.
  { eapply CallPubTy.
    + constructor.
      by rewrite lookup_insert.
    + by apply has_method_get0.
    + by left.
    + done.
    + by set_solver.
    + move => ????; by rewrite lookup_empty.
  }
  eapply SeqTy.
  { eapply NewTy.
    + by exists [].
    + by econstructor.
    + by econstructor.
    + by econstructor.
    + by apply has_fields_IntBoxS.
    + by set_solver.
    + move => f fty arg.
      rewrite !lookup_singleton_Some.
      case => <- <- [_ <-].
      constructor.
      by rewrite lookup_insert.
  }
  eapply SeqTy.
  { eapply CallPubTy.
    + econstructor.
      by rewrite lookup_insert.
    + by apply has_method_get1.
    + by left.
    + done.
    + by set_solver.
    + by move => x ty arg; rewrite /Get /= lookup_empty.
  }
  eapply SeqTy.
  { eapply LetTy.
    constructor; first done.
    + constructor; by rewrite lookup_insert.
    + by constructor.
  }
  eapply SeqTy.
  { eapply CallPubTy.
    + econstructor.
      rewrite lookup_insert_ne // lookup_insert_ne //.
      by rewrite lookup_insert.
    + by apply has_method_set.
    + by left.
    + done.
    + by set_solver.
    + move => x ty arg; rewrite /Get /= !lookup_singleton_Some.
      case => <- <- [_ <-].
      constructor; first done.
      - constructor; by rewrite lookup_insert.
      - by constructor.
  }
  rewrite /IntBoxSSet /=.
  eapply SubTy; last first.
  - eapply GetPubTy; [ | by apply has_fields_IntBoxS | by right ].
    constructor.
    do 3 (rewrite lookup_insert_ne //).
    by rewrite lookup_insert.
  - apply insert_bounded_lty; first done.
    apply map_Forall_insert_2; first done.
    apply map_Forall_insert_2.
    { apply bounded_ge with 0; last by lia.
      constructor.
      by apply Forall_nil.
    }
    apply map_Forall_insert_2; first done.
    apply map_Forall_insert_2.
    { apply bounded_ge with 0; last by lia.
      constructor.
      by apply Forall_singleton.
    }
    by apply hb.
  - move => v ty.
    rewrite lookup_insert_Some.
    case => [[<- <-] | [? h]].
    + exists IntT; by rewrite lookup_insert.
    + rewrite lookup_insert_ne //.
      destruct (decide (v = "$_")) as [-> | ?].
      * rewrite lookup_insert in h.
        case: h => <-.
        exists NullT; by rewrite lookup_insert.
      * rewrite lookup_insert_ne //.
        rewrite lookup_insert_ne //.
        rewrite lookup_insert_ne //.
      destruct (decide (v = "$box")) as [-> | ?].
      { rewrite lookup_insert.
        rewrite lookup_insert_ne // lookup_insert in h.
        case : h => <-.
        by eexists.
      }
      rewrite lookup_insert_ne // in h.
      rewrite lookup_insert_ne // in h.
      exists ty.
      by rewrite lookup_insert_ne.
Qed.

Lemma wf_mdef_ty_Main: wf_mdef_ty "Main" MainC 0 EntryPoint.
Proof.
  rewrite /wf_mdef_ty.
  exists (final_lty (methodargs EntryPoint)).
  repeat split.
  - rewrite /final_lty /wf_lty /=.
    rewrite map_Forall_lookup => k tk.
    rewrite lookup_insert_Some.
    case => [[? <-] | [?]]; first by constructor.
    rewrite lookup_insert_Some.
    case => [[? <-] | [?]]; first by econstructor.
    rewrite lookup_insert_Some.
    case => [[? <-] | [?]]; first by econstructor.
    rewrite lookup_insert_Some.
    case => [[? <-] | [?]]; first by econstructor.
    rewrite lookup_insert_Some.
    case => [[? <-] | [?]]; last by rewrite lookup_empty.
    econstructor => //.
    by constructor.
  - apply Main_ty .
    simpl.
    by apply map_Forall_empty.
  - rewrite /final_lty.
    constructor => //.
    + constructor.
      by rewrite /= lookup_insert.
    + by constructor.
Qed.

Lemma helper_ext: ∀ A B σ0, extends_using A B σ0 → A = "IntBoxS" ∧ B = "Box" ∧ σ0 = σ.
Proof.
  move => A B σ0 h; inv h.
  rewrite /pdefs /= lookup_insert_Some in H.
  destruct H as [[<- <-] | [? H]].
  { by rewrite /Box in H0. }
  rewrite lookup_insert_Some in H.
  destruct H as [[<- <-] | [? H]].
  { rewrite /Box /= in H0; by simplify_eq. }
  rewrite lookup_insert_Some in H.
  destruct H as [[<- <-] | [? H]].
  { rewrite /IntBoxS /= in H0; by simplify_eq. }
  rewrite lookup_singleton_Some in H.
  destruct H as [<- <-].
  rewrite /Main in H0; discriminate.
Qed.

Lemma helper_in_ROBox : ∀ T σt, inherits_using "ROBox" T σt → T = "ROBox" ∧ σt = [GenT 0].
Proof.
  move => T σt h; inv h.
  + rewrite /pdefs /=.
    rewrite lookup_insert in H.
    by simplify_eq.
  + apply helper_ext in H.
    destruct H; discriminate.
Qed.

Lemma helper_in_Main : ∀ T σt, inherits_using "Main" T σt → T = "Main" ∧ σt = [].
Proof.
  move => T σt h; inv h.
  + rewrite /pdefs /=.
    do 3 (rewrite lookup_insert_ne // in H).
    rewrite lookup_singleton_Some in H.
    by case : H => _ <-.
  + apply helper_ext in H.
    destruct H; discriminate.
Qed.

Lemma helper_in_Box : ∀ T σt, inherits_using "Box" T σt → T = "Box" ∧ σt = [GenT 0].
Proof.
  move => T σt h; inv h.
  + rewrite /pdefs /=.
    do 1 (rewrite lookup_insert_ne // in H).
    rewrite lookup_insert in H.
    by simplify_eq.
  + apply helper_ext in H.
    destruct H; discriminate.
Qed.

Lemma helper_in_IntBoxS : ∀ T σt, inherits_using "IntBoxS" T σt →
  (T = "IntBoxS" ∧ σt = []) ∨
  (T = "Box" ∧ σt = σ).
Proof.
  move => T σt h; inv h.
  + rewrite /pdefs /=.
    do 2 (rewrite lookup_insert_ne // in H).
    rewrite lookup_insert in H.
    left.
    by simplify_eq.
  + apply helper_ext in H.
    destruct H as [_ [-> ->]]; right.
    apply helper_in_Box in H0 as [-> ->].
    done.
Qed.

Lemma helper_in: ∀ A B σ0, inherits_using A B σ0 →
     (A = "IntBoxS" ∧ B = "Box" ∧ σ0 = σ) ∨
     (A = "IntBoxS" ∧ B = "IntBoxS" ∧ σ0 = []) ∨
     (A = "Box" ∧ B = "Box" ∧ σ0 = [GenT 0]) ∨
     (A = "ROBox" ∧ B = "ROBox" ∧ σ0 = [GenT 0]) ∨
     (A = "Main" ∧ B = "Main" ∧ σ0 = []).
Proof.
  move => A B σ0 h.
  inv h.
  + rewrite /pdefs /=.
    rewrite lookup_insert_Some in H.
    destruct H as [[<- ?]|[? H]]; first (right; right; right; left; by rewrite -H).
    rewrite lookup_insert_Some in H.
    destruct H as [[<- ?]|[? H]]; first (right; right; left; by rewrite -H).
    rewrite lookup_insert_Some in H.
    destruct H as [[<- ?]|[? H]]; first (right; left; by rewrite -H).
    rewrite lookup_insert_Some in H.
    destruct H as [[<- ?]|[? H]]; last by (by rewrite lookup_empty in H).
    right; right; right; right; by rewrite -H.
  + apply helper_ext in H as [-> [-> ->]].
    apply helper_in_Box in H0 as [-> ->].
    by left.
Qed.

Lemma wf_parent : map_Forall (λ _cname, wf_cdef_parent) pdefs.
Proof.
  apply: wf_cdef_parent_context_correct.
  exact (I <: True).
Qed.

Global Hint Resolve wf_parent : core.

Lemma wf_override : wf_method_override.
Proof.
  move => A B adef bdef m σ0 mA mB hA hB hin hmA hmB.
  apply helper_in in hin.
  destruct hin as [[-> [-> ->]] | hin].
  { rewrite /pdefs /= in hA, hB.
    do 2 (rewrite lookup_insert_ne // in hA).
    do 1 (rewrite lookup_insert_ne // in hB).
    rewrite !lookup_insert in hA, hB.
    simplify_eq.
    rewrite /IntBoxS /= in hmA.
    rewrite /Box /= in hmB.
    rewrite lookup_singleton_Some in hmA.
    destruct hmA as [<- <-].
    rewrite lookup_insert in hmB.
    case : hmB => <-.
    rewrite /mdef_incl /IntBoxSSet /BoxSet /subst_mdef /σ /=.
    split; first by set_solver.
    split; last done.
    move => k A B.
    rewrite lookup_singleton_Some.
    case => [<- <-].
    rewrite lookup_fmap_Some.
    case => [ty [<-]].
    rewrite lookup_insert.
    by case => <-.
  }
  destruct hin as [[-> [-> ->]] | hin].
  { simplify_eq.
    rewrite /pdefs /=.
    do 2 (rewrite  lookup_insert_ne // in hA).
    rewrite lookup_insert in hA.
    injection hA; intros; subst; clear hA.
    rewrite /Main /= in hmA.
    rewrite lookup_singleton_Some in hmA.
    destruct hmA as [_ <-].
    rewrite subst_mdef_nil.
    by apply mdef_incl_reflexive.
  }
  destruct hin as [[-> [-> ->]] | hin].
  { simplify_eq.
    rewrite /pdefs /=.
    do 1 (rewrite  lookup_insert_ne // in hA).
    rewrite lookup_insert in hA.
    injection hA; intros; subst; clear hA.
    rewrite /Box /= in hmA.
    rewrite lookup_insert_Some in hmA.
    destruct hmA as [[<- <-]|[? hmA]].
    + rewrite /mdef_incl /BoxSet /subst_mdef /=.
      split; first by set_solver.
      split; last done.
      move => k A B.
      rewrite lookup_singleton_Some.
      case => [<- <-].
      rewrite lookup_fmap lookup_insert /=.
      by case => <-.
    + rewrite lookup_singleton_Some in hmA.
      destruct hmA as [<- <-].
      rewrite /mdef_incl /Get /subst_mdef /=.
      split; first by set_solver.
      split; last done.
      move => k A B.
      by rewrite lookup_empty.
  }
  destruct hin as [[-> [-> ->]] | hin].
  { simplify_eq.
    rewrite /pdefs /=.
    rewrite lookup_insert in hA.
    injection hA; intros; subst; clear hA.
    rewrite /IntBoxS /= in hmA.
    rewrite lookup_singleton_Some in hmA.
    destruct hmA as [<- <-].
    rewrite /mdef_incl /IntBoxSSet /subst_mdef /=.
    split; first by set_solver.
    split; last done.
    move => k A B.
    by rewrite lookup_empty.
  }
  destruct hin as [-> [-> ->]].
  { simplify_eq.
    rewrite /pdefs /=.
    do 3 (rewrite lookup_insert_ne // in hA).
    rewrite lookup_singleton_Some in hA.
    destruct hA as [_ <-].
    rewrite /Main /= in hmA.
    rewrite lookup_singleton_Some in hmA.
    destruct hmA as [<- <-].
    rewrite /mdef_incl /EntryPoint /subst_mdef /=.
    split; first by set_solver.
    split; last done.
    move => k A B.
    by rewrite lookup_empty.
  }
Qed.

Lemma wf_fields : map_Forall (λ _cname, wf_cdef_fields) pdefs.
Proof.
  apply (wf_fields_correct _ 100).
  by exact (I <: True).
Qed.

Lemma wf_fields_bounded : map_Forall (λ _cname, wf_cdef_fields_bounded) pdefs.
Proof.
  apply wf_cdef_fields_bounded_context_correct.
  by exact (I <: True).
Qed.

Lemma wf_fields_wf  : map_Forall (λ _cname, wf_cdef_fields_wf) pdefs.
Proof.
  apply: wf_cdef_fields_wf_context_correct.
  exact (I <: True).
Qed.

Lemma wf_fields_mono : map_Forall (λ _cname, wf_field_mono) pdefs.
Proof.
  apply wf_fields_mono_correct.
  exact (I <: True).
Qed.

Lemma wf_methods_bounded : map_Forall (λ _cname, cdef_methods_bounded) pdefs.
Proof.
  apply cdef_methods_bounded_context_correct.
  by exact (I <: True).
Qed.

Lemma wf_methods_wf : map_Forall (λ _cname, wf_cdef_methods_wf) pdefs.
Proof.
  apply: wf_cdef_methods_wf_context_correct.
  exact (I <: True).
Qed.

Lemma wf_methods_mono : map_Forall (λ _cname, wf_cdef_methods_mono) pdefs.
Proof.
  apply wf_methods_mono_correct.
  exact (I <: True).
Qed.

Lemma wf_mdefs : map_Forall cdef_wf_mdef_ty pdefs.
Proof.
  rewrite map_Forall_lookup => c0 d0.
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]].
  { rewrite /cdef_wf_mdef_ty /ROBox /=.
    rewrite map_Forall_singleton.
    eexists.
    split; first last.
    - rewrite /Get /=; split.
      + by eapply GetPrivTy.
      + by econstructor.
    - rewrite /wf_lty map_Forall_lookup => x tx /=.
      rewrite lookup_insert_Some.
      case => [[? <-]|[?]]; last by rewrite lookup_empty.
      by constructor.
  }
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]].
  { rewrite /cdef_wf_mdef_ty /Box /=.
    rewrite map_Forall_lookup => x mx.
    rewrite lookup_insert_Some.
    case => [[? <-]|[?]].
    * rewrite /wf_mdef_ty /BoxSet /=.
      eexists.
      split; first last.
      { split ; last by constructor.
        eapply SetThisTy.
        - by constructor.
        - done.
        - simpl.
          change Public with (Public, GenT 0).1.
          by eapply HasField.
        - by constructor.
      }
      rewrite /wf_lty map_Forall_lookup => k t /=.
      rewrite lookup_singleton_Some.
      case => [? <-].
      by constructor.
    * rewrite lookup_insert_Some.
      case => [[? <-]|[?]]; last by rewrite lookup_empty.
      rewrite /wf_mdef_ty /Get /=.
      eexists; split; first last.
      { split.
        - eapply GetThisTy.
          + by constructor.
          + done.
          + change Public with (Public, GenT 0).1.
            by eapply HasField.
        - by constructor.
      }
      rewrite /wf_lty map_Forall_lookup => k t /=.
      rewrite lookup_insert_Some.
      case => [[? <-]|[?]]; first by constructor.
      by rewrite lookup_empty.
  }
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]].
  { rewrite /cdef_wf_mdef_ty /IntBoxS /=.
    rewrite map_Forall_singleton.
    eexists.
    split; first last.
    - split; last by constructor.
      rewrite /IntBoxSSet /=.
      eapply SetThisTy.
      + by constructor.
      + done.
      + eapply InheritsField => //.
        change Public with (Public, GenT 0).1.
        by eapply HasField.
      + constructor => //.
        * constructor.
          by rewrite /= lookup_insert.
        * by constructor.
    - rewrite /wf_lty map_Forall_lookup => x tx /=.
      rewrite lookup_singleton_Some.
      case => [? <-].
      by constructor.
  }
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]]; last by rewrite lookup_empty.
  rewrite /cdef_wf_mdef_ty /Main /=.
  apply map_Forall_singleton.
  by apply wf_mdef_ty_Main.
Qed.

Lemma wf_mono : map_Forall (λ _cname, wf_cdef_mono) pdefs.
Proof.
  apply wf_mono_correct.
  exact (I <: True).
Qed.

Lemma wf_constraints_wf : map_Forall (λ _cname, wf_cdef_constraints_wf) pdefs.
Proof.
  apply: wf_cdef_constraints_wf_context_correct.
  exact (I <: True).
Qed.

Lemma wf_constraints_bounded : map_Forall (λ _cname, wf_cdef_constraints_bounded) pdefs.
Proof.
  apply wf_cdef_constraints_bounded_context_correct.
  by exact (I <: True).
Qed.

Lemma wf_constraints_no_this: map_Forall (λ _ : string, wf_cdef_constraints_no_this) pdefs.
Proof.
 apply wf_constraints_no_this_correct.
  by exact (I <: True).
Qed.

Lemma wf_parent_ok : map_Forall (λ _cname, wf_cdef_parent_ok) pdefs.
Proof.
  rewrite map_Forall_lookup => c0 d0.
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]].
  { by rewrite /wf_cdef_parent_ok . }
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]].
  { by rewrite /wf_cdef_parent_ok. }
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]].
  { rewrite /wf_cdef_parent_ok /=.
    econstructor => //.
    rewrite /σ => i ty.
    rewrite list_lookup_singleton_Some => [[? <-]].
    by constructor.
  }
  rewrite lookup_singleton_Some.
  case => [? <-].
  by rewrite /wf_cdef_parent_ok.
Qed.

Lemma wf_constraints_ok : map_Forall (λ _cname, wf_cdef_constraints_ok) pdefs.
Proof.
  rewrite map_Forall_lookup => c0 d0.
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]].
  { rewrite /wf_cdef_constraints_ok /ROBox /= /ok_constraints Forall_singleton.
    split => /=; by repeat constructor.
  }
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]].
  { rewrite /wf_cdef_constraints_ok; by constructor. }
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]].
  { rewrite /wf_cdef_constraints_ok; by constructor. }
  rewrite lookup_singleton_Some.
  case => [? <-].
  rewrite /wf_cdef_constraints_ok; by constructor.
Qed.

Lemma wf_methods_ok : map_Forall (λ _cname, cdef_methods_ok) pdefs.
Proof.
  rewrite map_Forall_lookup => c0 d0.
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]].
  { rewrite /cdef_methods_ok /ROBox /=.
    apply map_Forall_singleton.
    rewrite /mdef_ok /Get /=.
    split; last by constructor.
    by apply map_Forall_empty.
  }
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]].
  { rewrite /cdef_methods_ok /Box /=.
    rewrite map_Forall_lookup => x mx.
    rewrite lookup_insert_Some.
    case => [[? <-]|[?]].
    * rewrite /mdef_ok /BoxSet /=.
      split; last by constructor.
      apply map_Forall_singleton.
      by constructor.
    * rewrite lookup_insert_Some.
      case => [[? <-]|[?]]; last by rewrite lookup_empty.
      rewrite /mdef_ok /Get /=.
      split; first by apply map_Forall_empty.
      by constructor.
  }
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]].
  { rewrite /cdef_methods_ok /IntBoxS /=.
    apply map_Forall_singleton.
    rewrite /mdef_ok /IntBoxSSet /=.
    split; last by constructor.
    apply map_Forall_singleton.
    by constructor.
  }
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]]; last by rewrite lookup_empty.
  rewrite /cdef_methods_ok /Main /=.
  apply map_Forall_singleton.
  split; last by constructor.
  by apply map_Forall_empty.
Qed.

Lemma wf_extends_dyn : map_Forall wf_cdef_extends_dyn pdefs.
Proof.
  rewrite map_Forall_lookup => c0 d0.
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]] //.
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]] //.
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]] //.
  { rewrite /wf_cdef_extends_dyn /IntBoxS /=.
    exists Box; split => //.
    move => i c /=.
    rewrite list_lookup_singleton_Some.
    case => ? <-.
    constructor; by set_solver.
  }
  rewrite lookup_insert_Some.
  case => [[? <-]|[?]]; last by rewrite lookup_empty.
  done.
Qed.

Lemma has_method_ROBox m o mdef:
  has_method m "ROBox" o mdef →
  m = "get" ∧ o = "ROBox" ∧ mdef = Get.
Proof.
  move => h; inv h; last first.
  { rewrite lookup_insert in H.
    by simplify_eq.
  }
  rewrite lookup_insert in H.
  simplify_eq.
  rewrite lookup_singleton_Some in H0.
  by firstorder.
Qed.

Lemma has_method_Box m o mdef:
  has_method m "Box" o mdef →
  (m = "get" ∧ o = "Box" ∧ mdef = Get) ∨
  (m = "set" ∧ o = "Box" ∧ mdef = BoxSet).
Proof.
  move => h; inv h; last first.
  { rewrite lookup_insert_ne // lookup_insert in H.
    by simplify_eq.
  }
  rewrite lookup_insert_ne // lookup_insert in H.
  simplify_eq.
  rewrite lookup_insert_Some in H0.
  case: H0 => [[? <-]|[?]].
  - by firstorder.
  - rewrite lookup_singleton_Some => h.
    by firstorder.
Qed.

Lemma has_method_IntBoxS m o mdef:
  has_method m "IntBoxS" o mdef →
  (m = "get" ∧ o = "Box" ∧ mdef = subst_mdef σ Get) ∨
  (m = "set" ∧ o = "Box" ∧ mdef = subst_mdef σ BoxSet) ∨
  (m = "set" ∧ o = "IntBoxS" ∧ mdef = IntBoxSSet).
Proof.
  move => h; inv h.
  - rewrite lookup_insert_ne // in H.
    rewrite lookup_insert_ne // lookup_insert in H.
    simplify_eq.
    rewrite lookup_singleton_Some in H0.
    by firstorder.
  - rewrite lookup_insert_ne // in H.
    rewrite lookup_insert_ne // lookup_insert in H.
    simplify_eq.
    rewrite /IntBoxS /= in H1.
    simplify_eq.
    apply has_method_Box in H2.
    case : H2 => [ [<- [<- <-]]| ].
    { by left. }
    case => <- [<- <-].
    right; by left.
Qed.

Lemma has_method_Main m o mdef:
  has_method m "Main" o mdef →
  m = "entry_point" ∧ o = "Main" ∧ mdef = EntryPoint.
Proof.
  move => h; inv h; last first.
  { rewrite lookup_insert_ne // in H.
    rewrite lookup_insert_ne // in H.
    rewrite lookup_insert_ne // lookup_insert in H.
    by simplify_eq.
  }
  rewrite lookup_insert_ne // in H.
  rewrite lookup_insert_ne // in H.
  rewrite lookup_insert_ne // lookup_insert in H.
  simplify_eq.
  rewrite lookup_singleton_Some in H0.
  by firstorder.
Qed.

Lemma wf_methods_dyn : map_Forall wf_cdef_methods_dyn_wf pdefs.
Proof.
  rewrite map_Forall_lookup => c0 d0.
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]].
  { move => m o mdef hm.
    apply has_method_ROBox in hm as (-> & -> & ->).
    exists (gen_targs (length ROBox.(generics))).
    split; first by constructor.
    move => i c /=.
    rewrite list_lookup_singleton_Some.
    case => ? <-.
    constructor; by set_solver.
  }
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]].
  { move => m o mdef hm.
    apply has_method_Box in hm as [(-> & -> & ->) | (-> & -> & ->)].
    + exists (gen_targs (length Box.(generics))).
      split; first by constructor.
      move => i c /=.
      rewrite list_lookup_singleton_Some.
      case => ? <-.
      constructor; by set_solver.
    + exists (gen_targs (length Box.(generics))).
      split; first by constructor.
      move => i c /=.
      rewrite list_lookup_singleton_Some.
      case => ? <-.
      constructor; by set_solver.
  }
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]].
  { move => m o mdef hm.
    apply has_method_IntBoxS in hm as [(-> & -> & ->) | [(-> & -> & ->) | (-> & -> & ->)]].
    + exists σ.
      split.
      { apply inherits_using_extends => //.
        by econstructor.
      }
      move => i c /=.
      rewrite list_lookup_singleton_Some.
      case => ? <-.
      constructor; by set_solver.
    + exists σ.
      split.
      { apply inherits_using_extends => //.
        by econstructor.
      }
      move => i c /=.
      rewrite list_lookup_singleton_Some.
      case => ? <-.
      constructor; by set_solver.
    + exists (gen_targs (length IntBoxS.(generics))).
      split; first by constructor.
      move => i c /=.
      rewrite list_lookup_singleton_Some.
      case => ? <-.
      constructor; by set_solver.
  }
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]]; last by rewrite lookup_empty.
  { move => m o mdef hm.
    apply has_method_Main in hm as (-> & -> & ->).
    exists (gen_targs (length Main.(generics))).
    split; first by constructor.
    move => i c /=.
    rewrite list_lookup_singleton_Some.
    case => ? <-.
    constructor; by set_solver.
  }
Qed.

Lemma wf_fields_dyn : map_Forall wf_cdef_fields_dyn_wf pdefs.
Proof.
  rewrite map_Forall_lookup => c0 d0.
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]].
  { move => fields hf.
    move : has_fields_ROBox => hf0.
    rewrite (has_fields_fun _ _ _  hf hf0).
    by apply map_Forall_singleton.
  }
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]].
  { move => fields hf.
    move : has_fields_Box => hf0.
    rewrite (has_fields_fun _ _ _  hf hf0).
    apply map_Forall_singleton => /=; split.
    + apply SubFalse; first done.
      constructor; by set_solver.
    + apply SubFalse; first done.
      constructor; by set_solver.
  }
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]].
  { move => fields hf.
    move : has_fields_IntBoxS => hf0.
    rewrite (has_fields_fun _ _ _  hf hf0).
    apply map_Forall_singleton => /=; split.
    + apply SubFalse; first done.
      constructor; by set_solver.
    + apply SubFalse; first done.
      constructor; by set_solver.
  }
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]]; last by rewrite lookup_empty.
  { move => fields hf.
    move : has_fields_Main => hf0.
    rewrite (has_fields_fun _ _ _ hf hf0).
    by apply map_Forall_empty.
  }
Qed.

Lemma wf_mdefs_dyn : map_Forall cdef_wf_mdef_dyn_ty pdefs.
Proof.
  rewrite map_Forall_lookup => c0 d0.
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]].
  { move => k m hm.
    assert (wf_lty ∅) by done.
    exists ∅; split; first done.
    split.
    - apply FalseCmdTy => //.
      apply SubConstraint.
      by set_solver.
    - apply FalseTy => //.
      apply SubConstraint.
      by set_solver.
  }
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]] //.
  { move => k m hm.
    assert (wf_lty ∅) by done.
    exists ∅; split; first done.
    split.
    - apply FalseCmdTy => //.
      apply SubConstraint.
      by set_solver.
    - apply FalseTy => //.
      apply SubConstraint.
      by set_solver.
  }
  rewrite lookup_insert_Some.
  case => [[<- <-]|[?]] //.
  { move => k m hm.
    assert (wf_lty ∅) by done.
    exists ∅; split; first done.
    split.
    - apply FalseCmdTy => //.
      apply SubConstraint.
      by set_solver.
    - apply FalseTy => //.
      apply SubConstraint.
      by set_solver.
  }
  rewrite lookup_singleton_Some.
  case => <- <-.
  { move => k m hm.
    assert (wf_lty ∅) by done.
    exists ∅; split; first done.
    split.
    - apply FalseCmdTy => //.
      apply SubConstraint.
      by set_solver.
    - apply FalseTy => //.
      apply SubConstraint.
      by set_solver.
  }
Qed.

Lemma wf: wf_cdefs.
Proof.
  split.
  by apply wf_parent.
  by apply wf_parent_ok.
  by apply wf_constraints_wf.
  by apply wf_constraints_ok.
  by apply wf_constraints_bounded.
  by apply wf_constraints_no_this.
  by apply wf_override.
  by apply wf_fields.
  by apply wf_fields_bounded.
  by apply wf_fields_wf.
  by apply wf_fields_mono.
  by apply wf_methods_bounded.
  by apply wf_methods_wf.
  by apply wf_methods_mono.
  by apply wf_methods_ok.
  by apply wf_mdefs.
  by apply wf_mono.
  by apply wf_extends_dyn.
  by apply wf_methods_dyn.
  by apply wf_fields_dyn.
  by apply wf_mdefs_dyn.
Qed.

(* Director level theorem: every execution that should produce an int
 * actually produceGs an int.
 *)
Theorem int_soundness cmd st lty n:
  cmd_eval "Main" (main_le, main_heap "Main") cmd st n →
  cmd_has_ty "Main" MainC Plain 0 main_lty cmd lty →
  ∀ v, lty !! v = Some IntT →
  ∃ z, st.1.(lenv) !! v = Some (IntV z).
Proof.
  assert (wfinit : wf_lty main_lty ) by done.
  assert (hinit: pdefs !! "Main" = Some (main_cdef {["entry_point" := EntryPoint ]})) by done.
  move => he ht v hin.
  apply (@step_updN_soundness sem_heapΘ n).
  iMod sem_heap_init as (Hheap) "Hmain" => //.
  iModIntro.
  iAssert (□ interp_env_as_mixed [])%I as "#wfΣ".
  { iModIntro; iIntros (? ? h).
    by rewrite lookup_nil in h.
  }
  iAssert (□ Σinterp
     (interp_exact_tag interp_type "Main" []) [] MainC)%I as "Σcoherency".
  { iModIntro; iIntros (? ? h).
    apply list_lookup_singleton_Some in h as [-> <-] => /=.
    iIntros (w) "hw".
    rewrite interp_this_unfold interp_tag_unfold /=.
    by iApply exact_subtype_is_inclusion_aux.
  }
  assert (wfΔ : Forall wf_constraint MainC).
  { apply Forall_singleton.
    split; first by constructor.
    econstructor => //.
    by apply Forall_nil.
  }
  assert (hbounded: bounded_lty 0 main_lty).
  { by repeat constructor. }
  assert (hΔb : Forall (bounded_constraint 0) MainC).
  { by repeat econstructor. }
  assert (heqΣ: interp_list interp_nothing [] [] ≡ []) by done.
  iDestruct ((cmd_soundness "Main" Main MainC _ _ _ _ [] wf wfinit
    hbounded wfΔ hΔb _ "Main" Main [] _ _ _ _ ht  _ _ _ _ he)
    $! heqΣ with "wfΣ wfΣ Σcoherency Hmain") as "H" => /=.
  iRevert "H".
  iApply updN_mono.
  iIntros "[Hh [Hthis Hl]]".
  iSpecialize ("Hl" $! v IntT hin).
  iDestruct "Hl" as (w hw) "Hw".
  rewrite interp_type_unfold /=.
  iDestruct "Hw" as (z) "->".
  by eauto.
  Unshelve.
  - done.
  - done.
  - done.
  - change [] with (gen_targs (length Main.(generics))).
    by constructor.
  - simpl.
    by lia.
Qed.

(* Don't distinguish between exact and inexact classes.
 * We could state a stronger lemma if the type's exact !
 *)
Theorem class_soundness cmd st lty n:
  cmd_eval "Main" (main_le, main_heap "Main") cmd st n →
  cmd_has_ty "Main" MainC Plain 0 main_lty cmd lty →
  ∀ x exact_ t σ, lty !! x = Some (ClassT exact_ t σ) →
  ∃ l Tdyn vs, st.1.(lenv) !! x = Some (LocV l) ∧
          st.2 !! l = Some (Tdyn, vs) ∧
          inherits Tdyn t.
Proof.
  assert (wfinit : wf_lty main_lty ) by done.
  assert (hinit: pdefs !! "Main" = Some (main_cdef {["entry_point" := EntryPoint ]})) by done.
  move => he ht x exact_ t σ hin.
  assert (wfΔ : Forall wf_constraint MainC).
  { apply Forall_singleton.
    split; first by constructor.
    econstructor => //.
    by apply Forall_nil.
  }
  assert (hwflty : wf_lty lty).
  { apply cmd_has_ty_wf in ht => //.
    + by apply wf_fields_wf.
    + by apply wf_methods_wf.
  }
  apply (@step_updN_soundness sem_heapΘ n).
  iMod sem_heap_init as (Hheap) "Hmain" => //.
  iModIntro.
  iAssert (□ interp_env_as_mixed [])%I as "#wfΣ".
  { iModIntro; iIntros (? ? h).
    by rewrite lookup_nil in h.
  }
  pose (Σthis := interp_exact_tag interp_type "Main" []).
  iAssert (□ Σinterp Σthis [] MainC)%I as "Σcoherency".
  { iModIntro; iIntros (? ? h).
    apply list_lookup_singleton_Some in h as [-> <-] => /=.
    iIntros (w) "hw".
    rewrite interp_this_unfold interp_tag_unfold /=.
    by iApply exact_subtype_is_inclusion_aux.
  }
  assert (hwft: wf_ty (ClassT true t σ)).
  { apply hwflty in hin.
    by eapply wf_ty_exact.
  }
  assert (hx: ∃ Tdef, pdefs !! t = Some Tdef ∧
              length (go interp_type Σthis [] <$> σ) = length Tdef.(generics)).
  { apply wf_tyI in hwft as (Tdef & ? & ? & ?).
    exists Tdef; by rewrite map_length.
  }
  destruct hx as (Tdef & hTdef & hlen).
  assert (hbounded: bounded_lty 0 main_lty).
  { by apply map_Forall_empty. }
  assert (hΔb : Forall (bounded_constraint 0) MainC).
  { by repeat econstructor. }
  assert (heqΣ: interp_list interp_nothing [] [] ≡ []) by done.
  iDestruct ((cmd_soundness "Main" Main MainC _ _ _ _ [] wf wfinit
    hbounded wfΔ hΔb _ "Main" Main [] _ _ _ _ ht  _ _ _ _ he)
    $! heqΣ with "wfΣ wfΣ Σcoherency Hmain") as "H" => /=.
  iRevert "H".
  iApply updN_mono.
  iIntros "[Hh [_ Hl]]".
  iSpecialize ("Hl" $! x (ClassT exact_ t σ) hin).
  iDestruct "Hl" as (w hw) "Hw".
  iAssert (□ interp_env_as_mixed [])%I as "#wfΣ".
  { iModIntro; iIntros (? ? h).
    by rewrite lookup_nil in h.
  }
  iAssert (□ interp_as_mixed Σthis)%I as "#hΣthis".
  { iModIntro; iIntros (w0) "hw0".
    iLeft; iRight; iRight.
    iExists "Main", [], Main; iSplit; first done.
    by iApply (exact_subtype_is_inclusion_aux with "wfΣ hw0").
  }
  iDestruct (exact_subtype_is_inclusion with "wfΣ hΣthis Hw") as "Hw" => //.
  rewrite interp_type_unfold /=.
  rewrite interp_tag_equiv //; first last.
  iDestruct "Hw" as (l dynt cdef tdef σ0 Σt fields ifields) "(%hpure & #hmixed & #hΣt & #hinst & #hdyn & #Hl)".
  destruct hpure as (-> & hcdef & htdef & hl1 & hinherits & hfields & hidom).
  destruct st as [le h]; simpl in *.
  iDestruct "Hh" as (sh) "(H● & %Hdom & #Hh)".
  iDestruct (sem_heap_own_valid_2 with "H● Hl") as "#HΦ".
  iAssert (⌜is_Some (sh !! l)⌝)%I as "%h_sh_l".
  { by iRewrite "HΦ". }
  assert (h_h_l : is_Some (h !! l)).
  { assert (hh: l ∈ dom sh) by (by apply elem_of_dom).
    rewrite Hdom in hh.
    by apply elem_of_dom in hh.
  }
  destruct h_h_l as [[Tdyn vs] hl].
  iDestruct ("Hh" with "[//]") as (?) "[H H▷]".
  iRewrite "H" in "HΦ".
  rewrite option_equivI prod_equivI /=.
  iDestruct "HΦ" as "[%Ht HΦ]".
  fold_leibniz; subst.
  iPureIntro.
  exists l, dynt, vs; repeat split => //.
  by apply inherits_using_erase in hinherits.
  Unshelve.
  - done.
  - done.
  - done.
  - change [] with (gen_targs (length Main.(generics))).
    by constructor.
  - simpl.
    by lia.
Qed.

Print Assumptions int_soundness.
Print Assumptions class_soundness.

author: facebookresearch

repo: shack

save_path: github-repos/coq/facebookresearch-shack


text:
Require Import mathcomp.ssreflect.all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".

(* A basic "language" that consists only of adding and constants *)
Inductive term : Set :=
| N : nat -> term
| Plus : term -> term -> term.
Hint Constructors term.

(* (1 + 0) + 5 *)
Definition randomTerm : term := (Plus (Plus (N 1) (N 0)) (N 5)).

(* An evaluator for our language *)
Fixpoint teval (t : term) :=
  match t with
    | (N x) => x
    | (Plus t1 t2) => (teval t1) + (teval t2)
  end.

(* Prints out 6 *)
Eval compute in (teval randomTerm).

(* Get rid of some +0s *)
Fixpoint compile (t : term) :=
  match t with
  | (N x) => (N x)
  | (Plus (N 0) t2) => compile t2
  | (Plus t1 (N 0)) => compile t1
  | (Plus t1 t2) => (Plus (compile t1) (compile t2))
  end.

Definition compiledRandomTerm : term := (compile randomTerm).

(* Print it out *)
(* Plus (N 1) (N 5) *)
Eval compute in compiledRandomTerm.

(* Also 6 *)
Eval compute in (teval randomTerm).

(* Ignore what this really bad proof is actually doing, this is a whole bunch of code generation steps *)
Lemma compile_correct : forall t,
    (eq (teval t) (teval (compile t))).
  elim.
  - eauto.
  - move=> l IH_l r IH_r.
    simpl.
    case: l IH_l.
    + case.
      * rewrite IH_r.
        reflexivity.
      * move=> n _.
        case: r IH_r.
        -- case.
           ++ simpl.
                rewrite addn0.
                reflexivity.
           ++ by simpl.
        -- move=> t t0 te.
           rewrite te.
           reflexivity.
    + elim: r IH_r.
      * case.
        -- simpl (teval (N 0)).
           intros.
           rewrite addn0.
           assumption.
        -- intros.
           rewrite IH_l.
           constructor.
      * intros.
        rewrite IH_r IH_l.
        constructor.
Qed.

Print compile_correct.

(* Formally define what it means for a step to occur *)
Inductive step : term -> term -> Prop :=
| SPlus1 : forall e1 e1' e2, step e1 e1' -> step (Plus e1 e2) (Plus e1' e2)
| SPlus2 : forall n e2 e2', step e2 e2' -> step (Plus (N n) e2) (Plus (N n) e2')
| SPlus : forall n1 n2, step (Plus (N n1) (N n2)) (N (n1 + n2)).
Hint Constructors step.

(* You can step from (1 + 0) to 1 *)
Definition step_n01 : step (Plus (N 1) (N 0)) (N 1) := SPlus 1 0.

(* You can step from ((1 + 0) + 5) to (1 + 5) *)
(* We could omit the first two arguments to SPlus1 because they can be deduced from its last argument *)
Definition step_randomTerm : step randomTerm (Plus (N 1) (N 5)) := SPlus1 (N 5) step_n01.

(* Less tedious way to do this *)
Lemma step_randomTerm_codegen : step randomTerm (Plus (N 1) (N 5)).
  unfold randomTerm.
  apply: SPlus1.
  apply: SPlus.
Qed.

(* It generates the same code as what we just put in step_randomTerm *)
Print step_randomTerm_codegen.

(* Relation between source and compiled code *)
Inductive sim : term -> term -> Prop :=
| sim_comp t : sim t (compile t).

(* Example of the sim relation *)
Definition example_sim : sim randomTerm compiledRandomTerm := sim_comp randomTerm.

(* Doing something 0 or more times *)
Inductive Rstar {T : Type} (P : T -> T -> Prop) : T -> T -> Prop :=
| RRefl : forall a, Rstar P a a
| RStep : forall a b c, P a b -> Rstar P b c -> Rstar P a c.
Hint Constructors Rstar.

Definition rstar_example : Rstar step randomTerm (N 6).
  apply: RStep.
  exact step_randomTerm.
  apply: RStep.
  exact (SPlus 1 5).
  apply: RRefl.
Qed.

(* Prints out RStep step_randomTerm (RStep (SPlus 1 5) (RRefl step (N (1 + 5)))), we could have manually typed this. *)
Print rstar_example.

(* This proof would be finished if I remembered more from that class *)
Lemma sim_step : forall t1 t1',
   step t1 t1' ->
   forall t2,
   sim t1 t2 ->
   exists t2', Rstar step t2 t2' /\ sim t1' t2'.
 Admitted.

repo: coq-lunch-learn


text:
From iris.proofmode Require Import tactics.
From iris.algebra Require Export sts.
From iris.base_logic.lib Require Export invariants.
From iris Require Import options.
Import uPred.

(** The CMRA we need. *)
Class stsG Σ (sts : stsT) := StsG {
  sts_inG :> inG Σ (stsR sts);
  sts_inhabited :> Inhabited (sts.state sts);
}.

Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (stsR sts) ].
Instance subG_stsΣ Σ sts :
  subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
Proof. solve_inG. Qed.

Section definitions.
  Context `{!stsG Σ sts} (γ : gname).

  Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iProp Σ :=
    own γ (sts_frag S T).
  Definition sts_own (s : sts.state sts) (T : sts.tokens sts) : iProp Σ :=
    own γ (sts_frag_up s T).
  Definition sts_inv (φ : sts.state sts → iProp Σ) : iProp Σ :=
    ∃ s, own γ (sts_auth s ∅) ∗ φ s.
  Definition sts_ctx `{!invG Σ} (N : namespace) (φ: sts.state sts → iProp Σ) : iProp Σ :=
    inv N (sts_inv φ).

  Global Instance sts_inv_ne n :
    Proper (pointwise_relation _ (dist n) ==> dist n) sts_inv.
  Proof. solve_proper. Qed.
  Global Instance sts_inv_proper :
    Proper (pointwise_relation _ (≡) ==> (≡)) sts_inv.
  Proof. solve_proper. Qed.
  Global Instance sts_ownS_proper : Proper ((≡) ==> (≡) ==> (⊣⊢)) sts_ownS.
  Proof. solve_proper. Qed.
  Global Instance sts_own_proper s : Proper ((≡) ==> (⊣⊢)) (sts_own s).
  Proof. solve_proper. Qed.
  Global Instance sts_ctx_ne `{!invG Σ} n N :
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx N).
  Proof. solve_proper. Qed.
  Global Instance sts_ctx_proper `{!invG Σ} N :
    Proper (pointwise_relation _ (≡) ==> (⊣⊢)) (sts_ctx N).
  Proof. solve_proper. Qed.
  Global Instance sts_ctx_persistent `{!invG Σ} N φ : Persistent (sts_ctx N φ).
  Proof. apply _. Qed.
  Global Instance sts_own_persistent s : Persistent (sts_own s ∅).
  Proof. apply _. Qed.
  Global Instance sts_ownS_persistent S : Persistent (sts_ownS S ∅).
  Proof. apply _. Qed.
End definitions.

Instance: Params (@sts_inv) 4 := {}.
Instance: Params (@sts_ownS) 4 := {}.
Instance: Params (@sts_own) 5 := {}.
Instance: Params (@sts_ctx) 6 := {}.

Section sts.
  Context `{!invG Σ, !stsG Σ sts}.
  Implicit Types φ : sts.state sts → iProp Σ.
  Implicit Types N : namespace.
  Implicit Types P Q R : iProp Σ.
  Implicit Types γ : gname.
  Implicit Types S : sts.states sts.
  Implicit Types T : sts.tokens sts.

  (* The same rule as implication does *not* hold, as could be shown using
     sts_frag_included. *)
  Lemma sts_ownS_weaken γ S1 S2 T1 T2 :
    T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 →
    sts_ownS γ S1 T1 ==∗ sts_ownS γ S2 T2.
  Proof. intros ???. by apply own_update, sts_update_frag. Qed.

  Lemma sts_own_weaken γ s S T1 T2 :
    T2 ⊆ T1 → s ∈ S → sts.closed S T2 →
    sts_own γ s T1 ==∗ sts_ownS γ S T2.
  Proof. intros ???. by apply own_update, sts_update_frag_up. Qed.

  Lemma sts_own_weaken_state γ s1 s2 T :
    sts.frame_steps T s2 s1 → sts.tok s2 ## T →
    sts_own γ s1 T ==∗ sts_own γ s2 T.
  Proof.
    intros ??. apply own_update, sts_update_frag_up; [|done..].
    intros Hdisj. apply sts.closed_up. done.
  Qed.

  Lemma sts_own_weaken_tok γ s T1 T2 :
    T2 ⊆ T1 → sts_own γ s T1 ==∗ sts_own γ s T2.
  Proof.
    intros ?. apply own_update, sts_update_frag_up; last done.
    - intros. apply sts.closed_up. set_solver.
    - apply sts.elem_of_up.
  Qed.

  Lemma sts_ownS_op γ S1 S2 T1 T2 :
    T1 ## T2 → sts.closed S1 T1 → sts.closed S2 T2 →
    sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ⊣⊢ (sts_ownS γ S1 T1 ∗ sts_ownS γ S2 T2).
  Proof. intros. by rewrite /sts_ownS -own_op sts_frag_op. Qed.

  Lemma sts_own_op γ s T1 T2 :
    T1 ## T2 → sts_own γ s (T1 ∪ T2) ==∗ sts_own γ s T1 ∗ sts_own γ s T2.
    (* The other direction does not hold -- see sts.up_op. *)
  Proof.
    intros. rewrite /sts_own -own_op. iIntros "Hown".
    iDestruct (own_valid with "Hown") as %Hval%sts_frag_up_valid.
    rewrite -sts_frag_op.
    - iApply (sts_own_weaken with "Hown"); first done.
      + split; apply sts.elem_of_up.
      + eapply sts.closed_op; apply sts.closed_up; set_solver.
    - done.
    - apply sts.closed_up; set_solver.
    - apply sts.closed_up; set_solver.
  Qed.

  Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.

  Lemma sts_alloc φ E N s :
    ▷ φ s ={E}=∗ ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s).
  Proof.
    iIntros "Hφ". rewrite /sts_ctx /sts_own.
    iMod (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as (γ) "Hγ".
    { apply sts_auth_valid; set_solver. }
    iExists γ; iRevert "Hγ"; rewrite -sts_auth_frag_up_op; iIntros "[Hγ $]".
    iMod (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
    rewrite /sts_inv. iNext. iExists s. by iFrame.
  Qed.

  Lemma sts_inv_accS φ E γ S T :
    ▷ sts_inv γ φ ∗ sts_ownS γ S T ={E}=∗ ∃ s,
      ⌜s ∈ S⌝ ∗ ▷ φ s ∗ ∀ s' T',
      ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E}=∗ ▷ sts_inv γ φ ∗ sts_own γ s' T'.
  Proof.
    iIntros "[Hinv Hγf]". rewrite /sts_ownS /sts_inv /sts_own.
    iDestruct "Hinv" as (s) "[>Hγ Hφ]".
    iDestruct (own_valid_2 with "Hγ Hγf") as %Hvalid.
    assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
    assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
    iModIntro; iExists s; iSplit; [done|]; iFrame "Hφ".
    iIntros (s' T') "[% Hφ]".
    iMod (own_update_2 with "Hγ Hγf") as "Hγ".
    { rewrite sts_auth_frag_op; [|done..]. by apply sts_update_auth. }
    iRevert "Hγ"; rewrite -sts_auth_frag_up_op; iIntros "[Hγ $]".
    iModIntro. iNext. iExists s'; by iFrame.
  Qed.

  Lemma sts_inv_acc φ E γ s0 T :
    ▷ sts_inv γ φ ∗ sts_own γ s0 T ={E}=∗ ∃ s,
      ⌜sts.frame_steps T s0 s⌝ ∗ ▷ φ s ∗ ∀ s' T',
      ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E}=∗ ▷ sts_inv γ φ ∗ sts_own γ s' T'.
  Proof. by apply sts_inv_accS. Qed.

  Lemma sts_accS φ E N γ S T :
    ↑N ⊆ E →
    sts_ctx γ N φ ∗ sts_ownS γ S T ={E,E∖↑N}=∗ ∃ s,
      ⌜s ∈ S⌝ ∗ ▷ φ s ∗ ∀ s' T',
      ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E∖↑N,E}=∗ sts_own γ s' T'.
  Proof.
    iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
    (* The following is essentially a very trivial composition of the accessors
       [sts_inv_acc] and [inv_acc] -- but since we don't have any good support
       for that currently, this gets more tedious than it should, with us having
       to unpack and repack various proofs.
       TODO: Make this mostly automatic, by supporting "opening accessors
       around accessors". *)
    iMod (sts_inv_accS with "[Hinv Hγf]") as (s) "(?&?& HclSts)"; first by iFrame.
    iModIntro. iExists s. iFrame. iIntros (s' T') "H".
    iMod ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
  Qed.

  Lemma sts_acc φ E N γ s0 T :
    ↑N ⊆ E →
    sts_ctx γ N φ ∗ sts_own γ s0 T ={E,E∖↑N}=∗ ∃ s,
      ⌜sts.frame_steps T s0 s⌝ ∗ ▷ φ s ∗ ∀ s' T',
      ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E∖↑N,E}=∗ sts_own γ s' T'.
  Proof. by apply sts_accS. Qed.
End sts.

Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.

author: SkySkimmer

repo: iris

save_path: github-repos/coq/SkySkimmer-iris