Problem
If we prove simulation as follows,
src 1 step && tgt 0 step (bsim, or fsim_self_stutter)
src 0 step && tgt 1 step (fsim, or bsim_self_stutter)
current simulation definition does not allow us to refresh the index.
However, src/tgt together made the progress, so we should be able to refresh the index.
Solution
Adopting the idea from gpaco, we can generalize the simulation with additional parameters: gs gt: bool.
gs/gt means whether src/tgt is guarded: it is guarded if it haven't took a step since last refresh, and unguarded otherwise.
Then, we can relax the simulation definition as follows:
Inductive fsim_step xsim (gs gt: bool) (i0: index) (st_src0: L1.(state)) (st_tgt0: L2.(state)): Prop :=
| fsim_step_step
(mt: match_traces)
(STEP: forall st_src1 tr
(STEPSRC: Step L1 st_src0 tr st_src1),
exists i1 st_tgt1,
((<<PLUS: DPlus mt L2 st_tgt0 tr st_tgt1 /\ (<<RECEPTIVE: receptive_at mt L1 st_src0>>)>>) \/
<<STUTTER: st_tgt0 = st_tgt1 /\ tr = E0 /\ order i1 i0>>)
/\ <<XSIM: xsim false gt i1 st_src1 st_tgt1>>)
(*** NOTE: if needed, we can do it smarter: when tgt took a step, unguard gt ***)
(FINAL: forall retv
(FINALSRC: final_state L1 st_src0 retv),
<<FINALTGT: Dfinal_state L2 st_tgt0 retv>>)
| fsim_step_stutter
i1 st_tgt1
(PLUS: SDPlus L2 st_tgt0 nil st_tgt1 /\ order i1 i0)
(XSIM: xsim gs false i1 st_src0 st_tgt1)
| fsim_step_step_ug
(mt: match_traces)
(UNGUARDED: ~gs)
(STEP: forall st_src1 tr
(STEPSRC: Step L1 st_src0 tr st_src1),
exists i1 st_tgt1,
(<<STUTTER: st_tgt0 = st_tgt1 /\ tr = E0>>)
/\ <<XSIM: xsim true true i1 st_src1 st_tgt1>>)
(FINAL: forall retv
(FINALSRC: final_state L1 st_src0 retv),
<<FINALTGT: Dfinal_state L2 st_tgt0 retv>>)
| fsim_step_stutter_ug
i1 st_tgt1
(UNGUARDED: ~gs)
(PLUS: SDPlus L2 st_tgt0 nil st_tgt1)
(XSIM: xsim true true i1 st_src0 st_tgt1)
(** NOTE: If needed, we can do it smarter:
when SDPlus took >= 2 steps, we can unguard tgt again **)
.
(bsim, sfsim are omitted)
Note: proving the soundness might require future-aware simulation. To be more specific, proving soundness transitively "xsim => bsim => adequacy" might && proving directly (xsim => adequacy) might not.
Problem
If we prove simulation as follows,
current simulation definition does not allow us to refresh the index.
However, src/tgt together made the progress, so we should be able to refresh the index.
Solution
Adopting the idea from gpaco, we can generalize the simulation with additional parameters:
gs gt: bool.gs/gt means whether src/tgt is guarded: it is guarded if it haven't took a step since last refresh, and unguarded otherwise.
Then, we can relax the simulation definition as follows:
(bsim, sfsim are omitted)
Note: proving the soundness might require future-aware simulation. To be more specific, proving soundness transitively "xsim => bsim => adequacy" might && proving directly (xsim => adequacy) might not.