cleaned ClockIntegers.v

src/ClockIntegers.v

@@ -5,152 +5,136 @@ Require Import stdpp.numbers.
 Open Scope Z_scope.
 
 Definition w : nat := 64.
-(*Definition max_uint : Z := Eval compute in 1 ≪ w.
-Definition max_int : Z := Eval compute in 1 ≪ (w-1).
-Definition min_int : Z := Eval compute in - max_int.*)
 Definition max_int : Z := 1 ≪ (w-1).
 Definition min_int : Z := - max_int.
 Definition max_uint : Z := 2 * max_int.
 
+(*
+ * Bare machine integers can overflow.
+ *)
+
 Section machine_int.
 
-Context `{heapG Σ}.
-
-Definition is_machine_int (n : Z) : iProp Σ :=
-  ⌜min_int ≤ n < max_int⌝%I.
-
-Definition machine_int_add : val :=
-  λ: "x" "y",
-    ("x" + "y" + #max_int) `rem` #max_uint - #max_int.
-
-Lemma machine_int_add_spec n1 n2 :
-  {{{ is_machine_int n1 ∗ is_machine_int n2 ∗ ⌜min_int ≤ n1+n2 < max_int⌝ }}}
-  machine_int_add #n1 #n2
-  {{{ RET #(n1+n2) ; is_machine_int (n1+n2) }}}.
-Proof.
-  iIntros (Φ) "(_ & _ & %) Post". repeat (wp_pure _).
-  (* boring arithmetic proof: *)
-  assert ((n1 + n2 + max_int) `rem` max_uint - max_int = n1 + n2) as ->. {
-    assert ((n1 + n2 + max_int) `rem` max_uint = n1 + n2 + max_int). {
-      (*assert (min_int = -max_int) by done.
-      assert (max_int + max_int = max_uint) by done.*)
-      apply Z.rem_small. unfold min_int, max_uint in *. lia.
+  Context `{heapG Σ}.
+
+  Definition is_machine_int (n : Z) : iProp Σ :=
+    ⌜min_int ≤ n < max_int⌝%I.
+
+  Definition machine_int_add : val :=
+    λ: "x" "y",
+      ("x" + "y" + #max_int) `rem` #max_uint - #max_int.
+
+  (* Machine addition does not overflow when some inequality is met: *)
+  Lemma machine_int_add_spec n1 n2 :
+    {{{ is_machine_int n1 ∗ is_machine_int n2 ∗ ⌜min_int ≤ n1+n2 < max_int⌝ }}}
+    machine_int_add #n1 #n2
+    {{{ RET #(n1+n2) ; is_machine_int (n1+n2) }}}.
+  Proof.
+    iIntros (Φ) "(_ & _ & %) Post". repeat (wp_pure _).
+    (* boring arithmetic proof: *)
+    assert ((n1 + n2 + max_int) `rem` max_uint - max_int = n1 + n2) as ->. {
+      assert ((n1 + n2 + max_int) `rem` max_uint = n1 + n2 + max_int). {
+        apply Z.rem_small. unfold min_int, max_uint in *. lia.
+      }
+      lia.
     }
-    lia.
-  }
-  by iApply "Post".
-Qed.
+    by iApply "Post".
+  Qed.
 
 End machine_int.
 
-Section clock_int.
+(*
+ * A “clock integer” (“onetime integer” in Clochard’s thesis) is a non-duplicable
+ * integer which supports addition.
+ *)
 
-Context `{timeReceiptHeapG Σ}.
-Context (nmax : nat).
-Context `(nmax ≤ max_int).
+Section clock_int.
 
-Definition is_clock_int (n : nat) : iProp Σ :=
-  TR n.
+  Context `{timeReceiptHeapG Σ}.
+  Context (nmax : nat).
+  Context `(nmax ≤ max_int).
 
-  Lemma TR_weaken (n₁ n₂ : nat) :
-    (n₂ ≤ n₁)%nat →
-    TR n₁ -∗ TR n₂.
-  Require Import Auth_nat.
-  Proof. apply own_auth_nat_weaken. Qed.
+  Definition is_clock_int (n : nat) : iProp Σ :=
+    TR n.
 
-  Lemma TR_lt_nmax n (E : coPset) :
-    ↑timeReceiptN ⊆ E →
-    TR_invariant nmax -∗ TR n ={E}=∗ TR n ∗ ⌜n < nmax⌝%nat.
+  (* Clock integers support addition, which consumes its arguments: *)
+  Lemma clock_int_add_spec n1 n2 :
+    TR_invariant nmax -∗
+    {{{ is_clock_int n1 ∗ is_clock_int n2 }}}
+    machine_int_add #n1 #n2
+    {{{ RET #(n1+n2) ; is_clock_int (n1+n2) }}}.
   Proof.
-    iIntros (?) "#Inv Hγ1◯".
-    destruct (le_lt_dec nmax n) as [ I | I ] ; last by iFrame.
-    iDestruct (TR_weaken n nmax with "Hγ1◯") as "Hγ1◯" ; first done.
-    iDestruct (TR_nmax_absurd with "Inv Hγ1◯") as ">?" ; first done.
-    done.
+    iIntros "#Htrinv" (Φ) "!# (H1 & H2) Post".
+    iAssert (TR (n1+n2)) with "[H1 H2]" as "H" ; first by (rewrite TR_plus ; iFrame).
+    iDestruct (TR_lt_nmax with "Htrinv H") as ">(H & %)" ; first done.
+    wp_apply (machine_int_add_spec n1 n2 with "[] [H Post]") .
+    {
+      iPureIntro. unfold min_int in *. lia.
+    }
+    {
+      iNext ; iIntros "%". iApply "Post". iFrame "H".
+    }
   Qed.
 
-Lemma clock_int_add_spec n1 n2 :
-  TR_invariant nmax -∗
-  {{{ is_clock_int n1 ∗ is_clock_int n2 }}}
-  machine_int_add #n1 #n2
-  {{{ RET #(n1+n2) ; is_clock_int (n1+n2) }}}.
-Proof.
-  iIntros "#Htrinv" (Φ) "!# (H1 & H2) Post".
-  iAssert (TR (n1+n2)) with "[H1 H2]" as "H" ; first by (rewrite TR_plus ; iFrame).
-  iDestruct (TR_lt_nmax with "Htrinv H") as ">(H & %)" ; first done.
-  wp_apply (machine_int_add_spec n1 n2 with "[] [H Post]") .
-  {
-    iPureIntro. unfold min_int in *. lia.
-  }
-  {
-    iNext ; iIntros "%". iApply "Post". iFrame "H".
-  }
-Qed.
-
 End clock_int.
 
+(*
+ * A “snapclock integer” (“peano integer” in Clochard’s thesis) is a duplicable
+ * integer which only supports incrementation.
+ *)
+
 Section snapclock_int.
 
-Context `{timeReceiptHeapG Σ}.
-Context (nmax : nat).
-Context `(nmax ≤ max_int).
+  Context `{timeReceiptHeapG Σ}.
+  Context (nmax : nat).
+  Context `(nmax ≤ max_int).
 
-Definition is_snapclock_int (n : nat) : iProp Σ :=
-  TRdup n.
+  Definition is_snapclock_int (n : nat) : iProp Σ :=
+    TRdup n.
 
-  Lemma TRdup_weaken (n₁ n₂ : nat) :
-    (n₂ ≤ n₁)%nat →
-    TRdup n₁ -∗ TRdup n₂.
-  Require Import Auth_mnat.
-  Proof. apply own_auth_mnat_weaken. Qed.
+  (* Snapclock integers are persistent (in particular they are duplicable): *)
+  Lemma snapclock_int_persistent (n : nat) :
+    Persistent (is_snapclock_int n).
+  Proof. exact _. Qed.
 
-  Lemma TRdup_lt_nmax n (E : coPset) :
-    ↑timeReceiptN ⊆ E →
-    TR_invariant nmax -∗ TRdup n ={E}=∗ TRdup n ∗ ⌜n < nmax⌝%nat.
+  (* Snapclock integers support incrementation: *)
+  Lemma snapclock_int_incr_spec n1 :
+    TR_invariant nmax -∗
+    {{{ is_snapclock_int n1 }}}
+    tock #() ;; machine_int_add #n1 #1
+    {{{ RET #(n1+1) ; is_snapclock_int (n1+1) }}}.
   Proof.
-    iIntros (?) "#Inv Hγ1◯".
-    destruct (le_lt_dec nmax n) as [ I | I ] ; last by iFrame.
-    iDestruct (TRdup_weaken n nmax with "Hγ1◯") as "Hγ1◯" ; first done.
-    iDestruct (TRdup_nmax_absurd with "Inv Hγ1◯") as ">?" ; first done.
-    done.
+    iIntros "#Htrinv" (Φ) "!# H1 Post".
+    wp_apply (tock_spec_simple nmax #() with "Htrinv H1"). iIntros "(_ & H)".
+    iDestruct (TRdup_lt_nmax with "Htrinv H") as ">(H & %)" ; first done.
+    wp_seq.
+    wp_apply (machine_int_add_spec n1 1 with "[] [H Post]") .
+    {
+      iPureIntro. unfold min_int in *. lia.
+    }
+    {
+      iNext ; iIntros "%". iApply "Post". iFrame "H".
+    }
   Qed.
 
-Lemma snapclock_int_incr_spec n1 :
-  TR_invariant nmax -∗
-  {{{ is_snapclock_int n1 }}}
-  tock #() ;; machine_int_add #n1 #1
-  {{{ RET #(n1+1) ; is_snapclock_int (n1+1) }}}.
-Proof.
-  iIntros "#Htrinv" (Φ) "!# H1 Post".
-  wp_apply (tock_spec_simple nmax #() with "Htrinv H1"). iIntros "(_ & H)".
-  iDestruct (TRdup_lt_nmax with "Htrinv H") as ">(H & %)" ; first done.
-  wp_seq.
-  wp_apply (machine_int_add_spec n1 1 with "[] [H Post]") .
-  {
-    iPureIntro. unfold min_int in *. lia.
-  }
-  {
-    iNext ; iIntros "%". iApply "Post". iFrame "H".
-  }
-Qed.
-
-Lemma snapclock_int_add_spec n1 n2 m :
-  TR_invariant nmax -∗
-  {{{ is_snapclock_int n1 ∗ is_snapclock_int n2
-    ∗ is_snapclock_int m ∗ ⌜n1+n2 ≤ m⌝ }}}
-  machine_int_add #n1 #n2
-  {{{ RET #(n1+n2) ; is_snapclock_int (n1+n2) }}}.
-Proof.
-  iIntros "#Htrinv" (Φ) "!# (_ & _ & Hm & %) Post".
-  iDestruct (TRdup_lt_nmax with "Htrinv Hm") as ">(Hm & %)" ; first done.
-  iDestruct (TRdup_weaken m (n1 + n2) with "Hm") as "H" ; first lia.
-  wp_apply (machine_int_add_spec n1 n2 with "[] [H Post]") .
-  {
-    iPureIntro. unfold min_int in *. lia.
-  }
-  {
-    iNext ; iIntros "%". iApply "Post". iFrame "H".
-  }
-Qed.
+  (* Snapclock integers also support a limited form of addition: *)
+  Lemma snapclock_int_add_spec n1 n2 m :
+    TR_invariant nmax -∗
+    {{{ is_snapclock_int n1 ∗ is_snapclock_int n2
+      ∗ is_snapclock_int m ∗ ⌜n1+n2 ≤ m⌝ }}}
+    machine_int_add #n1 #n2
+    {{{ RET #(n1+n2) ; is_snapclock_int (n1+n2) }}}.
+  Proof.
+    iIntros "#Htrinv" (Φ) "!# (_ & _ & Hm & %) Post".
+    iDestruct (TRdup_lt_nmax with "Htrinv Hm") as ">(Hm & %)" ; first done.
+    iDestruct (TRdup_weaken m (n1 + n2) with "Hm") as "H" ; first lia.
+    wp_apply (machine_int_add_spec n1 n2 with "[] [H Post]") .
+    {
+      iPureIntro. unfold min_int in *. lia.
+    }
+    {
+      iNext ; iIntros "%". iApply "Post". iFrame "H".
+    }
+  Qed.
 
 End snapclock_int.
\ No newline at end of file

src/TimeReceipts.v

@@ -100,6 +100,11 @@ Section TockSpec.
   Lemma TR_succ n :
     TR (S n) ≡ (TR 1 ∗ TR n)%I.
   Proof. by rewrite (eq_refl : S n = 1 + n)%nat TR_plus. Qed.
+  Lemma TR_weaken (n₁ n₂ : nat) :
+    (n₂ ≤ n₁)%nat →
+    TR n₁ -∗ TR n₂.
+  Require Import Auth_nat.
+  Proof. apply own_auth_nat_weaken. Qed.
 
   Lemma TR_timeless n :
     Timeless (TR n).
@@ -118,6 +123,11 @@ Section TockSpec.
   Lemma TRdup_max m n :
     TRdup (m `max` n) ≡ (TRdup m ∗ TRdup n)%I.
   Proof. by rewrite /TRdup auth_frag_op own_op. Qed.
+  Lemma TRdup_weaken (n₁ n₂ : nat) :
+    (n₂ ≤ n₁)%nat →
+    TRdup n₁ -∗ TRdup n₂.
+  Require Import Auth_mnat.
+  Proof. apply own_auth_mnat_weaken. Qed.
 
   Lemma TRdup_timeless n :
     Timeless (TRdup n).
@@ -164,6 +174,16 @@ Section TockSpec.
     iDestruct (own_auth_nat_le with "Hγ1● Hγ1◯") as %In'.
     exfalso ; lia.
   Qed.
+  Lemma TR_lt_nmax n (E : coPset) :
+    ↑timeReceiptN ⊆ E →
+    TR_invariant -∗ TR n ={E}=∗ TR n ∗ ⌜n < nmax⌝%nat.
+  Proof.
+    iIntros (?) "#Inv Hγ1◯".
+    destruct (le_lt_dec nmax n) as [ I | I ] ; last by iFrame.
+    iDestruct (TR_weaken n nmax with "Hγ1◯") as "Hγ1◯" ; first done.
+    iDestruct (TR_nmax_absurd with "Inv Hγ1◯") as ">?" ; first done.
+    done.
+  Qed.
 
   Lemma TRdup_nmax_absurd (E : coPset) :
     ↑timeReceiptN ⊆ E →
@@ -174,6 +194,16 @@ Section TockSpec.
     iDestruct (own_auth_mnat_le with "Hγ2● Hγ2◯") as %In'.
     exfalso ; lia.
   Qed.
+  Lemma TRdup_lt_nmax n (E : coPset) :
+    ↑timeReceiptN ⊆ E →
+    TR_invariant -∗ TRdup n ={E}=∗ TRdup n ∗ ⌜n < nmax⌝%nat.
+  Proof.
+    iIntros (?) "#Inv Hγ1◯".
+    destruct (le_lt_dec nmax n) as [ I | I ] ; last by iFrame.
+    iDestruct (TRdup_weaken n nmax with "Hγ1◯") as "Hγ1◯" ; first done.
+    iDestruct (TRdup_nmax_absurd with "Inv Hγ1◯") as ">?" ; first done.
+    done.
+  Qed.
 
   Lemma TR_TRdup (E : coPset) n :
     ↑timeReceiptN ⊆ E →