ClockIntegers.v 4.18 KB
Newer Older
MEVEL Glen's avatar
MEVEL Glen committed
1
From stdpp Require Import numbers.
2 3
From iris_time.heap_lang Require Import proofmode notation.
From iris_time Require Import TimeReceipts.
4 5 6

Open Scope Z_scope.

MEVEL Glen's avatar
MEVEL Glen committed
7 8 9 10
(*
 * A “clock integer” (“onetime integer” in Clochard’s thesis) is a non-duplicable
 * integer which supports addition.
 *)
11

MEVEL Glen's avatar
MEVEL Glen committed
12
Section clock_int.
13

MEVEL Glen's avatar
MEVEL Glen committed
14 15
  Context `{timeReceiptHeapG Σ}.
  Context (nmax : nat).
16
  Context `(nmax  max_mach_int).
17

18 19
  Definition is_clock_int (n : Z) : iProp Σ :=
    (0  n  TR (Z.to_nat n))%I.
20

MEVEL Glen's avatar
MEVEL Glen committed
21
  (* Clock integers support addition, which consumes its arguments: *)
22
  Lemma clock_int_add_spec (n1 n2 : mach_int) :
MEVEL Glen's avatar
MEVEL Glen committed
23
    TR_invariant nmax -
24
    {{{ is_clock_int (`n1)  is_clock_int (`n2) }}}
25
    «#n1 + #n2»
26
    {{{ H, RET #(LitMachInt ((`n1+`n2)  H)) ; is_clock_int (`n1+`n2) }}}.
27
  Proof.
28 29 30 31 32 33 34 35 36 37 38
    iIntros "#Htrinv" (Φ) "!# ([% H1] & [% H2]) Post".
    iAssert (TR (Z.to_nat (`n1+`n2))) with "[H1 H2]" as "H".
    { rewrite Z2Nat.inj_add // TR_plus. iFrame. }
    iDestruct (TR_lt_nmax with "Htrinv H") as ">(H & Hnmax)" ; [done|].
    iDestruct "Hnmax" as %Hnmax.
    assert (`n1 + `n2 < max_mach_int).
    { rewrite -(Nat2Z.id nmax) in Hnmax. apply Z2Nat.inj_lt in Hnmax; lia. }
    assert (bool_decide (mach_int_bounded (`n1 + `n2))).
    { apply bool_decide_pack. split; [|done].
      (* FIXME : why isn't lia able to do this directly? *)
      trans 0. unfold min_mach_int; lia. lia. }
39 40
    iDestruct ("Post" with "[H]") as "Post".
    { iIntros "{$H} !%". lia. }
41
    wp_tick_op=>//.
42
    by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left.
43 44 45 46
  Qed.

End clock_int.

MEVEL Glen's avatar
MEVEL Glen committed
47 48 49 50 51
(*
 * A “snapclock integer” (“peano integer” in Clochard’s thesis) is a duplicable
 * integer which only supports incrementation.
 *)

52 53
Section snapclock_int.

MEVEL Glen's avatar
MEVEL Glen committed
54 55
  Context `{timeReceiptHeapG Σ}.
  Context (nmax : nat).
56
  Context `(nmax < max_mach_int).
57

58 59
  Definition is_snapclock_int (n : Z) : iProp Σ :=
    (0  n  TRdup (Z.to_nat n))%I.
60

MEVEL Glen's avatar
MEVEL Glen committed
61
  (* Snapclock integers are persistent (in particular they are duplicable): *)
62
  Lemma snapclock_int_persistent (n : Z) :
MEVEL Glen's avatar
MEVEL Glen committed
63 64
    Persistent (is_snapclock_int n).
  Proof. exact _. Qed.
65

MEVEL Glen's avatar
MEVEL Glen committed
66
  (* Snapclock integers support incrementation: *)
67
  Lemma snapclock_int_incr_spec (n1 : mach_int) :
MEVEL Glen's avatar
MEVEL Glen committed
68
    TR_invariant nmax -
69
    {{{ is_snapclock_int (`n1) }}}
70
    «#n1 + #mach_int_1»
71
    {{{ H, RET #(LitMachInt ((`n1+1)  H)) ; is_snapclock_int (`n1+1) }}}.
72
  Proof.
73
    iIntros "#Htrinv" (Φ) "!# [% H] Post".
74
    iDestruct (TRdup_lt_nmax with "Htrinv H") as ">(H & Hnmax)" ; first done.
75
    iDestruct "Hnmax" as %Hnmax.
76
    assert (`n1 + 1 < max_mach_int).
77
    { rewrite -(Nat2Z.id nmax) in Hnmax. apply Z2Nat.inj_lt in Hnmax; lia. }
78 79 80 81
    assert (bool_decide (mach_int_bounded (`n1 + 1))).
    { apply bool_decide_pack. split; [|done].
      (* FIXME : why isn't lia able to do this directly? *)
      trans 0. unfold min_mach_int; lia. lia. }
82
    wp_tick_op.
83 84
    { by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left. }
    iApply "Post". iSplit. auto with lia.
85
    rewrite Z2Nat.inj_add // Nat.add_comm //.
86 87
  Qed.

MEVEL Glen's avatar
MEVEL Glen committed
88
  (* Snapclock integers also support a limited form of addition: *)
89
  Lemma snapclock_int_add_spec (n1 n2 : mach_int) (m : Z) :
MEVEL Glen's avatar
MEVEL Glen committed
90
    TR_invariant nmax -
91 92
    {{{ is_snapclock_int (`n1)  is_snapclock_int (`n2)
       is_snapclock_int m  ⌜`n1+`n2  m }}}
93
    «#n1 + #n2»
94
    {{{ H, RET #(LitMachInt ((`n1+`n2)  H)) ; is_snapclock_int (`n1+`n2) }}}.
MEVEL Glen's avatar
MEVEL Glen committed
95
  Proof.
96 97 98 99 100 101 102 103 104 105 106
    iIntros "#Htrinv" (Φ) "!# ([% _] & [% _] & [% Hm] & %) Post".
    iDestruct (TRdup_lt_nmax with "Htrinv Hm") as ">(Hm & Hnmax)" ; first done.
    iDestruct "Hnmax" as %Hnmax.
    assert (m < max_mach_int).
    { rewrite -(Nat2Z.id nmax) in Hnmax. apply Z2Nat.inj_lt in Hnmax; lia. }
    iDestruct (TRdup_weaken (Z.to_nat m) (Z.to_nat (`n1 + `n2)) with "Hm") as "H".
    { apply Z2Nat.inj_le; lia. }
    assert (bool_decide (mach_int_bounded (`n1 + `n2))).
    { apply bool_decide_pack. split; [|lia].
      (* FIXME : why isn't lia able to do this directly? *)
      trans 0. unfold min_mach_int; lia. lia. }
107 108
    iDestruct ("Post" with "[H]") as "Post".
    { iSplit; auto with lia. }
109
    wp_tick_op=>//.
110
    by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left.
MEVEL Glen's avatar
MEVEL Glen committed
111
  Qed.
112

113
End snapclock_int.