Commit f23eb72c authored by Hai Dang's avatar Hai Dang


parent ee56df0d
......@@ -170,7 +170,7 @@ Proof.
apply POST; eauto.
Lemma sim_body_alloc_shared fs ft r n T σs σt Φ :
Lemma sim_body_alloc_public fs ft r n T σs σt Φ :
let l := (fresh_block σt.(shp), 0) in
let t := (Tagged σt.(snp)) in
let σs' := mkState (init_mem l (tsize T) σs.(shp))
......@@ -325,7 +325,7 @@ Lemma sim_simple_alloc_public fs ft r n T css cst Φ :
Φ (r rt) n (PlaceR l (Tagged tg) T) css (PlaceR l (Tagged tg) T) cst)
r ⊨ˢ{n,fs,ft} (Alloc T, css) (Alloc T, cst) : Φ.
intros HH σs σt <-<-. apply sim_body_alloc_shared=>/=. exact: HH.
intros HH σs σt <-<-. apply sim_body_alloc_public=>/=. exact: HH.
Lemma sim_simple_write_public fs ft r n (rs1 rs2 rt1 rt2: result) css cst Φ :
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