WIP: frame

theories/sim/one_step.v

@@ -57,16 +57,27 @@ Qed.
 Lemma sim_body_frame fs ft n rf r es σs et σt Φ :
   r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ →
   rf ⋅ r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) :
-    (λ r' n' es' σs' et' σt', ∃ r0, r' = rf ⋅ r0 ∧ Φ r0 n' es' σs' et' σt').
+    (λ r' n' es' σs' et' σt', ∃ r0, r' ≡ rf ⋅ r0 ∧ Φ r0 n' es' σs' et' σt').
 Proof.
   revert n rf r es σs et σt Φ. pcofix CIH.
   intros n rf r0 es σs et σt Φ SIM.
   pfold. punfold SIM.
   intros NT r_f. rewrite cmra_assoc. intros WSAT.
   specialize (SIM NT _ WSAT) as [SU TE ST]. split; [done|..].
-  - intros. destruct (TE _ TERM) as (vs' & σs' & r' & idx' & STEP' & WSAT' & POST).
-    exists vs', σs', (rf ⋅ r'), idx'. admit.
-  - admit.
+  { intros. destruct (TE _ TERM) as (vs' & σs' & r' & idx' & STEP' & WSAT' & POST).
+    exists vs', σs', (rf ⋅ r'), idx'.
+    split; last split; [done|by rewrite cmra_assoc|by exists r']. }
+  inversion ST.
+  - constructor 1. intros.
+    specialize (STEP _ _ STEPT) as (es' & σs' & r' & idx' & STEPS' & WSAT' & SIM').
+    exists es', σs', (rf ⋅ r'), idx'.
+    split; last split; [done|by rewrite cmra_assoc|].
+    pclearbot. right. by apply CIH.
+  - econstructor 2; eauto.
+    { instantiate (1:= (rf ⋅ rc)). by rewrite -cmra_assoc (cmra_assoc r_f). }
+    intros.
+    specialize (CONT _ _ _ σs' σt' VRET STACK) as [idx' SIM'].
+    exists idx'. pclearbot. right. Fail apply CIH.
 Abort.
 
 Lemma sim_body_result fs ft r n es et σs σt Φ :