ClockIntegers.v 4.23 KB
Newer Older
1 2
From iris_time.heap_lang Require Import proofmode notation.
From iris_time Require Import TimeReceipts.
3
From stdpp Require Import numbers.
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 25 26
    {{{ is_clock_int (`n1)  is_clock_int (`n2) }}}
    #n1 + #n2
    {{{ H, RET #(LitMachInt ((`n1+`n2)  H)) ; is_clock_int (`n1+`n2) }}}.
27
  Proof.
28 29 30 31 32 33 34 35 36 37 38 39 40 41
    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. }
    wp_op.
    { by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left. }
    iApply "Post". iIntros "{$H} /= !%". lia.
42 43 44 45
  Qed.

End clock_int.

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

51 52
Section snapclock_int.

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

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

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

MEVEL Glen's avatar
MEVEL Glen committed
65
  (* Snapclock integers support incrementation: *)
66
  Lemma snapclock_int_incr_spec (n1 : mach_int) :
MEVEL Glen's avatar
MEVEL Glen committed
67
    TR_invariant nmax -
68 69 70
    {{{ is_snapclock_int (`n1) }}}
    tick #() ;; #n1 + #mach_int_1
    {{{ H, RET #(LitMachInt ((`n1+1)  H)) ; is_snapclock_int (`n1+1) }}}.
71
  Proof.
72
    iIntros "#Htrinv" (Φ) "!# [% H1] Post".
73
    wp_apply (tick_spec_simple nmax #() with "Htrinv H1"). iIntros "(_ & H)".
74 75 76 77 78 79 80 81 82 83 84 85 86
    iDestruct (TRdup_lt_nmax with "Htrinv H") as ">(H & Hnmax)" ; first done.
    iDestruct "Hnmax" as %Hnmax. wp_seq.
    assert (`n1 + 1 < max_mach_int).
    { rewrite -(Nat2Z.id nmax) (_:1%nat = Z.to_nat 1) // -Z2Nat.inj_add // in Hnmax.
      apply Z2Nat.inj_lt in Hnmax; lia. }
    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. }
    wp_op.
    { by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left. }
    iApply "Post". iSplit. auto with lia.
    by rewrite Z2Nat.inj_add //.
87 88
  Qed.

MEVEL Glen's avatar
MEVEL Glen committed
89
  (* Snapclock integers also support a limited form of addition: *)
90
  Lemma snapclock_int_add_spec (n1 n2 : mach_int) (m : Z) :
MEVEL Glen's avatar
MEVEL Glen committed
91
    TR_invariant nmax -
92 93 94 95
    {{{ is_snapclock_int (`n1)  is_snapclock_int (`n2)
       is_snapclock_int m  ⌜`n1+`n2  m }}}
    #n1 + #n2
    {{{ H, RET #(LitMachInt ((`n1+`n2)  H)) ; is_snapclock_int (`n1+`n2) }}}.
MEVEL Glen's avatar
MEVEL Glen committed
96
  Proof.
97 98 99 100 101 102 103 104 105 106 107 108 109 110
    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. }
    wp_op.
    { by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left. }
    iApply "Post". iSplit; [|done]. auto with lia.
MEVEL Glen's avatar
MEVEL Glen committed
111
  Qed.
112

113
End snapclock_int.