ClockIntegers.v 4.05 KB
Newer Older
1
From iris.heap_lang Require Import proofmode notation.
2 3
From iris_time Require Import TimeReceipts.
From stdpp Require Import numbers.
4 5 6 7 8 9 10 11

Open Scope Z_scope.

Definition w : nat := 64.
Definition max_int : Z := 1  (w-1).
Definition min_int : Z := - max_int.
Definition max_uint : Z := 2 * max_int.

Glen Mével's avatar
Glen Mével committed
12 13 14 15
(*
 * Bare machine integers can overflow.
 *)

16 17
Section machine_int.

Glen Mével's avatar
Glen Mével committed
18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
  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.
40
    }
Glen Mével's avatar
Glen Mével committed
41 42
    by iApply "Post".
  Qed.
43 44 45

End machine_int.

Glen Mével's avatar
Glen Mével committed
46 47 48 49
(*
 * A “clock integer” (“onetime integer” in Clochard’s thesis) is a non-duplicable
 * integer which supports addition.
 *)
50

Glen Mével's avatar
Glen Mével committed
51
Section clock_int.
52

Glen Mével's avatar
Glen Mével committed
53 54 55
  Context `{timeReceiptHeapG Σ}.
  Context (nmax : nat).
  Context `(nmax  max_int).
56

Glen Mével's avatar
Glen Mével committed
57 58
  Definition is_clock_int (n : nat) : iProp Σ :=
    TR n.
59

Glen Mével's avatar
Glen Mével committed
60 61 62 63 64 65
  (* 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) }}}.
66
  Proof.
Glen Mével's avatar
Glen Mével committed
67 68 69 70 71 72 73 74 75 76
    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".
    }
77 78 79 80
  Qed.

End clock_int.

Glen Mével's avatar
Glen Mével committed
81 82 83 84 85
(*
 * A “snapclock integer” (“peano integer” in Clochard’s thesis) is a duplicable
 * integer which only supports incrementation.
 *)

86 87
Section snapclock_int.

Glen Mével's avatar
Glen Mével committed
88 89 90
  Context `{timeReceiptHeapG Σ}.
  Context (nmax : nat).
  Context `(nmax  max_int).
91

Glen Mével's avatar
Glen Mével committed
92 93
  Definition is_snapclock_int (n : nat) : iProp Σ :=
    TRdup n.
94

Glen Mével's avatar
Glen Mével committed
95 96 97 98
  (* Snapclock integers are persistent (in particular they are duplicable): *)
  Lemma snapclock_int_persistent (n : nat) :
    Persistent (is_snapclock_int n).
  Proof. exact _. Qed.
99

Glen Mével's avatar
Glen Mével committed
100 101 102 103 104 105
  (* 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) }}}.
106
  Proof.
Glen Mével's avatar
Glen Mével committed
107 108 109 110 111 112 113 114 115 116 117
    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".
    }
118 119
  Qed.

Glen Mével's avatar
Glen Mével committed
120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
  (* 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.
139 140

End snapclock_int.