Commit dabf169f authored by Glen Mével's avatar Glen Mével

implemented Clochard’s integer types

parent 397fbe27
......@@ -86,6 +86,8 @@ Important modules are highlighted.
* `Examples`: a very simple example illustrating the use of time credits to
specify a program with lists
* __`Thunks`: implementation of timed thunks using time credits__
* __`ClockedIntegers`: reconstruction of Clochard’s integer types (`onetime`
and `peano`) using time receipts__
### From the paper to the Coq code
......
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 Σ}.
Definition is_machine_int (v : val) (n : Z) : iProp Σ :=
v = #n min_int n < max_int%I.
Definition machine_int_add : val :=
λ: "x" "y",
("x" + "y" + #max_int) `rem` #max_uint - #max_int.
Lemma machine_int_add_spec v1 n1 v2 n2 :
{{{ is_machine_int v1 n1 is_machine_int v2 n2 min_int n1+n2 < max_int }}}
machine_int_add v1 v2
{{{ v, RET v ; is_machine_int v (n1+n2) }}}.
Proof.
iIntros (Φ) "([->_] & [->_] & %) Post".
repeat (wp_pure _). iApply "Post". iPureIntro.
split ; last done. do 2 f_equal.
(* boring arithmetic proof: *)
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.
Qed.
End machine_int.
Section clock_int.
Context `{timeReceiptHeapG Σ}.
Context (nmax : nat).
Context `(nmax max_int).
Definition is_clock_int (v : val) (n : nat) : iProp Σ :=
(v = #n TR n)%I.
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.
Lemma clock_int_add_spec v1 n1 v2 n2 :
TR_invariant nmax -
{{{ is_clock_int v1 n1 is_clock_int v2 n2 }}}
machine_int_add v1 v2
{{{ v, RET v ; is_clock_int v (n1+n2) }}}.
Proof.
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]") .
{
iSplitR ; last iSplitR ; iPureIntro.
- split ; first done. unfold min_int in *. lia.
- split ; first done. unfold min_int in *. lia.
- unfold min_int in *. lia.
}
{
iNext ; iIntros (v) "[->%]". iApply "Post". iFrame "H".
iPureIntro. do 2 f_equal. lia.
}
Qed.
End clock_int.
Section snapclock_int.
Context `{timeReceiptHeapG Σ}.
Context (nmax : nat).
Context `(nmax max_int).
Definition is_snapclock_int (v : val) (n : nat) : iProp Σ :=
(v = #n TRdup n)%I.
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.
Lemma snapclock_int_incr_spec v1 n1 :
TR_invariant nmax -
{{{ is_snapclock_int v1 n1 }}}
tock #() ;; machine_int_add v1 #1
{{{ v, RET v ; is_snapclock_int v (n1+1) }}}.
Proof.
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.
rewrite (_ : (#n1)%E = of_val (#n1)%V) // ;
rewrite (_ : (#1)%E = of_val (#1)%V) //.
wp_apply (machine_int_add_spec _ n1 _ 1 with "[] [H Post]") .
{
iSplitR ; last iSplitR ; iPureIntro.
- split ; first done. unfold min_int in *. lia.
- split ; first done. done.
- unfold min_int in *. lia.
}
{
iNext ; iIntros (v) "[->%]".
iApply "Post". iFrame "H".
iPureIntro. do 2 f_equal. lia.
}
Qed.
Lemma snapclock_int_add_spec v1 n1 v2 n2 w m :
TR_invariant nmax -
{{{ is_snapclock_int v1 n1 is_snapclock_int v2 n2
is_snapclock_int w m n1+n2 m }}}
machine_int_add v1 v2
{{{ v, RET v ; is_snapclock_int v (n1+n2) }}}.
Proof.
iIntros "#Htrinv" (Φ) "!# ([->H1] & [->H2] & [_ 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]") .
{
iSplitR ; last iSplitR ; iPureIntro.
- split ; first done. unfold min_int in *. lia.
- split ; first done. unfold min_int in *. lia.
- unfold min_int in *. lia.
}
{
iNext ; iIntros (v) "[->%]". iApply "Post". iFrame "H".
iPureIntro. do 2 f_equal. lia.
}
Qed.
End snapclock_int.
\ No newline at end of file
-Q . ""
Auth_mnat.v
Auth_nat.v
ClockIntegers.v
Examples.v
Misc.v
Reduction.v
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment