Commit 78a6143e authored by Hai Dang's avatar Hai Dang
Browse files

fix syntactic condition on lookup of function tables

parent 8814e3ea
......@@ -136,6 +136,11 @@ Definition sim_local_funs (esat: A → call_id → Prop) : Prop :=
length fn_src.(fun_b) = length fn_tgt.(fun_b)
sim_local_fun esat fn_src fn_tgt.
Definition sim_local_funs_lookup : Prop :=
name fn_src, fns !! name = Some fn_src fn_tgt,
fnt !! name = Some fn_tgt
length fn_src.(fun_b) = length fn_tgt.(fun_b).
End local.
Hint Resolve sim_local_body_mono : paco.
......@@ -26,7 +26,8 @@ Proof.
- econs 1.
- ss.
- ss.
- eapply (sim_body_step_over_call _ _ init_res ε _ _ [] []); [done..|].
- eapply (sim_body_step_over_call _ _ init_res ε _ _ [] []); [done|..].
{ intros fid fn_src. specialize (FUNS fid fn_src). naive_solver. }
intros. simpl. exists 1%nat.
apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)).
intros VALID.
......
......@@ -1153,7 +1153,7 @@ Qed.
Lemma sim_body_step_over_call fs ft
rc rv n fid vls vlt σs σt Φ
(VREL: Forall2 (vrel rv) vls vlt)
(FUNS: sim_local_funs wsat vrel fs ft end_call_sat) :
(FUNS: sim_local_funs_lookup fs ft) :
( r' vs vt σs' σt' (VRET: vrel r' vs vt)
(STACKS: σs.(scs) = σs'.(scs))
(STACKT: σt.(scs) = σt'.(scs)), n',
......@@ -1166,7 +1166,7 @@ Proof.
apply tstep_call_inv in RED; last first.
{ apply list_Forall_to_value. eauto. }
destruct RED as (xls & ebs & HCs & ebss & Eqfs & Eqss & ? & ?). subst e2 σ2.
destruct (FUNS _ _ Eqfs) as ([xlt ebt HCt] & Eqft & Eql & SIMf).
destruct (FUNS _ _ Eqfs) as ([xlt ebt HCt] & Eqft & Eql).
simpl in Eql.
destruct (subst_l_is_Some xlt (Val <$> vlt) ebt) as [est Eqst].
{ rewrite fmap_length -(Forall2_length _ _ _ VREL) -Eql
......
......@@ -104,7 +104,7 @@ Qed.
(* [Val <$> _] in the goal makes this not work with [apply], but
we'd need tactic support for anything better. *)
Lemma sim_simple_call n' vls vlt rv fs ft r r' n fid css cst Φ :
sim_local_funs wsat vrel fs ft end_call_sat
sim_local_funs_lookup fs ft
Forall2 (vrel rv) vls vlt
r r' rv
( rret vs vt, vrel rret vs vt
......
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