Smarter mixed simulation

[alxest]

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.

[alxest]

Such "refresh"ability is useful in the following scenario. We define simulation primitive as follows in SimSIR.v:

| sim_st_choose_src
    X_src
    k_src i_tgt
    (SIM: exists x_src, sim_st (k_src x_src) i_tgt)
  :
    _sim_st sim_st
            (Vis (subevent _ (EChoose X_src)) k_src)
            (i_tgt)
| sim_st_choose_tgt
    X_tgt
    k_tgt i_src
    (INHAB: inhabited X_tgt)
    (SIM: forall x_tgt, sim_st i_src (k_tgt x_tgt))
  :
    _sim_st sim_st
            (i_src)
            (Vis (subevent _ (EChoose X_tgt)) k_tgt)
[[SIMULATION INDEXES OMITTED]]

and by composing them, I would also like to simulate "choose_both" case, like:

            (Vis (subevent _ (EChoose X)) k_src)
            (Vis (subevent _ (EChoose X)) k_tgt)

[alxest]

About future sim --> maybe just lexicographic order would suffice. Recall f2b simulation.