Merge 'attestation' into attestation_wp

_CoqProject

@@ -126,11 +126,11 @@ theories/proofmode/disjoint_regions_tactics.v
 # theories/proofmode/mkregion_helpers.v
 
 # Common Cerise (assembly) macros
-# theories/examples/malloc.v
-# theories/examples/salloc.v
-# theories/examples/assert.v
-# theories/examples/macros.v
-# theories/examples/macros_new.v
+theories/examples/malloc.v
+theories/examples/salloc.v
+theories/examples/assert.v
+theories/examples/macros.v
+theories/examples/macros_new.v
 
 # Template Adequacy
 # theories/examples/template_adequacy.v

theories/cap_lang.v

@@ -142,10 +142,7 @@ Qed.
 (*--- addr_of_argument ---*)
 
 Definition addr_of_argument regs src :=
-  match z_of_argument regs src with
-  | Some n => z_to_addr n
-  | None => None
-  end.
+  n ← z_of_argument regs src ; z_to_addr n.
 
 Lemma addr_of_argument_Some_inv (regs: Reg) (arg: Z + RegName) (a:Addr) :
   addr_of_argument regs arg = Some a →
@@ -174,17 +171,14 @@ regs ⊆ r
 Proof.
   intros.
   unfold addr_of_argument, z_of_argument in *.
-  destruct arg; auto. destruct (_ !! _)  eqn:Heq; [| congruence].
+  destruct arg; auto. destruct (regs !! _) eqn:Heq; cbn in * ; [| congruence].
   eapply lookup_weaken in Heq as ->; auto.
 Qed.
 
 (*--- otype_of_argument ---*)
 
 Definition otype_of_argument regs src : option OType :=
-  match z_of_argument regs src with
-  | Some n => (z_to_otype n) : option OType
-  | None => None : option OType
-  end.
+  n ← z_of_argument regs src ; z_to_otype n.
 
 Lemma otype_of_argument_Some_inv (regs: Reg) (arg: Z + RegName) (o:OType) :
   otype_of_argument regs arg = Some o →
@@ -213,7 +207,7 @@ regs ⊆ r
 Proof.
   intros.
   unfold otype_of_argument, z_of_argument in *.
-  destruct arg; auto. destruct (_ !! _)  eqn:Heq; [| congruence].
+  destruct arg; auto. destruct (_ !! _)  eqn:Heq ; cbn in *; [| congruence].
   eapply lookup_weaken in Heq as ->; auto.
 Qed.
 
@@ -515,6 +509,7 @@ Section opsem.
           end
       | _ => None
       end
+
     | Restrict dst ρ =>
       n ← z_of_argument (reg φ) ρ ;
       wdst ← (reg φ) !! dst;
@@ -619,7 +614,8 @@ Section opsem.
     wr2 ← (reg φ) !! r2;
     match wr1, wr2 with
     | WSealRange p b e a, WSealed a' sb =>
-        if decide (permit_unseal p = true ∧ withinBounds b e a = true ∧ a' = a) then updatePC (update_reg φ dst (WSealable sb))
+        if decide (permit_unseal p = true ∧ withinBounds b e a = true ∧ a' = a)
+        then updatePC (update_reg φ dst (WSealable sb))
         else None
     | _,_ => None
     end

theories/examples/addr_reg_sample.v

@@ -73,3 +73,19 @@ Proof.
   rewrite (finz_dist_split a). 2: solve_addr.
   rewrite replicate_add //.
 Qed.
+
+Definition region_addrs_zeroesL (b e : Addr) (v : Version) : list LWord :=
+  replicate (finz.dist b e) (LWInt 0%Z).
+
+Lemma region_addrs_zeroesL_lookup (b e : Addr) (v : Version) i y :
+  region_addrs_zeroesL b e v !! i = Some y → y = LInt 0%Z.
+Proof. apply lookup_replicate. Qed.
+
+Lemma region_addrs_zeroesL_split (b a e: Addr) (v : Version) :
+  (b <= a)%a ∧ (a <= e)%a →
+  region_addrs_zeroesL b e v = region_addrs_zeroesL b a v ++ region_addrs_zeroesL a e v.
+Proof.
+  intros. rewrite /region_addrs_zeroesL.
+  rewrite (finz_dist_split a). 2: solve_addr.
+  rewrite replicate_add //.
+Qed.

theories/examples/assert.v

@@ -13,7 +13,7 @@ Section Assert.
 
   (* assert (r4 == r5) *)
   Definition assert_subroutine_instrs :=
-    encodeInstrsW [
+    encodeInstrsLW [
       Sub r_t4 r_t4 r_t5;
       Mov r_t5 PC;
       Lea r_t5 6;
@@ -36,29 +36,29 @@ Section Assert.
     end:
   *)
 
-  Definition assert_inv (b a_flag e : Addr) : iProp Σ :=
+  Definition assert_inv (b a_flag e : Addr) (v : Version) : iProp Σ :=
     (∃ cap_addr,
-       codefrag b assert_subroutine_instrs ∗
+       codefrag b v assert_subroutine_instrs ∗
        ⌜(b + length assert_subroutine_instrs)%a = Some cap_addr⌝ ∗
        ⌜(cap_addr + 1)%a = Some a_flag⌝ ∗
        ⌜(a_flag + 1)%a = Some e⌝ ∗
-       cap_addr ↦ₐ WCap RW a_flag e a_flag).
+       (cap_addr, v) ↦ₐ LCap RW a_flag e a_flag v).
 
-  Lemma assert_subroutine_spec b a_flag e cont n1 n2 flag N E φ :
+  Lemma assert_subroutine_spec b a_flag e v cont n1 n2 flag N E φ :
     ↑N ⊆ E →
-    (  na_inv logrel_nais N (assert_inv b a_flag e)
+    (  na_inv logrel_nais N (assert_inv b a_flag e v)
      ∗ na_own logrel_nais E
-     ∗ PC ↦ᵣ WCap RX b e b
+     ∗ PC ↦ᵣ LCap RX b e b v
      ∗ r_t0 ↦ᵣ cont
-     ∗ r_t4 ↦ᵣ WInt n1
-     ∗ r_t5 ↦ᵣ WInt n2
-     ∗ a_flag ↦ₐ WInt flag
+     ∗ r_t4 ↦ᵣ LInt n1
+     ∗ r_t5 ↦ᵣ LInt n2
+     ∗ (a_flag, v) ↦ₐ LInt flag
      ∗ ▷ (na_own logrel_nais E
-          ∗ PC ↦ᵣ updatePcPerm cont
+          ∗ PC ↦ᵣ updatePcPermL cont
           ∗ r_t0 ↦ᵣ cont
-          ∗ r_t4 ↦ᵣ WInt 0
-          ∗ r_t5 ↦ᵣ WInt 0
-          ∗ a_flag ↦ₐ WInt (if (n1 =? n2)%Z then flag else 1%Z)
+          ∗ r_t4 ↦ᵣ LInt 0
+          ∗ r_t5 ↦ᵣ LInt 0
+          ∗ (a_flag, v) ↦ₐ LInt (if (n1 =? n2)%Z then flag else 1%Z)
           -∗ WP Seq (Instr Executable) {{ φ }})
      ⊢ WP Seq (Instr Executable) {{ φ }})%I.
   Proof.
@@ -87,20 +87,20 @@ Section Assert.
       by apply Z.eqb_neq. }
   Qed.
 
-  Lemma assert_success_spec b a_flag e cont n1 n2 N E φ :
+  Lemma assert_success_spec b a_flag e v cont n1 n2 N E φ :
     ↑N ⊆ E →
     n1 = n2 →
-    (  na_inv logrel_nais N (assert_inv b a_flag e)
+    (  na_inv logrel_nais N (assert_inv b a_flag e v)
      ∗ na_own logrel_nais E
-     ∗ PC ↦ᵣ WCap RX b e b
+     ∗ PC ↦ᵣ LCap RX b e b v
      ∗ r_t0 ↦ᵣ cont
-     ∗ r_t4 ↦ᵣ WInt n1
-     ∗ r_t5 ↦ᵣ WInt n2
+     ∗ r_t4 ↦ᵣ LInt n1
+     ∗ r_t5 ↦ᵣ LInt n2
      ∗ ▷ (na_own logrel_nais E
-          ∗ PC ↦ᵣ updatePcPerm cont
+          ∗ PC ↦ᵣ updatePcPermL cont
           ∗ r_t0 ↦ᵣ cont
-          ∗ r_t4 ↦ᵣ WInt 0
-          ∗ r_t5 ↦ᵣ WInt 0
+          ∗ r_t4 ↦ᵣ LInt 0
+          ∗ r_t5 ↦ᵣ LInt 0
           -∗ WP Seq (Instr Executable) {{ φ }})
      ⊢ WP Seq (Instr Executable) {{ φ }})%I.
   Proof.