WIP import griotte

theories/proofmode/contiguous.v

@@ -289,52 +289,3 @@ Section Contiguous.
   Qed.
 
 End Contiguous.
-
-Definition isCorrectPC_range p b e a0 an :=
-  ∀ ai, (a0 <= ai)%a ∧ (ai < an)%a → isCorrectPC (WCap p b e ai).
-
-Lemma isCorrectPC_inrange p b (e a0 an a: Addr) :
-  isCorrectPC_range p b e a0 an →
-  (a0 <= a < an)%Z →
-  isCorrectPC (WCap p b e a).
-Proof.
-  unfold isCorrectPC_range. move=> /(_ a) HH ?. apply HH. eauto.
-Qed.
-
-Lemma isCorrectPC_contiguous_range p b e a0 an a l :
-  isCorrectPC_range p b e a0 an →
-  contiguous_between l a0 an →
-  a ∈ l →
-  isCorrectPC (WCap p b e a).
-Proof.
-  intros Hr Hc Hin.
-  eapply isCorrectPC_inrange; eauto.
-  eapply contiguous_between_middle_bounds'; eauto.
-Qed.
-
-Lemma isCorrectPC_range_perm p b e a0 an :
-  isCorrectPC_range p b e a0 an →
-  (a0 < an)%a →
-  p = RX ∨ p = RWX.
-Proof.
-  intros Hr H0n.
-  assert (isCorrectPC (WCap p b e a0)) as HH by (apply Hr; solve_addr).
-  inversion HH; auto.
-Qed.
-
-Lemma isCorrectPC_range_perm_non_E p b e a0 an :
-  isCorrectPC_range p b e a0 an →
-  (a0 < an)%a →
-  p ≠ E.
-Proof.
-  intros HH1 HH2. pose proof (isCorrectPC_range_perm _ _ _ _ _ HH1 HH2).
-  naive_solver.
-Qed.
-
-Lemma isCorrectPC_range_restrict p b e a0 an a0' an' :
-  isCorrectPC_range p b e a0 an →
-  (a0 <= a0')%a ∧ (an' <= an)%a →
-  isCorrectPC_range p b e a0' an'.
-Proof.
-  intros HR [? ?] a' [? ?]. apply HR. solve_addr.
-Qed.

theories/proofmode/proofmode.v

@@ -67,11 +67,11 @@ Ltac solve_block_move :=
 
 (* Ltac specifically meant for switching to the next block. Use `changePCto` to perform more arbitrary moves *)
 Ltac changePC_next_block new_a :=
-  match goal with |- context [ Esnoc _ _ (PC ↦ᵣ WCap _ _ _ ?prev_a)%I ] =>
+  match goal with |- context [ Esnoc _ _ (PC ↦ᵣ WCap _ _ _ _ ?prev_a)%I ] =>
                     rewrite (_: prev_a = new_a) ; [ | solve_block_move  ] end.
 (* More powerful ltac to change the address of the pc. Might take longer to solve than the more specific alternative above.*)
 Ltac changePCto0 new_a :=
-  match goal with |- context [ Esnoc _ _ (PC ↦ᵣ WCap _ _ _ ?a)%I ] =>
+  match goal with |- context [ Esnoc _ _ (PC ↦ᵣ WCap _ _ _ _ ?a)%I ] =>
     rewrite (_: a = new_a); [| solve_addr]
   end.
 Tactic Notation "changePCto" constr(a) := changePCto0 a.
@@ -553,7 +553,7 @@ Proof. solve_addr. Qed.
 Ltac iInstr_lookup0 hprog hi hcont :=
   let hprog := constr:(hprog:ident) in
   lazymatch goal with |- context [ Esnoc _ hprog (codefrag ?a_base _) ] =>
-  lazymatch goal with |- context [ Esnoc _ ?hpc (PC ↦ᵣ (WCap _ _ _ ?pc_a))%I ] =>
+  lazymatch goal with |- context [ Esnoc _ ?hpc (PC ↦ᵣ (WCap _ _ _ _ ?pc_a))%I ] =>
     let base_off := eval unfold as_weak_addr_incr in (@as_weak_addr_incr pc_a a_base _ _) in
     lazymatch base_off with
     | (?base, ?off) =>

theories/proofmode/proofmode_instr_rules.v

@@ -69,9 +69,9 @@ Ltac dispatch_instr_rule instr cont :=
   | Store _ (inl _) =>
     (cont (@wp_store_success_same) ||
      cont (@wp_store_success_z))
-  | Store _ (inr PC) =>
-    (cont (@wp_store_success_reg_frominstr_same) ||
-     cont (@wp_store_success_reg_frominstr))
+  (* | Store _ (inr PC) => *)
+  (*   (cont (@wp_store_success_reg_frominstr_same) || *)
+  (*    cont (@wp_store_success_reg_frominstr)) *)
   | Store ?r (inr ?r) =>
     (cont (@wp_store_success_reg_same') ||
      cont (@wp_store_success_reg_same))

theories/proofmode/solve_pure.v

@@ -87,6 +87,7 @@ Proof. auto. Qed.
 (* is_Get *)
 #[export] Hint Mode is_Get ! - - : solve_pure.
 #[export] Hint Resolve is_Get_GetP : solve_pure.
+#[export] Hint Resolve is_Get_GetL : solve_pure.
 #[export] Hint Resolve is_Get_GetB : solve_pure.
 #[export] Hint Resolve is_Get_GetE : solve_pure.
 #[export] Hint Resolve is_Get_GetA : solve_pure.
@@ -115,23 +116,23 @@ Goal forall (r_t1 PC: RegName) `{MachineParameters}, exists r1 r2,
   r1 = r_t1 ∧ r2 = inr PC.
 Proof. do 2 eexists. repeat apply conj. solve_pure. all: reflexivity. Qed.
 
-Goal forall p b e a,
+Goal forall p g b e a,
   ExecPCPerm p →
   SubBounds b e a (a ^+ 5)%a →
   ContiguousRegion a 5 →
-  isCorrectPC (WCap p b e a).
+  isCorrectPC (WCap p g b e a).
 Proof. intros. solve_pure. Qed.
 
 Goal forall (r_t1 r_t2: RegName), exists r1 r2,
   is_Get (GetB r_t2 r_t1) r1 r2 ∧
   r1 = r_t2 ∧ r2 = r_t1.
 Proof. do 2 eexists. repeat apply conj. solve_pure. all: reflexivity. Qed.
 
-Goal forall p b e a,
+Goal forall p g b e a,
   ExecPCPerm p →
   SubBounds b e a (a ^+ 5)%a →
   ContiguousRegion a 5 →
-  isCorrectPC (WCap p b e (a ^+ 1)%a).
+  isCorrectPC (WCap p g b e (a ^+ 1)%a).
 Proof. intros. solve_pure. Qed.
 
 Goal forall (r_t1 r_t2 r_t3: RegName), exists r1 r2 r3,

theories/proofmode/tactics_helpers.v

@@ -7,49 +7,57 @@ From cap_machine Require Import cap_lang region contiguous.
 Section helpers.
 
   (* ---------------------------- Helper Lemmas --------------------------------------- *)
+  Definition isCorrectPC_range p g b e a0 an :=
+    ∀ ai, (a0 <= ai)%a ∧ (ai < an)%a → isCorrectPC (WCap p g b e ai).
 
-  Definition isCorrectPC_range p b e a0 an :=
-    ∀ ai, (a0 <= ai)%a ∧ (ai < an)%a → isCorrectPC (WCap p b e ai).
-
-  Lemma isCorrectPC_inrange p b (e a0 an a: Addr) :
-    isCorrectPC_range p b e a0 an →
+  Lemma isCorrectPC_inrange p g b (e a0 an a: Addr) :
+    isCorrectPC_range p g b e a0 an →
     (a0 <= a < an)%Z →
-    isCorrectPC (WCap p b e a).
+    isCorrectPC (WCap p g b e a).
   Proof.
     unfold isCorrectPC_range. move=> /(_ a) HH ?. apply HH. eauto.
   Qed.
 
-  Lemma isCorrectPC_contiguous_range p b e a0 an a l :
-    isCorrectPC_range p b e a0 an →
+  Lemma isCorrectPC_contiguous_range p g b e a0 an a l :
+    isCorrectPC_range p g b e a0 an →
     contiguous_between l a0 an →
     a ∈ l →
-    isCorrectPC (WCap p b e a).
+    isCorrectPC (WCap p g b e a).
   Proof.
     intros Hr Hc Hin.
     eapply isCorrectPC_inrange; eauto.
     eapply contiguous_between_middle_bounds'; eauto.
   Qed.
 
-  Lemma isCorrectPC_range_perm p b e a0 an :
-    isCorrectPC_range p b e a0 an →
+  Lemma isCorrectPC_range_perm p g b e a0 an :
+    isCorrectPC_range p g b e a0 an →
     (a0 < an)%a →
-    p = RX ∨ p = RWX.
+    p = RX ∨ p = RWX \/ p = RWLX.
   Proof.
     intros Hr H0n.
-    assert (isCorrectPC (WCap p b e a0)) as HH by (apply Hr; solve_addr).
+    assert (isCorrectPC (WCap p g b e a0)) as HH by (apply Hr; solve_addr).
     inversion HH; auto.
   Qed.
 
-  Lemma isCorrectPC_range_npE p b e a0 an :
-    isCorrectPC_range p b e a0 an →
+  Lemma isCorrectPC_range_perm_non_E p g b e a0 an :
+    isCorrectPC_range p g b e a0 an →
     (a0 < an)%a →
     p ≠ E.
   Proof.
     intros HH1 HH2.
-    destruct (isCorrectPC_range_perm _ _ _ _ _ HH1 HH2) as [?| ? ];
-      congruence.
+    pose proof (isCorrectPC_range_perm _ _ _ _ _ _ HH1 HH2).
+    naive_solver.
   Qed.
 
+  Lemma isCorrectPC_range_restrict p g b e a0 an a0' an' :
+    isCorrectPC_range p g b e a0 an →
+    (a0 <= a0')%a ∧ (an' <= an)%a →
+    isCorrectPC_range p g b e a0' an'.
+  Proof.
+    intros HR [? ?] a' [? ?]. apply HR. solve_addr.
+  Qed.
+
+
 End helpers.
 
 (* Ltacs *)