text:
(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Lia.

From Undecidability.Shared.Libs.DLW
  Require Import utils_tac utils_nat pos vec sss.

From Undecidability.MinskyMachines
  Require Import mm_defs.

From Undecidability.MuRec.Util
  Require Import recalg ra_mm.

Set Implicit Arguments.

Local Notation "'⟦' f '⟧'" := (@ra_rel _ f) (at level 0).

Local Notation "P // s -+> t" := (sss_progress (@mm_sss _) P s t).
Local Notation "P // s ->> t" := (sss_compute (@mm_sss _) P s t).
Local Notation "P // s ~~> t" := (sss_output (@mm_sss _) P s t).
Local Notation "P // s ↓"     := (sss_terminates (@mm_sss _) P s).

Theorem ra_mm_simulator n (f : recalg n) :
      { m & { P : list (mm_instr (pos (n+S m))) | forall v, ex (⟦f⟧ v) <-> (1,P) // (1,vec_app v vec_zero) ↓ } }.
Proof.
  destruct (ra_mm_compiler f) as (m & P & H1 & H2).
  exists m, P; split.
  + intros (x & Hx).
    exists (1+length P,vec_app v (x##vec_zero)); split; auto.
    simpl; lia.
  + intros H; apply H2; eq goal H; do 2 f_equal.
Qed.

Corollary ra_mm_simulator_0 (f : recalg 0) :
      { m & { P : list (mm_instr (pos (S m))) | ex (⟦f⟧ vec_nil) <-> (1,P) // (1,vec_zero) ↓ } }.
Proof.
  destruct (ra_mm_simulator f) as (m & P & HP).
  exists m, P; rewrite (HP vec_nil), vec_app_nil; tauto.
Qed.

author: uds-psl

repo: coq-library-undecidability


text:
Load LFindLoad.
Load LFindLoad.
From adtind Require Import goal56.

From lfind Require Import LFind.
Lemma lfind_state  (v:natural) (w:natural) (x:natural) (y:natural) (z:lst):@eq lst (drop (Succ v) (drop w (drop x (Cons y z))))
  (drop v (drop w (drop x z))).
Admitted.
From QuickChick Require Import QuickChick.
QCInclude "/home/yousef/lemmafinder/benchmark/_lfind_clam_lf_goal56_theorem0_35_lem/".
QCInclude ".".
Extract Constant defNumTests => "50".
Derive Show for natural.

              Derive Arbitrary for natural.

              Instance Dec_Eq_natural : Dec_Eq natural.

              Proof. dec_eq. Qed.
Derive Show for lst.

              Derive Arbitrary for lst.

              Instance Dec_Eq_lst : Dec_Eq lst.

              Proof. dec_eq. Qed.

Open Scope string_scope.

Parameter print : natural -> string -> natural.
Extract Constant print => "Extract.print".
Definition collect_data  (v:natural) (w:natural) (x:natural) (y:natural) (z:lst) :=
 let lfind_var := "v:" ++ "(" ++ show v ++ ")"++ "|" ++"w:" ++ "(" ++ show w ++ ")"++ "|" ++"x:" ++ "(" ++ show x ++ ")"++ "|" ++"y:" ++ "(" ++ show y ++ ")"++ "|" ++"z:" ++ "(" ++ show z ++ ")"
 in let lfind_v := print v lfind_var
 in lfind_state lfind_v  w x y z.
QuickChick collect_data.
Success.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
Require Import Category.Types.
Require Import Category.Setoids.
Require Import Category.Types_Setoids.
Require Import Category.RComonad.
Require Import Category.RComod.
Require Import Theory.Category.
Require Import Theory.Functor.
Require Import Theory.RelativeComonad.
Require Import Theory.PushforwardComodule.
Require Import Theory.Comodule.

Generalizable All Variables.

(*------------------------------------------------------------------------------
  -- ＣＡＴＥＧＯＲＹ  ＯＦ  ＳＴＲＥＡＭＳ
  ----------------------------------------------------------------------------*)
(** * Category of streams **)

(** ** Object and morphism definitions **)
Module Stream.

  Structure Obj : Type := mkObj
  { T         :>  𝑹𝑪𝒐𝒎𝒐𝒏𝒂𝒅 𝑬𝑸
  ; tail      :> [T] ⇒ [T] }.

  Arguments mkObj     {_ } _.
  Arguments T         _.
  Arguments tail      _.

  Notation "'Stream.make' ⦃ 'T' ≔ T ; 'tail' ≔ tail ⦄" :=
           (@mkObj T tail) (only parsing).

  Structure Morphism (T S : Obj) : Type := mkMorphism
  { τ           :> T ⇒ S
  ; τ_commutes  : ⟨τ⟩ ∘ τ⁎⋅T ≈ S ∘ ⟨τ⟩ }.

  Arguments mkMorphism  {_ _ _} _.
  Arguments τ           {_ _} _.
  Arguments τ_commutes  {_ _} _ _.

  Notation "'Stream.make' ⦃ 'τ' ≔ τ ⦄" := (@mkMorphism _ _ τ _) (only parsing).

  Program Definition Hom (T S : Obj) : Setoid :=
    Setoid.make   ⦃ Carrier  ≔ Morphism T S
                  ; Equiv    ≔ (λ g f ∙ g ≈ f) ⦄.
  (** equivalence **)
  Next Obligation.
    constructor.
    - repeat intro. now rewrite H.
    - repeat intro. symmetry; now rewrite H.
    - repeat intro; etransitivity; eauto. now apply H0.
  Qed.

End Stream.

Export Stream.

(** ** Identity and compositon definitions **)

Section Defs.

  Implicit Types (T S R U : Obj).

  Infix "⇒" := Hom.

  Program Definition id {T} : T ⇒ T :=
    Stream.make ⦃ τ ≔ id[T] ⦄.
  (** τ-cong **)
  Next Obligation.
    now rewrite H.
  Qed.

  Obligation Tactic := idtac.
  Program Definition compose {T S R} : [ S ⇒ R ⟶ T ⇒ S ⟶ T ⇒ R ] :=
    λ g f ↦₂ Stream.make ⦃ τ ≔ g ∘ f ⦄.
  (** τ-commutes **)
  Next Obligation.
    intros T S R g f.
    destruct g as [g g_commutes]. simpl in g_commutes.
    destruct f as [f f_commutes]. simpl in f_commutes. simpl.
    intros.
    rewrite H.
    etransitivity.
    eapply Setoids.cong.
    apply f_commutes.
    reflexivity.
    apply g_commutes.
    reflexivity.
  Qed.
  (** τ-proper **)
  Next Obligation.
    repeat intro.
    simpl.
    etransitivity. eapply Setoids.cong.
    eapply Setoids.cong. apply H1.
    etransitivity. eapply Setoids.cong.
    apply H0. reflexivity.
    apply H.
    reflexivity.
  Qed.

  Infix "∘" := compose.

  Lemma left_id : ∀ T S (f : T ⇒ S), id ∘ f ≈ f.
  Proof.
    intros. simpl. intros. rewrite H.
    reflexivity.
  Qed.

  Lemma right_id : ∀ T S (f : T ⇒ S), f ∘ id ≈ f.
  Proof.
    repeat intro. simpl. now rewrite H.
  Qed.

  Lemma compose_assoc T R S U (f : T ⇒ R) (g : R ⇒ S) (h : S ⇒ U) : h ∘ g ∘ f ≈ h ∘ (g ∘ f).
  Proof.
    repeat intro.
    simpl. now rewrite H.
  Qed.

  Canonical Structure 𝑺𝒕𝒓𝒆𝒂𝒎 : Category :=
    mkCategory left_id right_id compose_assoc.

End Defs.

author: verimath

repo: termination

save_path: github-repos/coq/verimath-termination


text:
Require Import VST.floyd.proofauto.
Require Import malloc_lemmas.
Require Import malloc_sep.
Require Import malloc.
Require Import spec_malloc.
Require Import linking.

Definition Gprog : funspecs := external_specs ++ private_specs.

Lemma body_free_large:  semax_body Vprog Gprog f_free_large free_large_spec.
Proof.
start_function.
forward_call( (offset_val (-(WA+WORD)) p), (s+WA+WORD) ). (*! munmap( p-(WASTE+WORD), s+WASTE+WORD ) !*)
+ entailer!. destruct p; try contradiction; simpl. normalize.
  rewrite Ptrofs.sub_add_opp. reflexivity.
+ (* munmap pre *)
  entailer!.
  sep_apply (free_large_chunk s p); try rep_omega.
  entailer!.
+ rep_omega.
+ entailer!.
Qed.

Definition module := [mk_body body_free_large].

author: PrincetonUniversity

repo: DeepSpecDB


text:
Inductive bool : Set :=
|true : bool
|false : bool.

Inductive False : Prop:=.

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

Inductive True : Prop :=
I : True.

(* Inductive eq (A: Type) (x : A) : A-> Prop:= *)
(* eq_refl : x = x :>A. *)

Definition not (A : Prop) := A-> False.

Notation "~ x" := (not x).

Theorem sample : 1 <> 2.
Proof.
  unfold not.
  intros.
  (* Error: No such hypothesis: H *)
  inversion H. Qed.

author: denjiry

repo: pgeneral

save_path: github-repos/coq/denjiry-pgeneral


text:
From iris.algebra Require Import auth agree excl gmap frac.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import invariants.
From iris.program_logic Require Import adequacy.
From stdpp Require Import gmap fin_maps fin_sets.
Require Import Eqdep_dec.
From cap_machine Require Import
     stdpp_extra iris_extra mkregion_helpers
     logrel_binary fundamental_binary linking malloc macros malloc_binary.
From cap_machine.examples Require Import
  disjoint_regions_tactics counter_binary_preamble_def counter_binary_preamble counter_binary_preamble_left.

Definition machine_component: Type := component nat _ _ Word.

Program Definition initial_state `{MachineParameters} (c: machine_component): cfg cap_lang :=
  match c with
  | Lib _ _ _ _ pre_comp => ([Seq (Instr Executable)], (∅, ∅)) (* dummy value *)
  | Main _ _ _ _ (ms, _, _) c_main => ([Seq (Instr Executable)], (<[PC := c_main]> (gset_to_gmap (WInt 0%Z) (list_to_set all_registers)), ms))
  end.

Definition can_address_only (w: Word) (addrs: gset Addr): Prop :=
  match w with
  | WInt _ => True
  | WSealable (SCap p b e _) =>
      forall a, (b <= a < e)%a -> a ∈ addrs
  | _ => False
  end.

Instance DisjointList_list_Addr : DisjointList (list Addr).
Proof. exact (@disjoint_list_default _ _ app []). Defined.

(* Definition mbkregion (r_start r_end: Addr) (contents: list Word) (contents_spec: list Word): gmap Addr (Word * Word) := *)
(*   list_to_map (zip (region_addrs r_start r_end) (zip contents contents_spec)). *)

(* Instance segment_union : Union (segment Word). *)
(* Proof. rewrite /segment. apply _. Qed. *)

Class memory_layout `{MachineParameters} := {
  (* counter example: preamble & body *)
  counter_region_start : Addr;
  counter_preamble_start : Addr;
  counter_body_start : Addr;
  counter_region_end : Addr;

  (* pointer to the linking table, at the beginning of the region *)
  counter_linking_ptr_size :
    (counter_region_start + 1)%a = Some counter_preamble_start;

  (* preamble code, that allocates the closure *)
  counter_preamble_size :
    (counter_preamble_start + counter_preamble_instrs_length)%a
    = Some counter_body_start;

  (* code of the body, wrapped in the closure allocated by the preamble *)
  counter_body_size :
    (counter_body_start + counter_left_instrs_length)%a (* we need to pad the entry points to mask the bounds, both counters will thus be of the largest possible size *)
    = Some counter_region_end;

  (* malloc routine *)
  malloc_start : Addr;
  malloc_memptr : Addr;
  malloc_mem_start : Addr;
  malloc_end : Addr;

  malloc_code_size :
    (malloc_start + length malloc_subroutine_instrs)%a
    = Some malloc_memptr;

  malloc_memptr_size :
    (malloc_memptr + 1)%a = Some malloc_mem_start;

  malloc_mem_size :
    (malloc_mem_start <= malloc_end)%a;

  (* link table *)
  link_table_start : Addr;
  link_table_end : Addr;

  link_table_size :
    (link_table_start + 1)%a = Some link_table_end;

  (* disjointness of all the regions above *)
  regions_disjoint :
    ## [
        finz.seq_between link_table_start link_table_end;
        finz.seq_between malloc_mem_start malloc_end;
        [malloc_memptr];
        finz.seq_between malloc_start malloc_memptr;
        finz.seq_between counter_body_start counter_region_end;
        finz.seq_between counter_preamble_start counter_body_start;
        [counter_region_start]
       ];
  }.

Definition initial_state_stk `{MachineParameters} (c: machine_component): cfg cap_lang :=
  match c with
  | Lib _ _ _ _ pre_comp => ([Seq (Instr Executable)], (∅, ∅)) (* dummy value *)
  | Main _ _ _ _ (ms, _, _) c_main => ([Seq (Instr Executable)], (<[PC := c_main]> (gset_to_gmap (WInt 0%Z) (list_to_set all_registers)), (ms : Mem)))
  end.

Definition offset_to_awkward `{memory_layout} : Z :=
  (* in this setup, the body of the counter comes just after the code
     of the preamble *)
  (counter_preamble_instrs_length - counter_preamble_move_offset)%Z.

Definition mk_initial_memory_left `{memory_layout} : gmap Addr Word :=
  (* pointer to the linking table *)
    list_to_map [(counter_region_start,
                  WCap RO link_table_start link_table_end link_table_start)]
  ∪ mkregion counter_preamble_start counter_body_start
       (* preamble: code that creates the awkward example closure *)
      (counter_left_preamble_instrs 0%Z (* offset to malloc in linking table *)
         offset_to_awkward (* offset to the body of the example *))
  ∪ mkregion counter_body_start counter_region_end
       (* body of the counter, that will be encapsulated in the closure
          created by the preamble *)
      (counter_left_instrs)

  (* ∪ mkregion adv_start adv_end *)
  (*     (* adversarial code: any code or data, but no capabilities (see condition below) except for malloc *) *)
  (*     (adv_val ++ [WCap E malloc_start malloc_end malloc_start]) *)
  ∪ mkregion malloc_start malloc_memptr
      (* code for the malloc subroutine *)
      malloc_subroutine_instrs
  ∪ list_to_map
      (* Capability to malloc's memory pool, used by the malloc subroutine *)
      [(malloc_memptr, WCap RWX malloc_memptr malloc_end malloc_mem_start)]
  ∪ mkregion malloc_mem_start malloc_end
      (* Malloc's memory pool, initialized to zero *)
      (region_addrs_zeroes malloc_mem_start malloc_end)
  ∪ mkregion link_table_start link_table_end
      (* link table, with pointers to the malloc subroutines *)
      [WCap E malloc_start malloc_end malloc_start]
.

Definition mk_initial_memory_right `{memory_layout} : gmap Addr Word :=
  (* pointer to the linking table *)
    list_to_map [(counter_region_start,
                  WCap RO link_table_start link_table_end link_table_start)]
  ∪ mkregion counter_preamble_start counter_body_start
       (* preamble: code that creates the awkward example closure *)
      (counter_left_preamble_instrs 0%Z (* offset to malloc in linking table *)
         offset_to_awkward (* offset to the body of the example *))
  ∪ mkregion counter_body_start counter_region_end
       (* body of the counter, that will be encapsulated in the closure
          created by the preamble *)
      (counter_right_instrs)

  (* ∪ mkregion adv_start adv_end *)
  (*     (* adversarial code: any code or data, but no capabilities (see condition below) except for malloc *) *)
  (*     (adv_val ++ [WCap E malloc_start malloc_end malloc_start]) *)
  ∪ mkregion malloc_start malloc_memptr
      (* code for the malloc subroutine *)
      malloc_subroutine_instrs
  ∪ list_to_map
      (* Capability to malloc's memory pool, used by the malloc subroutine *)
      [(malloc_memptr, WCap RWX malloc_memptr malloc_end malloc_mem_start)]
  ∪ mkregion malloc_mem_start malloc_end
      (* Malloc's memory pool, initialized to zero *)
      (region_addrs_zeroes malloc_mem_start malloc_end)
  ∪ mkregion link_table_start link_table_end
      (* link table, with pointers to the malloc subroutines *)
      [WCap E malloc_start malloc_end malloc_start]
.

Definition comp1 `{memory_layout} : machine_component :=
  Lib _ _ _ _ (mk_initial_memory_left, ∅, {[ 0 := WSealable (SCap E counter_region_start counter_region_end counter_preamble_start) ]}).

Definition comp2 `{memory_layout} : machine_component :=
  Lib _ _ _ _ (mk_initial_memory_right, ∅, {[ 0 := WSealable (SCap E counter_region_start counter_region_end counter_preamble_start) ]}).

Definition code_all_ints (ms : segment Word) :=
  ∀ a w, ms !! a = Some w → is_z w = true.

Definition is_initial_context (c : machine_component) :=
  match c with
  | Lib _ _ _ _ (pre_ms,_,_) => code_all_ints pre_ms
  | Main _ _ _ _ (pre_ms,i,e) c_main => code_all_ints pre_ms ∧ (∃ p b e a, c_main = WSealable (SCap p b e a) ∧
                                                                   (p = RX ∨ p = RWX))
                                       ∧ (∃ a, {[(0,a)]} = i) ∧ e = ∅
  (* extra assumptions on adv imports and exports that make the proof easier to go through *)
  end.

Definition is_machine_program `{memory_layout} (c : machine_component) :=
  is_program _ _ _ _ can_address_only isCorrectPC c.
Definition is_machine_context `{memory_layout} (c comp p : machine_component) :=
  is_context _ _ _ _ can_address_only isCorrectPC c comp p.

Lemma initial_registers_full_map `{MachineParameters, memory_layout} (c : machine_component) reg :
  is_machine_program c →
  (initial_state_stk c).2.1 = reg →
  (∀ r, is_Some (reg !! r)).
Proof.
  intros Hprog Hini.
  inv Hprog.
  intros r.
  destruct (decide (r = PC)) as [->|]. by eauto.
  rewrite lookup_insert_ne//.
  pose proof (all_registers_s_correct r) as Hin. clear -Hin.
  apply elem_of_dom. eauto.
Qed.

Definition ms_of (c : machine_component) : Mem :=
  match c with
  | Lib _ _ _ _ (ms,_,_) => ms
  | Main _ _ _ _ (ms, _, _) _ => ms
  end.

Definition main_of (c : machine_component) : Word :=
  match c with
  | Lib _ _ _ _ (_,_,_) => WInt 0%Z
  | Main _ _ _ _ (_,_,_) c_main => c_main
  end.

(* Instance merge_diagnone : DiagNone (λ o1 o2 : option Word, match o1 with *)
(*                                   | Some _ => o1 *)
(*                                   | None => o2 *)
(*                                                            end). *)
(* Proof. *)
(*   rewrite /DiagNone //. *)
(* Qed. *)

(* Instance merge_LeftId : LeftId eq None (λ o1 o2 : option Word, match o1 with *)
(*                                         | Some _ => o1 *)
(*                                         | None => o2 *)
(*                                                                end). *)
(* Proof. rewrite /LeftId //. Qed. *)
(* Instance addr_semiset : SemiSet Addr (list Addr). *)
(* Proof. apply listset_simple_set. *)

Lemma regions_disjoint_eq `{MachineParameters, memory_layout} c_adv p1 p2 (mem mem' : Mem) (reg reg' : Reg) :
  is_machine_context c_adv comp1 p1 →
  is_machine_context c_adv comp2 p2 →
  is_initial_context c_adv →
  mem = (initial_state_stk p1).2.2 →
  mem' = (initial_state_stk p2).2.2 →
  reg = (initial_state_stk p1).2.1 →
  reg' = (initial_state_stk p2).2.1 →

  ∃ (resolved_ms : gmap Addr Word), mem = mk_initial_memory_left ∪ resolved_ms
                 ∧ mem' = mk_initial_memory_right ∪ resolved_ms
                 ∧ can_address_only (main_of c_adv) (dom (resolved_ms))
  ∧ (∀ a w, resolved_ms !! a = Some w → (is_z w = true
                                         ∨ w = WSealable (SCap E counter_region_start counter_region_end counter_preamble_start)))
  ∧ reg = reg'
  ∧ (∃ c_main, reg = <[PC := c_main]> (gset_to_gmap (WInt 0%Z) (list_to_set all_registers)) ∧ can_address_only c_main (dom resolved_ms) ∧ isCorrectPC c_main)
  ∧ mk_initial_memory_left ##ₘresolved_ms
  ∧ mk_initial_memory_right ##ₘresolved_ms
.
Proof.
  intros Hp1 Hp2 Hinit Hmem Hmem'.
  subst mem mem'. rewrite /comp1 in Hp1. rewrite /comp2 in Hp2.
  inv Hp1. inv Hp2. destruct His_program as [Hlink His_program].
  destruct His_program0 as [Hlink0 His_program0].
  inv His_program. inv His_program0. inv Hlink. inv Hlink0.
  revert ms ms0 Hwfcomp Hwfcomp0 Hlink Hlink1. rewrite /segment. intros.
  inv Hwfcomp. inv Hwf_pre. inv Hwfcomp0. inv Hwf_pre. simpl in *.
  rename Hw_main into Hcanaddress.
  rename Hw_main0 into Hcanaddress0.
  destruct comp3,p. revert s Hinit Hlink Hlink1 Hwf_l Hwf_l0. rewrite /segment. intros.
  destruct Hinit as [Hints [Hw_main [ [a Hin] He] ] ]. subst e i.
  destruct Hw_main as (p&b&e&a_main&->&?).
  simpl in *.

  inversion Hlink1. subst ms1 imp1 exp1 ms2 imp2 exp2 ms3 imp exp3.
  inversion Hlink. subst ms1 imp1 exp1 ms2 imp2 exp2 ms3 imp exp3.
  rewrite /resolve_imports /set_fold /= elements_empty elements_singleton /= in Hms.
  rewrite /resolve_imports /set_fold /= elements_empty elements_singleton /= in Hms0.
  assert (exp !! 0 = Some (WSealable (SCap E counter_region_start counter_region_end counter_preamble_start))) as Hin0.
  { rewrite Hexp1. rewrite lookup_merge lookup_empty. eauto. }
  assert (exp0 !! 0 = Some (WSealable (SCap E counter_region_start counter_region_end counter_preamble_start))) as Hin1.
  { rewrite Hexp2. rewrite lookup_merge lookup_empty. eauto. }
  rewrite Hin0 in Hms. subst ms.
  rewrite Hin1 in Hms0. subst ms0.
  erewrite fin_maps.LeftId_instance_0 in Hexp2. subst exp0.
  2: { unfold LeftId. auto. }
  erewrite fin_maps.LeftId_instance_0 in Hexp1. subst exp. clear Hin1.
  2: { unfold LeftId. auto. }
  inv Hwf_l. inv Hwf_r.
  inv Hwf_l0. inv Hwf_r0.
  inv Hwf_pre. inv Hwf_pre0. inv Hwf_pre1. inv Hwf_pre2.

  assert (<[a:=WSealable (SCap E counter_region_start counter_region_end counter_preamble_start)]> s ##ₘ mk_initial_memory_left)
    as Hdisj_ms2.
  { apply map_disjoint_alt. intros a'.
    destruct ((<[a:=WSealable (SCap E counter_region_start counter_region_end counter_preamble_start)]> s) !! a') eqn:Hsome;auto. right.
    destruct (decide (a = a')).
    { subst a. destruct Himp3 with 0 a';[apply elem_of_singleton;auto|].
      apply eq_None_not_Some. intros Hcontr. apply Hms_disj in Hcontr;eauto. }
    rewrite lookup_insert_ne// in Hsome.
    apply eq_None_not_Some. intros Hcontr. apply Hms_disj in Hcontr;eauto. }
  assert (<[a:=WSealable (SCap E counter_region_start counter_region_end counter_preamble_start)]> s ##ₘ mk_initial_memory_right)
    as Hdisj_ms3.
  { apply map_disjoint_alt. intros a'.
    destruct ((<[a:=WSealable (SCap E counter_region_start counter_region_end counter_preamble_start)]> s) !! a') eqn:Hsome;auto. right.
    destruct (decide (a = a')).
    { subst a. destruct Himp5 with 0 a';[apply elem_of_singleton;auto|].
      apply eq_None_not_Some. intros Hcontr. apply Hms_disj0 in Hcontr;eauto. }
    rewrite lookup_insert_ne// in Hsome.
    apply eq_None_not_Some. intros Hcontr. apply Hms_disj0 in Hcontr;eauto. }

  pose proof regions_disjoint as Hdisjoint.
  repeat (rewrite disjoint_list_cons in Hdisjoint |- *; destruct Hdisjoint as (? & Hdisjoint)).

  exists (<[a:=WSealable (SCap E counter_region_start counter_region_end counter_preamble_start)]> s : Mem).
  split;[|split;[|split;[|split;[|split;[|split] ] ] ] ].
  - rewrite map_union_comm//.
    assert (map_union s mk_initial_memory_left = (s ∪ mk_initial_memory_left))
      as ->;auto.

    erewrite insert_union_l. auto.
    (* annoying type class stuff... *)
    Unshelve.  all: unfold segment; simpl; try apply _.
    apply gmap_fmap.
    apply gmap_omap.
    apply gmap_finmap.
  - rewrite map_union_comm//.
    assert (map_union s mk_initial_memory_right = (s ∪ mk_initial_memory_right))
      as ->;auto.

    erewrite insert_union_l. auto.
    (* annoying type class stuff... *)
    Unshelve. all: unfold segment;simpl; try apply _.
    apply gmap_fmap.
    apply gmap_omap.
    apply gmap_finmap.
  - clear -H2 Hw_main Hw_main_addr1. simpl in *.
    destruct H2 as [-> | ->].
    intros. rewrite dom_insert_L. apply elem_of_union_r. auto.
    intros. rewrite dom_insert_L. apply elem_of_union_r. auto.
  - intros. destruct (decide (a = a0)).
    + subst. rewrite lookup_insert in H10. inv H10. auto.
    + rewrite lookup_insert_ne// in H10. apply Hints in H10. auto.
  - auto.
  - exists (WCap p b e a_main). split;auto. clear -Hw_main Hw_main_addr1. simpl in *.
    split;auto. intros a' Ha'. apply Hw_main_addr1 in Ha'. rewrite dom_insert_L. set_solver.
  - auto.
Qed.

Section Adequacy.
  Context (Σ: gFunctors).
  Context {inv_preg: invGpreS Σ}.
  Context {mem_preg: gen_heapGpreS Addr Word Σ}.
  Context {reg_preg: gen_heapGpreS RegName Word Σ}.
  Context {seal_store_preg: sealStorePreG Σ}.
  Context {na_invg: na_invG Σ}.
  Context `{MP: MachineParameters}.

  Lemma regspec_mapsto_alloc {cfg: cfgSG Σ} e (σ : gmap RegName Word * gmap Addr Word) r (w : Word) :
    σ.1 !! r = None →
    spec_res e σ ==∗ spec_res e (<[r:=w]> σ.1,σ.2) ∗ r ↣ᵣ w.
  Proof.
    iIntros (Hnone) "Hσ".
    rewrite /spec_res /regspec_mapsto.
    iMod (own_update with "Hσ") as "[Hσ Hr]".
    { eapply auth_update_alloc,prod_local_update_2,prod_local_update_1.
      eapply (alloc_singleton_local_update (to_spec_map σ.1) r (1%Qp, to_agree w)).
      by rewrite lookup_fmap Hnone. done. }
    iModIntro. iFrame "Hr". rewrite -fmap_insert. iFrame.
  Qed.
  Lemma memspec_mapsto_alloc {cfg: cfgSG Σ} e (σ : gmap RegName Word * gmap Addr Word) a (w : Word) :
    σ.2 !! a = None →
    spec_res e σ ==∗ spec_res e (σ.1,<[a:=w]> σ.2) ∗ a ↣ₐ w.
  Proof.
    iIntros (Hnone) "Hσ".
    rewrite /spec_res /memspec_mapsto.
    iMod (own_update with "Hσ") as "[Hσ Hr]".
    { eapply auth_update_alloc,prod_local_update_2,prod_local_update_2.
      eapply (alloc_singleton_local_update (to_spec_map σ.2) a (1%Qp, to_agree w)).
      by rewrite lookup_fmap Hnone. done. }
    iModIntro. iFrame "Hr". rewrite -fmap_insert. iFrame.
  Qed.
  Lemma regspec_alloc_big {cfg: cfgSG Σ} e σ σ' σs :
    σ' ##ₘ σ →
    spec_res e (σ,σs) ==∗
    spec_res e (σ' ∪ σ,σs) ∗ ([∗ map] l ↦ v ∈ σ', l ↣ᵣ v).
  Proof.
    revert σ; induction σ' as [| l v σ' Hl IH] using map_ind; iIntros (σ Hdisj) "Hσ".
    { rewrite left_id_L. auto. }
    iMod (IH with "Hσ") as "[Hσ'σ Hσ']"; first by eapply map_disjoint_insert_l.
    decompose_map_disjoint.
    rewrite !big_opM_insert // -insert_union_l //.
    iMod (regspec_mapsto_alloc with "Hσ'σ") as "($ & $)".
      by apply lookup_union_None. done.
  Qed.
  Lemma memspec_alloc_big {cfg: cfgSG Σ} e σ σ' σr :
    σ' ##ₘ σ →
    spec_res e (σr, σ) ==∗
    spec_res e (σr, map_union σ' σ) ∗ ([∗ map] l ↦ v ∈ σ', l ↣ₐ v).
  Proof.
    revert σ; induction σ' as [| l v σ' Hl IH] using map_ind; iIntros (σ Hdisj) "Hσ".
    { rewrite left_id_L. auto. }
    iMod (IH with "Hσ") as "[Hσ'σ Hσ']"; first by eapply map_disjoint_insert_l.
    decompose_map_disjoint.
    rewrite !big_opM_insert //.
    assert (map_union (<[l:=v]> σ') σ = <[l:=v]> (map_union σ' σ)) as ->.
    { rewrite insert_union_l. auto. }
    iMod (memspec_mapsto_alloc with "Hσ'σ") as "($ & $)".
    simpl. rewrite lookup_union_None//. done.
  Qed.

  Instance list_addr_semiset : SemiSet Addr (list Addr).
  Proof.
    apply Build_SemiSet.
    - intros. intros Hcontr. inversion Hcontr.
    - intros. split;intros.
      inversion H;subst;auto. inversion H2.
      rewrite /singleton /Singleton_list. apply elem_of_list_singleton. auto.
    - intros. split;intros.
      rewrite /union /Union_list in H.
      apply elem_of_app in H. auto.
      rewrite /union /Union_list.
      apply elem_of_app. auto.
  Qed.

  Lemma establish_interp `{memG Σ,regG Σ,cfgSG Σ,logrel_na_invs Σ} ms v :
    (∀ a w, ms !! a = Some w → (is_z w = true ∨ w = v)) ->
    interp (v,v) -∗
    ([∗ map] k↦x ∈ ms, k ↦ₐ x ∗ k ↣ₐ x) ={⊤}=∗ ([∗ map] k↦x ∈ ms, inv (logN .@ k) (∃ x1 x2, k ↦ₐ x1 ∗ k ↣ₐ x2 ∗ interp(x1,x2))).
  Proof.
    iIntros (Hcond) "#Hv".
    iInduction (ms) as [] "IH" using map_ind.
    { rewrite !big_sepM_empty. done. }
    { rewrite !big_sepM_insert//.
      iIntros "[[Hi Hsi] Hmap]".
      iDestruct ("IH" with "[] Hmap") as ">Hmap".
      { iPureIntro. intros a w Hin. apply Hcond with a.
        rewrite lookup_insert_ne. auto. intros Hcontr;subst. rewrite H3 in Hin. done. }
      iFrame.
      specialize Hcond with i x.
      rewrite lookup_insert in Hcond.
      destruct Hcond as [Hint | Heq];auto.
      - iApply inv_alloc. iNext. iExists x,x. iFrame.
        iApply fixpoint_interp1_eq.
        destruct x;[|destruct sb;inv Hint|inv Hint].
        iSimpl. auto.
      - subst x.
        iApply inv_alloc.
        iNext. iExists v,v. iFrame "∗ #".
    }
  Qed.

  Context {cfgg : inG Σ (authR cfgUR)}.

  Definition codeN : namespace := nroot .@ "conf" .@ "code".

  Lemma confidentiality_adequacy_l' {ML:memory_layout} c_adv p1 p2 (es: list cap_lang.expr)
        reg' m' :
    is_machine_context c_adv comp1 p1 →
    is_machine_context c_adv comp2 p2 →
    is_initial_context c_adv →
    rtc erased_step (initial_state_stk p1) (of_val HaltedV :: es, (reg', m')) →
    (∃ es' conf', rtc erased_step (initial_state_stk p2) (of_val HaltedV :: es', conf')).
  Proof.
    intros Hm1 Hm2 Hc Hstep.
    set (reg1 := (initial_state_stk p1).2.1).
    set (m1 := (initial_state_stk p1).2.2).
    set (reg2 := (initial_state_stk p2).2.1).
    set (m2 := (initial_state_stk p2).2.2).
    cut (@adequate cap_lang NotStuck (Seq (Instr Executable)) (reg1,m1)
                   (λ v _, v = HaltedV → ∃ thp' conf', rtc erased_step (initial_state_stk p2)
                                             (of_val HaltedV :: thp', conf'))).
    { destruct 1. inv Hm1. destruct His_program as [Hlink Hprog]. inv Hprog.
      apply adequate_result in Hstep. auto. auto. }
    eapply (wp_adequacy Σ _); iIntros (Hinv ?).

    iMod (gen_heap_init (m1:Mem)) as (mem_heapg) "(Hmem_ctx & Hmem & _)".
    iMod (gen_heap_init (reg1:Reg)) as (reg_heapg) "(Hreg_ctx & Hreg & _)".
    iMod (seal_store_init) as (seal_storeg) "Hseal_store".
    iMod (@na_alloc Σ na_invg) as (logrel_nais) "Hna".

    iMod (own_alloc (● (Excl' (Seq (Instr Executable)) : optionUR (exclR (leibnizO expr)), (∅,∅))
                       ⋅ ◯ ((Excl' (Seq (Instr Executable)) : optionUR (exclR (leibnizO expr)), (∅,∅)) : cfgUR)))
      as (γc) "[Hcfg1 Hcfg2]".
    { apply auth_both_valid_discrete. split=>//. }

    pose memg := MemG Σ Hinv mem_heapg.
    pose regg := RegG Σ Hinv reg_heapg.
    pose logrel_na_invs := Build_logrel_na_invs _ na_invg logrel_nais.
    set (Hcfg := CFGSG _ _ γc).

    iMod (regspec_alloc_big _ ∅ reg2 ∅ with "[Hcfg1]") as "(Hcfg1 & Hregspec)".
      by apply map_disjoint_empty_r. rewrite /spec_res /= !/to_spec_map !fmap_empty //.
    rewrite right_id_L.
    iMod (memspec_alloc_big _ ∅ m2 reg2 with "[Hcfg1]") as "(Hcfg1 & Hmemspec)".
      by apply map_disjoint_empty_r. rewrite /spec_res /= !/to_spec_map !fmap_empty //.
    rewrite right_id_L.

    pose proof (
      @counter_binary_preamble.counter_preamble_spec Σ memg regg logrel_na_invs Hcfg
      ) as Spec.

    pose proof (regions_disjoint_eq c_adv p1 p2 m1 m2 reg1 reg2 Hm1 Hm2 Hc eq_refl eq_refl eq_refl eq_refl)
      as [resolved_ms [Hm1eq [Hm2eq [Hcan_address_to_main [Hresolved_ms_spec [Heqreg [Hreg [Hdisj Hdisj'] ] ] ] ] ] ] ].

    rewrite {2}Hm1eq.
    rewrite {2}Hm2eq.

    iDestruct (big_sepM_union with "Hmem") as "[Hmem Hadv]";[auto|].
    iDestruct (big_sepM_union with "Hmemspec") as "[Hmemspec Hadvspec]";[auto|].

    pose proof regions_disjoint as Hdisjoint.
    rewrite disjoint_list_cons in Hdisjoint |- *. destruct Hdisjoint as (Hdisj_link_table & Hdisjoint).
    rewrite /mk_initial_memory_left /mk_initial_memory_right.

    iDestruct (big_sepM_union with "Hmem") as "[Hmem Hlink_table]".
    { disjoint_map_to_list. set_solver+ Hdisj_link_table. }
    iDestruct (big_sepM_union with "Hmemspec") as "[Hmemspec Hlink_table_spec]".
    { disjoint_map_to_list. set_solver+ Hdisj_link_table. }

    rewrite disjoint_list_cons in Hdisjoint |- *. destruct Hdisjoint as (Hdisj_malloc_mem & Hdisjoint).
    iDestruct (big_sepM_union with "Hmem") as "[Hmem Hmalloc_mem]".
    { disjoint_map_to_list. set_solver +Hdisj_malloc_mem. }
    iDestruct (big_sepM_union with "Hmemspec") as "[Hmemspec Hmalloc_mem_spec]".
    { disjoint_map_to_list. set_solver +Hdisj_malloc_mem. }

    rewrite disjoint_list_cons in Hdisjoint |- *. destruct Hdisjoint as (Hdisj_malloc_memptr & Hdisjoint).
    iDestruct (big_sepM_union with "Hmem") as "[Hmem Hmalloc_memptr]".
    { disjoint_map_to_list. set_solver +Hdisj_malloc_memptr. }
    iDestruct (big_sepM_union with "Hmemspec") as "[Hmemspec Hmalloc_memptr_spec]".
    { disjoint_map_to_list. set_solver +Hdisj_malloc_memptr. }

    iDestruct (big_sepM_insert with "Hmalloc_memptr") as "[Hmalloc_memptr _]".
    by apply lookup_empty. cbn [fst snd].
    iDestruct (big_sepM_insert with "Hmalloc_memptr_spec") as "[Hmalloc_memptr_spec _]".
    by apply lookup_empty. cbn [fst snd].

    rewrite disjoint_list_cons in Hdisjoint |- *. destruct Hdisjoint as (Hdisj_malloc_code & Hdisjoint).
    iDestruct (big_sepM_union with "Hmem") as "[Hmem Hmalloc_code]".
    { disjoint_map_to_list. set_solver +Hdisj_malloc_code. }
    iDestruct (big_sepM_union with "Hmemspec") as "[Hmemspec Hmalloc_code_spec]".
    { disjoint_map_to_list. set_solver +Hdisj_malloc_code. }

    rewrite disjoint_list_cons in Hdisjoint |- *. destruct Hdisjoint as (Hdisj_counter_body & Hdisjoint).
    iDestruct (big_sepM_union with "Hmem") as "[Hmem Hcounter_body]".
    { disjoint_map_to_list. set_solver +Hdisj_counter_body. }
    iDestruct (big_sepM_union with "Hmemspec") as "[Hmemspec Hcounter_body_spec]".
    { disjoint_map_to_list. set_solver +Hdisj_counter_body. }

    rewrite disjoint_list_cons in Hdisjoint |- *. destruct Hdisjoint as (Hdisj_counter_preamble & _).
    iDestruct (big_sepM_union with "Hmem") as "[Hcounter_link Hcounter_preamble]".
    { disjoint_map_to_list. set_solver +Hdisj_counter_preamble. }
    iDestruct (big_sepM_union with "Hmemspec") as "[Hcounter_link_spec Hcounter_preamble_spec]".
    { disjoint_map_to_list. set_solver +Hdisj_counter_preamble. }

    iDestruct (big_sepM_insert with "Hcounter_link") as "[Hcounter_link _]". by apply lookup_empty.
    iDestruct (big_sepM_insert with "Hcounter_link_spec") as "[Hcounter_link_spec _]". by apply lookup_empty.
    cbn [fst snd].

    clear Hdisj_link_table Hdisj_malloc_mem
      Hdisj_malloc_memptr Hdisj_malloc_code Hdisj_counter_body Hdisj_counter_preamble.

    (* Massage points-to into sepL2s with permission-pointsto *)

    iDestruct (mkregion_prepare with "[$Hlink_table]") as ">Hlink_table". by apply link_table_size.
    iDestruct (mkregion_prepare with "[$Hmalloc_mem]") as ">Hmalloc_mem".
    { rewrite replicate_length /finz.dist. clear.
      generalize malloc_mem_start malloc_end malloc_mem_size. solve_addr. }
    iDestruct (mkregion_prepare with "[$Hmalloc_code]") as ">Hmalloc_code".
      by apply malloc_code_size.
    iDestruct (mkregion_prepare with "[$Hcounter_preamble]") as ">Hcounter_preamble".
      by apply counter_preamble_size.
    iDestruct (mkregion_prepare with "[$Hcounter_body]") as ">Hcounter_body". by apply counter_body_size.
    iDestruct (mkregion_prepare_spec with "[$Hlink_table_spec]") as ">Hlink_table_spec". by apply link_table_size.
    iDestruct (mkregion_prepare_spec with "[$Hmalloc_mem_spec]") as ">Hmalloc_mem_spec".
    { rewrite replicate_length /finz.dist. clear.
      generalize malloc_mem_start malloc_end malloc_mem_size. solve_addr. }
    iDestruct (mkregion_prepare_spec with "[$Hmalloc_code_spec]") as ">Hmalloc_code_spec".
      by apply malloc_code_size.
    iDestruct (mkregion_prepare_spec with "[$Hcounter_preamble_spec]") as ">Hcounter_preamble_spec".
      by apply counter_preamble_size.
    iDestruct (mkregion_prepare_spec with "[$Hcounter_body_spec]") as ">Hcounter_body_spec". by apply counter_body_size.

    rewrite -/(counter_left _) -/(counter_left_preamble _ _ _).
    rewrite -/(counter_right _) -/(counter_right_preamble _ _ _).

    (* Allocate the spec invariant *)
    iMod (inv_alloc specN _ (spec_inv ([Seq (Instr Executable)],(reg2,m2)) ) with "[Hcfg1]") as "#Hspec_∅".
    { iNext. iExists _,_. iFrame. iPureIntro. rewrite /reg2 /m2 /=. left. }
    iAssert (spec_ctx)%I as "#Hspec".
    { iExists _. iFrame "#". }

    (* Split the link table *)
    rewrite (finz_seq_between_cons link_table_start link_table_end).
    2: { generalize link_table_size; clear; solve_addr. }
    rewrite (_: (link_table_start ^+ 1)%a = link_table_end).
    2: { generalize link_table_size; clear.
         generalize link_table_start link_table_end. solve_addr. }
    iDestruct (big_sepL2_cons with "Hlink_table") as "[Hlink1 _]".
    iDestruct (big_sepL2_cons with "Hlink_table_spec") as "[Hlink1' _]".

    (* Allocate malloc invariant *)
    iMod (na_inv_alloc logrel_nais ⊤ mallocN (malloc_inv_binary malloc_start malloc_end)
            with "[Hmalloc_code Hmalloc_memptr Hmalloc_mem Hmalloc_code_spec Hmalloc_memptr_spec Hmalloc_mem_spec]") as "#Hinv_malloc".
    { iNext. unfold malloc_inv_binary. iExists _,_. iFrame.
      iPureIntro. generalize malloc_code_size malloc_mem_size malloc_memptr_size. cbn.
      clear; unfold malloc_subroutine_instrs_length; intros; repeat split; solve_addr. }

    (* Facts about layout *)
    assert (isCorrectPC_range RX counter_region_start counter_region_end
              counter_preamble_start counter_body_start).
    { intros a [Ha1 Ha2]. constructor; auto.
      generalize counter_linking_ptr_size counter_preamble_size counter_body_size. revert Ha1 Ha2. clear.
      unfold counter_left_instrs_length, counter_preamble_instrs_length. solve_addr. }
    set counter_preamble_move_addr := (counter_preamble_start ^+ counter_preamble_move_offset)%a.
    assert ((counter_preamble_start + counter_preamble_move_offset)%a = Some counter_preamble_move_addr).
    { clear. subst counter_preamble_move_addr.
      generalize counter_preamble_size.
      unfold counter_preamble_instrs_length, counter_preamble_move_offset.
      generalize counter_preamble_start counter_body_start. solve_addr. }
    assert (counter_preamble_move_addr + offset_to_awkward = Some counter_body_start)%a.
    { generalize counter_preamble_size.
      unfold counter_preamble_move_addr, offset_to_awkward, counter_preamble_instrs_length.
      unfold counter_preamble_move_offset. clear.
      generalize counter_preamble_start counter_body_start. solve_addr. }
    assert (isCorrectPC_range RX counter_region_start counter_region_end
              counter_body_start counter_region_end).
    { intros a [Ha1 Ha2]. constructor; auto.
      generalize counter_linking_ptr_size counter_preamble_size counter_body_size. revert Ha1 Ha2; clear.
      unfold counter_left_instrs_length, counter_preamble_instrs_length. solve_addr. }

    (* Extract validity of library *)
    iMod (Spec with "[$Hspec $Hinv_malloc $Hcounter_preamble $Hcounter_body
                    $Hcounter_preamble_spec $Hcounter_body_spec $Hcounter_link $Hcounter_link_spec $Hlink1 $Hlink1']") as "#Hlib".
    apply H. apply H.
    { apply contiguous_between_region_addrs. generalize counter_preamble_size; clear.
      unfold counter_preamble_instrs_length. solve_addr. }
    { apply contiguous_between_region_addrs. generalize counter_preamble_size; clear.
      unfold counter_preamble_instrs_length. solve_addr. }
    { apply le_addr_withinBounds. clear; solve_addr.
      generalize link_table_size; clear; solve_addr. }
    { generalize link_table_start; clear; solve_addr. }
    { apply le_addr_withinBounds. solve_addr.
      generalize link_table_start link_table_end link_table_size. clear; solve_addr. }
    { generalize link_table_start; clear; solve_addr. }
    { eassumption. }
    { eassumption. }
    { apply H2. }
    { apply contiguous_between_region_addrs. generalize counter_body_size; clear.
      unfold counter_left_instrs_length. solve_addr. }
    { eassumption. }
    { eassumption. }
    { apply H2. }
    { apply contiguous_between_region_addrs. generalize counter_body_size; clear.
      unfold counter_left_instrs_length. solve_addr. }
    { auto. }

    (* Validity of the adv region *)
    iDestruct (big_sepM_sep with "[$Hadv $Hadvspec]") as "Hadv".
    iMod (establish_interp with "Hlib Hadv") as "#Hadvvalid"; [auto|].

    (* Validity of Main *)
    rewrite -Heqreg.
    destruct Hreg as [c_main [Hreg1 [Hcanaddress Hcorrect] ] ].
    inversion Hcorrect as [p b e a Hbounds Hp Heq].
    iAssert (interp (WCap p b e a,WCap p b e a)) as "#Hval".
    { clear -Hcanaddress Hbounds Hp Heq.
      subst c_main. simpl in Hcanaddress.
      iApply fixpoint_interp1_eq.
      destruct Hp as [-> | ->];simpl.
      - iSplit;auto.
        iApply big_sepL_forall.
        iIntros (k x Hin).
        apply elem_of_list_lookup_2 in Hin.
        apply elem_of_finz_seq_between in Hin. apply Hcanaddress in Hin.
        apply elem_of_dom in Hin as [? ?].
        iExists interp. iSplit;auto.
        iDestruct (big_sepM_lookup with "Hadvvalid") as "$".
        eauto.
      - iSplit;auto.
        iApply big_sepL_forall.
        iIntros (k x Hin).
        apply elem_of_list_lookup_2 in Hin.
        apply elem_of_finz_seq_between in Hin. apply Hcanaddress in Hin.
        apply elem_of_dom in Hin as [? ?].
        iExists interp. iSplit;auto.
        iDestruct (big_sepM_lookup with "Hadvvalid") as "$".
        eauto.
    }

    iDestruct (fundamental_binary (reg1,reg1) with "[Hspec] Hval") as "Hval_exec".
    { iExact "Hspec". }

    unfold interp_expression. iSimpl in "Hval_exec".
    iDestruct ("Hval_exec" with "[Hreg Hregspec Hcfg2 $Hna]") as "[_ Hconf]".
    { iSplitR;[|iSplitL "Hreg";[|iSplitL "Hregspec"] ];[..|iExact "Hcfg2"].
      - iSplit.
        + iPureIntro. intros x. simpl.
          rewrite Hreg1;clear.
          destruct (decide (x = PC));[subst;rewrite lookup_insert;eauto|].
          rewrite lookup_insert_ne//. pose proof (all_registers_correct x).
          rewrite -elem_of_dom dom_gset_to_gmap elem_of_list_to_set.
          auto.
        + iIntros (r v1 v2 Hne Hr Hr'). rewrite Hreg1 in Hr,Hr'.
          destruct (decide (PC = r));[subst;rewrite lookup_insert in Hr,Hr';inv Hr;inv Hr';auto|].
          rewrite lookup_insert_ne in Hr,Hr';auto.
          apply lookup_gset_to_gmap_Some in Hr as [? <-].
          apply lookup_gset_to_gmap_Some in Hr' as [? <-].
          iApply fixpoint_interp1_eq. auto.
      - rewrite Hreg1 insert_insert Heq. iFrame.
      - rewrite Hreg1 insert_insert Heq. iFrame. }

    unfold interp_conf.
    iModIntro.
    iExists (fun σ κs => ((gen_heap_interp σ.1) ∗ (gen_heap_interp σ.2)))%I.
    iExists (fun _ => True)%I. iFrame. iApply wp_fupd. iApply wp_wand_r. iFrame.

    iIntros (v) "Hcond".
    destruct v;[|iModIntro;iIntros (Hcontr);done..].
    iDestruct ("Hcond" $! eq_refl) as (r) "(Hj & Hcond)".
    iInv specN as ">Hres" "Hcls". iDestruct "Hres" as (e' σ') "[Hown Hsteps]".
    iDestruct "Hsteps" as %Hsteps.
    iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
    iMod ("Hcls" with "[Hown]") as "_".
    { iNext. iExists _,_. eauto. }
    iModIntro.
    apply auth_both_valid_discrete in Hvalid as [Hincl Hvalid].
    iIntros (_).
    apply prod_included in Hincl as [Hincl Hincl']. simpl in *.
    revert Hincl; rewrite Excl_included =>Hincl.
    apply leibniz_equiv in Hincl as <-.
    iExists [],σ'. iPureIntro.
    inv Hm1; inv Hm2. destruct His_program as [Hlink His_program].
    destruct His_program0 as [Hlink0 His_program0].
    inv His_program; inv His_program0.
    inv Hlink. inv Hlink1. inv Hlink0. inv Hlink.
    apply Hsteps.

  Qed.

  Lemma confidentiality_adequacy_r' {ML:memory_layout} c_adv p1 p2 (es: list cap_lang.expr)
        reg' m' :
    is_machine_context c_adv comp1 p1 →
    is_machine_context c_adv comp2 p2 →
    is_initial_context c_adv →
    rtc erased_step (initial_state_stk p2) (of_val HaltedV :: es, (reg', m')) →
    (∃ es' conf', rtc erased_step (initial_state_stk p1) (of_val HaltedV :: es', conf')).
  Proof.
    intros Hm1 Hm2 Hc Hstep.
    set (reg1 := (initial_state_stk p1).2.1).
    set (m1 := (initial_state_stk p1).2.2).
    set (reg2 := (initial_state_stk p2).2.1).
    set (m2 := (initial_state_stk p2).2.2).
    cut (@adequate cap_lang NotStuck (Seq (Instr Executable)) (reg2,m2)
                   (λ v _, v = HaltedV → ∃ thp' conf', rtc erased_step (initial_state_stk p1)
                                             (of_val HaltedV :: thp', conf'))).
    { destruct 1. inv Hm2. destruct His_program as [Hlink Hprog]. inv Hprog.
      apply adequate_result in Hstep. auto. auto. }
    eapply (wp_adequacy Σ _); iIntros (Hinv ?).

    iMod (gen_heap_init (m2:Mem)) as (mem_heapg) "(Hmem_ctx & Hmem & _)".
    iMod (gen_heap_init (reg2:Reg)) as (reg_heapg) "(Hreg_ctx & Hreg & _)".
    iMod (seal_store_init) as (seal_storeg) "Hseal_store".
    iMod (@na_alloc Σ na_invg) as (logrel_nais) "Hna".

    iMod (own_alloc (● (Excl' (Seq (Instr Executable)) : optionUR (exclR (leibnizO expr)), (∅,∅))
                       ⋅ ◯ ((Excl' (Seq (Instr Executable)) : optionUR (exclR (leibnizO expr)), (∅,∅)) : cfgUR)))
      as (γc) "[Hcfg1 Hcfg2]".
    { apply auth_both_valid_discrete. split=>//. }

    pose memg := MemG Σ Hinv mem_heapg.
    pose regg := RegG Σ Hinv reg_heapg.
    pose logrel_na_invs := Build_logrel_na_invs _ na_invg logrel_nais.
    set (Hcfg := CFGSG _ _ γc).

    iMod (regspec_alloc_big _ ∅ reg1 ∅ with "[Hcfg1]") as "(Hcfg1 & Hregspec)".
      by apply map_disjoint_empty_r. rewrite /spec_res /= !/to_spec_map !fmap_empty //.
    rewrite right_id_L.
    iMod (memspec_alloc_big _ ∅ m1 reg1 with "[Hcfg1]") as "(Hcfg1 & Hmemspec)".
      by apply map_disjoint_empty_r. rewrite /spec_res /= !/to_spec_map !fmap_empty //.
    rewrite right_id_L.

    pose proof (
      @counter_binary_preamble_left.counter_preamble_spec Σ memg regg logrel_na_invs Hcfg
      ) as Spec.

    pose proof (regions_disjoint_eq c_adv p1 p2 m1 m2 reg1 reg2 Hm1 Hm2 Hc eq_refl eq_refl eq_refl eq_refl)
      as [resolved_ms [Hm1eq [Hm2eq [Hcan_address_to_main [Hresolved_ms_spec [Heqreg [Hreg [Hdisj Hdisj'] ] ] ] ] ] ] ].

    rewrite {2}Hm1eq.
    rewrite {2}Hm2eq.

    iDestruct (big_sepM_union with "Hmem") as "[Hmem Hadv]";[auto|].
    iDestruct (big_sepM_union with "Hmemspec") as "[Hmemspec Hadvspec]";[auto|].

    pose proof regions_disjoint as Hdisjoint.
    rewrite disjoint_list_cons in Hdisjoint |- *. destruct Hdisjoint as (Hdisj_link_table & Hdisjoint).
    rewrite /mk_initial_memory_left /mk_initial_memory_right.

    iDestruct (big_sepM_union with "Hmem") as "[Hmem Hlink_table]".
    { disjoint_map_to_list. set_solver+ Hdisj_link_table. }
    iDestruct (big_sepM_union with "Hmemspec") as "[Hmemspec Hlink_table_spec]".
    { disjoint_map_to_list. set_solver+ Hdisj_link_table. }

    rewrite disjoint_list_cons in Hdisjoint |- *. destruct Hdisjoint as (Hdisj_malloc_mem & Hdisjoint).
    iDestruct (big_sepM_union with "Hmem") as "[Hmem Hmalloc_mem]".
    { disjoint_map_to_list. set_solver +Hdisj_malloc_mem. }
    iDestruct (big_sepM_union with "Hmemspec") as "[Hmemspec Hmalloc_mem_spec]".
    { disjoint_map_to_list. set_solver +Hdisj_malloc_mem. }

    rewrite disjoint_list_cons in Hdisjoint |- *. destruct Hdisjoint as (Hdisj_malloc_memptr & Hdisjoint).
    iDestruct (big_sepM_union with "Hmem") as "[Hmem Hmalloc_memptr]".
    { disjoint_map_to_list. set_solver +Hdisj_malloc_memptr. }
    iDestruct (big_sepM_union with "Hmemspec") as "[Hmemspec Hmalloc_memptr_spec]".
    { disjoint_map_to_list. set_solver +Hdisj_malloc_memptr. }

    iDestruct (big_sepM_insert with "Hmalloc_memptr") as "[Hmalloc_memptr _]".
    by apply lookup_empty. cbn [fst snd].
    iDestruct (big_sepM_insert with "Hmalloc_memptr_spec") as "[Hmalloc_memptr_spec _]".
    by apply lookup_empty. cbn [fst snd].

    rewrite disjoint_list_cons in Hdisjoint |- *. destruct Hdisjoint as (Hdisj_malloc_code & Hdisjoint).
    iDestruct (big_sepM_union with "Hmem") as "[Hmem Hmalloc_code]".
    { disjoint_map_to_list. set_solver +Hdisj_malloc_code. }
    iDestruct (big_sepM_union with "Hmemspec") as "[Hmemspec Hmalloc_code_spec]".
    { disjoint_map_to_list. set_solver +Hdisj_malloc_code. }

    rewrite disjoint_list_cons in Hdisjoint |- *. destruct Hdisjoint as (Hdisj_counter_body & Hdisjoint).
    iDestruct (big_sepM_union with "Hmem") as "[Hmem Hcounter_body]".
    { disjoint_map_to_list. set_solver +Hdisj_counter_body. }
    iDestruct (big_sepM_union with "Hmemspec") as "[Hmemspec Hcounter_body_spec]".
    { disjoint_map_to_list. set_solver +Hdisj_counter_body. }

    rewrite disjoint_list_cons in Hdisjoint |- *. destruct Hdisjoint as (Hdisj_counter_preamble & _).
    iDestruct (big_sepM_union with "Hmem") as "[Hcounter_link Hcounter_preamble]".
    { disjoint_map_to_list. set_solver +Hdisj_counter_preamble. }
    iDestruct (big_sepM_union with "Hmemspec") as "[Hcounter_link_spec Hcounter_preamble_spec]".
    { disjoint_map_to_list. set_solver +Hdisj_counter_preamble. }

    iDestruct (big_sepM_insert with "Hcounter_link") as "[Hcounter_link _]". by apply lookup_empty.
    iDestruct (big_sepM_insert with "Hcounter_link_spec") as "[Hcounter_link_spec _]". by apply lookup_empty.
    cbn [fst snd].

    clear Hdisj_link_table Hdisj_malloc_mem
      Hdisj_malloc_memptr Hdisj_malloc_code Hdisj_counter_body Hdisj_counter_preamble.

    (* Massage points-to into sepL2s with permission-pointsto *)

    iDestruct (mkregion_prepare with "[$Hlink_table]") as ">Hlink_table". by apply link_table_size.
    iDestruct (mkregion_prepare with "[$Hmalloc_mem]") as ">Hmalloc_mem".
    { rewrite replicate_length /finz.dist. clear.
      generalize malloc_mem_start malloc_end malloc_mem_size. solve_addr. }
    iDestruct (mkregion_prepare with "[$Hmalloc_code]") as ">Hmalloc_code".
      by apply malloc_code_size.
    iDestruct (mkregion_prepare with "[$Hcounter_preamble]") as ">Hcounter_preamble".
      by apply counter_preamble_size.
    iDestruct (mkregion_prepare with "[$Hcounter_body]") as ">Hcounter_body". by apply counter_body_size.
    iDestruct (mkregion_prepare_spec with "[$Hlink_table_spec]") as ">Hlink_table_spec". by apply link_table_size.
    iDestruct (mkregion_prepare_spec with "[$Hmalloc_mem_spec]") as ">Hmalloc_mem_spec".
    { rewrite replicate_length /finz.dist. clear.
      generalize malloc_mem_start malloc_end malloc_mem_size. solve_addr. }
    iDestruct (mkregion_prepare_spec with "[$Hmalloc_code_spec]") as ">Hmalloc_code_spec".
      by apply malloc_code_size.
    iDestruct (mkregion_prepare_spec with "[$Hcounter_preamble_spec]") as ">Hcounter_preamble_spec".
      by apply counter_preamble_size.
    iDestruct (mkregion_prepare_spec with "[$Hcounter_body_spec]") as ">Hcounter_body_spec". by apply counter_body_size.

    rewrite -/(counter_left _) -/(counter_left_preamble _ _ _).
    rewrite -/(counter_right _) -/(counter_right_preamble _ _ _).

    (* Allocate the spec invariant *)
    iMod (inv_alloc specN _ (spec_inv ([Seq (Instr Executable)],(reg1,m1)) ) with "[Hcfg1]") as "#Hspec_∅".
    { iNext. iExists _,_. iFrame. iPureIntro. rewrite /reg1 /m1 /=. left. }
    iAssert (spec_ctx)%I as "#Hspec".
    { iExists _. iFrame "#". }

    (* Split the link table *)
    rewrite (finz_seq_between_cons link_table_start link_table_end).
    2: { generalize link_table_size; clear; solve_addr. }
    rewrite (_: (link_table_start ^+ 1)%a = link_table_end).
    2: { generalize link_table_size; clear.
         generalize link_table_start link_table_end. solve_addr. }
    iDestruct (big_sepL2_cons with "Hlink_table") as "[Hlink1 _]".
    iDestruct (big_sepL2_cons with "Hlink_table_spec") as "[Hlink1' _]".

    (* Allocate malloc invariant *)
    iMod (na_inv_alloc logrel_nais ⊤ mallocN (malloc_inv_binary malloc_start malloc_end)
            with "[Hmalloc_code Hmalloc_memptr Hmalloc_mem Hmalloc_code_spec Hmalloc_memptr_spec Hmalloc_mem_spec]") as "#Hinv_malloc".
    { iNext. unfold malloc_inv_binary. iExists _,_. iFrame.
      iPureIntro. generalize malloc_code_size malloc_mem_size malloc_memptr_size. cbn.
      clear; unfold malloc_subroutine_instrs_length; intros; repeat split; solve_addr. }

    (* Facts about layout *)
    assert (isCorrectPC_range RX counter_region_start counter_region_end
              counter_preamble_start counter_body_start).
    { intros a [Ha1 Ha2]. constructor; auto.
      generalize counter_linking_ptr_size counter_preamble_size counter_body_size. revert Ha1 Ha2. clear.
      unfold counter_left_instrs_length, counter_preamble_instrs_length. solve_addr. }
    set counter_preamble_move_addr := (counter_preamble_start ^+ counter_preamble_move_offset)%a.
    assert ((counter_preamble_start + counter_preamble_move_offset)%a = Some counter_preamble_move_addr).
    { clear. subst counter_preamble_move_addr.
      generalize counter_preamble_size.
      unfold counter_preamble_instrs_length, counter_preamble_move_offset.
      generalize counter_preamble_start counter_body_start. solve_addr. }
    assert (counter_preamble_move_addr + offset_to_awkward = Some counter_body_start)%a.
    { generalize counter_preamble_size.
      unfold counter_preamble_move_addr, offset_to_awkward, counter_preamble_instrs_length.
      unfold counter_preamble_move_offset. clear.
      generalize counter_preamble_start counter_body_start. solve_addr. }
    assert (isCorrectPC_range RX counter_region_start counter_region_end
              counter_body_start counter_region_end).
    { intros a [Ha1 Ha2]. constructor; auto.
      generalize counter_linking_ptr_size counter_preamble_size counter_body_size. revert Ha1 Ha2; clear.
      unfold counter_left_instrs_length, counter_preamble_instrs_length. solve_addr. }

    (* Extract validity of library *)
    iMod (Spec with "[$Hspec $Hinv_malloc $Hcounter_preamble $Hcounter_body
                    $Hcounter_preamble_spec $Hcounter_body_spec $Hcounter_link $Hcounter_link_spec $Hlink1 $Hlink1']") as "#Hlib".
    apply H. apply H.
    { apply contiguous_between_region_addrs. generalize counter_preamble_size; clear.
      unfold counter_preamble_instrs_length. solve_addr. }
    { apply contiguous_between_region_addrs. generalize counter_preamble_size; clear.
      unfold counter_preamble_instrs_length. solve_addr. }
    { apply le_addr_withinBounds. clear; solve_addr.
      generalize link_table_size; clear; solve_addr. }
    { generalize link_table_start; clear; solve_addr. }
    { apply le_addr_withinBounds. solve_addr.
      generalize link_table_start link_table_end link_table_size. clear; solve_addr. }
    { generalize link_table_start; clear; solve_addr. }
    { eassumption. }
    { eassumption. }
    { apply H2. }
    { apply contiguous_between_region_addrs. generalize counter_body_size; clear.
      unfold counter_left_instrs_length. solve_addr. }
    { eassumption. }
    { eassumption. }
    { apply H2. }
    { apply contiguous_between_region_addrs. generalize counter_body_size; clear.
      unfold counter_left_instrs_length. solve_addr. }
    { auto. }

    (* Validity of the adv region *)
    iDestruct (big_sepM_sep with "[$Hadv $Hadvspec]") as "Hadv".
    iMod (establish_interp with "Hlib Hadv") as "#Hadvvalid"; [auto|].

    (* Validity of Main *)
    rewrite Heqreg.
    destruct Hreg as [c_main [Hreg1 [Hcanaddress Hcorrect] ] ].
    rewrite Heqreg in Hreg1.
    inversion Hcorrect as [p b e a Hbounds Hp Heq].
    iAssert (interp (WCap p b e a,WCap p b e a)) as "#Hval".
    { clear -Hcanaddress Hbounds Hp Heq.
      subst c_main. simpl in Hcanaddress.
      iApply fixpoint_interp1_eq.
      destruct Hp as [-> | ->];simpl.
      - iSplit;auto.
        iApply big_sepL_forall.
        iIntros (k x Hin).
        apply elem_of_list_lookup_2 in Hin.
        apply elem_of_finz_seq_between in Hin. apply Hcanaddress in Hin.
        apply elem_of_dom in Hin as [? ?].
        iExists interp. iSplit;auto.
        iDestruct (big_sepM_lookup with "Hadvvalid") as "$".
        eauto.
      - iSplit;auto.
        iApply big_sepL_forall.
        iIntros (k x Hin).
        apply elem_of_list_lookup_2 in Hin.
        apply elem_of_finz_seq_between in Hin. apply Hcanaddress in Hin.
        apply elem_of_dom in Hin as [? ?].
        iExists interp. iSplit;auto.
        iDestruct (big_sepM_lookup with "Hadvvalid") as "$".
        eauto.
    }

    iDestruct (fundamental_binary (reg2,reg2) with "[Hspec] Hval") as "Hval_exec".
    { iExact "Hspec". }

    unfold interp_expression. iSimpl in "Hval_exec".
    iDestruct ("Hval_exec" with "[Hreg Hregspec Hcfg2 $Hna]") as "[_ Hconf]".
    { iSplitR;[|iSplitL "Hreg";[|iSplitL "Hregspec"] ];[..|iExact "Hcfg2"].
      - iSplit.
        + iPureIntro. intros x. simpl.
          rewrite Hreg1;clear.
          destruct (decide (x = PC));[subst;rewrite lookup_insert;eauto|].
          rewrite lookup_insert_ne//. pose proof (all_registers_correct x).
          rewrite -elem_of_dom dom_gset_to_gmap elem_of_list_to_set.
          auto.
        + iIntros (r v1 v2 Hne Hr Hr'). rewrite Hreg1 in Hr,Hr'.
          destruct (decide (PC = r));[subst;rewrite lookup_insert in Hr,Hr';inv Hr;inv Hr';auto|].
          rewrite lookup_insert_ne in Hr,Hr';auto.
          apply lookup_gset_to_gmap_Some in Hr as [? <-].
          apply lookup_gset_to_gmap_Some in Hr' as [? <-].
          iApply fixpoint_interp1_eq. auto.
      - rewrite Hreg1 insert_insert Heq. iFrame.
      - rewrite Hreg1 insert_insert Heq. iFrame. }

    unfold interp_conf.
    iModIntro.
    iExists (fun σ κs => ((gen_heap_interp σ.1) ∗ (gen_heap_interp σ.2)))%I.
    iExists (fun _ => True)%I. iFrame. iApply wp_fupd. iApply wp_wand_r. iFrame.

    iIntros (v) "Hcond".
    destruct v;[|iModIntro;iIntros (Hcontr);done..].
    iDestruct ("Hcond" $! eq_refl) as (r) "(Hj & Hcond)".
    iInv specN as ">Hres" "Hcls". iDestruct "Hres" as (e' σ') "[Hown Hsteps]".
    iDestruct "Hsteps" as %Hsteps.
    iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
    iMod ("Hcls" with "[Hown]") as "_".
    { iNext. iExists _,_. eauto. }
    iModIntro.
    apply auth_both_valid_discrete in Hvalid as [Hincl Hvalid].
    iIntros (_).
    apply prod_included in Hincl as [Hincl Hincl']. simpl in *.
    revert Hincl; rewrite Excl_included =>Hincl.
    apply leibniz_equiv in Hincl as <-.
    iExists [],σ'. iPureIntro.
    inv Hm1; inv Hm2. destruct His_program as [Hlink His_program].
    destruct His_program0 as [Hlink0 His_program0].
    inv His_program; inv His_program0.
    inv Hlink. inv Hlink1. inv Hlink0. inv Hlink.
    apply Hsteps.
  Qed.

End Adequacy.

author: logsem

repo: cerise

save_path: github-repos/coq/logsem-cerise


text:
(** * Dijkstra monad hierarchy *)

(** Implementation of Dijkstra Monad framework in a series of Typeclasses *)

From ExtLib Require Import
     Structures.Monad.

From ITree Require Import
     Basics.Basics
     Basics.Monad.

Import MonadNotation.

Declare Scope dijkstra_scope.
Delimit Scope dijkstra_scope with dijkstra.

#[local] Open Scope dijkstra_scope.
#[local] Open Scope monad_scope.

(** ** Ordered monads *)

Class OrderM (M : Type -> Type) :=
  lem : forall A, M A -> M A -> Prop.

Arguments lem { M OrderM A }.

Infix "<≈" := lem (at level 70) : dijkstra_scope.

Section OrderedMonad.

  Context (W : Type -> Type).
  Context {Eq : Eq1 W}.
  Context {MonadW : Monad W}.
  Context {MonadLawsW : MonadLawsE W}.
  Context {OrderW : OrderM W}.
  Class OrderedMonad :=
    {
      reflex : forall A (w : W A), w <≈ w;
      trans : forall A (w1 w2 w3 : W A), w1 <≈ w2 -> w2 <≈ w3 -> w1 <≈ w3;
      monot : forall A B w1 w2 (f1 f2 : A -> W B), w1 <≈ w2 ->
                            (forall (a : A), (f1 a) <≈  (f2 a) ) -> (bind w1 f1) <≈ (bind w2 f2)
    }.

End OrderedMonad.

(** ** Specification monads *)

Section SpecMonad.

  Context (W : Type -> Type).
  Context {MonadW : Monad W}.
  Context {OrderW : OrderM W}.
  Context {OrderedMonadW : OrderedMonad W}.
  Class SpecMonad :=
    {
      Input : Type -> Type;
      In : forall {A : Type}, Input A -> W A -> Prop
    }.

  Infix "∈" := In (at level 70) : dijkstra_scope.
End SpecMonad.

(** ** Effect observations *)

Class EffectObs (M W : Type -> Type) :=
  obs : M ~> W.

Section EffectObservation.

  Context (M W : Type -> Type).
  Context {MMonad : Monad M}.
  Context {WMonad : Monad W}.
  Context {EqW : Eq1 W}.
  Context {MonadLawsW : MonadLawsE W}.
  Context {WOrder : OrderM W}.
  Context {WOrderLaws : OrderedMonad W}.
  Context (Obs : EffectObs M W).

  Class MonadMorphism :=
    {
      ret_pres : forall A (a : A), obs A (ret a) ≈ ret a;
      bind_pres : forall A B (m : M A) (f : A -> M B),
          obs _ (bind m f) ≈ bind (obs _ m) (fun a => obs _ (f a))
    }.

End EffectObservation.

(** ** Dijkstra monads *)

Section DijkstraMonad.
  Context (M W : Type -> Type).
  Context {MMonad : Monad M}.
  Context {WMonad : Monad W}.
  Context {EqW : Eq1 W}.
  Context {MonadLawsW : MonadLawsE W}.
  Context {WOrder : OrderM W}.
  Context { WOrderLaws : OrderedMonad W }.
  Context ( Obs : EffectObs M W ).

  (*Note that the Dijkstra Monad is only a monad-like structure
    not an actual monad*)
  Definition DijkstraMonad (A : Type) (w : W A) :=
    { m : M A |  obs A m <≈ w }.

  Definition DijkstraProp (A : Type) (w : W A) (m : M A)  : Prop :=
    obs A m <≈ w.

End DijkstraMonad.

author: DeepSpec

repo: InteractionTrees


text:
(**********************************************************************************

 The iso-comma category

 Contents
 1. Definition via two-sided displayed categories
 2. Discreteness and univalence

 **********************************************************************************)
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete.

Local Open Scope cat.

Section IsoCommaTwoSidedDispCat.
  Context {C₁ C₂ C₃ : category}
          (F : C₁ ⟶ C₃)
          (G : C₂ ⟶ C₃).

  (**
   1. Definition via two-sided displayed categories
   *)
  Definition iso_comma_twosided_disp_cat_ob_mor
    : twosided_disp_cat_ob_mor C₁ C₂.
  Proof.
    simple refine (_ ,, _).
    - exact (λ x y, z_iso (F x) (G y)).
    - exact (λ x₁ x₂ y₁ y₂ h₁ h₂ f g, #F f · h₂ = h₁ · #G g).
  Defined.

  Definition iso_comma_twosided_disp_cat_id_comp
    : twosided_disp_cat_id_comp iso_comma_twosided_disp_cat_ob_mor.
  Proof.
    split.
    - intros x y xy ; cbn.
      rewrite !functor_id.
      rewrite id_left, id_right.
      apply idpath.
    - intros x₁ x₂ x₃ y₁ y₂ y₃ h₁ h₂ h₃ f₁ f₂ g₁ g₂ hh₁ hh₂ ; cbn in *.
      rewrite !functor_comp.
      rewrite !assoc'.
      rewrite hh₂.
      rewrite !assoc.
      apply maponpaths_2.
      exact hh₁.
  Qed.

  Definition iso_comma_twosided_disp_cat_data
    : twosided_disp_cat_data C₁ C₂.
  Proof.
    simple refine (_ ,, _).
    - exact iso_comma_twosided_disp_cat_ob_mor.
    - exact iso_comma_twosided_disp_cat_id_comp.
  Defined.

  Definition isaprop_iso_comma_twosided_mor
             {x₁ x₂ : C₁}
             {y₁ y₂ : C₂}
             (xy₁ : iso_comma_twosided_disp_cat_data x₁ y₁)
             (xy₂ : iso_comma_twosided_disp_cat_data x₂ y₂)
             (f : x₁ --> x₂)
             (g : y₁ --> y₂)
    : isaprop (xy₁ -->[ f ][ g ] xy₂).
  Proof.
    apply homset_property.
  Qed.

  Definition iso_comma_twosided_disp_cat_axioms
    : twosided_disp_cat_axioms iso_comma_twosided_disp_cat_data.
  Proof.
    repeat split.
    - intro ; intros.
      apply isaprop_iso_comma_twosided_mor.
    - intro ; intros.
      apply isaprop_iso_comma_twosided_mor.
    - intro ; intros.
      apply isaprop_iso_comma_twosided_mor.
    - intro ; intros.
      apply isasetaprop.
      apply isaprop_iso_comma_twosided_mor.
  Qed.

  Definition iso_comma_twosided_disp_cat
    : twosided_disp_cat C₁ C₂.
  Proof.
    simple refine (_ ,, _).
    - exact iso_comma_twosided_disp_cat_data.
    - exact iso_comma_twosided_disp_cat_axioms.
  Defined.

  (**
   2. Discreteness and univalence
   *)
  Definition iso_comma_twosided_disp_cat_is_iso
    : all_disp_mor_iso iso_comma_twosided_disp_cat.
  Proof.
    intro ; intros.
    simple refine (_ ,, _ ,, _) ; cbn in *.
    - rewrite !functor_on_inv_from_z_iso.
      use z_iso_inv_on_right.
      rewrite assoc.
      use z_iso_inv_on_left ; cbn.
      exact fg.
    - apply isaprop_iso_comma_twosided_mor.
    - apply isaprop_iso_comma_twosided_mor.
  Qed.

  Definition is_univalent_iso_comma_twosided_disp_cat
    : is_univalent_twosided_disp_cat iso_comma_twosided_disp_cat.
  Proof.
    intros x₁ x₂ y₁ y₂ p₁ p₂ xy₁ xy₂.
    induction p₁, p₂ ; cbn.
    use isweqimplimpl.
    - intros f.
      pose (p := pr1 f) ; cbn in p.
      rewrite !functor_id in p.
      rewrite id_left, id_right in p.
      use subtypePath ; [ intro ; apply isaprop_is_z_isomorphism | ].
      exact (!p).
    - apply isaset_z_iso.
    - use isaproptotal2.
      + intro.
        apply isaprop_is_iso_twosided_disp.
      + intros.
        apply homset_property.
  Qed.

  Definition discrete_iso_comma_twosided_disp_cat
    : discrete_twosided_disp_cat iso_comma_twosided_disp_cat.
  Proof.
    repeat split.
    - intro ; intros.
      apply homset_property.
    - exact iso_comma_twosided_disp_cat_is_iso.
    - exact is_univalent_iso_comma_twosided_disp_cat.
  Qed.
End IsoCommaTwoSidedDispCat.

author: UniMath

repo: UniMath

save_path: github-repos/coq/UniMath-UniMath


text:
(** This file defines a Symbol instantiation that
 ** has a special case for [eq] and [not] and supports
 ** other symbols through a polymorphic function
 ** environment.
 **
 ** NOTE
 **  It is not generic because it builds on top of Ext.Types
 **)
Require Import Coq.Lists.List.
Require Import Coq.FSets.FMapPositive.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Data.Positive.
Require Import ExtLib.Tactics.Consider.
Require Import MirrorCore.SymI.
Require Import MirrorCore.TypesI.

Set Implicit Arguments.
Set Strict Implicit.

Definition func : Set := positive.

Global Instance RelDec_eq_func : RelDec (@eq func) := _.

Global Instance RelDec_Correct_eq_func : RelDec_Correct RelDec_eq_func := _.

Section RSym.
  Variable typ : Set.
  Variable RType_typ : RType typ.

  Record function := F
  { ftype : typ
  ; fdenote : typD ftype
  }.

  Definition functions := PositiveMap.t function.

  Fixpoint join_functions (a b : functions) : functions :=
    match a with
    | PositiveMap.Leaf _ => b
    | PositiveMap.Node l x r =>
      PositiveMap.Node (join_functions l match b with
                             | PositiveMap.Leaf _ => b
                             | PositiveMap.Node l _ _ => l
                             end)
           match x with
           | Some x => Some x
           | None => match b with
                     | PositiveMap.Leaf _ => None
                     | PositiveMap.Node _ x _ => x
                     end
           end
           (join_functions r match b with
                             | PositiveMap.Leaf _ => b
                             | PositiveMap.Node _ _ r => r
                             end)
    end.

  Variable fs : functions.

  Definition func_typeof_sym (i : func) : option typ :=
    match PositiveMap.find i fs with
      | None => None
      | Some ft => Some ft.(ftype)
    end.

  Definition funcD (f : func) : match func_typeof_sym f with
                                  | None => unit:Type
                                  | Some t => typD t
                                end :=
    match PositiveMap.find f fs as Z
          return
          match
            match Z with
              | Some ft => Some (ftype ft)
              | None => None
            end
          with
            | Some t => typD t
            | None => unit
          end
    with
      | Some ft => ft.(fdenote)
      | None => tt
    end.

  Global Instance RSym_func : RSym func :=
  { sym_eqb := fun l r => Some (l ?[ eq ] r)
  ; typeof_sym := func_typeof_sym
  ; symD := funcD
  }.

  Global Instance RSymOk_func : RSymOk RSym_func.
  Proof.
    constructor.
    unfold sym_eqb; simpl.
    intros; consider (a ?[ eq ] b); auto.
  Qed.

  Definition from_list {T} (ls : list T) : PositiveMap.t T :=
    (fix from_list ls : positive -> PositiveMap.t T :=
       match ls with
         | nil => fun _ => PositiveMap.empty _
         | l :: ls => fun p =>
                        PositiveMap.add p l (from_list ls (Pos.succ p))
       end) ls 1%positive.

End RSym.

Arguments functions _ _ : clear implicits.
Arguments function _ _ : clear implicits.
Arguments F {_ _} _ _ : clear implicits.
Arguments join_functions {_ _} _ _ : clear implicits.

author: gmalecha

repo: mirror-core

save_path: github-repos/coq/gmalecha-mirror-core


(* This software is governed by the CeCILL license under French law and
 * abiding by the rules of distribution of free software.  You can  use,
 * modify and/ or redistribute the software under the terms of the CeCILL
 * license as circulated by CEA, CNRS and INRIA at the following URL
 * "http://www.cecill.info".

 * As a counterpart to the access to the source code and  rights to copy,
 * modify and redistribute granted by the license, users are provided only
 * with a limited warranty  and the software's author,  the holder of the
 * economic rights,  and the successive licensors  have only  limited
 * liability.

 * In this respect, the user's attention is drawn to the risks associated
 * with loading,  using,  modifying and/or developing or reproducing the
 * software by the user in light of its specific status of free software,
 * that may mean  that it is complicated to manipulate,  and  that  also
 * therefore means  that it is reserved for developers  and  experienced
 * professionals having in-depth computer knowledge. Users are therefore
 * encouraged to load and test the software's suitability as regards their
 * requirements in conditions enabling the security of their systems and/or
 * data to be ensured and,  more generally, to use and operate it in the
 * same conditions as regards security.

 * The fact that you are presently reading this means that you have had
 * knowledge of the CeCILL license and that you accept its terms.
 *)

From Scheduler.Model Require Import Monad.
From Scheduler.Model.Interface.Types Require Import TypesModel.
Require Import List.

(* primitive *)

Parameter Jobs : CNat -> Job.

Fixpoint insert_Entry_aux (entry : Entry)
                          (entry_list : list Entry)
                          (comp_func : Entry -> Entry -> CBool)
                          : list Entry :=
  match entry_list with
  | nil => cons entry nil
  | cons head tail =>
      match comp_func entry head with
      | true => cons entry (cons head tail)
      | false => cons head (insert_Entry_aux entry tail comp_func)
      end
  end.

Fixpoint insert_Entries_aux (entries_to_be_added : list Entry)
                            (entry_list : list Entry)
                            (comp_func : Entry -> Entry -> CBool)
                            : list Entry :=
  match entries_to_be_added with
  | nil => entry_list
  | cons entry remaining_entries =>
      insert_Entries_aux remaining_entries (insert_Entry_aux entry entry_list comp_func) comp_func
  end.


text:
Require Import VST.floyd.proofauto.
Require Import VST.progs.message.

#[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

(* This program, and its verification, are described in Chapter 29
   of _Program Logics for Certified Compilers_, by Appel et al., 2014 *)

Local Open Scope Z.
Local Open Scope logic.

(*   mf_assert msgfmt sh buf len data  := the [data] is formatted into a message
         at most [len] bytes,  stored starting at address [buf] with share [sh] *)

Record message_format (t: type) : Type :=
mf_build {
   mf_size: Z;
   mf_data_assert: forall (data: reptype t), Prop;
   mf_assert: forall (sh: share) (buf: val) (len: Z) (data: reptype t), mpred;
   mf_size_range:  0 <= mf_size <= Int.max_signed;
   mf_bufprop: forall sh buf len data,
           mf_assert sh buf len data |--
                 !!(0 <= len <= mf_size) && memory_block sh len buf;
   mf_restbuf := fun (sh: share) (buf: val) (len: Z) =>
          memory_block sh (mf_size-len) (offset_val len buf)
}.

Arguments mf_build {t}.
Arguments mf_size {t}.
Arguments mf_data_assert {t}.
Arguments mf_assert {t}.
Arguments mf_bufprop {t}.
Arguments mf_size_range {t}.
Arguments mf_restbuf {t}.

Lemma mf_assert_local_facts: forall t (mf: message_format t) sh buf len (data: reptype t),
   mf_assert mf sh buf len data |--
    !! (0 <= len <= mf_size mf /\ isptr buf).
Proof.
intros.
eapply derives_trans;[ apply mf_bufprop | ].
entailer!.
Qed.

#[export] Hint Resolve mf_assert_local_facts : saturate_local.

Definition t_struct_intpair := Tstruct _intpair noattr.
Definition t_struct_message := Tstruct _message noattr.

Program Definition intpair_message: message_format t_struct_intpair :=
  mf_build 8 (fun data => is_int I32 Signed (fst data) /\ is_int I32 Signed (snd data))
             (fun sh buf len data => !!(len=8/\ is_int I32 Signed (fst data) /\ is_int I32 Signed (snd data))
                           && data_at sh (tarray tint 2) [fst data; snd data] buf)
      _ _.
Next Obligation.
compute; split; congruence.
Qed.
Next Obligation.
  entailer!!.
  change 8 with (sizeof (tarray tint 2)).
  apply data_at_memory_block.
Qed.

Definition serialize_spec {t: type} (format: message_format t) :=
  WITH data: reptype t, p: val, buf: val, sh: share, sh': share
  PRE [ tptr tvoid, tptr tuchar ]
          PROP (readable_share sh; writable_share sh';
                mf_data_assert format data;
                align_compatible tint buf)
          PARAMS (p; buf)
          SEP (data_at sh t data p;
                 memory_block sh' (mf_size format) buf)
  POST [ tint ]
         EX len: Z,
          PROP() RETURN (Vint (Int.repr len))
          SEP( data_at sh t data p;
                 mf_assert format sh' buf len data;
                 mf_restbuf format sh' buf len).

Definition deserialize_spec {t: type} (format: message_format t) :=
  WITH data: reptype t, p: val, buf: val, sh: share, sh': share, len: Z
  PRE [ tptr tvoid, tptr tuchar, tint ]
          PROP (readable_share sh'; writable_share sh;
                0 <= len <= mf_size format)
          PARAMS (p; buf; Vint (Int.repr len))
          SEP (mf_assert format sh' buf len data;
                 data_at_ sh t p)
  POST [ tvoid ]
          PROP (mf_data_assert format data)  RETURN ()
          SEP (mf_assert format sh' buf len data;
                 data_at sh t data p).

Definition intpair_serialize_spec :=
 DECLARE _intpair_serialize (serialize_spec intpair_message).

Definition intpair_deserialize_spec :=
 DECLARE _intpair_deserialize (deserialize_spec intpair_message).

Definition main_spec :=
 DECLARE _main
  WITH gv: globals
  PRE  [] main_pre prog tt gv
  POST [ tint ] main_post prog gv.

Definition message (sh: share) {t: type} (format: message_format t) (m: val) : mpred :=
  EX fg: val*val,
          func_ptr' (serialize_spec format) (fst fg) *
          func_ptr' (deserialize_spec format) (snd fg) *
       data_at sh t_struct_message (Vint (Int.repr (mf_size format)), (fst fg, snd fg)) m.

Definition Gprog : funspecs :=   ltac:(with_library prog [
    intpair_serialize_spec; intpair_deserialize_spec; main_spec]).

Lemma body_intpair_serialize: semax_body Vprog Gprog f_intpair_serialize intpair_serialize_spec.
Proof.
unfold intpair_serialize_spec.
unfold serialize_spec.
start_function.
destruct H as [Dx Dy].
destruct data as [[|x1 | | | | ] [|y1 | | | | ]]; try contradiction. clear Dx Dy.

change (mf_size intpair_message) with (sizeof (tarray tint 2)).
assert_PROP (field_compatible (tarray tint 2) [] buf).
  entailer!.
  hnf in H; decompose[and] H; repeat split; auto.
  (* TODO: abstract the following proof. *)
  unfold align_compatible in H0 |- *.
  destruct buf; auto.
  constructor.
  intros.
  eapply align_compatible_rec_by_value_inv in H0; [| reflexivity].
  econstructor; [reflexivity |].
  apply Z.divide_add_r; auto.
  exists i0; rewrite Z.mul_comm; auto.
rewrite memory_block_data_at_; auto.
change (data_at_ sh' (tarray tint 2) buf) with
   (data_at sh' (tarray tint 2) [Vundef;Vundef] buf).
forward. (* x = p->x; *)
forward. (* y = p->y; *)
forward. (*  ((int * )buf)[0]=x; *)
forward. (*  ((int * )buf)[1]=y; *)
forward. (* return 8; *)
Exists 8.
unfold mf_restbuf. simpl.
rewrite memory_block_zero.
entailer!!.
Qed.

Lemma body_intpair_deserialize: semax_body Vprog Gprog f_intpair_deserialize intpair_deserialize_spec.
Proof.
unfold intpair_deserialize_spec, deserialize_spec.
start_function.
hnf in data; simpl in data. (* This speeds things up dramatically *)
simpl. Intros. subst len.
destruct data as [[|x1 | | | | ] [|y1 | | | | ]]; try contradiction.
clear H H1 H2.
forward. (* x = ((int * )buf)[0]; *)
forward. (* y = ((int * )buf)[1]; *)
forward. (* p->x = x; *)
forward. (* p->y = y; *)
entailer!.
split; simpl; auto.
unfold mf_assert.
simpl.
entailer!!.
Qed.

Lemma body_main: semax_body Vprog Gprog f_main main_spec.
Proof.
function_pointers.
start_function.
set (ipm := gv _intpair_message).
fold cc_default noattr.
make_func_ptr _intpair_deserialize.
make_func_ptr _intpair_serialize.
set (des := gv _intpair_deserialize).
set (ser := gv _intpair_serialize).
match goal with
 |- context [mapsto_zeros 4 Ews _] =>
  (* 64-bit mode *)
  sep_apply mapsto_zeros_memory_block; auto;
  gather_SEP (mapsto _ _ _ (offset_val 0 des))
      (mapsto _ _ _ (offset_val 0 ser))
      (memory_block Ews 4 _)
      (data_at _ _ _ ipm)
 | _ => (*32-bit mode *)
  gather_SEP (mapsto _ _ _ (offset_val 0 des))
      (mapsto _ _ _ (offset_val 0 ser))
      (data_at _ _ _ ipm)
end.
replace_SEP 0
    (data_at Ews t_struct_message
      (Vint (Int.repr (mf_size intpair_message)), (ser, des)) ipm). {
 entailer!.
 unfold_data_at (data_at _ t_struct_message _ ipm).
 rewrite (field_at_data_at _ _ _ _ ipm).
rewrite data_at_tuint_tint.
(* rewrite <- (mapsto_field_at _ _ [StructField _bufsize] (Vint (Int.repr 8))) by auto with field_compatible. *)
 rewrite <- (mapsto_field_at _ _ [StructField _deserialize] des) by auto with field_compatible.
 rewrite <- (mapsto_field_at _ _ [StructField _serialize] ser) by auto with field_compatible.
 rewrite !field_compatible_field_address by auto with field_compatible.
 simpl.
 normalize.
 unfold spacer, at_offset; simpl.
 cancel.
}
forward. (* p.x = 1; *)
forward. (* p.y = 2; *)
forward. (* ser = intpair_message.serialize; *)

rewrite <- memory_block_data_at__tarray_tuchar_eq by computable.
change (memory_block Tsh 8 v_buf)
with (memory_block Tsh (mf_size intpair_message) v_buf).

assert_PROP (align_compatible tint v_buf).
  entailer!.
  destruct HPv_buf; subst; simpl.
  econstructor; [reflexivity | apply Z.divide_0_r].
forward_call (* len = ser(&p, buf); *)
      ((Vint (Int.repr 1), Vint (Int.repr 2)), v_p, v_buf, Tsh, Tsh).
  split3; auto.
  repeat split; auto.
Intros rest.
simpl.
Intros. subst rest.

forward. (* des = intpair_message.deserialize; *)
forward_call (* des(&q, buf, 8); *)
        ((Vint (Int.repr 1), Vint (Int.repr 2)), v_q, v_buf, Tsh, Tsh, 8).
  simpl. fold t_struct_intpair. entailer!.
  simpl; computable.
(* after the call *)
forward. (* x = q.x; *)
forward. (* y = q.y; *)
forward. (* return x+y; *)
simpl.
entailer!.
sep_apply (data_at_memory_block Tsh (tarray tint 2) [Vint (Int.repr 1); Vint (Int.repr 2)] v_buf).
unfold sizeof; simpl Ctypes.sizeof.
sep_apply (memory_block_data_at__tarray_tuchar Tsh v_buf 8).
   computable.
entailer!!.
Qed.

repo: VST


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

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

Print Assumptions mul.


text:
Require Import Bedrock.Bedrock Bedrock.Platform.tests.MiniMasterDriver Bedrock.AMD64_gas.

Definition compiled := moduleS E.m.
Unset Extraction AccessOpaque.  Recursive Extraction compiled.

author: mit-plv

repo: bedrock

save_path: github-repos/coq/mit-plv-bedrock


text:
Load LFindLoad.
From lfind Require Import LFind.
Unset Printing Notations.
Set Printing Implicit.

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

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

Inductive tree : Type := Node : natural -> tree -> tree -> tree |  Leaf : tree.

Inductive Pair : Type := mkpair : natural -> natural -> Pair
with Zlst : Type := zcons : Pair -> Zlst -> Zlst |  znil : Zlst.

Fixpoint drop (drop_arg0 : natural) (drop_arg1 : lst) : lst
           := match drop_arg0, drop_arg1 with
              | x, Nil => Nil
              | Zero, x => x
              | Succ x, Cons y z => drop x z
              end.

Lemma lem: forall n1 n2 l, drop (Succ n1) (drop n2 l) = drop n1 (drop (Succ n2) l).
Proof.
intros. generalize dependent n1. generalize dependent n2. induction l.
- intros. assert (forall n x l, drop (Succ n) (Cons x l) = drop n l).
   + intros. reflexivity.
   + destruct n2.
   * rewrite H. rewrite H. rewrite <- IHl. reflexivity.
   * simpl. destruct l. reflexivity. reflexivity.
- intros. assert (forall n, drop n Nil = Nil).
   + intros. destruct n. reflexivity. reflexivity.
   + rewrite H. rewrite H. rewrite H. reflexivity.
Qed.

Theorem theorem0 : forall (v : natural) (w : natural) (x : natural) (y : natural) (z : lst), eq (drop (Succ v) (drop w (drop x (Cons y z)))) (drop v (drop w (drop x z))).
Proof.
intros.
rewrite lem.
lfind.  reflexivity.
Admitted.