path: root/scheduling/BTL_SEtheory.v

(* A theory of symbolic execution on BTL

NB: an efficient implementation with hash-consing will be defined in another file (some day)

*)

Require Import Coqlib Maps Floats.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL BTL OptionMonad.

(* TODO remove this, when copy-paste of RTLpathSE_theory is clearly over... *)
Ltac inversion_SOME := fail.  (* deprecated tactic of OptionMonad: use autodestruct instead *)
Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *)


Record iblock_exec_context := {
  cge: BTL.genv;
  csp: val;
  cstk: list stackframe;
  cf: function;
  crs0: regset;
  cm0: mem
}.

(** * Syntax and semantics of symbolic values *)

(* symbolic value *)
Inductive sval :=
  | Sinput (r: reg)
  | Sop (op:operation) (lsv: list_sval)  (sm: smem)
  | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) 
with list_sval := 
  | Snil
  | Scons (sv: sval) (lsv: list_sval)
(* symbolic memory *)
with smem :=
  | Sinit 
  | Sstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval).

Scheme sval_mut := Induction for sval Sort Prop
with list_sval_mut := Induction for list_sval Sort Prop
with smem_mut := Induction for smem Sort Prop.

Fixpoint list_sval_inj (l: list sval): list_sval :=
  match l with
  | nil => Snil
  | v::l => Scons v (list_sval_inj l)
  end.

Local Open Scope option_monad_scope.

Fixpoint eval_sval ctx (sv: sval): option val :=
  match sv with
  | Sinput r => Some ((crs0 ctx)#r)
  | Sop op l sm =>
     SOME args <- eval_list_sval ctx l IN
     SOME m <- eval_smem ctx sm IN
     eval_operation (cge ctx) (csp ctx) op args m
  | Sload sm trap chunk addr lsv =>
      match trap with
      | TRAP =>
          SOME args <- eval_list_sval ctx lsv IN
          SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN
          SOME m <- eval_smem ctx sm IN
          Mem.loadv chunk m a
      | NOTRAP =>
          SOME args <- eval_list_sval ctx lsv IN
          match (eval_addressing (cge ctx) (csp ctx) addr args) with
          | None => Some (default_notrap_load_value chunk)
          | Some a =>
              SOME m <- eval_smem ctx sm IN
              match (Mem.loadv chunk m a) with
              | None => Some (default_notrap_load_value chunk)
              | Some val => Some val
              end
          end
      end
  end
with eval_list_sval ctx (lsv: list_sval): option (list val) :=
  match lsv with
  | Snil => Some nil
  | Scons sv lsv' => 
    SOME v <- eval_sval ctx sv IN
    SOME lv <- eval_list_sval ctx lsv' IN
    Some (v::lv)
  end
with eval_smem ctx (sm: smem): option mem :=
  match sm with
  | Sinit => Some (cm0 ctx)
  | Sstore sm chunk addr lsv srce =>
     SOME args <- eval_list_sval ctx lsv IN
     SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN
     SOME m <- eval_smem ctx sm IN
     SOME sv <- eval_sval ctx srce IN
     Mem.storev chunk m a sv
  end.

Lemma eval_list_sval_inj ctx l (sreg: reg -> sval) rs: 
  (forall r : reg, eval_sval ctx (sreg r) = Some (rs # r)) ->
  eval_list_sval ctx (list_sval_inj (map sreg l)) = Some (rs ## l).
Proof.
  intros H; induction l as [|r l]; simpl; repeat autodestruct; auto.
Qed.

Definition seval_condition ctx (cond: condition) (lsv: list_sval) (sm: smem) : option bool :=
  SOME args <- eval_list_sval ctx lsv IN
  SOME m <- eval_smem ctx sm IN
  eval_condition cond args m.


(** * Auxiliary definitions on Builtins *)
(* TODO: clean this. Some (cge ctx)neric stuffs could be put in [AST.v] *)

Section SEVAL_BUILTIN_ARG. (* adapted from Events.v *)

Variable ctx: iblock_exec_context.
Variable m: mem.

Inductive seval_builtin_arg: builtin_arg sval -> val -> Prop :=
  | seval_BA: forall x v,
      eval_sval ctx x = Some v ->
      seval_builtin_arg (BA x) v
  | seval_BA_int: forall n,
      seval_builtin_arg (BA_int n) (Vint n)
  | seval_BA_long: forall n,
      seval_builtin_arg (BA_long n) (Vlong n)
  | seval_BA_float: forall n,
      seval_builtin_arg (BA_float n) (Vfloat n)
  | seval_BA_single: forall n,
      seval_builtin_arg (BA_single n) (Vsingle n)
  | seval_BA_loadstack: forall chunk ofs v,
      Mem.loadv chunk m (Val.offset_ptr (csp ctx) ofs) = Some v ->
      seval_builtin_arg (BA_loadstack chunk ofs) v
  | seval_BA_addrstack: forall ofs,
      seval_builtin_arg (BA_addrstack ofs) (Val.offset_ptr (csp ctx) ofs)
  | seval_BA_loadglobal: forall chunk id ofs v,
      Mem.loadv chunk m (Senv.symbol_address (cge ctx) id ofs) = Some v ->
      seval_builtin_arg (BA_loadglobal chunk id ofs) v
  | seval_BA_addrglobal: forall id ofs,
      seval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address (cge ctx) id ofs)
  | seval_BA_splitlong: forall hi lo vhi vlo,
      seval_builtin_arg hi vhi -> seval_builtin_arg lo vlo ->
      seval_builtin_arg (BA_splitlong hi lo) (Val.longofwords vhi vlo)
  | seval_BA_addptr: forall a1 a2 v1 v2,
      seval_builtin_arg a1 v1 -> seval_builtin_arg a2 v2 ->
      seval_builtin_arg (BA_addptr a1 a2)
                       (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2)
.

Definition seval_builtin_args (al: list (builtin_arg sval)) (vl: list val) : Prop :=
  list_forall2 seval_builtin_arg al vl.

Lemma seval_builtin_arg_determ:
  forall a v, seval_builtin_arg a v -> forall v', seval_builtin_arg a v' -> v' = v.
Proof.
  induction 1; intros v' EV; inv EV; try congruence.
  f_equal; eauto.
  apply IHseval_builtin_arg1 in H3. apply IHseval_builtin_arg2 in H5. subst; auto. 
Qed.

Lemma eval_builtin_args_determ:
  forall al vl, seval_builtin_args al vl -> forall vl', seval_builtin_args al vl' -> vl' = vl.
Proof.
  induction 1; intros v' EV; inv EV; f_equal; eauto using seval_builtin_arg_determ.
Qed.

End SEVAL_BUILTIN_ARG.

(* NB: (cge ctx)neric function that could be put into [AST] file *)
Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B :=
  match arg with
  | BA x => BA (f x)
  | BA_int n => BA_int n
  | BA_long n => BA_long n
  | BA_float f => BA_float f
  | BA_single s => BA_single s
  | BA_loadstack chunk ptr => BA_loadstack chunk ptr
  | BA_addrstack ptr => BA_addrstack ptr
  | BA_loadglobal chunk id ptr => BA_loadglobal chunk id ptr
  | BA_addrglobal id ptr => BA_addrglobal id ptr
  | BA_splitlong ba1 ba2 => BA_splitlong (builtin_arg_map f ba1) (builtin_arg_map f ba2)
  | BA_addptr ba1 ba2 => BA_addptr (builtin_arg_map f ba1) (builtin_arg_map f ba2)
  end.

Lemma seval_builtin_arg_correct ctx rs m sreg: forall arg varg,
  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
  eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg ->
  seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg.
Proof.
  induction arg.
  all: try (intros varg SEVAL BARG; inv BARG; constructor; congruence).
  - intros varg SEVAL BARG. inv BARG. simpl. constructor.
    eapply IHarg1; eauto. eapply IHarg2; eauto.
  - intros varg SEVAL BARG. inv BARG. simpl. constructor.
    eapply IHarg1; eauto. eapply IHarg2; eauto.
Qed.

Lemma seval_builtin_args_correct ctx rs m sreg args vargs:
  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
  eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs ->
  seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs.
Proof.
  induction 2.
  - constructor.
  - simpl. constructor; [| assumption].
    eapply seval_builtin_arg_correct; eauto.
Qed.

Lemma seval_builtin_arg_complete ctx rs m sreg: forall arg varg,
  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
  seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg ->
  eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg.
Proof.
  induction arg.
  all: intros varg SEVAL BARG; try (inv BARG; constructor; congruence).
  - inv BARG. rewrite SEVAL in H0. inv H0. constructor.
  - inv BARG. simpl. constructor.
    eapply IHarg1; eauto. eapply IHarg2; eauto.
  - inv BARG. simpl. constructor.
    eapply IHarg1; eauto. eapply IHarg2; eauto.
Qed.

Lemma seval_builtin_args_complete ctx rs m sreg: forall args vargs,
  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
  seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs ->
  eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs.
Proof.
  induction args.
  - simpl. intros. inv H0. constructor.
  - intros vargs SEVAL BARG. simpl in BARG. inv BARG.
    constructor; [| eapply IHargs; eauto].
    eapply seval_builtin_arg_complete; eauto.
Qed.

Fixpoint seval_builtin_sval ctx bsv :=
  match bsv with
  | BA sv => SOME v <- eval_sval ctx sv IN Some (BA v)
  | BA_splitlong sv1 sv2 =>
      SOME v1 <- seval_builtin_sval ctx sv1 IN
      SOME v2 <- seval_builtin_sval ctx sv2 IN
      Some (BA_splitlong v1 v2)
  | BA_addptr sv1 sv2 =>
      SOME v1 <- seval_builtin_sval ctx sv1 IN
      SOME v2 <- seval_builtin_sval ctx sv2 IN
      Some (BA_addptr v1 v2)
  | BA_int i => Some (BA_int i)
  | BA_long l => Some (BA_long l)
  | BA_float f => Some (BA_float f)
  | BA_single s => Some (BA_single s)
  | BA_loadstack chk ptr => Some (BA_loadstack chk ptr)
  | BA_addrstack ptr => Some (BA_addrstack ptr)
  | BA_loadglobal chk id ptr => Some (BA_loadglobal chk id ptr)
  | BA_addrglobal id ptr => Some (BA_addrglobal id ptr)
  end.

Fixpoint eval_list_builtin_sval ctx lbsv :=
  match lbsv with
  | nil => Some nil
  | bsv::lbsv => SOME v <- seval_builtin_sval ctx bsv IN
                 SOME lv <- eval_list_builtin_sval ctx lbsv IN
                 Some (v::lv)
  end.

Lemma eval_list_builtin_sval_nil ctx lbs2:
  eval_list_builtin_sval ctx lbs2 = Some nil ->
  lbs2 = nil.
Proof.
  destruct lbs2; simpl; repeat autodestruct; congruence.
Qed.

Lemma seval_builtin_sval_arg ctx bs:
   forall ba m v, 
   seval_builtin_sval ctx bs = Some ba ->
   eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v ->
   seval_builtin_arg ctx m bs v.
Proof.
   induction bs; simpl; 
   try (intros ba m v H; inversion H; subst; clear H;
        intros H; inversion H; subst;
        econstructor; auto; fail).
   - intros ba m v; destruct (eval_sval _ _) eqn: SV;
     intros H; inversion H; subst; clear H.
     intros H; inversion H; subst.
     econstructor; auto.
   - intros ba m v. 
     destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence.
     destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence.
     intros H; inversion H; subst; clear H.
     intros H; inversion H; subst.
     econstructor; eauto.
   - intros ba m v. 
     destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence.
     destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence.
     intros H; inversion H; subst; clear H.
     intros H; inversion H; subst.
     econstructor; eauto.
Qed.

Lemma seval_builtin_arg_sval ctx m v: forall bs,
  seval_builtin_arg ctx m bs v ->
  exists ba,
    seval_builtin_sval ctx bs = Some ba
    /\ eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v.
Proof.
  induction 1.
  all: try (eexists; constructor; [simpl; reflexivity | constructor]).
  2-3: try assumption.
  - eexists. constructor.
    + simpl. rewrite H. reflexivity.
    + constructor.
  - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1).
    destruct IHseval_builtin_arg2 as (ba2 & A2 & B2).
    eexists. constructor.
    + simpl. rewrite A1. rewrite A2. reflexivity.
    + constructor; assumption. 
  - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1).
    destruct IHseval_builtin_arg2 as (ba2 & A2 & B2).
    eexists. constructor.
    + simpl. rewrite A1. rewrite A2. reflexivity.
    + constructor; assumption.
Qed.

Lemma seval_builtin_sval_args ctx lbs:
   forall lba m v, 
   eval_list_builtin_sval ctx lbs = Some lba ->
   list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba v ->
   seval_builtin_args ctx m lbs v.
Proof.
  unfold seval_builtin_args; induction lbs; simpl; intros lba m v.
  - intros H; inversion H; subst; clear H.
    intros H; inversion H. econstructor.
  - destruct (seval_builtin_sval _ _) eqn:SV; try congruence.
    destruct (eval_list_builtin_sval _ _) eqn: SVL; try congruence.
    intros H; inversion H; subst; clear H.
    intros H; inversion H; subst; clear H. 
    econstructor; eauto.
    eapply seval_builtin_sval_arg; eauto.
Qed.

Lemma seval_builtin_args_sval ctx m lv: forall lbs,
  seval_builtin_args ctx m lbs lv ->
  exists lba,
    eval_list_builtin_sval ctx lbs = Some lba
    /\ list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba lv.
Proof.
  induction 1.
  - eexists. constructor.
    + simpl. reflexivity.
    + constructor.
  - destruct IHlist_forall2 as (lba & A & B).
    apply seval_builtin_arg_sval in H. destruct H as (ba & A' & B').
    eexists. constructor.
    + simpl. rewrite A'. rewrite A. reflexivity.
    + constructor; assumption.
Qed.

Lemma seval_builtin_sval_correct ctx m: forall bs1 v bs2,
  seval_builtin_arg ctx m bs1 v ->
  (seval_builtin_sval ctx bs1) = (seval_builtin_sval ctx bs2) ->
  seval_builtin_arg ctx m bs2 v.
Proof.
  intros. exploit seval_builtin_arg_sval; eauto.
  intros (ba & X1 & X2).
  eapply seval_builtin_sval_arg; eauto.
  congruence.
Qed.

Lemma eval_list_builtin_sval_correct ctx m vargs: forall lbs1,
  seval_builtin_args ctx m lbs1 vargs ->
  forall lbs2, (eval_list_builtin_sval ctx lbs1) = (eval_list_builtin_sval ctx lbs2) ->
  seval_builtin_args ctx m lbs2 vargs.
Proof.
  intros. exploit seval_builtin_args_sval; eauto.
  intros (ba & X1 & X2).
  eapply seval_builtin_sval_args; eauto.
  congruence.
Qed.

(** * Symbolic (final) value of a block *)

Inductive sfval :=
  | Sgoto (pc: exit)
  | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:exit)
    (* NB: [res] the return register is hard-wired ! Is it restrictive ? *)
  | Stailcall: signature -> sval + ident -> list_sval -> sfval
  | Sbuiltin (ef:external_function) (sargs: list (builtin_arg sval)) (res: builtin_res reg) (pc:exit)
  | Sjumptable (sv: sval) (tbl: list exit)
  | Sreturn: option sval -> sfval
.

Definition sfind_function ctx (svos : sval + ident): option fundef :=
  match svos with
  | inl sv => SOME v <- eval_sval ctx sv IN Genv.find_funct (cge ctx) v
  | inr symb => SOME b <- Genv.find_symbol (cge ctx) symb IN Genv.find_funct_ptr (cge ctx) b
  end
.

Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop :=
  | exec_Sgoto pc rs m:
      sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc rs m)
  | exec_Sreturn stk osv rs m m' v:
      (csp ctx) = (Vptr stk Ptrofs.zero) ->
      Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' ->
      match osv with Some sv => eval_sval ctx sv | None => Some Vundef end = Some v ->
      sem_sfval ctx (Sreturn osv) rs m 
         E0 (Returnstate (cstk ctx) v m')
  | exec_Scall rs m sig svos lsv args res pc fd:
      sfind_function ctx svos = Some fd ->
      funsig fd = sig ->
      eval_list_sval ctx lsv = Some args ->
      sem_sfval ctx (Scall sig svos lsv res pc) rs m
        E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc rs :: (cstk ctx)) fd args m)
  | exec_Stailcall stk rs m sig svos args fd m' lsv:
      sfind_function ctx svos = Some fd ->
      funsig fd = sig ->
      (csp ctx) = Vptr stk Ptrofs.zero ->
      Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' ->
      eval_list_sval ctx lsv = Some args ->
      sem_sfval ctx (Stailcall sig svos lsv) rs m
        E0 (Callstate (cstk ctx) fd args m')
  | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs:
      seval_builtin_args ctx m sargs vargs ->
      external_call ef (cge ctx) vargs m t vres m' ->
      sem_sfval ctx (Sbuiltin ef sargs res pc) rs m
        t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres rs) m')
  | exec_Sjumptable sv tbl pc' n rs m:
      eval_sval ctx sv = Some (Vint n) ->
      list_nth_z tbl (Int.unsigned n) = Some pc' ->
      sem_sfval ctx (Sjumptable sv tbl) rs m
        E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs m)
.



(* Syntax and Semantics of symbolic internal states *)
(* [si_pre] is a precondition on initial context *)
Record sistate := { si_pre: iblock_exec_context -> Prop; si_sreg: reg -> sval; si_smem: smem }.

(* Predicate on which (rs, m) is a possible final state after evaluating [st] on ((crs0 ctx), (cm0 ctx)) *)
Definition sem_sistate ctx (st: sistate) (rs: regset) (m: mem): Prop :=
  st.(si_pre) ctx
  /\ eval_smem ctx st.(si_smem) = Some m
  /\ forall (r:reg), eval_sval ctx (st.(si_sreg) r) = Some (rs#r).

Definition abort_sistate ctx (st: sistate): Prop :=
  ~(st.(si_pre) ctx)
  \/ eval_smem ctx st.(si_smem) = None
  \/ exists (r: reg), eval_sval ctx (st.(si_sreg) r) = None.

(** * Symbolic execution of final step *)
Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
  match i with
  | Bgoto pc => Sgoto pc
  | Bcall sig ros args res pc => 
    let svos := sum_left_map sis.(si_sreg) ros in
    let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
    Scall sig svos sargs res pc
  | Btailcall sig ros args =>
    let svos := sum_left_map sis.(si_sreg) ros in
    let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
    Stailcall sig svos sargs
  | Bbuiltin ef args res pc =>
    let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in
    Sbuiltin ef sargs res pc
  | Breturn or => 
    let sor := SOME r <- or IN Some (sis.(si_sreg) r) in
    Sreturn sor
  | Bjumptable reg tbl =>
    let sv := sis.(si_sreg) reg in
    Sjumptable sv tbl
  end.

Local Hint Constructors sem_sfval: core.

Lemma sexec_final_svf_correct ctx i sis t rs m s:
  sem_sistate ctx sis rs m ->
  final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s -> 
  sem_sfval ctx (sexec_final_sfv i sis) rs m t s.
Proof.
  intros (PRE&MEM&REG). 
  destruct 1; subst; try_simplify_someHyps; simpl; intros; try autodestruct; eauto.
  + (* Bcall *) intros; eapply exec_Scall; auto.
    - destruct ros; simpl in * |- *; auto.
      rewrite REG; auto.
    - erewrite eval_list_sval_inj; simpl; auto.
  + (* Btailcall *) intros. eapply exec_Stailcall; eauto.
    - destruct ros; simpl in * |- *; eauto.
      rewrite REG; eauto.
    - erewrite eval_list_sval_inj; simpl; auto.
  + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto.
    eapply seval_builtin_args_correct; eauto.
  + (* Bjumptable *) intros. eapply exec_Sjumptable; eauto. congruence.
Qed.

Local Hint Constructors final_step: core.
Local Hint Resolve seval_builtin_args_complete: core.

Lemma sexec_final_svf_complete ctx i sis t rs m s:
  sem_sistate ctx sis rs m ->
  sem_sfval ctx (sexec_final_sfv i sis) rs m t s
  -> final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s.
Proof.
  intros (PRE&MEM&REG).
  destruct i; simpl; intros LAST; inv LAST; eauto.
  + (* Breturn *)
    enough (v=regmap_optget res Vundef rs) as ->; eauto.
    destruct res; simpl in *; congruence.
  + (* Bcall *)
    erewrite eval_list_sval_inj in *; try_simplify_someHyps.
    intros; eapply exec_Bcall; eauto.
    destruct fn; simpl in * |- *; auto.
    rewrite REG in * |- ; auto.
  + (* Btailcall *)
    erewrite eval_list_sval_inj in *; try_simplify_someHyps.
    intros; eapply exec_Btailcall; eauto.
    destruct fn; simpl in * |- *; auto.
    rewrite REG in * |- ; auto.
  + (* Bjumptable *)
    eapply exec_Bjumptable; eauto.
    congruence.
Qed.

(* symbolic state *)
Inductive sstate :=
  | Sfinal (sis: sistate) (sfv: sfval)
  | Scond (cond: condition) (args: list_sval) (sm: smem) (ifso ifnot: sstate)
 .

Inductive sem_internal_sstate ctx rs m t s: sstate -> Prop :=
  | sem_Sfinal sis sfv
     (SIS: sem_sistate ctx sis rs m)
     (SFV: sem_sfval ctx sfv rs m t s)
     : sem_internal_sstate ctx rs m t s (Sfinal sis sfv)
  | sem_Scond b cond args sm ifso ifnot
     (SEVAL: seval_condition ctx cond args sm = Some b)
     (SELECT: sem_internal_sstate ctx rs m t s (if b then ifso else ifnot))
     : sem_internal_sstate ctx rs m t s (Scond cond args sm ifso ifnot)
  .