ClockIntegers.v 4.5 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
From iris.heap_lang Require Import proofmode notation.
Require Import TimeReceipts.
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.

Section machine_int.

Context `{heapG Σ}.

19 20
Definition is_machine_int (n : Z) : iProp Σ :=
  min_int  n < max_int%I.
21 22 23 24 25

Definition machine_int_add : val :=
  λ: "x" "y",
    ("x" + "y" + #max_int) `rem` #max_uint - #max_int.

26 27 28 29
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) }}}.
30
Proof.
31
  iIntros (Φ) "(_ & _ & %) Post". repeat (wp_pure _).
32
  (* boring arithmetic proof: *)
33 34 35 36 37 38 39
  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.
    }
    lia.
40
  }
41
  by iApply "Post".
42 43 44 45 46 47 48 49 50 51
Qed.

End machine_int.

Section clock_int.

Context `{timeReceiptHeapG Σ}.
Context (nmax : nat).
Context `(nmax  max_int).

52 53
Definition is_clock_int (n : nat) : iProp Σ :=
  TR n.
54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71

  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_lt_nmax n (E : coPset) :
    timeReceiptN  E 
    TR_invariant nmax - 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.

72
Lemma clock_int_add_spec n1 n2 :
73
  TR_invariant nmax -
74 75 76
  {{{ is_clock_int n1  is_clock_int n2 }}}
  machine_int_add #n1 #n2
  {{{ RET #(n1+n2) ; is_clock_int (n1+n2) }}}.
77
Proof.
78
  iIntros "#Htrinv" (Φ) "!# (H1 & H2) Post".
79 80
  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.
81
  wp_apply (machine_int_add_spec n1 n2 with "[] [H Post]") .
82
  {
83
    iPureIntro. unfold min_int in *. lia.
84 85
  }
  {
86
    iNext ; iIntros "%". iApply "Post". iFrame "H".
87 88 89 90 91 92 93 94 95 96 97
  }
Qed.

End clock_int.

Section snapclock_int.

Context `{timeReceiptHeapG Σ}.
Context (nmax : nat).
Context `(nmax  max_int).

98 99
Definition is_snapclock_int (n : nat) : iProp Σ :=
  TRdup n.
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117

  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_lt_nmax n (E : coPset) :
    timeReceiptN  E 
    TR_invariant nmax - 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.

118
Lemma snapclock_int_incr_spec n1 :
119
  TR_invariant nmax -
120 121 122
  {{{ is_snapclock_int n1 }}}
  tock #() ;; machine_int_add #n1 #1
  {{{ RET #(n1+1) ; is_snapclock_int (n1+1) }}}.
123
Proof.
124
  iIntros "#Htrinv" (Φ) "!# H1 Post".
125 126 127
  wp_apply (tock_spec_simple nmax #() with "Htrinv H1"). iIntros "(_ & H)".
  iDestruct (TRdup_lt_nmax with "Htrinv H") as ">(H & %)" ; first done.
  wp_seq.
128
  wp_apply (machine_int_add_spec n1 1 with "[] [H Post]") .
129
  {
130
    iPureIntro. unfold min_int in *. lia.
131 132
  }
  {
133
    iNext ; iIntros "%". iApply "Post". iFrame "H".
134 135 136
  }
Qed.

137
Lemma snapclock_int_add_spec n1 n2 m :
138
  TR_invariant nmax -
139 140 141 142
  {{{ 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) }}}.
143
Proof.
144
  iIntros "#Htrinv" (Φ) "!# (_ & _ & Hm & %) Post".
145 146
  iDestruct (TRdup_lt_nmax with "Htrinv Hm") as ">(Hm & %)" ; first done.
  iDestruct (TRdup_weaken m (n1 + n2) with "Hm") as "H" ; first lia.
147
  wp_apply (machine_int_add_spec n1 n2 with "[] [H Post]") .
148
  {
149
    iPureIntro. unfold min_int in *. lia.
150 151
  }
  {
152
    iNext ; iIntros "%". iApply "Post". iFrame "H".
153 154 155 156
  }
Qed.

End snapclock_int.