Commit cd7f2ee5 authored by Léon Gondelman 's avatar Léon Gondelman

cbv_of_args

parent 7b59d2c8
From iris_c.vcgen Require Import proofmode.
Section Incr_Ptr.
(* In the program below, after the execution of 'main',
the global pointer 'l' has the value 43. *)
(* // C
void incr(int* x) {
*x = *x + 1;
}
int* l = 42;
int main() {
incr(&l);
return 0
}
*)
(* // λMC (paper version)
incr(x) {
*x = *x + 1;
}
l <- alloc 42;
main() {
incr(l);
0;
}
*)
Let incr : val := λᶜ "x",
(c_ret "x") = ∗ᶜ (c_ret "x") + 1 ; ().
Let main : val := λᶜ "()",
"r" ←ᶜ alloc (1, 42) ;
call (c_ret incr) (c_ret "r") ;
0.
Let main_spec `{cmonadG Σ} :
CWP main #() {{ v, v = #0 ptr, ptr C #43%nat }}%I.
Proof.
iIntros.
iApply cwp_fun; simpl.
vcg.
iIntros (ptr) "_ _ Hptr !> _ !>".
iApply cwp_fun; simpl.
vcg.
iIntros "Hptr !>". iSplit; eauto.
vcg_continue.
eauto with iFrame.
Qed.
End Incr_Ptr.
Section Incr_Int.
(* In the program below, after the execution of 'main',
the global pointer 'l' has the value 42. *)
(* // C
void incr(int x) {
x = x + 1;
}
int* l = 42;
int main() {
incr(l);
return 0
}
*)
(* // λMC (paper version)
incr(x) {
r <- alloc x ;
*r = *r + 1;
}
l <- alloc 42 ;
main() {
incr(∗l);
0
}
*)
Let incr : val := λᶜ "x",
"r" mut (c_ret "x") ;
(c_ret "r") = ∗ᶜ (c_ret "r") + 1 ; ().
Let main : val := λᶜ "()",
"r" ←ᶜ alloc (1, 42) ;
call (c_ret incr) ( ∗ᶜ c_ret "r") ;
0.
Let main_spec `{cmonadG Σ} :
CWP main #() {{ v, v = #0 ptr, ptr C #42%nat }}%I.
Proof.
iIntros.
iApply cwp_fun; simpl.
vcg.
iIntros (ptr) "_ _ Hptr !> _ !>".
iApply cwp_fun; simpl.
vcg.
iIntros (?) "Hptr !>". iSplit; eauto.
vcg_continue.
eauto with iFrame.
Qed.
\ No newline at end of file
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