Skip to content
Snippets Groups Projects
Commit 4522e163 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

notes from meeting'

parent f59d897f
No related branches found
No related tags found
No related merge requests found
...@@ -79,7 +79,7 @@ Section fix_bi. ...@@ -79,7 +79,7 @@ Section fix_bi.
Definition input_loop : expr := Definition input_loop : expr :=
let: "cont" := Alloc #true in let: "cont" := Alloc #true in
while: !"cont" do while: !"cont" do
"cont" <- Call ## "external" #() "cont" <- Call ##"external" #()
od. od.
Lemma val_rel_bool_source v_t b : Lemma val_rel_bool_source v_t b :
...@@ -99,10 +99,11 @@ Section fix_bi. ...@@ -99,10 +99,11 @@ Section fix_bi.
Definition input_rec : ectx := Definition input_rec : ectx :=
λ: "cont", λ: "cont",
if: "cont" then if: "cont" then
let: "cont" := Call ## "external" #() in let: "cont" := Call ##"external" #() in
Call ## "rec" "cont" Call ##"rec" "cont"
else #(). else #().
(* TODO: avoid equalities? *)
Lemma loop_rec : Lemma loop_rec :
"rec" @s input_rec -∗ "rec" @s input_rec -∗
input_loop Call ##"rec" #true {{ val_rel }}. input_loop Call ##"rec" #true {{ val_rel }}.
...@@ -122,4 +123,26 @@ Section fix_bi. ...@@ -122,4 +123,26 @@ Section fix_bi.
- iApply sim_expr_base. iLeft. iExists #(), #(); eauto. - iApply sim_expr_base. iLeft. iExists #(), #(); eauto.
Qed. Qed.
(* TODO: lemma for rec rec *)
(*JAR memory model compcert*)
Lemma loop_rec' :
"rec" @t input_rec -∗
Call ##"rec" #true input_loop {{ val_rel }}.
Proof.
iIntros "#Hs". rewrite /input_loop. source_alloc lc_s as "Hlc_s". sim_pures.
iApply (sim_rec_while _ _ _ _ _ (λ v_t, v_s, val_rel v_t v_s lc_s s v_s)%I with "[Hlc_s] Hs").
{ iExists #true. eauto. }
iModIntro. iIntros (v_t') "He". iDestruct "He" as (v_s) "[Hv Hlc_s]". sim_pures.
source_load.
discr_source.
iIntros ((b & ->)); iPoseProof (val_rel_bool_source with "Hv") as "->"; sim_pures.
destruct b; sim_pures.
- sim_bind (Call _ _) (Call _ _).
iApply sim_wand; first by iApply sim_call.
iIntros (??) "Hv". source_store. sim_pures. iApply sim_expr_base.
iRight. iExists v_t. eauto.
- iApply sim_expr_base. iLeft. iExists #(), #(); eauto.
Qed.
End fix_bi. End fix_bi.
...@@ -296,6 +296,7 @@ Section fix_sim. ...@@ -296,6 +296,7 @@ Section fix_sim.
Since we do not have any means to keep track of this in the simulation relation, this lemma Since we do not have any means to keep track of this in the simulation relation, this lemma
requires to take steps in the beginning, before escaping to the simulation relation again. requires to take steps in the beginning, before escaping to the simulation relation again.
*) *)
(* TODO: differnt symbols for expr thing *)
Lemma sim_lift_coind (inv : expr Λ expr Λ PROP) e_t e_s Φ : Lemma sim_lift_coind (inv : expr Λ expr Λ PROP) e_t e_s Φ :
( e_t e_s P_t P_s σ_t σ_s, ( e_t e_s P_t P_s σ_t σ_s,
inv e_t e_s -∗ state_interp P_t σ_t P_s σ_s ⌜¬ reach_stuck P_s e_s σ_s ==∗ inv e_t e_s -∗ state_interp P_t σ_t P_s σ_s ⌜¬ reach_stuck P_s e_s σ_s ==∗
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment