text:
Require Export Iron.Language.SystemF2Effect.Type.Exp.Base.
Require Export Iron.Language.SystemF2Effect.Type.Relation.WfT.

(********************************************************************)
(* Type Utils *)
(* Construct a type application from a constructor type
   and a list of argument types. *)
Fixpoint makeTApps (t1: ty) (tt: list ty) : ty :=
 match tt with
 | nil     => t1
 | t :: ts => makeTApps (TApp t1 t) ts
 end.

Fixpoint takeTCon (tt: ty) : ty :=
 match tt with
 | TApp t1 t2 => takeTCon t1
 | _          => tt
 end.

Fixpoint takeTArgs (tt: ty) : list ty :=
 match tt with
 | TApp t1 t2 => snoc t2 (takeTArgs t1)
 | _          => cons tt nil
 end.

(* Break apart a type application into the constructor type
   and a list of argument types. *)
Definition takeTApps (tt: ty) : (ty * list ty)
 := (takeTCon tt, takeTArgs tt).

(* Take the region identifier from an effect, if any. *)
Fixpoint handleOfEffect (e : ty) : option nat :=
 match e with
 | TCon1 tc (TRgn p)  => if isEffectTyCon_b tc then Some p else None
 | _                  => None
 end.

(********************************************************************)
Lemma makeTApps_snoc
 : forall t1 t2 t3 ts
 , makeTApps (TApp t1 t2) (snoc t3 ts)
 = TApp (makeTApps t1 (cons t2 ts)) t3.
Proof.
 intros. gen t1 t2.
 induction ts; burn.
Qed.

Lemma makeTApps_snoc'
 :  forall t1 t2 ts
 ,  makeTApps t1 (snoc t2 ts)
 =  TApp (makeTApps t1 ts) t2.
Proof.
 intros. gen t1 t2.
 induction ts; burn.
Qed.

Lemma takeTCon_makeTApps
 :  forall t1 ts
 ,  takeTCon (makeTApps t1 ts) = takeTCon t1.
Proof.
 intros. gen t1.
 induction ts; rip; burn.
 simpl. rewritess. burn.
Qed.
Hint Resolve takeTCon_makeTApps.

Lemma makeTApps_takeTCon
 :  forall t1 t2 ts
 ,  makeTApps t1 ts = t2
 -> takeTCon t1     = takeTCon t2.
Proof.
 intros. gen t1 t2.
 induction ts; intros.
 - simpl in H. subst. auto.
 - eapply IHts in H. simpl in H. auto.
Qed.
Hint Resolve makeTApps_takeTCon.

Lemma makeTApps_rewind
 :  forall t1 t2 ts
 ,  makeTApps (TApp t1 t2) ts
 =  makeTApps t1 (t2 :: ts).
Proof. burn. Qed.

(* A type application constructed from well formed components is
   itself well formed. *)
Lemma makeTApps_wfT
 :  forall n t1 ts
 ,  WfT n t1
 -> Forall (WfT n) ts
 -> WfT n (makeTApps t1 ts).
Proof.
 intros. gen t1.
 induction ts; intros.
 - simpl. auto.
 - simpl.
   inverts H0.
   have HS: (ts = nil \/ (exists t ts', ts = t <: ts'))
    by (apply snocable).
   inverts HS.
   + simpl. auto.
   + dest H0. dest H0. subst.
     eapply IHts; auto.
Qed.

Lemma handleOfEffect_form_some
 :  forall e p
 ,  handleOfEffect e = Some p
 -> exists tc
     ,  e    = TCon1 tc (TRgn p)
     /\ true = isEffectTyCon_b tc.
Proof.
 intros.
 destruct e; snorm.
 - destruct e; snorm.
   destruct t0; snorm.
   exists t. rip.
 - destruct e; snorm.
   destruct t0; snorm.
Qed.
Hint Resolve handleOfEffect_form_some.

author: discus-lang

repo: iron

save_path: github-repos/coq/discus-lang-iron


text:
Require Import ImpPrelude.
Require Import PCM.
Require Import ModSem.
Require Import Imp.
Require Import ImpNotations.

Set Implicit Arguments.

Section STACK.

  Context `{Σ: GRA.t}.

  Import ImpNotations.
  Local Open Scope expr_scope.
  Local Open Scope stmt_scope.

  Definition new :=
    mk_function
      []
      ["new_node"]
      (
        "new_node" =# malloc# 1%Z ;#
        "new_node" *=# 0%Z ;#
        return# "new_node"
      ).

  Definition pop :=
    mk_function
      ["stk"]
      ["hd"; "b"; "v"; "next"]
      (
        "hd" =#* "stk" ;#
        "b" =# ("hd" == 0%Z) ;#
        if# "b"
        then# return# (-1)%Z
        else# ("v" =#* "hd" ;#
               "next" =#* ("hd" + 8%Z) ;#
               free# "hd" ;#
               free# ("hd" + 8%Z) ;#
               "stk" *=# "next" ;#
               return# "v")
        fi#
      ).

  Definition push :=
    mk_function
      ["stk"; "v"]
      ["new_node"; "addr_next"; "hd"]
      (
        "new_node" =# malloc# 2%Z ;#
        "addr_next" =# "new_node" + 8%Z ;#
        "hd" =#* "stk" ;#
        "new_node" *=# "v" ;#
        "addr_next" *=# "hd" ;#
        "stk" *=# "new_node"
      ).

  Definition Stack_prog : program :=
    mk_program
      "Stack"
      []
      []
      []
      [("new", new); ("pop", pop); ("push", push)]
  .

  Definition StackSem ge : ModSem.t := ImpMod.modsem Stack_prog ge.
  Definition Stack : Mod.t := ImpMod.get_mod Stack_prog.

End STACK.

author: alxest

repo: CCR

save_path: github-repos/coq/alxest-CCR


text:
(* This file contains Example 7.38 of the Iris Lecture Notes. We implement a
   concurrent course grained bag based on the lock in `lock.v`.
*)

From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import auth.
Import uPred.

From iris_examples.lecture_notes Require Import lock.

Definition newbag : val :=
  λ: <>, let: "ℓ" := ref NONE in
         let: "v" := newlock #() in ("ℓ", "v").

Definition insert : val :=
  λ: "x" "e", let: "ℓ" := Fst "x" in
                  let: "lock" := Snd "x" in
                  acquire "lock" ;;
                  "ℓ" <- SOME ("e", !"ℓ") ;;
                  release "lock".

Definition remove : val :=
  λ: "x", let: "ℓ" := Fst "x" in
          let: "lock" := Snd "x" in
          acquire "lock" ;;
          let: "r" := !"ℓ" in
          let: "res" := match: "r" with
                          NONE => NONE
                        | SOME "p" => "ℓ" <- Snd "p" ;; SOME (Fst "p")
                        end
          in release "lock" ;; "res".

Section spec.
  Context `{!heapGS Σ, lockG Σ}.
  Local Notation iProp := (iProp Σ).

  Fixpoint isBag (Ψ : val → iProp) (v : val) : iProp :=
    match v with
    | NONEV => ⌜True⌝%I
    | SOMEV (x, r) => (Ψ x ∗ isBag Ψ r)%I
    | _ => ⌜False⌝%I
    end.

  Definition is_bag (v : val) (Ψ : val → iProp) :=
    (∃ (ℓ : loc) (v₂ : val) γ, ⌜v = (#ℓ, v₂)%V⌝ ∗ is_lock γ v₂ (∃ u, ℓ ↦ u ∗ isBag Ψ u))%I.

  Global Instance bag_persistent v Ψ: Persistent (is_bag v Ψ).
  Proof. apply _. Qed.

  Lemma newbag_triple_spec Ψ:
    {{{ True }}} newbag #() {{{ b, RET b; is_bag b Ψ}}}.
  Proof.
    iIntros (ϕ) "_ Hcont".
    wp_lam ; wp_alloc ℓ as "Hℓ"; wp_let.
    wp_apply ((newlock_spec (∃ u, ℓ ↦ u ∗ isBag Ψ u))%I with "[Hℓ]").
    { iExists NONEV. auto. }
    iIntros (v). iDestruct 1 as (γ) "IL".
    wp_pures. iApply "Hcont".
    iExists ℓ, v, γ. iFrame. done.
  Qed.

  Lemma bag_insert_triple_spec v Ψ e:
    {{{ is_bag v Ψ ∗ Ψ e }}} insert v e {{{ RET #(); True }}}.
  Proof.
    iIntros (ϕ) "[Hb Hψ] Hcont".
    iDestruct "Hb" as (ℓ u γ) "[% #IL]"; subst.
    wp_lam. wp_pures.
    wp_apply (acquire_spec with "IL"); first done.
    iIntros (v) "[P HLocked]".
    iDestruct "P" as (b) "[Hp Hb]".
    wp_load. wp_store.
    iApply (release_spec with "[$IL $HLocked Hp Hψ Hb]"); first done.
    { iExists _. iFrame "Hp". iFrame. }
    done.
  Qed.

  Lemma bag_remove_triple_spec v Ψ:
    {{{ is_bag v Ψ }}} remove v {{{ u, RET u; ⌜u = NONEV⌝ ∨ ∃ x, ⌜u = SOMEV x⌝ ∗ Ψ x }}}.
  Proof.
    iIntros (ϕ) "Hb Hcont".
    iDestruct "Hb" as (ℓ u γ) "[% #IL]"; subst.
    wp_lam. wp_pures.
    wp_apply (acquire_spec with "IL"); first done.
    iIntros (v) "[P HLocked]". iDestruct "P" as (b) "[Hp Hb]".
    wp_load.
    destruct b as [| | |b|b]; try (iDestruct "Hb" as "%"; contradiction).
    - wp_smart_apply (release_spec with "[$IL $HLocked Hp Hb]"); first done.
      { iExists _. iFrame. }
      iIntros. wp_pures. iApply "Hcont". iLeft. done.
    - destruct b; try (iDestruct "Hb" as "%"; contradiction).
      simpl. iDestruct "Hb" as "[Hψ Hb]".
      wp_store.
      wp_smart_apply (release_spec with "[$IL $HLocked Hp Hb]"); first done.
      { iExists _. iFrame. }
      iIntros (_).
      wp_pures.
      iApply "Hcont".
      iRight. iExists _. by iFrame.
  Qed.

End spec.

author: pavel-ivanov-rnd


text:
Require Import CSet Util Filter Take MoreList OUnion AllInRel.
Require Import IL Annotation LabelsDefined Sawtooth.
Require Import PartialOrder Liveness.Liveness TrueLiveness.
Require SimF SimI.

Set Implicit Arguments.
Unset Printing Records.

(** * Dead Variable Elimination *)

Fixpoint flt (lv:set var) X (Z:params) (L:list X) :=
  match Z, L with
  | x::Z, a::L => if [ x ∈ lv ] then a::flt (lv \ singleton x) Z L
                 else flt (lv \ singleton x) Z L
  | _, _  => nil
  end.

Lemma flt_length X Y Z lv (L:list X) (L':list Y)
  (LEN:length L = length L')
  : ❬flt lv Z L❭ = ❬flt lv Z L'❭.
Proof.
  general induction LEN; destruct Z; simpl; eauto.
  cases; simpl; rewrite IHLEN; eauto.
Qed.

Local Hint Resolve flt_length.
Hint Resolve flt_length : len.

Lemma get_flt X lv Z (Y:list X) n y
      (Get:get (flt lv Z Y) n y)
  : exists z k, get Z k z /\ get Y k y /\ z ∈ lv.
Proof.
  general induction Z; destruct Y; simpl in *; isabsurd.
  - cases in Get; eauto 20 using get.
    + inv Get; eauto using get.
      edestruct IHZ; dcr; eauto.
      exists x0, (S x1). repeat split; eauto using get. cset_tac.
    + edestruct IHZ; dcr; eauto.
      exists x0, (S x1). repeat split; eauto using get. cset_tac.
Qed.

Lemma omap_flt A B Z (Y:list A) lv f (l:list B)
: omap f Y = Some l
  -> length Y = length Z
  -> omap f (flt lv Z Y) = Some (flt lv Z l).
Proof.
  intros.
  general induction H0; simpl in * |- *; eauto.
  monad_inv H. cases; simpl; eauto.
  rewrite EQ. erewrite IHlength_eq; simpl; eauto.
Qed.

Lemma flt_InA (A : Type) (eqA : A -> A -> Prop) lv Z Y x
  : InA eqA x (flt lv Z Y) -> InA eqA x Y.
Proof.
  intros.
  general induction Z; destruct Y; isabsurd; simpl in *.
  cases in H.
  - inv H; eauto using InA.
  - edestruct IHZ; eauto.
Qed.

Lemma nodup_flt X lv (R:X->X->Prop) Z (Y:list X)
  : NoDupA R Y
    -> NoDupA R (flt lv Z Y).
Proof.
  general induction Z; destruct Y; simpl in *; dcr; eauto.
  - cases; eauto using NoDupA.
    constructor; eauto.
    intro XX. eapply flt_InA in XX.
    inv H. eauto.
Qed.

Lemma of_list_flt lv Z
  : of_list (flt lv Z Z) [=] lv ∩ of_list Z.
Proof.
  general induction Z; simpl.
  - cset_tac.
  - cases; simpl.
    + rewrite IHZ; eauto. cset_tac.
    + rewrite IHZ; eauto. cset_tac.
Qed.

Lemma nodup_flt' lv Z
  : NoDupA _eq (flt lv Z Z).
Proof.
  general induction Z; dcr; eauto.
  - eauto using NoDupA.
  - simpl flt. cases; eauto using NoDupA.
    constructor; eauto.
    rewrite <- of_list_1.
    rewrite of_list_flt.
    cset_tac.
Qed.

Lemma argsLive_liveSound lv blv Y Z
  : argsLive lv blv Y Z
    -> forall (n : nat) (y : op) blv',
      get (flt blv' Z Y) n y ->
      blv' ⊆ blv ->
      live_op_sound y lv.
Proof.
  intros. general induction H; simpl in * |- *.
  - isabsurd.
  - cases in H1; eauto with cset.
    + inv H1; eauto with cset.
Qed.

Lemma agree_on_update_flt Y `{Equivalence (option Y)} (lv:set var) (V V':env (option Y)) (Z:params) VL

: length Z = length VL
  -> agree_on R (lv \ of_list Z) V V'
  -> agree_on R lv
             (V [Z <-- List.map Some VL])
             (V' [(flt lv Z Z) <-- (List.map Some (flt lv Z VL))]).
Proof.
  intros.
  eapply agree_on_trans. eapply H.
  eapply update_with_list_agree; eauto with len.
  general induction Z; destruct VL; simpl; eauto.
  - exfalso; isabsurd.
  - cases; simpl in *.
    + eapply agree_on_update_same. reflexivity.
      eapply IHZ; eauto.
      eapply agree_on_incl; eauto. clear; cset_tac.
    + eapply agree_on_update_dead; eauto.
      assert (lv [=] lv \ singleton a) by cset_tac.
      rewrite H2 at 1. eapply IHZ; eauto.
      eapply agree_on_incl; eauto. clear; cset_tac.
Qed.

Fixpoint compile (LV:list ((set var) * params)) (s:stmt) (a:ann (set var)) :=
  match s, a with
    | stmtLet x e s, ann1 _ an =>
      if [x ∈ getAnn an \/ isCall e]
      then stmtLet x e (compile LV s an)
      else compile LV s an
    | stmtIf e s t, ann2 _ ans ant =>
        stmtIf e (compile LV s ans) (compile LV t ant)
    | stmtApp f Y, ann0 _ =>
      let lvZ := nth (counted f) LV (∅, nil) in
      stmtApp f (flt (fst lvZ) (snd lvZ) Y)
    | stmtReturn x, ann0 _ => stmtReturn x
    | stmtFun F t, annF lv ans ant =>
      let LV' := pair ⊜ (getAnn ⊝ ans) (fst ⊝ F) ++ LV in
      stmtFun (zip (fun Zs a => (flt (getAnn a) (fst Zs) (fst Zs), compile LV' (snd Zs) a)) F ans)
              (compile LV' t ant)
    | s, _ => s
  end.

(** ** Correctness with respect to the imperative semantics IL/I *)

Module I.

  Import SimI.

Instance SR : PointwiseProofRelationI ((set var) * params) := {
   ParamRelIP G Z Z' := Z' = flt (fst G) (snd G) Z /\ snd G = Z;
   ArgRelIP V V' G VL VL' :=
     VL' = (flt (fst G) (snd G) VL) /\
     length (snd G) = length VL /\
     agree_on eq (fst G \ of_list (snd G)) V V';
}.

Lemma sim_I ZL LV r L L' V V' s  lv
: agree_on eq (getAnn lv) V V'
-> true_live_sound Imperative ZL LV s lv
-> labenv_sim SimExt (sim r) SR (zip pair LV ZL) L L'
-> sim r SimExt (L,V, s) (L',V', compile (zip pair LV ZL) s lv).
Proof.
  unfold sim. revert_except s.
  sind s; destruct s; simpl; intros; invt true_live_sound; simpl in * |- *.
  - destruct e.
    + cases. exploit H9; eauto. inv H2.
      * eapply (sim_let_op il_statetype_I);
          eauto 20 using op_eval_live, agree_on_update_same, agree_on_incl.
      * case_eq (op_eval V e); intros.
        -- pone_step_left.
           eapply (IH s); eauto. eapply agree_on_update_dead; eauto.
           eapply agree_on_incl; eauto.
           rewrite <- H10. cset_tac; intuition.
        -- pno_step_left.
    + cases. exploit H9; eauto. inv H2.
      * eapply (sim_let_call il_statetype_I); eauto 10 using agree_on_update_same, agree_on_incl.
        erewrite <- omap_op_eval_live_agree; eauto. eapply agree_on_sym; eauto.
  - eapply (sim_cond il_statetype_I); intros; eauto 20 using op_eval_live, agree_on_incl.
  - eapply labenv_sim_app; eauto using zip_get.
    + intros; simpl in *; dcr; subst.
      split; [|split]; intros.
      * erewrite get_nth; eauto using zip_get; simpl.
        exploit (@omap_flt _ _ Z0 _ blv _ _ H7);
          eauto.
        exploit omap_op_eval_live_agree; eauto.
        intros; eapply argsLive_liveSound; eauto.
        rewrite H12. eexists; split; eauto.
        repeat split; eauto using filter_filter_by_length.
        eapply agree_on_incl; eauto.
  - pno_step.
    simpl. erewrite <- op_eval_live_agree; eauto. eapply agree_on_sym; eauto.
  - eapply sim_fun_ptw; eauto.
    + intros. left. rewrite <- zip_app;[| eauto with len]. eapply IH; eauto using agree_on_incl.
    + intros. hnf; intros; simpl in *; dcr; subst.
      inv_get.
      rewrite <- zip_app;[| eauto with len].
      eapply IH; eauto. simpl.
      eapply agree_on_update_flt; eauto.
    + hnf; intros; simpl in *; subst.
      inv_get; simpl; eauto.
    + eauto with len.
    + eauto with len.
Qed.

Lemma sim_DVE V V' s lv
: agree_on eq (getAnn lv) V V'
-> true_live_sound Imperative nil nil s lv
-> @sim I.state _ I.state _ bot3 SimExt (nil,V, s) (nil,V', compile nil s lv).
Proof.
  intros.
  eapply (@sim_I nil nil); eauto.
  eapply labenv_sim_nil.
Qed.

End I.

(** ** Correctness with respect to the functional semantics IL *)
(** Functional here means that variables are lexically scoped binders instead of assignables. *)

Module F.

  Import SimF.

Instance SR : PointwiseProofRelationF ((set var) * params) := {
   ParamRelFP G Z Z' := Z' = (flt (fst G) (snd G) Z) /\ snd G = Z;
   ArgRelFP E E' G VL VL' :=
     VL' = (flt (fst G) (snd G) VL) /\
     length (snd G) = length VL
}.

Lemma sim_F ZL LV r L L' V V' s  lv
: agree_on eq (getAnn lv) V V'
-> true_live_sound Functional ZL LV s lv
-> labenv_sim SimExt (sim r) SR (zip pair LV ZL) L L'
-> sim r SimExt (L,V, s) (L',V', compile (zip pair LV ZL) s lv).
Proof.
  unfold sim. revert_except s.
  sind s; destruct s; simpl; intros; invt true_live_sound; simpl in * |- *.
  - destruct e.
    + cases. exploit H9; eauto. inv H2.
      * eapply (sim_let_op il_statetype_F);
          eauto 20 using op_eval_live, agree_on_update_same, agree_on_incl.
      * case_eq (op_eval V e); intros.
        -- pone_step_left.
           eapply (IH s); eauto. eapply agree_on_update_dead; eauto.
           eapply agree_on_incl; eauto.
           rewrite <- H10. cset_tac; intuition.
        -- pno_step_left.
    + cases. exploit H9; eauto. inv H2.
      * eapply (sim_let_call il_statetype_F); eauto 10 using agree_on_update_same, agree_on_incl.
        erewrite <- omap_op_eval_live_agree; eauto. eapply agree_on_sym; eauto.
  - eapply (sim_cond il_statetype_F); intros; eauto 20 using op_eval_live, agree_on_incl.
  - eapply labenv_sim_app; eauto using zip_get.
    + intros; simpl in *; dcr; subst.
      split; [|split]; intros.
      * erewrite get_nth; eauto using zip_get; simpl.
        exploit (@omap_flt _ _ Z0 _ blv _ _ H7);
          eauto.
        exploit omap_op_eval_live_agree; eauto.
        intros; eapply argsLive_liveSound; eauto.
        rewrite H12. eexists; split; eauto.
  - pno_step.
    simpl. erewrite <- op_eval_live_agree; eauto. eapply agree_on_sym; eauto.
  - eapply sim_fun_ptw; eauto.
    + intros. left. rewrite <- zip_app;[| eauto with len].
      eapply IH; eauto using agree_on_incl.
    + intros. hnf; intros; simpl in *; dcr; subst.
      inv_get.
      rewrite <- zip_app; [| eauto with len].
      eapply IH; eauto. simpl in *.
      exploit H9; eauto.
      eapply agree_on_update_flt; eauto using agree_on_incl.
    + hnf; intros; simpl in *; subst.
      inv_get; simpl; eauto.
    + eauto with len.
    + eauto with len.
Qed.

Lemma sim_DVE V V' s lv
: agree_on eq (getAnn lv) V V'
-> true_live_sound Functional nil nil s lv
-> @sim F.state _ F.state _ bot3 SimExt (nil,V, s) (nil,V', compile nil s lv).
Proof.
  intros.
  eapply (@sim_F nil nil); eauto. eapply labenv_sim_nil.
Qed.

End F.

(** ** Reconstruction of Liveness Information after DVE *)
(** In this section we show that liveness information can
    be transformed alongside DVE.
    This means that liveness recomputation after the transformation is not neccessary. *)

Fixpoint compile_live (s:stmt) (a:ann (set var)) (G:set var) : ann (set var) :=
  match s, a with
    | stmtLet x (Operation e) s, ann1 lv an as a =>
      if [x ∈ getAnn an] then ann1 (G ∪ lv) (compile_live s an ∅)
      else compile_live s an (G ∪ lv)
    | stmtLet x (Call f Y) s, ann1 lv an as a =>
      ann1 (G ∪ lv) (compile_live s an {x})
    | stmtIf e s t, ann2 lv ans ant =>
      ann2 (G ∪ lv) (compile_live s ans ∅) (compile_live t ant ∅)
    | stmtApp f Y, ann0 lv => ann0 (G ∪ lv)
    | stmtReturn x, ann0 lv => ann0 (G ∪ lv)
    | stmtFun F t, annF lv ans ant =>
      let ans' := zip (fun Zs a => compile_live (snd Zs) a ∅) F ans
      in annF (G ∪ lv) ans' (compile_live t ant ∅)
    | _, a => a
  end.

Lemma compile_live_incl G i ZL LV s lv
  : true_live_sound i ZL LV s lv
    -> getAnn (compile_live s lv G) ⊆ G ∪ getAnn lv.
Proof.
  intros. general induction H; simpl; eauto.
  - repeat cases; simpl; try reflexivity.
    rewrite IHtrue_live_sound.
    cset_tac.
Qed.

Lemma compile_live_incl_empty i ZL LV s lv
  : true_live_sound i ZL LV s lv
    -> getAnn (compile_live s lv ∅) ⊆ getAnn lv.
Proof.
  intros.
  eapply compile_live_incl in H.
  rewrite H. cset_tac; intuition.
Qed.

Lemma incl_compile_live G i ZL LV s lv
  : true_live_sound i ZL LV s lv
    -> G ⊆ getAnn (compile_live s lv G).
Proof.
  intros. general induction H; simpl; eauto.
  - repeat cases; simpl; eauto with cset.
    rewrite <- IHtrue_live_sound.
    cset_tac.
Qed.

Lemma incl_compile_live' G i ZL LV s lv
  : true_live_sound i ZL LV s lv
    -> getAnn lv  ⊆ getAnn (compile_live s lv G).
Proof.
  intros. general induction H; simpl; eauto.
  - repeat cases; simpl; eauto with cset.
    rewrite <- incl_compile_live; eauto.
Qed.

Lemma incl_compile_live_eq G i ZL LV s lv
  : true_live_sound i ZL LV s lv
    -> G ∪ getAnn lv [=] getAnn (compile_live s lv G).
Proof.
  intros. general induction H; simpl; eauto.
  - repeat cases; simpl; eauto with cset.
    rewrite <- IHtrue_live_sound.
    cset_tac.
Qed.

Lemma dve_live i ZL LV s lv G
  : true_live_sound i ZL LV s lv
    -> live_sound i ((fun Z lv => flt lv Z Z) ⊜ ZL LV) LV (compile (zip pair LV ZL) s lv) (compile_live s lv G).
Proof.
  intros. general induction H; simpl; eauto using live_sound, compile_live_incl.
  - destruct e; simpl.
    + repeat cases; eauto; [| exfalso; cset_tac|exfalso; cset_tac].
      econstructor; eauto.
      * eapply live_exp_sound_incl; eauto.
      * rewrite compile_live_incl; eauto.
        rewrite <- H1. cset_tac; intuition.
      * rewrite <- incl_compile_live_eq; eauto.
    + repeat cases; eauto.
      econstructor; eauto.
      * eapply live_exp_sound_incl; eauto.
      * rewrite compile_live_incl; eauto.
        rewrite <- H1. cset_tac; intuition.
      * rewrite <- incl_compile_live_eq; eauto.
        eauto with cset.
  - repeat cases; eauto.
    + econstructor; eauto.
      eapply live_op_sound_incl; eauto.
      rewrite compile_live_incl_empty; eauto with cset.
      rewrite compile_live_incl_empty; eauto with cset.
  - econstructor; eauto using zip_get.
    + simpl. cases; eauto.
      rewrite <- H1. rewrite minus_inter_empty. eapply incl_right.
      rewrite of_list_flt. cset_tac.
    + erewrite get_nth; eauto using zip_get.
      simpl. eauto with len.
    + intros ? ? Get. erewrite get_nth in Get; eauto using zip_get. simpl in *.
      edestruct get_flt; eauto; dcr.
      eapply live_op_sound_incl.
      eapply argsLive_live_exp_sound; eauto. eauto with cset.
  - econstructor; eauto.
    eapply live_op_sound_incl; eauto using incl_right.
  - econstructor; simpl in *; eauto with len.
    + eapply live_sound_monotone.
      rewrite map_zip. simpl.
      do 2 rewrite zip_app in IHtrue_live_sound; eauto with len.
      rewrite zip_map_l, zip_map_r in IHtrue_live_sound.
      eapply IHtrue_live_sound.
      eapply PIR2_app; eauto.
      eapply PIR2_get; eauto 30 with len.
      intros; inv_get. simpl.
      rewrite compile_live_incl_empty; eauto.
    + intros; inv_get. simpl.
      eapply live_sound_monotone.
      rewrite map_zip. simpl.
      do 2 rewrite zip_app in H2; eauto with len.
      rewrite zip_map_l, zip_map_r in H2.
      eapply H2; eauto.
      eapply PIR2_app; eauto.
      eapply PIR2_get; eauto 30 with len.
      intros; inv_get. simpl.
      rewrite compile_live_incl_empty; eauto.
    + intros; inv_get.
      repeat rewrite getAnn_setTopAnn; simpl.
      split; eauto.
      * rewrite of_list_flt.
        rewrite <- incl_compile_live'; eauto.
        clear. cset_tac.
      * exploit H3; eauto.
        split; eauto.
        -- eapply nodup_flt'.
        -- cases; eauto.
           rewrite compile_live_incl_empty; eauto.
           rewrite of_list_flt.
           rewrite <- H5.
           clear_all; cset_tac.
    + rewrite compile_live_incl; eauto with cset.
Qed.

Require Import ReconstrLive.

(** ** DVE and Unreachable Code *)
(** We show that DVE does not introduce unreachable code. *)

Lemma DVE_callChain b Lv ZL F als n l'
  : ❬F❭ = ❬als❭
    -> (forall (n : nat) (Zs : params * stmt) (a : ann ⦃var⦄),
         get F n Zs ->
         get als n a ->
         forall n0 : nat,
           isCalled b (snd Zs) (LabI n0) ->
           isCalled b (compile (pair ⊜ (getAnn ⊝ als ++ Lv) (fst ⊝ F ++ ZL)) (snd Zs) a) (LabI n0))
     -> callChain (isCalled b) F (LabI l') (LabI n)
     -> callChain (isCalled b)
                 ((fun (Zs : params * stmt) (a : ann ⦃var⦄) =>
                     (flt (getAnn a) (fst Zs) (fst Zs),
                      compile (pair ⊜ (getAnn ⊝ als ++ Lv) (fst ⊝ F ++ ZL)) (snd Zs) a)) ⊜ F als)
                 (LabI l') (LabI n).
Proof.
  intros LEN IH CC.
  general induction CC.
  + econstructor.
  + inv_get. econstructor 2.
    eapply zip_get; eauto.
    eapply IH; eauto.
    eauto.
Qed.

Lemma DVE_isCalled i ZL LV s lv n
  : true_live_sound i ZL LV s lv
    -> isCalled true s (LabI n)
    -> isCalled true (compile (zip pair LV ZL) s lv) (LabI n).
Proof.
  intros LS IC.
  general induction LS; invt isCalled; simpl; repeat cases; eauto using isCalled;
    try congruence.
  - destruct l' as [l'].
    econstructor; rewrite <- zip_app; eauto with len.
    rewrite zip_length2; eauto. eapply DVE_callChain; eauto.
Qed.

Lemma DVE_noUnreachableCode i ZL LV s lv
  : true_live_sound i ZL LV s lv
    -> noUnreachableCode (isCalled true) s
    -> noUnreachableCode (isCalled true) (compile (zip pair LV ZL) s lv).
Proof.
  intros LS UC.
  general induction LS; inv UC; simpl; repeat cases; eauto using noUnreachableCode.
  - econstructor; intros; inv_get; rewrite <- zip_app; simpl; eauto with len.
    + edestruct H8 as [[l] [IC CC]]. rewrite zip_length2 in H4; eauto.
      eexists (LabI l); split; eauto.
      eapply DVE_isCalled; eauto.
      eapply DVE_callChain; eauto using DVE_isCalled.
Qed.

Require Import AppExpFree.

Lemma DVE_app_expfree LVZL s lv
: app_expfree s
  -> app_expfree (compile LVZL s lv).
Proof.
  intros AEF.
  general induction AEF; destruct lv; simpl;
    repeat let_pair_case_eq; repeat simpl_pair_eqs; subst; simpl;
      repeat cases; eauto using app_expfree.
  - econstructor. intros; inv_get; eauto.
    edestruct get_flt; eauto; dcr. eauto.
  - econstructor; intros; inv_get; eauto.
    eapply H0; eauto.
Qed.

Require Import RenamedApart PE.

Fixpoint compile_renamedApart (s:stmt) (lv:ann (set var)) (a:ann (set var * set var)) (D:set var)
  : ann (set var * set var) :=
  match s, lv, a with
  | stmtLet x e s, ann1 lv alv, ann1 (_, _) an as a =>

    if [x ∈ getAnn alv \/ isCall e] then
      let an' := compile_renamedApart s alv an {x;D} in
      ann1 (D, {x;snd (getAnn an')}) an'
    else compile_renamedApart s alv an D
  | stmtIf e s t, ann2 lv ans ant, ann2 (_,_) bns bnt =>
    let bns' := compile_renamedApart s ans bns D in
    let bnt' := compile_renamedApart t ant bnt D in
    ann2 (D, snd (getAnn bns') ∪ snd (getAnn bnt')) bns' bnt'
    | stmtApp f Y, ann0 lv, ann0 _ => ann0 (D, ∅)
    | stmtReturn x, ann0 lv, ann0 _ => ann0 (D, ∅)
    | stmtFun F t, annF lv anF ant, annF (_, _) bnF bnt =>
      let abnF := (pair ⊜ anF bnF) in
      let bnF' := zip (fun (Zs:params * stmt) ab =>
                        compile_renamedApart (snd Zs) (fst ab) (snd ab)
                                             (of_list (flt (getAnn (fst ab)) (fst Zs) (fst Zs)) ∪ D)) F abnF in
      let abnF' := (pair ⊜ anF bnF') in
      let bnt' := compile_renamedApart t ant bnt D in
      annF (D, list_union ((fun Zs ab => of_list (flt (getAnn (fst ab)) (fst Zs) (fst Zs)) ∪ snd (getAnn (snd ab))) ⊜ F abnF')
                          ∪ snd (getAnn bnt'))
           bnF' bnt'
    | _, _, a => a
  end.

Lemma fst_getAnn_renamedApart i LV ZL s lv G D
  : renamedApart s G
    -> true_live_sound i ZL LV s lv
    -> fst (getAnn (compile_renamedApart s lv G D)) = D.
Proof.
  intros RA TLS.
  general induction TLS; invt renamedApart; simpl; repeat cases; simpl; eauto.
Qed.

Lemma fst_getAnn_renamedApart' i LV ZL s lv G D
  : renamedApart s G
    -> true_live_sound i ZL LV s lv
    -> fst (getAnn (compile_renamedApart s lv G D)) [=] D.
Proof.
  intros RA TLS.
  general induction TLS; invt renamedApart; simpl; repeat cases; simpl; eauto.
Qed.

Hint Resolve fst_getAnn_renamedApart fst_getAnn_renamedApart'.

Lemma snd_getAnn_renamedApart i LV ZL s lv G D
  : renamedApart s G
    -> true_live_sound i ZL LV s lv
    -> snd (getAnn (compile_renamedApart s lv G D)) ⊆ snd (getAnn G).
Proof.
  intros RA TLS.
  general induction TLS; invt renamedApart; simpl; repeat cases; simpl; srewrite D'; eauto.
  - rewrite IHTLS; eauto. rewrite H9; eauto.
  - rewrite IHTLS; eauto. rewrite H9; eauto with cset.
  - rewrite IHTLS1, IHTLS2; eauto. pe_rewrite; eauto.
  - rewrite IHTLS, H11; eauto.
    eapply incl_union_lr; eauto.
    eapply list_union_incl; intros; inv_get; simpl.
    eapply incl_list_union; eauto using zip_get.
    rewrite H1; eauto.
    unfold defVars; rewrite of_list_flt; simpl.
    clear. cset_tac. clear; cset_tac.
Qed.

Lemma nodup_filter X R p `{Proper _ (R ==> eq) p} (L:list X)
  : NoDupA R L
    -> NoDupA R (filter p L).
Proof.
  intros ND.
  general induction ND; simpl in *; dcr; eauto.
  - cases; eauto using NoDupA.
    constructor; eauto.
    rewrite filter_InA; intuition.
Qed.

Lemma DVE_renamedApart i LV ZL s lv G D
  : renamedApart s G
    -> true_live_sound i ZL LV s lv
    -> D ⊆ fst (getAnn G)
    -> freeVars (compile (zip pair LV ZL)  s lv) ⊆ D
    -> renamedApart (compile (zip pair LV ZL)  s lv) (compile_renamedApart s lv G D).
Proof.
  intros RA TLS Dincl inclD.
  general induction TLS; invt renamedApart; simpl in * |- *; eauto using renamedApart.
  - cases; simpl in *.
    + econstructor; try reflexivity; eauto with cset.
      * rewrite <- inclD; eauto with cset.
      * eapply IHTLS; eauto.
        -- rewrite H9, Dincl; simpl; eauto with cset.
        -- rewrite <- inclD. clear; cset_tac.
      * eapply pe_eta_split; econstructor; simpl; eauto.
    + eapply IHTLS; eauto.
      * rewrite H9; simpl; cset_tac.
  - econstructor; try reflexivity; eauto.
    + rewrite <- inclD. eauto with cset.
    + rewrite !snd_getAnn_renamedApart, H11, H12; eauto.
    + exploit IHTLS1; eauto.
      pe_rewrite; eauto with cset.
      rewrite <- inclD; eauto with cset.
    + exploit IHTLS2; eauto.
      pe_rewrite; eauto with cset.
      rewrite <- inclD; eauto with cset.
    + eapply pe_eta_split; econstructor; simpl; eauto.
    + eapply pe_eta_split; econstructor; simpl; eauto.
  - econstructor; eauto with len; (try eapply eq_union_lr); eauto.
    * intros; inv_get. simpl in *.
      rewrite <- zip_app;[| eauto with len].
      eapply H1; eauto.
      -- edestruct H8; eauto; dcr. rewrite H4. rewrite Dincl;  eauto.
         rewrite of_list_flt. clear; cset_tac.
      -- rewrite of_list_flt.
         rewrite <- inclD.
         rewrite <- incl_list_union; eauto using zip_get; [| reflexivity].
         simpl. rewrite of_list_flt.
         rewrite <- union_assoc. eapply incl_union_left.
         rewrite zip_app; eauto with len.
         clear; cset_tac.
    * hnf; intros; inv_get.
      edestruct H8; eauto; dcr.
      simpl. econstructor; simpl in *.
      erewrite fst_getAnn_renamedApart; eauto with cset.
      split. eapply nodup_flt; eauto.
      split. eapply disj_2_incl; eauto. rewrite of_list_flt.
      eapply disj_1_incl; eauto. cset_tac.
      erewrite fst_getAnn_renamedApart, !snd_getAnn_renamedApart; only 2-7: eauto.
      pe_rewrite. rewrite of_list_flt. eapply disj_1_incl; eauto.
      clear; cset_tac.
    * hnf; intros. inv_get.
      unfold defVars; simpl.
      exploit H9; try eapply H4; only 1-2: eauto using zip_get.
      unfold defVars in*.
      rewrite !snd_getAnn_renamedApart; only 2-5: eauto.
      rewrite !of_list_flt.
      eapply disj_incl; eauto.
      clear; cset_tac.
      clear; cset_tac.
    * rewrite <- zip_app; eauto with len; simpl in *.
      eapply IHTLS; eauto.
      pe_rewrite. eauto. rewrite <- inclD; eauto.
    * eapply pe_eta_split; econstructor; eauto.
      erewrite fst_getAnn_renamedApart; eauto.
    * eapply list_union_eq; intros; eauto 20 with len.
      inv_get. unfold defVars; simpl.
      simpl. reflexivity.
Qed.

Lemma DVE_freeVars_live ZL LV s lv
      (LS:true_live_sound Functional ZL LV s lv)
  : freeVars (compile (zip pair LV ZL) s lv) ⊆ getAnn lv.
Proof.
  general induction LS; simpl; repeat cases; simpl;
    eauto using Ops.freeVars_live; set_simpl.
  - exploit Exp.freeVars_live; eauto with cset.
  - cset_tac.
  - exploit Ops.freeVars_live; eauto.
    rewrite IHLS1, IHLS2; eauto. rewrite H0, H1, H2; eauto.
    clear; cset_tac.
  - erewrite get_nth; eauto using zip_get; simpl.
    eapply list_union_incl; intros; inv_get; eauto with cset.
    edestruct get_flt; eauto; dcr.
    exploit argsLive_live_exp_sound; eauto.
    exploit Ops.freeVars_live; eauto with cset.
  - rewrite <- zip_app; eauto with len.
    rewrite IHLS; eauto.
    eapply union_incl_split; eauto.
    eapply list_union_incl; intros; inv_get; [|eauto with cset]; simpl.
    rewrite of_list_flt. rewrite H1; eauto.
    exploit H2 as INCL; dcr; eauto; simpl in *.
    rewrite <- INCL. clear; cset_tac.
Qed.

Lemma DVE_freeVars ZL LV s lv
      (LS:true_live_sound Functional ZL LV s lv)
  : freeVars (compile (zip pair LV ZL) s lv) ⊆ freeVars s.
Proof.
  general induction LS; simpl; repeat cases; simpl; eauto.
  - rewrite IHLS; eauto.
  - rewrite not_or_dist in NOTCOND; dcr.
    assert (x ∉ freeVars (compile (pair ⊜ Lv ZL) b al)). {
      exploit DVE_freeVars_live; eauto.
    }
    cset_tac.
  - rewrite IHLS1, IHLS2; eauto with cset.
  - erewrite get_nth; eauto using zip_get; simpl.
    eapply list_union_incl; intros; inv_get; eauto with cset.
    eapply get_flt in H4; eauto; dcr.
    eapply incl_list_union; eauto using get.
  - rewrite <- zip_app; eauto with len.
    rewrite IHLS; eauto. eapply incl_union_lr; eauto.
    eapply list_union_incl; intros; inv_get;[|eauto with cset]; simpl.
    eapply incl_list_union; eauto using get.
    rewrite of_list_flt.
    exploit H0; eauto. simpl in *.
    exploit DVE_freeVars_live; eauto.
    exploit H1; eauto.
    set (X:=compile (pair ⊜ (getAnn ⊝ als ++ Lv) (fst ⊝ F ++ ZL)) (snd x0) x1) in *.
    revert H7 H8; clear. cset_tac.
Qed.

Lemma DVE_paramsMatch i ZL LV s lv
  : true_live_sound i ZL LV s lv
    -> paramsMatch s (@length _ ⊝ ZL)
    -> paramsMatch (compile (zip pair LV ZL) s lv) (@length _ ⊝ ((fun Z lv => flt lv Z Z) ⊜ ZL LV)).
Proof.
  intros TLS PM.
  general induction PM; invt true_live_sound; simpl in * |- *; repeat cases;
    eauto 10 using paramsMatch.
  - erewrite !get_nth; eauto using zip_get.
    econstructor; eauto with get. simpl.
    eapply map_get_eq; eauto using zip_get.
    erewrite flt_length; eauto.
  - econstructor; intros; inv_get; simpl.
    + rewrite <- !zip_app; eauto with len.
      rewrite <- !List.map_app.
      exploit H0; eauto.
      * rewrite <- !List.map_app; eauto.
      * eqassumption.
        rewrite map_zip; simpl.
        rewrite zip_app. f_equal. f_equal.
        rewrite zip_map_l, zip_map_r. reflexivity.
        eauto with len.
    + rewrite <- !zip_app; eauto.
      exploit IHPM; eauto.
      * rewrite <- !List.map_app; eauto.
      * eqassumption.
        rewrite <- List.map_app.
        rewrite map_zip; simpl.
        rewrite zip_app. f_equal. f_equal.
        rewrite zip_map_l, zip_map_r. reflexivity.
        eauto with len.
      *  eauto with len.
Qed.

Lemma DVE_live_incl i (FNC:isFunctional i) ZL LV s ra (RA:renamedApart s ra) lv (G D:set var)
      (TLS:true_live_sound i ZL LV s lv)
      (AN:ann_R (fun x y => x ⊆ fst y) lv ra)
      (Incl1:getAnn lv ⊆ D)
      (Incl3:D ⊆ fst (getAnn ra))
      (Incl2:G ⊆ D)
  : ann_R (fun x y => x ⊆ fst y)
          (compile_live s lv G)
          (compile_renamedApart s lv ra D).
Proof.
  time (general induction AN; invt true_live_sound; invt renamedApart; simpl in *;
        set_simpl).
  - econstructor; eauto with cset len.
  - econstructor; eauto with cset len.
  - destruct e.
    + repeat cases; simpl in *; [|exfalso; cset_tac|].
      * econstructor. eauto with cset.
        eapply IHAN; try eassumption.
        eauto with cset. pe_rewrite. eauto with cset.
        eauto with cset.
      * eapply IHAN; eauto. cset_tac. pe_rewrite. cset_tac.
        cset_tac.
    + repeat cases; simpl in *.
      * econstructor. eauto with cset.
        eapply IHAN; try eassumption.
        eauto with cset. pe_rewrite. eauto with cset.
        eauto with cset.
  - econstructor. simpl. rewrite Incl1, Incl2; clear_all; cset_tac.
    + eapply IHAN1; eauto with cset. pe_rewrite. eauto with cset.
    + eapply IHAN2; eauto with cset. pe_rewrite. eauto.
  - econstructor; simpl; eauto.
    + rewrite Incl1, Incl2; clear; cset_tac.
    + eauto with len.
    + intros; inv_get.
      exploit H1; eauto.
      eapply ann_R_get in H3.
      edestruct H15; dcr; eauto.
      rewrite H9 in H3.
      exploit H14; try eassumption.
      exploit H12; try eassumption. simpl in *.
      cases in H21.
      rewrite Incl1 in H21.
      eapply H2; eauto.
      -- rewrite of_list_flt.
         rewrite <- H21.
         clear; cset_tac.
      -- rewrite of_list_flt.
         rewrite H9. rewrite <- Incl3.
         clear; cset_tac.
      -- eauto with cset.
    + eapply IHAN; eauto. eauto with cset.
      pe_rewrite. eauto with cset. eauto with cset.
Qed.

Require Import VarP.

Lemma DVE_var_P o (P:var -> Prop) LV ZL (s:stmt) lv
      (VP:var_P P s)
      (TLS:true_live_sound o ZL LV s lv)
  : var_P P (compile (zip pair LV ZL) s lv).
Proof.
  general induction VP; invt true_live_sound; simpl;
    repeat cases; eauto 10 using var_P.
  - econstructor; eauto.
    erewrite get_nth; eauto using zip_get. simpl.
    hnf; intros.
    eapply list_union_get in H0; destruct H0; dcr; inv_get.
    eapply get_flt in H0; dcr.
    eapply H; eauto. eapply incl_list_union; eauto using zip_get.
    reflexivity.
  - econstructor; eauto.
    + intros; inv_get; simpl.
      rewrite <- zip_app; eauto with len.
    + intros; inv_get; simpl.
      rewrite of_list_flt.
      rewrite meet_comm.
      rewrite meet_incl; eauto.
    + rewrite <- zip_app; eauto with len.
Qed.

author: sigurdschneider

repo: lvc

save_path: github-repos/coq/sigurdschneider-lvc


text:
From iris.algebra Require Import excl auth gmap agree.
From iris.proofmode Require Import proofmode.
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Import proofmode notation par.
From iris_examples.logatom.snapshot Require Import spec.
From iris.prelude Require Import options.

(** Specifying snapshots with histories
    Inspired by atomic pair snapshot data structure from Sergey et al. (ESOP 2015) *)

(*
     new_snapshot v :=
       ref (ref (v, 0))
 *)
Definition new_snapshot : val :=
  λ: "v",
    ref (ref ("v", #0)).

(*
    write xp x :=
      let xp1 = !xp in
      let v   = (!xp1).2
      let xp2 = ref (x, v + 1)
      // This is where we need the nested references: the CAS compares the old
      // inner reference with the new one, because it cannot atomically compared
      // a pair of values.
      if CAS xp xp1 xp2
        then ()
        else writeX (xp, yp) x
 *)
Definition write : val :=
  rec: "write" "xp" "x" :=
    let: "xp1"  := !"xp"                  in
    let: "v"    := Snd (!"xp1")           in
    let: "xp2"  := ref ("x", "v" + #1)    in
    if: CAS "xp" "xp1" "xp2"
    then #()
    else "write" "xp" "x".

(*
    read xp :=
      (!!xp).1
 *)
Definition read : val :=
  λ: "xp",
    Fst !(!"xp").

(*
    read_with xp l :=
      let (x, v)  = !!xp in
      let y       = !l in
      let (_, v') = !!xp in
      if v = v'
        then (x, y)
        else read_with l
 *)
Definition read_with_proph : val :=
  rec: "read_with" "xp" "l" :=
    let: "proph"  := NewProph in
    let: "x"  := ! !"xp" in
    let: "y"  := !"l" in
    let: "x'" := ! !"xp" in
    let: "v_eq"   := Snd "x" = Snd "x'" in
    resolve_proph: "proph" to: "v_eq" ;;
    if: "v_eq"
    then (Fst "x", "y")
    else  "read_with" "xp" "l".

(** The CMRA & functor we need. *)

Definition timestampUR := gmapUR Z $ agreeR valO.

Class atomic_snapshotG Σ := AtomicSnapshotG {
                                atomic_snapshot_stateG :> inG Σ $ authR $ optionUR $ exclR $ valO;
                                atomic_snapshot_timestampG :> inG Σ $ authR $ timestampUR
}.
Definition atomic_snapshotΣ : gFunctors :=
  #[GFunctor (authR $ optionUR $ exclR $ valO); GFunctor (authR timestampUR)].

Global Instance subG_atomic_snapshotΣ {Σ} : subG atomic_snapshotΣ Σ → atomic_snapshotG Σ.
Proof. solve_inG. Qed.

Section atomic_snapshot.

  Context {Σ} `{!heapGS Σ, !atomic_snapshotG Σ}.

  Variable N: namespace.

  Definition gmap_to_UR T : timestampUR := to_agree <$> T.

  Definition snapshot_inv γ1 γ2 l1 : iProp Σ :=
    (∃ (l1':loc) (T : gmap Z val) x (t : Z),
      (* we add the q to make the l1' map fractional. that way,
         we can take a fraction of the l1' map out of the invariant
         and do a case analysis on whether the pointer is the same
         throughout invariant openings *)
      l1 ↦ #l1' ∗ l1' ↦□ (x, #t) ∗
         own γ1 (● Excl' x) ∗ own γ2 (● gmap_to_UR T) ∗
         ⌜T !! t = Some x⌝ ∗
         ⌜∀ (t' : Z), t' ∈ dom (gset Z) T → (t' ≤ t)%Z⌝)%I.

  Definition is_snapshot (γs: gname * gname) (p : val) :=
    (∃ (l1 : loc), ⌜p = #l1%V⌝ ∗ inv N (snapshot_inv γs.1 γs.2 l1))%I.

  Global Instance is_snapshot_persistent γs p : Persistent (is_snapshot γs p) := _.

  Definition snapshot_content (γs : gname * gname) (a : val) :=
    (own γs.1 (◯ Excl' a))%I.

  Global Instance snapshot_content_timeless γs a : Timeless (snapshot_content γs a) := _.

  Lemma snapshot_content_exclusive γs a1 a2 :
    snapshot_content γs a1 -∗ snapshot_content γs a2 -∗ False.
  Proof.
    iIntros "H1 H2".
    iDestruct (own_valid_2 with "H1 H2") as %[]%auth_frag_op_valid_1.
  Qed.

  Definition new_timestamp t v : gmap Z val := {[ t := v ]}.

  Lemma new_snapshot_spec (v : val) :
      {{{ True }}}
        new_snapshot v
      {{{ γs p, RET p; is_snapshot γs p ∗ snapshot_content γs v }}}.
  Proof.
    iIntros (Φ _) "Hx". rewrite /new_snapshot. wp_lam.
    repeat (wp_proj; wp_let).
    wp_alloc lx' as "Hlx'".
    iMod (mapsto_persist with "Hlx'") as "Hlx'".
    wp_alloc lx as "Hlx".
    set (Excl' v) as p.
    iMod (own_alloc (● p ⋅ ◯ p)) as (γ1) "[Hx⚫ Hx◯]". {
      rewrite /p. apply auth_both_valid_discrete. split; done.
    }
    set (new_timestamp 0 v) as t.
    iMod (own_alloc (● gmap_to_UR t ⋅ ◯ gmap_to_UR t)) as (γ2) "[Ht⚫ Ht◯]". {
      rewrite /t /new_timestamp. apply auth_both_valid_discrete.
      split; first done. rewrite /gmap_to_UR map_fmap_singleton. apply singleton_valid. done.
    }
    iApply ("Hx" $! (γ1, γ2)).
    iMod (inv_alloc N _ (snapshot_inv γ1 γ2 _) with "[-Hx◯ Ht◯]") as "#Hinv". {
      iNext. rewrite /snapshot_inv. iExists _, _, _, 0. iFrame.
      iPureIntro. split; first done. intros ?. subst t. rewrite /new_timestamp dom_singleton.
      rewrite elem_of_singleton. lia.
    }
    iModIntro. rewrite /is_snapshot /snapshot_content. iFrame. iExists _.
    iSplitL; first done. done.
  Qed.

 Lemma excl_update γ n' n m :
    own γ (● (Excl' n)) -∗ own γ (◯ (Excl' m)) ==∗
      own γ (● (Excl' n')) ∗ own γ (◯ (Excl' n')).
  Proof.
    iIntros "Hγ● Hγ◯".
    iMod (own_update_2 _ _ _ (● Excl' n' ⋅ ◯ Excl' n') with "Hγ● Hγ◯") as "[$$]".
    { by apply auth_update, option_local_update, exclusive_local_update. }
    done.
  Qed.

  Lemma excl_sync γ n m :
    own γ (● (Excl' n)) -∗ own γ (◯ (Excl' m)) -∗ ⌜m = n⌝.
  Proof.
    iIntros "Hγ● Hγ◯".
    iDestruct (own_valid_2 with "Hγ● Hγ◯") as
        %[H%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
    done.
  Qed.

  Lemma timestamp_dupl γ T:
    own γ (● T) ==∗ own γ (● T) ∗ own γ (◯ T).
  Proof.
    iIntros "Ht". iApply own_op. iApply (own_update with "Ht").
    apply auth_update_alloc. apply local_update_unital_discrete => f Hv. rewrite left_id => <-.
    split; first done. apply core_id_dup. apply _.
  Qed.

  Lemma timestamp_update γ (T : gmap Z val) (t : Z) x :
    T !! t = None →
    own γ (● gmap_to_UR T) ==∗ own γ (● gmap_to_UR (<[ t := x ]> T)).
  Proof.
    iIntros (HT) "Ht".
    set (<[ t := x ]> T) as T'.
    iDestruct (own_update _ _ (● gmap_to_UR T' ⋅ ◯ gmap_to_UR {[ t := x ]}) with "Ht") as "Ht". {
      apply auth_update_alloc. rewrite /T' /gmap_to_UR map_fmap_singleton. rewrite fmap_insert.
      apply alloc_local_update; last done. rewrite lookup_fmap HT. done.
    }
    iMod (own_op with "Ht") as "[Ht● Ht◯]". iModIntro. iFrame.
  Qed.

  Lemma timestamp_sub γ (T1 T2 : gmap Z val):
    own γ (● gmap_to_UR T1) ∗ own γ (◯ gmap_to_UR T2) -∗
    ⌜∀ t x, T2 !! t = Some x → T1 !! t = Some x⌝.
  Proof.
    iIntros "[Hγ⚫ Hγ◯]".
    iDestruct (own_valid_2 with "Hγ⚫ Hγ◯") as
        %[H Hv]%auth_both_valid_discrete. iPureIntro. intros t x HT2.
    pose proof (iffLR (lookup_included (gmap_to_UR T2) (gmap_to_UR T1)) H t) as Ht.
    rewrite !lookup_fmap HT2 /= in Ht.
    destruct (is_Some_included _ _ Ht) as [? [t2 [Ht2 ->]]%fmap_Some_1]; first by eauto.
    revert Ht.
    rewrite Ht2 Some_included_total to_agree_included. fold_leibniz.
    by intros ->.
  Qed.

  Lemma write_spec γ (x2: val) p :
      is_snapshot γ p  -∗
      <<< ∀ x : val, snapshot_content γ x >>>
        write p x2 @ ↑N
      <<< snapshot_content γ x2, RET #() >>>.
  Proof.
    iIntros "Hx". iIntros (Φ) "AU". iLöb as "IH".
    iDestruct "Hx" as (l1 ->) "#Hinv". wp_pures. wp_lam. wp_pures.
    (* first read *)
    (* open invariant *)
    wp_bind (!_)%E. iInv N as (l1' T x v') "[Hl1 [#Hl1' [Hx⚫ Htime]]]".
      wp_load.
      iModIntro. iSplitR "AU".
      (* close invariant *)
      { iNext. rewrite /snapshot_inv. eauto 10 with iFrame. }
    wp_let. wp_bind (!_)%E. clear T.
    wp_load. wp_proj. wp_let. wp_op. wp_alloc l1'new as "Hl1'new".
    wp_let.
    (* CAS *)
    wp_bind (CmpXchg _ _ _)%E.
    (* open invariant *)
    iInv N as (l1'' T x' v'') ">[Hl1 [#Hl1'' [Hx⚫ [Ht● Ht]]]]".
    iDestruct "Ht" as %[Ht Hvt].
    destruct (decide (l1'' = l1')) as [-> | Hn].
    - wp_cmpxchg_suc.
      iMod (mapsto_persist with "Hl1'new") as "Hl1'new".
      iDestruct (mapsto_agree with "Hl1' Hl1''") as %[= -> ->].
      (* open AU *)
      iMod "AU" as (xv) "[Hx [_ Hclose]]".
        (* update snapshot ghost state to (x2, y') *)
        iDestruct (excl_sync with "Hx⚫ Hx") as %[= ->].
        iMod (excl_update _ x2 with "Hx⚫ Hx") as "[Hx⚫ Hx◯]".
        (* close AU *)
        iMod ("Hclose" with "Hx◯") as "HΦ".
      (* update timestamp *)
      iMod (timestamp_update _ T (v'' + 1)%Z x2 with "[Ht●]") as "Ht".
      { eapply (not_elem_of_dom (D:=gset Z) T). intros Hd. specialize (Hvt _ Hd). lia. }
      { done. }
      (* close invariant *)
      iModIntro. iSplitR "HΦ".
      + iNext. rewrite /snapshot_inv.
        set (<[ (v'' + 1)%Z := x2]> T) as T'.
        iExists l1'new, T', x2, (v'' + 1)%Z.
        iFrame.
        iPureIntro. split.
        * apply: lookup_insert.
        * intros t' Hv. destruct (decide (t' = (v'' + 1)%Z)) as [-> | Hn]; first done.
          assert (dom (gset Z) T' = {[(v'' + 1)%Z]} ∪ dom (gset Z) T) as Hd. {
            apply leibniz_equiv. rewrite dom_insert. done.
          }
          rewrite Hd in Hv. clear Hd. apply elem_of_union in Hv.
          destruct Hv as [Hv%elem_of_singleton_1 | Hv]; first done.
          specialize (Hvt _ Hv). lia.
      + wp_pures. done.
    - wp_cmpxchg_fail. iModIntro. iSplitR "AU".
      + iNext. rewrite /snapshot_inv. eauto 10 with iFrame.
      + wp_pures. iApply "IH"; last eauto. rewrite /is_snapshot. eauto.
  Qed.

  Lemma read_spec γ p :
    is_snapshot γ p -∗
    <<< ∀ v : val, snapshot_content γ v >>>
      read p @ ↑N
    <<< snapshot_content γ v, RET v >>>.
  Proof.
    iIntros "Hx". iIntros (Φ) "AU".
    iDestruct "Hx" as (l1 ->) "#Hinv".
    wp_lam. wp_bind (! #l1)%E.
    (* open invariant for 1st read *)
    iInv N as (l1' T x v') ">[Hl1 [#Hl1' [Hx⚫ Htime]]]".
      wp_load.
      iMod "AU" as (xv) "[Hx [_ Hclose]]".
      iDestruct (excl_sync with "Hx⚫ Hx") as %[= ->].
      iMod ("Hclose" with "Hx") as "HΦ".
      (* close invariant *)
      iModIntro. iSplitR "HΦ Hl1'". {
        iNext. unfold snapshot_inv. eauto 7 with iFrame.
      }
    iApply wp_fupd. wp_load. wp_pures. eauto.
  Qed.

  Definition prophecy_to_bool (v : list (val * val)) : bool :=
    match v with
    | (_, LitV (LitBool b)) :: _ => b
    | _                          => false
    end.

  Lemma read_with_spec γ p (l : loc) :
    is_snapshot γ p -∗
    <<< ∀ v1 v2 : val, snapshot_content γ v1 ∗ l ↦ v2 >>>
       read_with_proph p #l @ ↑N
    <<< snapshot_content γ v1 ∗ l ↦ v2, RET (v1, v2) >>>.
  Proof.
    iIntros "Hx". iIntros (Φ) "AU". iLöb as "IH". wp_lam. wp_pures.
    (* ************ new prophecy ********** *)
    wp_apply wp_new_proph; first done.
    iIntros (proph_val proph) "Hpr".
    wp_pures.
    (* ************ 1st readX ********** *)
    iDestruct "Hx" as (l1 ->) "#Hinv". wp_bind (! #l1)%E.
    (* open invariant for 1st read *)
    iInv N as (l1' T_x x1 v_x1) ">[Hl1 [#Hl1' [Hx⚫ [Ht_x Htime_x]]]]".
      iDestruct "Htime_x" as %[Hlookup_x Hdom_x].
      wp_load.
      iMod "AU" as (xv yv) "[[Hx Hy] [Hclose _]]".
      iDestruct (excl_sync with "Hx⚫ Hx") as %[= ->].
      iMod ("Hclose" with "[$Hx $Hy]") as "AU".
      (* duplicate timestamp T_x1 *)
      iMod (timestamp_dupl with "Ht_x") as "[Ht_x1⚫ Ht_x1◯]".
      (* close invariant *)
      iModIntro. iSplitR "AU Hl1' Ht_x1◯ Hpr". {
        iNext. unfold snapshot_inv. eauto 8 with iFrame.
      }
    wp_load. wp_let.
    (* ************ readY ********** *)
    repeat (wp_lam; wp_pures). wp_bind (!_)%E.
    iInv N as (l1'_y T_y x_y v_y) ">[Hl1 [#Hl1'_y [Hx⚫ [Ht_y Htime_y]]]]".
    iDestruct "Htime_y" as %[Hlookup_y Hdom_y].
    (* linearization point *)
    clear yv.
    iMod "AU" as (xv yv) "[[Hx Hy] Hclose]".
    wp_load.
    rewrite /snapshot_content.
    iDestruct (excl_sync with "Hx⚫ Hx") as %[= ->].
    destruct (prophecy_to_bool proph_val) eqn:Hproph.
    - (* prophecy value is predicting that timestamp has not changed, so we commit *)
      (* committing AU *)
      iMod ("Hclose" with "[$Hx $Hy]") as "HΦ".
      (* duplicate timestamp T_y *)
      iMod (timestamp_dupl with "Ht_y") as "[Ht_y● Ht_y◯]".
      (* show that T_x <= T_y *)
      iDestruct (timestamp_sub with "[Ht_y● Ht_x1◯]") as "%Hs"; first by iFrame.
      iModIntro. iModIntro.
      (* closing invariant *)
      iSplitR "HΦ Hl1' Ht_x1◯ Ht_y◯ Hpr".
      { iNext. unfold snapshot_inv. eauto 10 with iFrame. }
      wp_let.
      (* ************ 2nd readX ********** *)
      repeat (wp_lam; wp_pures). wp_bind (! #l1)%E.
      (* open invariant *)
      iInv N as (l1'_x2 T_x2 x2 v_x2) ">[Hl1 [#Hl1'_x2 [Hx⚫ [Ht_x2 Htime_x2]]]]".
      iDestruct "Htime_x2" as %[Hlookup_x2 Hdom_x2].
      wp_load.
      (* show that T_y <= T_x2 *)
      iDestruct (timestamp_sub with "[Ht_x2 Ht_y◯]") as "%Hs'"; first by iFrame.
      iModIntro. iSplitR "HΦ Hpr". {
        iNext. unfold snapshot_inv. eauto 8 with iFrame.
      }
      wp_load. wp_pures.
      case_bool_decide as Heq; wp_apply (wp_resolve_proph with "Hpr");
        iIntros (vs') "[Eq _]"; iDestruct "Eq" as %->; wp_seq; wp_if.
      + inversion Heq; subst; clear Heq. wp_pures.
        assert (v_x2 = v_y) as ->. {
          assert (v_x2 ≤ v_y)%Z as vneq. {
            apply Hdom_y.
            eapply (iffRL (elem_of_dom T_y _)). eauto using mk_is_Some.
          }
          assert (v_y ≤ v_x2)%Z as vneq'. {
            apply Hdom_x2.
            eapply (iffRL (elem_of_dom T_x2 _)). eauto using mk_is_Some.
          }
          apply Z.le_antisymm; auto.
        }
        assert (x1 = x_y) as ->. {
          specialize (Hs _ _ Hlookup_x). rewrite Hs in Hlookup_y. inversion Hlookup_y. done.
        }
        done.
      + inversion Hproph.
    - (* prophecy value is predicting that timestamp has not changed, so we abort *)
      iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "[$Hx $Hy]") as "AU".
      iModIntro. iModIntro.
      (* closing invariant *)
      iSplitR "AU Hpr".
      { iNext. unfold snapshot_inv. eauto 10 with iFrame. }
      wp_let.
      (* ************ 2nd readX ********** *)
      wp_bind (! #l1)%E.
      (* open invariant *)
      iInv N as (l1'_x2 T_x2 x2 v_x2) "[Hl1 [#Hl1'_x2 [Hx⚫ [Ht_x2 Htime_x2]]]]".
      wp_load.
      iModIntro. iSplitR "AU Hpr". {
        iNext. unfold snapshot_inv. eauto 8 with iFrame.
      }
      wp_load. wp_pures.
      wp_apply (wp_resolve_proph with "Hpr").
      iIntros (vs') "[Heq _]"; iDestruct "Heq" as %->.
      case_bool_decide as Heq.
      + inversion Heq; subst; clear Heq. inversion Hproph.
      + wp_seq. wp_if. iApply "IH"; rewrite /is_snapshot; eauto.
  Qed.

End atomic_snapshot.

Program Definition atomic_snapshot `{!heapGS Σ, atomic_snapshotG Σ} :
  spec.atomic_snapshot Σ :=
  {| spec.new_snapshot_spec := new_snapshot_spec;
     spec.write_spec := write_spec;
     spec.read_spec := read_spec;
     spec.read_with_spec := read_with_spec;
     spec.snapshot_content_exclusive := snapshot_content_exclusive |}.

Typeclasses Opaque snapshot_content is_snapshot.

repo: iris-heaplang-experiments


text:
Require Export Lambda.Util.Basic.
From Equations Require Export Equations.

(** * List helpers. *)

Section List.
  Context {A : Set}.

  Inductive Has : A -> list A -> Set :=
  | HasO : forall a t, Has a (a :: t)
  | HasS : forall a h t, Has a t -> Has a (h :: t).

  Global Arguments HasO {_} {_}.
  Global Arguments HasS {_} {_} {_}.

  Equations Derive NoConfusion NoConfusionHom Subterm for list.
  Equations Derive Signature NoConfusion for Has.

  Equations ext_has : forall {Γ Δ},
      (forall a : A, Has a Γ -> Has a Δ) ->
      forall b a : A, Has a (b :: Γ) -> Has a (b :: Δ) :=
    ext_has ρ _ _ HasO := HasO;
    ext_has ρ _ _ (HasS h) := HasS (ρ _ h).

  Equations ext_has_app_l : forall {Γ Δ},
      (forall a : A, Has a Γ -> Has a Δ) ->
      forall (l : list A) (a : A), Has a (l ++ Γ) -> Has a (l ++ Δ) :=
    ext_has_app_l ρ []:= ρ;
    ext_has_app_l ρ (h :: t) := ext_has (ext_has_app_l ρ t) h.

  Definition Has_nth_error : forall {Γ a},
      Has a Γ -> { n | nth_error Γ n = Some a}.
  Proof.
    intros l a h; induction h.
    - refine (exist _ 0 _); reflexivity.
    - destruct IHh as [k Hk].
      refine (exist _ (S k) _); assumption.
  Defined.

  Variant zilch : list A -> Prop := zilch_nil : zilch [].

  Definition lookup :
    forall {Γ : list A} {n : nat},
      n < length Γ -> A.
  Proof.
    refine
      (fix F Γ n HnΓ :=
         match Γ as Γ' return Γ = Γ' -> A with
         | []
           => fun HΓΓ' => _
         | a :: Δ
         => fun HΓΓ' =>
             match n as n' return n = n' -> A with
             | O   => fun _ => a
             | S k => fun Hnn' => F Δ k _
             end eq_refl
         end eq_refl).
    - inv HΓΓ'; cbn in *; lia.
    - subst; cbn in *; lia.
  Defined.

  (* Require Import Extraction.
     Recursive Extraction lookup. *)

  Definition length_nth_error' :
    forall {l : list A} {n : nat},
      n < length l -> { a | nth_error l n = Some a }.
  Proof.
    refine
    (fix F l n Hnl :=
       match
         l as l'
         return
         l = l' -> { a | nth_error l n = Some a } with
       | [] => fun H => _
       | h :: t
         => fun H =>
             match
               n as n'
               return
               n = n' -> { a | nth_error l n = Some a } with
             | O
               => fun _ => @exist _ _ h _
             | S k
               => fun Hnn' =>
                   match F t k _ with
                   | exist _ a' Hk => @exist _ _ a' _
                   end
             end eq_refl
       end eq_refl); subst; cbn in *;
      lia || reflexivity || assumption.
  Defined.

  Definition nth_error_lookup :
    forall {Γ : list A} {n : nat} (H : n < length Γ),
      nth_error Γ n = Some (lookup H).
  Proof.
    intro l; induction l as [| a l IHl];
      intros [| n] H; cbn in *;
        try lia; eauto using Lt.lt_S_n.
  Defined.

  Local Hint Constructors Has : core.

  Definition nth_error_Has : forall {Γ a n},
      nth_error Γ n = Some a -> Has a Γ.
  Proof.
    intro l; induction l as [| h t IHt];
      intros a [| n] Hnth; cbn in *; try discriminate; eauto.
    inv Hnth; auto.
  Defined.

  Definition nth_error_Has' : forall {Γ a},
      {n | nth_error Γ n = Some a} -> Has a Γ.
  Proof.
    intros l a [n H]; exact (nth_error_Has H).
  Defined.

  Definition ext_nth_error : forall {Γ Δ : list A},
      (forall a, {n | nth_error Γ n = Some a} ->
              {k | nth_error Δ k = Some a}) ->
      forall b a, {n | nth_error (b :: Γ) n = Some a} ->
               {k | nth_error (b :: Δ) k = Some a}.
  Proof.
    intros l d f b a Hab.
    apply Has_nth_error.
    apply nth_error_Has' in Hab.
    pose proof (fun a H => nth_error_Has' (f a (Has_nth_error H))) as H.
    eauto using ext_has.
  Defined.
End List.

Equations has_map :
  forall {A B : Set} (f : A -> B) {l : list A} {e : A},
    Has e l -> Has (f e) (map f l) :=
  has_map f  HasO     := HasO;
  has_map f (HasS hs) := HasS (has_map f hs).

Definition map_has : forall (A B : Set) (f : A -> B) (l : list A) b,
    Has b (map f l) -> {a : A & f a = b & Has a l}.
Proof.
  intros A B f l.
  induction l as [| a l ih]; intros b h; cbn in *; depelim h.
  - exact (existT2 _ _ a eq_refl HasO).
  - apply ih in h0 as [a' fab hasa].
    exact (existT2 _ _ a' fab (HasS hasa)).
Defined.

Section Hlist.
  Context {A : Set}.

  Inductive hlist (F : A -> Type) : list A -> Type :=
  | hnil : hlist F []
  | hcons : forall a l,
      F a ->
      hlist F l ->
      hlist F (a :: l).
  Equations Derive Signature NoConfusion NoConfusionHom for hlist.

  Global Arguments hnil {_}.
  Global Arguments hcons {_} {_} {_}.

  Equations lookup_has : forall {F : A -> Type} {Γ : list A} {a : A},
      hlist F Γ -> Has a Γ -> F a :=
    lookup_has (hcons v _) HasO      := v;
    lookup_has (hcons _ ϵ) (HasS hs) := lookup_has ϵ hs.
End Hlist.

author: rudynicolop

repo: Lambda-Calculi-Coq


text:
Require Export VST.zlist.sublist.
Require Export compcert.lib.Integers.
Require Export compcert.lib.Coqlib.
Require Export List. Import ListNotations.
Require Export aes.sbox.

(* substitute b for its counterpart in the sbox *)
Definition look_sbox (b: int) : int :=
  (* All possible values of b are covered in the sbox so the default should never be returned *)
  Int.repr (Znth (Int.unsigned b) sbox).

(* substitute b for its counterpart in the inverse sbox *)
Definition look_inv_sbox (b: int) : int :=
  Int.repr (Znth (Int.unsigned b) inv_sbox).

(********************* GF(256) arithmetic *******************)

(* xtime operation from section 4.2.1. Corresponds to multiplying by 2 in GF(256) *)
Definition xtime (b: int) : int :=
  let b' := Int.modu (Int.shl b (Int.one)) (Int.repr 256) in (* shift left by one, mod 256 *)
  let c_1b := Int.repr 27 in (* 0x1b *)
  let c_80 := Int.repr 128 in (* 0x80 *)
  (* test if highest bit of b is one. If so, then XOR b' with 0x1b, otherwise return b' *)
  if Int.eq (Int.and b c_80) Int.zero then b'
  else Int.xor b' c_1b.

(* Finite field multiplication using xtime operation and xor for finite field addition
 * (Russian peasant multiplication), not described directly but suggested in section 4.2.1. *)

(* Repeatedly double b using xtime as per Russian peasant multiplication. Add b to accumulator
 * if there is a "remainder," i.e., the tested bit of a is 1 *)
Definition ff_checkbit (a b : int) (acc : int) : int :=
  (* if lowest bit of a is one, add (xor) b to acc. Otherwise do nothing *)
  if Int.eq (Int.and a Int.one) Int.zero then acc
  else Int.xor acc b.

Fixpoint xtime_test (a b : int) (acc : int) (shifts : nat) : int :=
  if Int.eq a Int.zero then acc (* if a or b are zero, nothing to do *)
  else if Int.eq b Int.zero then acc
  else
    (* check lowest bit of a, add b to acc if it is positive. Shift a
     * right for next iteration unless we're finished *)
    match shifts with
    | S n =>
      let acc' := ff_checkbit a b acc in
      (* shift a right and double b *)
      let a' := Int.shru a Int.one in
      let b' := xtime b in
      xtime_test a' b' acc' n
    | O => acc
    end.

Definition ff_mult (a b : int) : int := xtime_test a b Int.zero 8%nat.

(******************************************************************************************)

(* Defining words and state as they are considered in the specification, using tuples
 * to enforce the length requirement -- a word is 4 bytes, while a state is 4 words,
 * illustrated as 4 rows of 4 bytes *)
Definition word := (int * int * int * int) % type.
Definition state := (word * word * word * word) % type.
Definition block := state%type. (* Used synonymously with state in the spec, aliased here for readability *)

(* SubBytes() transformation described in section 5.1.1 *)
Definition sub_word (w: word) : word :=
  match w with (b1, b2, b3, b4) => (look_sbox b1, look_sbox b2, look_sbox b3, look_sbox b4) end.
Definition SubBytes (s: state) : state :=
  match s with (w1, w2, w3, w4) => (sub_word w1, sub_word w2, sub_word w3, sub_word w4) end.

(* ShiftRows() transformation described in section 5.1.2 *)
Definition ShiftRows (s : state) : state :=
  match s with
  ((b11, b12, b13, b14),
   (b21, b22, b23, b24),
   (b31, b32, b33, b34),
   (b41, b42, b43, b44)) =>

  ((b11, b12, b13, b14),
   (b22, b23, b24, b21),
   (b33, b34, b31, b32),
   (b44, b41, b42, b43))
  end.

(* MixColumns() transformation described in section 5.1.3 *)

Definition transform_column (col: word) : word :=
  match col with (b1, b2, b3, b4) =>
    let two := Int.repr 2 in
    let three := Int.repr 3 in
    (* (2*b1)^(3*b2)^b3^b4 *)
    let c0 := Int.xor (Int.xor (ff_mult two b1) (ff_mult three b2)) (Int.xor b3 b4) in
    (* b1^(2*b2)^(3*b3)^b4 *)
    let c1 := Int.xor (Int.xor b1 (ff_mult two b2)) (Int.xor (ff_mult three b3) b4) in
    (* b1^b2^(2*b3)^(3*b4)*)
    let c2 := Int.xor (Int.xor b1 b2) (Int.xor (ff_mult two b3) (ff_mult three b4)) in
    (* (3*b1)^b2^b3^(2*b4)*)
    let c3 := Int.xor (Int.xor (ff_mult three b1) b2) (Int.xor b3 (ff_mult two b4)) in
    (c0, c1, c2, c3)
  end.

(* lets us treat state by columns rather than rows *)
Definition transpose (s: state) : state :=
  match s with
   ((b11, b12, b13, b14),
    (b21, b22, b23, b24),
    (b31, b32, b33, b34),
    (b41, b42, b43, b44)) =>

   ((b11, b21, b31, b41),
    (b12, b22, b32, b42),
    (b13, b23, b33, b43),
    (b14, b24, b34, b44))
end.

(* apply column transformation to each column in the state *)
Definition MixColumns (s: state) : state :=
  let cols := transpose s in
  match cols with (c1, c2, c3, c4) =>
    transpose (transform_column c1, transform_column c2, transform_column c3, transform_column c4)
  end.

(* Key expansion functions, section 5.2 *)

(* SubWord function from section 5.2: apply S-box to each byte in a word *)
Definition SubWord (w: word) : word :=
  match w with (b1, b2, b3, b4) => (look_sbox b1, look_sbox b2, look_sbox b3, look_sbox b4) end.

(* RotWord function from section 5.2: rotate bytes left, wrapping around *)
Definition RotWord (w: word) : word :=
  match w with (b1, b2, b3, b4) => (b2, b3, b4, b1) end.

(* round constant (RCon) array, described in section 5.2 and explicitly written
 * out in appendix A.3 (256-bit key expansion example) *)
Definition RCon : list word := [
  (* 0x01000000 *) (Int.repr 1, Int.zero, Int.zero, Int.zero);
  (* 0x02000000 *) (Int.repr 2, Int.zero, Int.zero, Int.zero);
  (* 0x04000000 *) (Int.repr 4, Int.zero, Int.zero, Int.zero);
  (* 0x08000000 *) (Int.repr 8, Int.zero, Int.zero, Int.zero);
  (* 0x10000000 *) (Int.repr 16, Int.zero, Int.zero, Int.zero);
  (* 0x20000000 *) (Int.repr 32, Int.zero, Int.zero, Int.zero);
  (* 0x40000000 *) (Int.repr 64, Int.zero, Int.zero, Int.zero)
].

(* For AES-256, figure 4 fixes the key length in words at 8 and the number
 * of rounds at 14 *)
Definition Nk := 8. (* number of words in key *)
Definition Nr := 14. (* number of cipher rounds *)
Definition Nb := 4. (* number of words in a block (state) *)

(* xor two words together, i.e., apply xor byte by byte *)
Definition xor_word (w1 w2 : word) : word :=
  match w1, w2 with (b1, b2, b3, b4), (b1', b2', b3', b4') =>
    (Int.xor b1 b1', Int.xor b2 b2', Int.xor b3 b3', Int.xor b4 b4')
  end.

(* Expanded key is Nb*(Nr+1) words, or Nr+1 blocks *)
Definition extended_key_blocks := Nr+1.

(* Based on Figure 11 and diagram in appendex A.3 *)

(* Note that "even" and "odd" are if you start counting blocks at 1, rather than 0 *)
(* b1 and b2 are the two blocks generated before this round. *)
Definition odd_round (b1 b2 : block) (rcon: word) : block :=
  match b1, b2 with (w1, w2, w3, w4), (_, _, _, w8) =>
    let w1' := xor_word w1 (xor_word (SubWord (RotWord w8)) rcon) in
    let w2' := xor_word w2 w1' in
    let w3' := xor_word w3 w2' in
    let w4' := xor_word w4 w3' in
    (w1', w2', w3', w4')
  end.
Definition even_round (b1 b2: block) : block :=
  match b1, b2 with (w1, w2, w3, w4), (_, _, _, w8) =>
    let w1' := xor_word w1 (SubWord w8) in
    let w2' := xor_word w2 w1' in
    let w3' := xor_word w3 w2' in
    let w4' := xor_word w4 w3' in
    (w1', w2', w3', w4')
  end.

Fixpoint grow_key (b1 b2: block) (rcs: list word) : list block :=
  match rcs with
  | rc :: [] =>
    (* for the last round constant, only apply an odd round *)
    (odd_round b1 b2 rc) :: []
  | rc :: tl =>
    (* generate a block with an odd round, use it in the next even round and keep going *)
    let b3 := odd_round b1 b2 rc in
	let b4 := even_round b2 b3 in
	b3 :: b4 :: (grow_key b3 b4 tl)
  | [] => [] (* should not happen *)
  end.

(* Note that RCon list (round constants) is described in section 5.2 and its values are given in A.3.
 * k should be a list of words of length Nk. Returns a list of blocks of length Nr+1 *)
Definition KeyExpansion (k : list word) : list block :=
  match k with
  | [w1; w2; w3; w4; w5; w6; w7; w8] =>
    let b1 := (w1, w2, w3, w4) in
	let b2 := (w5, w6, w7, w8) in
	b1 :: b2 :: (grow_key b1 b2 RCon)
  | l => [] (* should not happen *)
  end.

(* AddRoundKey() described in section 5.1.4: it uses a block from the expanded key, xoring
 * each word from the expanded key block with a column from the state *)
Definition AddRoundKey (s : state) (kb : block) : state :=
  let cols := transpose s in
  match cols, kb with (c1,c2,c3,c4), (k1,k2,k3,k4) =>
    transpose (xor_word c1 k1, xor_word c2 k2, xor_word c3 k3, xor_word c4 k4)
  end.

(* Based on figure 5, description of the cipher *)
Definition round (s : state) (kb: block) : state :=
  AddRoundKey (MixColumns (ShiftRows (SubBytes s))) kb.
(* omits mix columns step *)
Definition last_round (s : state) (kb : block) : state :=
  AddRoundKey (ShiftRows (SubBytes s)) kb.

(* Applies cipher rounds given an expanded key *)
Fixpoint apply_rounds (s : state) (ek: list block) : state :=
  match ek with
  | rk :: [] => last_round s rk (* last round *)
  | rk :: tl => apply_rounds (round s rk) tl
  | [] => s (* should not happen *)
  end.

(* exp_key should be length Nr+1 blocks, produced by applying KeyExpansion on a valid key. *)
Definition Cipher (exp_key : list block) (init : state) : state :=
  match exp_key with
  | k1 :: tl =>
    let r1 := AddRoundKey init k1 in
	apply_rounds r1 tl
  | [] => init (* should not happen *)
  end.

(* Inverse cipher and inverse operations -- section 5.3 *)

(* InvShiftRows in section 5.3.1 *)
Definition InvShiftRows (s: state) : state :=
  match s with
    ((b11, b12, b13, b14),
     (b21, b22, b23, b24),
	 (b31, b32, b33, b34),
	 (b41, b42, b43, b44)) =>

	((b11, b12, b13, b14),
	 (b24, b21, b22, b23),
	 (b33, b34, b31, b32),
	 (b42, b43, b44, b41))
  end.

(* InvSubBytes in section 5.3.2 *)
Definition inv_sub_word (w: word) : word :=
  match w with (b1, b2, b3, b4) =>
    (look_inv_sbox b1, look_inv_sbox b2, look_inv_sbox b3, look_inv_sbox b4)
  end.

Definition InvSubBytes (s : state) : state :=
  match s with (w1, w2, w3, w4) =>
    (inv_sub_word w1, inv_sub_word w2, inv_sub_word w3, inv_sub_word w4)
  end.

(* InvMixColumns in 5.3.3 *)
Definition inv_transform_column (w: word) : word :=
  let c_e := Int.repr 14 in (* 0x0e *)
  let c_b := Int.repr 11 in (* 0x0b *)
  let c_d := Int.repr 13 in (* 0x0d *)
  let c_9 := Int.repr 9 in (* 0x09 *)
  match w with (b1, b2, b3, b4) =>
    (* (0x0e * b1) ^ (0x0b * b2) ^ (0x0d * b3) ^ (0x09 * b4) *)
    let b1' := Int.xor (Int.xor (ff_mult c_e b1) (ff_mult c_b b2)) (Int.xor (ff_mult c_d b3) (ff_mult c_9 b4)) in
    (* (0x09 * b1) ^ (0x0e * b2) ^ (0x0b * b3) ^ (0x0d * b4) *)
    let b2' := Int.xor (Int.xor (ff_mult c_9 b1) (ff_mult c_e b2)) (Int.xor (ff_mult c_b b3) (ff_mult c_d b4)) in
    (* (0x0d * b1) ^ (0x09 * b2) ^ (0x0e * b3) ^ (0x0b * b4) *)
    let b3' := Int.xor (Int.xor (ff_mult c_d b1) (ff_mult c_9 b2)) (Int.xor (ff_mult c_e b3) (ff_mult c_b b4)) in
    (* (0x0b * b1) ^ (0x0d * b2) ^ (0x09 * b3) ^ (0x0e * b4) *)
    let b4' := Int.xor (Int.xor (ff_mult c_b b1) (ff_mult c_d b2)) (Int.xor (ff_mult c_9 b3) (ff_mult c_e b4)) in
    (b1', b2', b3', b4')
  end.

Definition InvMixColumns (s : state) : state :=
  let cols := transpose s in
  match cols with (c1, c2, c3, c4) =>
    transpose (inv_transform_column c1, inv_transform_column c2, inv_transform_column c3, inv_transform_column c4)
  end.

(* applies InvMixColumns to all members of expanded key but the last *)
Fixpoint grow_inv_key (ek : list block) : list block :=
  match ek with
  | rk :: [] => rk :: [] (* don't do anything to last one *)
  | rk :: tl => InvMixColumns rk :: grow_inv_key tl
  | [] => [] (* should not happen *)
  end.

(* Inverse key expansion briefly described at end of figure 15. k should be of length Nk. *)
Definition InverseKeyExpansion (k : list word) : list block :=
  let exp_key := KeyExpansion k in
  match exp_key with
  (* don't apply inv mix columns to first round key either *)
  | k1 :: tl => k1 :: grow_inv_key tl
  | ek => [] (* should not happen *)
  end.

(* Inverse cipher described in figure 15 *)
Definition inv_round (s : state) (kb : block) : state :=
  AddRoundKey (InvMixColumns (InvShiftRows (InvSubBytes s))) kb.
(* omits mix columns *)
Definition inv_last_round (s : state) (kb : block) : state :=
  AddRoundKey (InvShiftRows (InvSubBytes s)) kb.

Fixpoint apply_inv_rounds (s: state) (ek: list block) : state :=
  match ek with
  | kb :: [] => inv_last_round s kb
  | kb :: tl => apply_inv_rounds (inv_round s kb) tl
  | [] => s (* should not happen *)
  end.

(* exp_key should be length Nr+1 blocks, produced by applying InverseKeyExpansion on a valid
 * key and reversing the result, since the round keys are supposed to be applied starting with
 * the last. (We pass the key in this way for simplifying verification, since the implementation's
 * key expansion process also reverses the key, whereas the specification reverses it during the
 * decryption process) *)
Definition EqInvCipher (exp_key: list block) (init: state) : state :=
  match exp_key with
  | kb :: tl => apply_inv_rounds (AddRoundKey init kb) tl
  | l => init (* should not happen *)
  end.

author: PrincetonUniversity

repo: VST


text:
(** Generated by coq-of-ocaml *)
Require Import OCaml.OCaml.

Local Set Primitive Projections.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Open Scope type_scope.
Import ListNotations.

Unset Positivity Checking.
Unset Guard Checking.

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Inductive natural : Set :=
| Succ : natural -> natural
| Zero : natural.

Inductive lst : Set :=
| Cons : natural -> lst -> lst
| Nil : lst.

Fixpoint double (n : natural) {struct n} : natural :=
  match n with
  | Succ n => Succ (Succ (double n))
  | Zero => Zero
  end.

Fixpoint append (append_arg0 : lst) (append_arg1 : lst) {struct append_arg0}
  : lst :=
  match append_arg0 with
  | Cons x y => Cons x (append y append_arg1)
  | Nil => append_arg1
  end.

Fixpoint len (n : lst) {struct n} : natural :=
  match n with
  | Cons _ y => Succ (len y)
  | Nil => Zero
  end.

Definition synth (lf1 : lst) (x : lst) : natural := len (append x lf1).

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Specific.montgomery64_2e416m2e208m1_7limbs.Synthesis.

(* TODO : change this to field once field isomorphism happens *)
Definition mul :
  { mul : feBW_small -> feBW_small -> feBW_small
  | forall a b, phiM_small (mul a b) = F.mul (phiM_small a) (phiM_small b) }.
Proof.
  Set Ltac Profiling.
  Time synthesize_mul ().
  Show Ltac Profile.
Time Defined.

Print Assumptions mul.


text:
Require Import Definitions.
Import Def.

Definition FalseProp : Term := TFor 0 (TSort KProp) (TVar 0).

(*goal*)
Theorem consistency : forall (t:Term) , TypeJudge nil t FalseProp -> False.
Proof.
Admitted.

author: pdf-jube-joba

repo: formal-verification-type


text:
(** Coq coding by choukh, June 2021 **)

Require Export Coq.Logic.Epsilon.
Require Import ZFC.Axiom.ZFC2.

(* 由希尔伯特epsilon算子导出选择公理 *)

(* 希尔伯特epsilon算子相当于类（class）上的选择函数（全局选择公理）*)
Definition ClassChoice := λ P, epsilon (inhabits ∅) P.
Definition class_choice_spec := λ P, epsilon_spec (inhabits ∅) P.

(* 把epsilon的能力限制在集合上（选择公理）*)
Definition SetChoice := λ S, ClassChoice (λ x, x ∈ S).
Definition set_choice_spec := λ S, class_choice_spec (λ x, x ∈ S).

(* “答案确实是在题目选项里选的” *)
Lemma chosen_contained : ∀ s, ⦿ s → SetChoice s ∈ s.
Proof. intros s. apply set_choice_spec. Qed.

(* “答案集包含在问题集的并集里” *)
Theorem chosen_included : ∀ S, (∀s ∈ S, ⦿s) → {SetChoice s | s ∊ S} ⊆ ⋃S.
Proof.
  intros S H x Hx.
  apply ReplAx in Hx as [s [H1 H2]].
  eapply UnionI. apply H1.
  apply H in H1. subst.
  apply chosen_contained. apply H1.
Qed.

(* “单选题” *)
Theorem one_chosen : ∀ S, (∀s ∈ S, ⦿s) →
  (∀ s t ∈ S, s ≠ t → disjoint s t) →
  ∀s ∈ S, ∃ x, s ∩ {SetChoice s | s ∊ S} = {x,}.
Proof with eauto.
  intros S Hi Hdj s Hs.
  exists (SetChoice s). apply sub_antisym.
  - intros x Hx. apply BInterE in Hx as [Hx1 Hx2].
    cut (x = SetChoice s).
    + intros. subst...
    + apply ReplAx in Hx2 as [t [Ht Hteq]].
      destruct (classic (s = t)) as [|Hnq].
      * congruence.
      * pose proof (chosen_contained t (Hi t Ht)) as Hx2.
        rewrite Hteq in Hx2. apply Hdj in Hnq...
        exfalso. eapply disjointE...
  - apply single_of_member_is_subset. apply BInterI.
    + apply chosen_contained. apply Hi...
    + apply ReplI...
Qed.

author: choukh

repo: Set-Theory

save_path: github-repos/coq/choukh-Set-Theory


text:
Require Import VST.floyd.proofauto.
Require Import VST.floyd.VSU.
Require Import pile.
Require Import simple_spec_stdlib.
Require Import simple_spec_pile.
Require Import PileModel.

Definition surely_malloc_spec :=
  DECLARE _surely_malloc
   WITH t:type, gv: globals
   PRE [ size_t ]
       PROP (0 <= sizeof t <= Ptrofs.max_unsigned;
                complete_legal_cosu_type t = true;
                natural_aligned natural_alignment t = true)
       PARAMS (Vptrofs (Ptrofs.repr (sizeof t))) GLOBALS (gv)
       SEP (mem_mgr gv)
    POST [ tptr tvoid ] EX p:_,
       PROP ()
       LOCAL (temp ret_temp p)
       SEP (mem_mgr gv; malloc_token Ews t p * data_at_ Ews t p).

Definition pile_imported_specs:funspecs := MallocFreeASI.

Definition pile_internal_specs: funspecs := surely_malloc_spec::PileASI.

Definition PileVprog: varspecs. mk_varspecs prog. Defined.
Definition PileGprog: funspecs := pile_imported_specs ++ pile_internal_specs.

Lemma body_surely_malloc: semax_body PileVprog PileGprog f_surely_malloc surely_malloc_spec.
Proof.
start_function.
forward_call (malloc_spec_sub t) gv.
Intros p.
if_tac.
{ subst.
  forward_if False.
  - forward_call 1. contradiction.
  - congruence. }
forward_if True.
+ contradiction.
+ forward. entailer!.
+ forward. Exists p. entailer!.
Qed.

Lemma body_Pile_new: semax_body PileVprog PileGprog f_Pile_new Pile_new_spec.
Proof.
start_function.
forward_call (tpile, gv).
Intros p.
repeat step!.
unfold pilerep, listrep, pile_freeable.
repeat step!.
Qed.

Lemma body_Pile_add: semax_body PileVprog PileGprog f_Pile_add Pile_add_spec.
Proof.
start_function.
forward_call (tlist, gv).
Intros q.
unfold pilerep.
Intros head.
forward.
forward.
forward.
forward.
unfold pilerep.
Exists q.
unfold listrep at 2; fold listrep.
Exists head.
entailer!; try apply derives_refl.
Qed.

Lemma body_Pile_count: semax_body PileVprog PileGprog f_Pile_count Pile_count_spec.
Proof.
start_function.
unfold pilerep. Intros head.
forward.
unfold Sfor.
forward.
forward_loop (EX r:val, EX s2: list Z,
   PROP(0 <= sumlist s2 <= sumlist sigma)
   LOCAL(temp _c (Vint (Int.repr (sumlist sigma - sumlist s2)));
              temp _p p; temp _q r)
   SEP (data_at Ews tpile head p;
          listrep s2 r -* listrep sigma head;
          listrep s2 r))%assert
   break:
  (PROP()
   LOCAL(temp _c (Vint (Int.repr (sumlist sigma))); temp _p p)
   SEP (data_at Ews tpile head p;
          listrep sigma head))%assert.
-
Exists head sigma.
entailer!. rewrite Z.sub_diag. auto.
apply wand_sepcon_adjoint. cancel.
-
Intros r s2.
forward_if (r<>nullval).
forward.
entailer!.
subst r.
forward.
entailer!.
assert (s2=nil) by intuition; subst s2.
simpl. rewrite Z.sub_0_r; auto.
sep_apply (modus_ponens_wand (listrep s2 nullval)).
cancel.
Intros.
destruct s2.
assert_PROP False; [ | contradiction]. {
 entailer!. assert (r=nullval) by intuition; subst r. congruence.
}
unfold listrep at 3; fold listrep.
Intros r'.
forward.
forward. {
 entailer!.
 simpl in H0.
 clear - H0 H H2 H9.
 rewrite (Int.signed_repr z) by rep_lia.
 rewrite (Int.signed_repr) by rep_lia.
 assert (0 <= sumlist s2). {
 clear - H9. induction s2; simpl; auto. lia.
 inv H9. apply IHs2 in H2. lia.
 }
 rep_lia.
}
forward.
Exists r' s2.
entailer!.
simpl. split.
simpl in H0.
 assert (0 <= sumlist s2). {
 clear - H9. induction s2; simpl; auto. lia.
 inv H9. apply IHs2 in H2. lia.
 }
 rep_lia.
 f_equal; f_equal; lia.
apply -> wand_sepcon_adjoint.
match goal with |- (_ * ?A * ?B * ?C)%logic |-- _ =>
 assert ((A * B * C)%logic |-- listrep (z::s2) r) end.
unfold listrep at 2; fold listrep. Exists r'. entailer!.
sep_apply H10.
sep_apply modus_ponens_wand.
auto.
 -
forward.
unfold pilerep.
Exists head.
cancel.
Qed.

Lemma body_Pile_free: semax_body PileVprog PileGprog f_Pile_free Pile_free_spec.
Proof.
start_function.
unfold pilerep.
unfold pile_freeable. Intros head.
forward.
forward_while (EX q:val, EX s2: list Z,
   PROP ( )
   LOCAL (temp _q q; temp _p p; gvars gv)
   SEP (data_at Ews tpile head p;
       listrep s2 q; malloc_token Ews tpile p;
   mem_mgr gv))%assert.
{ Exists head sigma; entailer!. }
{ entailer!. }
{ destruct s2.
   assert_PROP False; [|contradiction]. unfold listrep. entailer!.
  unfold listrep; fold listrep.
  Intros y.
  forward.
  forward_call (free_spec_sub (Tstruct _list noattr)) (q, gv).
  rewrite if_false by (intro; subst; contradiction).
  cancel.
  forward.
  Exists (y, s2).
  entailer!. cancel. }
subst.
assert_PROP (p<>nullval). entailer!.
forward_call (free_spec_sub (Tstruct _pile noattr))  (p, gv).
rewrite if_false by auto.
cancel.
forward.
rewrite (proj1 H0) by auto.
unfold listrep.
entailer!.
Qed.

Definition PileVSU: @VSU NullExtension.Espec
      nil pile_imported_specs ltac:(QPprog prog) PileASI emp.
  Proof.
    mkVSU prog pile_internal_specs.
    + solve_SF_internal body_surely_malloc.
    + solve_SF_internal body_Pile_new.
    + solve_SF_internal body_Pile_add.
    + solve_SF_internal body_Pile_count.
    + solve_SF_internal body_Pile_free.
  Qed.

author: anshumanmohan

repo: CertiGraph-VST


text:
Require Import Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability.
Require Import Undecidability.PCP.PCP_undec.
From Undecidability.FOL Require Import binZF_undec FOL.
From Undecidability.FOL.Sets Require Import binZF.
Require Import Undecidability.FOL.ZF.
Require Import Undecidability.FOL.Syntax.Core.
Require Import Undecidability.FOL.Syntax.BinSig.
Require Import Undecidability.FOL.Semantics.Tarski.FullFacts.
Require Import Undecidability.FOL.Deduction.FullNDFacts.

Lemma binZF_binFOL_valid :
  entailment_binZF ⪯ binFOL_valid.
Proof.
  exists (impl binZF). intros phi. unfold binFOL_valid, valid, entailment_binZF.
  setoid_rewrite impl_sat. reflexivity.
Qed.

Lemma binFOL_valid_undec :
  undecidable binFOL_valid.
Proof.
  apply (undecidability_from_reducibility undecidable_entailment_binZF), binZF_binFOL_valid.
Qed.

Lemma binZF_binFOL_prv_intu :
  deduction_binZF ⪯ binFOL_prv_intu.
Proof.
  exists (impl binZF). intros phi. unfold binFOL_prv_intu, deduction_binZF.
  setoid_rewrite <- impl_prv. rewrite List.app_nil_r.
  split; intros H; apply (Weak H); unfold List.incl; apply List.in_rev.
Qed.

Lemma binFOL_prv_intu_undec :
  undecidable binFOL_prv_intu.
Proof.
  apply (undecidability_from_reducibility undecidable_deduction_binZF), binZF_binFOL_prv_intu.
Qed.

author: uds-psl

repo: coq-library-undecidability


text:
(** Definition of algebras, homomorphisms, h-initiality, and related
    concepts for Two.
**)

Require Import HoTT.

Local Open Scope path_scope.
Local Open Scope fibration_scope.
Local Open Scope equiv_scope.

Section AssumeFunext.
Context `{Funext}.

(* Algebras. *)
Definition TwoAlg : Type := { C : Type &  C * C }.

(* Homomorphisms. *)
Definition TwoHom (X Y : TwoAlg) : Type
  := { h : X.1 -> Y.1 &
     (h (fst X.2) = fst Y.2) * (h (snd X.2) = snd Y.2) }.

(* Algebra 2-cells. *)
Definition Two2Cell (X Y : TwoAlg) (i j : TwoHom X Y) : Type
  := { a : forall (x : X.1), i.1 x = j.1 x &
     (a (fst X.2) = fst i.2 @ (fst j.2)^) *
     (a (snd X.2) = snd i.2 @ (snd j.2)^) }.

(* Algebra fibrations, also known as 'dependent algebras'. *)
Definition TwoAlgFib (X : TwoAlg) : Type
  := { E : X.1 -> Type & E (fst X.2) * E (snd X.2) }.

(* Algebra fibration maps, also known as 'dependent homomorphisms'. *)
Definition TwoAlgFibMap (X : TwoAlg) (Z : TwoAlgFib X) : Type
  := { h : forall (x : X.1), Z.1 x &
     (h (fst X.2) = fst Z.2) * (h (snd X.2) = snd Z.2) }.

(* Algebra fibration cells, a special kind of fibration maps. *)
Definition TwoAlgFibCell (X : TwoAlg) (Z : TwoAlgFib X) (k l : TwoAlgFibMap X Z) : Type
  := TwoAlgFibMap X (fun x : X.1 => k.1 x = l.1 x;
                    (fst k.2 @ (fst l.2)^, snd k.2 @ (snd l.2)^)).

(* H-initiality. *)
Definition twoHinit (X : TwoAlg) : Type
  := forall (Y : TwoAlg), Contr (TwoHom X Y).

(***********************************************************************)
(***********************************************************************)

(** We now show that for any fibration maps k and l, the existence
    of a path k = l implies the existence of a fibration cell between k and l,
    and vice versa.

    Remark: This correspondence can in fact be strengthened to an equivalence;
    however, the HoTT library does not yet have the tools to prove this
    in an elegant way.
*)

Theorem twoAlgFibMapPath_to_AlgFibCell (X : TwoAlg) (Z : TwoAlgFib X) (k l : TwoAlgFibMap X Z) :
  k = l -> TwoAlgFibCell X Z k l.
Proof.
intro p; induction p.
unfold TwoAlgFibCell.
unfold TwoAlgFibMap.
simpl.
split with (fun x => 1).
rewrite concat_pV.
rewrite concat_pV.
exact (1,1).
Defined.

Theorem twoAlgFibCell_to_AlgFibMapPath (X : TwoAlg) (Z : TwoAlgFib X) (k l : TwoAlgFibMap X Z) :
  TwoAlgFibCell X Z k l -> k = l.
Proof.
unfold TwoAlgFibCell.
unfold TwoAlgFibMap.
simpl.
intros [a [t_0 t_1]].
destruct k as [f [p_0 p_1]].
destruct l as [g [q_0 q_1]].
apply path_sigma_uncurried.
split with (path_forall _ _ a).
rewrite transport_prod.
apply path_prod'.

rewrite transport_paths_FlFr.
rewrite ap_Dapply_l.
rewrite apD10_path_forall.
rewrite ap_const.
rewrite t_0.
simpl.
rewrite inv_pV.
rewrite concat_p1.
apply concat_pV_p.

rewrite transport_paths_FlFr.
rewrite ap_Dapply_l.
rewrite apD10_path_forall.
rewrite ap_const.
rewrite t_1.
simpl.
rewrite inv_pV.
rewrite concat_p1.
apply concat_pV_p.
Defined.

(** As a special case, we show that for any homomorphisms i and j,
    the existence of a path i = j implies the existence of a 2-cell
    between i and j, and vice versa.

    This correspondence can likewise be strengthened to an equivalence.
*)
Theorem twoHomPath_to_2Cell (X Y : TwoAlg) (i j : TwoHom X Y) :
  i = j -> Two2Cell X Y i j.
Proof.
intro p.
set (Z := (fun _ => Y.1; Y.2) : TwoAlgFib X).
apply twoAlgFibMapPath_to_AlgFibCell with (Z := Z).
assumption.
Defined.

Theorem two2Cell_to_HomPath (X Y : TwoAlg) (i j : TwoHom X Y) :
  Two2Cell X Y i j -> i = j.
Proof.
intro c.
set (Z := (fun _ => Y.1; Y.2) : TwoAlgFib X).
apply twoAlgFibCell_to_AlgFibMapPath with (Z := Z).
assumption.
Defined.

(***********************************************************************)
(***********************************************************************)

(* H-initiality is an h-proposition. *)
Theorem twoHinit_is_hprop (X : TwoAlg) : IsHProp (twoHinit X).
Proof.
apply trunc_forall.
Defined.

End AssumeFunext.

author: ybertot

repo: hinitiality

save_path: github-repos/coq/ybertot-hinitiality