ClockIntegers.v 2.99 KB
Newer Older
1
From iris.heap_lang Require Import proofmode notation.
2
From iris_time Require Import TimeReceipts MachineIntegers.
3
From stdpp Require Import numbers.
4 5 6

Open Scope Z_scope.

Glen Mével's avatar
Glen Mével committed
7 8 9 10
(*
 * A clock integer (onetime integer in Clochards thesis) is a non-duplicable
 * integer which supports addition.
 *)
11

Glen Mével's avatar
Glen Mével committed
12
Section clock_int.
13

Glen Mével's avatar
Glen Mével committed
14 15 16
  Context `{timeReceiptHeapG Σ}.
  Context (nmax : nat).
  Context `(nmax  max_int).
17

Glen Mével's avatar
Glen Mével committed
18 19
  Definition is_clock_int (n : nat) : iProp Σ :=
    TR n.
20

Glen Mével's avatar
Glen Mével committed
21 22 23 24 25 26
  (* 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) }}}.
27
  Proof.
Glen Mével's avatar
Glen Mével committed
28 29 30 31 32 33 34 35 36 37
    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".
    }
38 39 40 41
  Qed.

End clock_int.

Glen Mével's avatar
Glen Mével committed
42 43 44 45 46
(*
 * A snapclock integer (peano integer in Clochards thesis) is a duplicable
 * integer which only supports incrementation.
 *)

47 48
Section snapclock_int.

Glen Mével's avatar
Glen Mével committed
49 50 51
  Context `{timeReceiptHeapG Σ}.
  Context (nmax : nat).
  Context `(nmax  max_int).
52

Glen Mével's avatar
Glen Mével committed
53 54
  Definition is_snapclock_int (n : nat) : iProp Σ :=
    TRdup n.
55

Glen Mével's avatar
Glen Mével committed
56 57 58 59
  (* Snapclock integers are persistent (in particular they are duplicable): *)
  Lemma snapclock_int_persistent (n : nat) :
    Persistent (is_snapclock_int n).
  Proof. exact _. Qed.
60

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

Glen Mével's avatar
Glen Mével committed
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
  (* 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.
100 101

End snapclock_int.