A theory of symbolic simulation (i.e. simulation of symbolic executions) on BTL blocks.

Require Import Coqlib Maps RelationClasses.
Require Import AST Integers Values Events Memory Globalenvs.
Require Import Op Registers.
Require Import RTL BTL OptionMonad.
Require Export BTL_Invariants.
Require Import ValueDomain.
Import HConsing.

Semantics of Symbolic Values

Record iblock_common_context := Bcctx {
  cge: BTL.genv;
  csp: val;
  crs0: regset;
  cmbc: mem * option block_classification;
}.

Definition cm0 ctx : mem := fst (cmbc ctx).
Definition ctx_bc ctx : option block_classification := snd (cmbc ctx).

Inductive ctx_strict_reflect : option block_classification -> bool -> Prop :=
  | mode_strict bc : ctx_strict_reflect (Some bc) true
  | mode_lax : ctx_strict_reflect None false.


Local Open Scope option_monad_scope.

Import ListNotations.

Fixpoint eval_sval ctx (sv: sval): option val :=
  match sv with
  | Sinput r _ => Some ((crs0 ctx)#r)
  | Sop op l _ =>
     SOME args <- eval_list_sval ctx l IN
     eval_operation (cge ctx) (csp ctx) op args (cm0 ctx)
  | Sfoldr op l sv0 _ =>
     SOME args <- eval_list_sval ctx l IN
     SOME v0 <- eval_sval ctx sv0 IN
     fold_right (fun a ob => SOME b <- ob IN
       eval_operation (cge ctx) (csp ctx) op [a;b] (cm0 ctx)) (Some v0) args
  | Sload sm trap chunk addr lsv aaddr _ =>
      SOME args <- eval_list_sval ctx lsv IN
      SOME m <- eval_smem ctx sm IN
      match trap with
      | TRAP =>
          SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN
          ASSERT (vmatch_opt_dec (ctx_bc ctx) a aaddr) IN
          Mem.loadv chunk m a
      | NOTRAP =>
          match eval_addressing (cge ctx) (csp ctx) addr args with
          | None => Some Vundef
          | Some a =>
              match vmatch_opt_dec (ctx_bc ctx) a aaddr, Mem.loadv chunk m a with
              | left _, Some val => Some val
              | _, _ => Some Vundef
              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 sinfo srce _ =>
     SOME args <- eval_list_sval ctx lsv IN
     SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN
     ASSERT (vmatch_opt_dec (ctx_bc ctx) a (store_aaddr sinfo)) IN
     SOME m <- eval_smem ctx sm IN
     SOME sv <- eval_sval ctx srce IN
     Mem.storev chunk m a sv
  end.



Definition eval_osv ctx (osv: option sval): option val :=
  SOME sv' <- osv IN eval_sval ctx sv'.

Module SvalNotations.
Notation "'sval_equiv' ctx sv1 sv2" := (eval_sval ctx sv1 = eval_sval ctx sv2)
  (only parsing, at level 0, ctx at next level, sv1 at next level, sv2 at next level).

Notation "'osval_equiv' ctx osv1 osv2" := (eval_osv ctx osv1 = eval_osv ctx osv2)
  (only parsing, at level 0, ctx at next level, osv1 at next level, osv2 at next level).

Notation "'list_sval_equiv' ctx lsv1 lsv2" := (eval_list_sval ctx lsv1 = eval_list_sval ctx lsv2)
  (only parsing, at level 0, ctx at next level, lsv1 at next level, lsv2 at next level).

Notation "'smem_equiv' ctx sm1 sm2" := (eval_smem ctx sm1 = eval_smem ctx sm2)
  (only parsing, at level 0, ctx at next level, sm1 at next level, sm2 at next level).

Notation "'alive' o" := (o = None -> False) (at level 0).

End SvalNotations.
Import SvalNotations.



Section Scale.

Variable scalev: val -> val.
Variable select_op: operation -> bool.

Hypothesis scalev_distr: forall ctx op v1 scv1 v2,
  select_op op = true ->
  scalev v1 = scv1 ->
  eval_operation (cge ctx) (csp ctx) op [scv1; scalev v2] (cm0 ctx) =
  SOME r <- eval_operation (cge ctx) (csp ctx) op [v1; v2] (cm0 ctx) IN Some (scalev r).

Lemma scalev_distr_list ctx op v0 scv0
  (SCALE_v0: scalev v0 = scv0)
  (OK_op: select_op op = true)
  :forall l scl
  (SCALE_l: fold_right (fun a l0 => scalev a::l0) nil l = scl),
  fold_right (fun a ob => SOME b <- ob IN
    eval_operation (cge ctx) (csp ctx) op [a;b] (cm0 ctx)) (Some scv0) scl =
  SOME r <- fold_right (fun a ob => SOME b <- ob IN
      eval_operation (cge ctx) (csp ctx) op [a;b] (cm0 ctx)) (Some v0) l IN
  Some (scalev r).

Variable scale: sval -> sval.

Hypothesis scale_correct: forall ctx sv,
  eval_sval ctx (scale sv) = SOME v <- eval_sval ctx sv IN Some (scalev v).

Fixpoint scale_l (lsv: list_sval): list_sval :=
  match lsv with
  | Snil _ => fSnil
  | Scons sv lsv' _ => fScons (scale sv) (scale_l lsv')
  end.

Lemma scale_l_correct: forall ctx lsv,
  eval_list_sval ctx (scale_l lsv) = SOME lv <- eval_list_sval ctx lsv IN
  Some (fold_right (fun a l0 => scalev a::l0) nil lv).

Definition rescale (sv: sval): sval :=
  match sv with
  | Sfoldr op l sv0 _ =>
      if select_op op then fSfoldr op (scale_l l) (scale sv0)
      else scale sv
  | _ => scale sv
  end.

Theorem rescale_correct ctx sv v:
  eval_sval ctx (scale sv) = Some v ->
  eval_sval ctx (rescale sv) = Some v.

End Scale.

Import Datatypes.


Section Accumulate.

Variable accv: val -> val -> val.
Variable select_op: operation -> bool.

Hypothesis accv_eval: forall ctx v1 v2 op,
    select_op op = true ->
    eval_operation (cge ctx) (csp ctx) op [v1; v2] (cm0 ctx) = Some (accv v1 v2).

Hypothesis accv_commut: forall v1 v2, accv v1 v2 = accv v2 v1.

Hypothesis accv_assoc: forall v1 v2 v3, accv v1 (accv v2 v3) = accv (accv v1 v2) v3.

Lemma accv_assoc_list ctx op vl v0 accv0
  (ACC_vr: accv vl v0 = accv0)
  (OK_op: select_op op = true)
  :forall l vr
  (ACC_l: fold_right (fun a ob => SOME b <- ob IN
    eval_operation (cge ctx) (csp ctx) op [a;b] (cm0 ctx)) (Some v0) l = Some vr),
  fold_right (fun a ob => SOME b <- ob IN
    eval_operation (cge ctx) (csp ctx) op [a;b] (cm0 ctx)) (Some accv0) l =
  Some (accv vl vr).

Variable merge1: sval -> sval -> option sval.
Variable acc0: sval -> sval -> sval.
Variable compare: sval -> sval -> comparison.

Hypothesis compare_correct: forall ctx sv1 sv2 sv3,
  compare sv1 sv2 = Eq ->
  merge1 sv1 sv2 = Some sv3 ->
  eval_sval ctx sv3 =
  SOME v1 <- eval_sval ctx sv1 IN
  SOME v2 <- eval_sval ctx sv2 IN Some (accv v1 v2).

Hypothesis acc0_correct: forall ctx (sv1 sv2: sval),
  eval_sval ctx (acc0 sv1 sv2) =
  SOME v1 <- eval_sval ctx sv1 IN
  SOME v2 <- eval_sval ctx sv2 IN Some (accv v1 v2).

Fixpoint merge (l1 l2: list_sval) {struct l1}: list_sval :=
  match l1 with
  | Snil _ => l2
  | Scons sv1 l1' _ =>
     (fix merge_in l2 { struct l2 } :=
     match l2 with
     | Snil _ => l1
     | Scons sv2 l2' _ =>
       match compare sv1 sv2 with
       | Lt => fScons sv1 (merge l1' l2)
       | Eq => match merge1 sv1 sv2 with
               | Some sv3 => fScons sv3 (merge l1' l2')
               | None => fScons sv1 (fScons sv2 (merge l1' l2'))
               end
       | Gt => fScons sv2 (merge_in l2')
       end
    end) l2
  end.

Theorem merge_correct ctx l1 op
  (OK_op: select_op op = true): forall l2 v1 v2 sv0_1 sv0_2 h1 h2,
  eval_sval ctx (Sfoldr op l1 sv0_1 h1) = Some v1 ->
  eval_sval ctx (Sfoldr op l2 sv0_2 h2) = Some v2 ->
  eval_sval ctx (fSfoldr op (merge l1 l2) (acc0 sv0_1 sv0_2)) = Some (accv v1 v2).

End Accumulate.


Lemma root_apply_morph_equiv o args0 args1 sm0 sm1 ctx
  (EARGS: list_sval_equiv ctx args0 args1)
  (EMEM: smem_equiv ctx sm0 sm1):
  sval_equiv ctx (root_apply o args0 sm0) (root_apply o args1 sm1).

Inductive optsv_simu ctx: option sval -> option sval -> Prop :=
  | Ssome_simu sv1 sv2
      (SIMU: sval_equiv ctx sv1 sv2)
     :optsv_simu ctx (Some sv1) (Some sv2)
  | Snone_simu: optsv_simu ctx None None
.

Global Instance optsv_simu_Equivalence {ctx} : Equivalence (optsv_simu ctx).

Lemma eval_osv_morph [ctx osv0 osv1]
  (EQ : optsv_simu ctx osv0 osv1):
  eval_osv ctx osv0 = eval_osv ctx osv1.

Definition eval_scondition ctx (cond: condition) (lsv: list_sval): option bool :=
  SOME args <- eval_list_sval ctx lsv IN
  eval_condition cond args (cm0 ctx).

Lemma valid_pointer_preserv ctx sm:
  forall m b ofs, eval_smem ctx sm = Some m ->
  Mem.valid_pointer (cm0 ctx) b ofs = Mem.valid_pointer m b ofs.
Local Hint Resolve valid_pointer_preserv: core.


Local Hint Resolve si_wf: core.

Definition si_ok ctx (si: fpasv): Prop :=
  forall sv, List.In sv (fpa_ok si) -> eval_sval ctx sv <> None.

Lemma si_ok_eval si r sv ctx:
  si_ok ctx si -> si r=Some sv -> eval_sval ctx sv <> None.

Definition eval_map_sreg (ctx:iblock_common_context) (map: sval -> sval) (sreg : PTree.tree sval): regset :=
  let default := fst (crs0 ctx) in
  let rsmap := PTree.map (fun r sv =>
       match eval_sval ctx (map sv) with
       | Some v => v
       | None => (crs0 ctx)#r end) sreg
  in (default,
    PTree.combine (fun oa ob =>
      match ob with
      | Some x => Some x
      | None => oa
      end) (snd (crs0 ctx)) rsmap).

Lemma eval_map_sreg_correct ctx map sreg r:
  (eval_map_sreg ctx map sreg)#r
  = match (SOME sv <- sreg!r IN eval_sval ctx (map sv)) with
    | Some v => v
    | None => (crs0 ctx)#r
    end.

Lemma eval_map_sreg_correct_some ctx map (sreg: PTree.t sval) sv r:
  sreg!r = Some sv ->
  (eval_map_sreg ctx map sreg)#r =
       match eval_sval ctx (map sv) with
       | Some v => v
       | None => (crs0 ctx)#r
       end.

Lemma eval_map_sreg_correct_none ctx map (sreg: PTree.t sval) r:
  sreg!r = None ->
  (eval_map_sreg ctx map sreg)#r = (crs0 ctx)#r.

Lemma si_ok_eval_map si r sv ctx:
  si_ok ctx si -> si r=Some sv -> eval_sval ctx sv = Some ((eval_map_sreg ctx (fun sv => sv) si)#r).

Definition sreg_ok ctx (sreg: reg -> option sval): Prop :=
  forall r sv, sreg r = Some sv -> eval_sval ctx sv <> None.

Lemma si_ok_sreg ctx (si: fpasv): si_ok ctx si -> sreg_ok ctx si.

Definition match_sreg ctx (sreg: reg -> option sval) (rs: regset): Prop :=
  forall r sv, sreg r = Some sv -> eval_sval ctx sv = Some (rs#r).

Lemma match_sreg_ok ctx sreg rs:
  match_sreg ctx sreg rs -> sreg_ok ctx sreg.
Local Hint Resolve match_sreg_ok: core.

Definition match_si ctx (si: fpasv) (rs: regset): Prop :=
  si_ok ctx si /\ match_sreg ctx si rs.

Lemma match_si_ok ctx si rs:
  match_si ctx si rs -> si_ok ctx si.
Local Hint Resolve match_si_ok si_ok_sreg: core.

Definition match_invs ctx (csix: invariants) (rs: regset): Prop :=
  match_si ctx (history csix) (crs0 ctx)
  /\ match_si ctx (glue csix) rs.

Lemma only_liveness_match_si ctx si:
  only_liveness si -> match_si ctx si (crs0 ctx).
Local Hint Resolve only_liveness_match_si: core.

Lemma only_liveness_match_invs ctx csix:
  only_liveness (history csix) ->
  only_liveness (glue csix) ->
  match_invs ctx csix (crs0 ctx).

Lemma svfree_preserv ge sp rs1 rs2 m r sv
  (EQREGS: forall r0, r0 <> r -> rs1#r0 = rs2#r0):
  svfree sv r ->
  eval_sval (Bcctx ge sp rs1 m) sv = eval_sval (Bcctx ge sp rs2 m) sv.

Lemma fold_right_ext {A B} (f1 f2: A -> B -> B) b l:
  (forall x y, f1 x y = f2 x y) ->
  fold_right f1 b l = fold_right f2 b l.

Lemma svfreem_preserv ge sp rs m1 m2 sv:
  svfreem sv ->
  eval_sval (Bcctx ge sp rs m1) sv = eval_sval (Bcctx ge sp rs m2) sv.

Lemma matchsi_update_r ge sp rs1 rs2 m res (csi: csasv)
  (FREE: sifree csi res)
  (ONLYLIVEr: forall sv, csi res = Some sv -> sv = fSinput res)
  (MATCH: match_si (Bcctx ge sp rs1 m) (csi_remove res csi) rs2)
  :forall v, match_si (Bcctx ge sp (rs1#res <- v) m) csi (rs2#res <- v).

Lemma matchsi_update_m ge sp rs1 rs2 m1 m2 (si: fpasv)
  (FREEm: sifreem si)
  (MATCH: match_si (Bcctx ge sp rs1 m1) si rs2)
  :match_si (Bcctx ge sp rs1 m2) si rs2.
Local Hint Resolve matchsi_update_m: core.

Lemma matchinvs_update_m ge sp rs1 rs2 m1 m2 csix:
  sifreem (history csix) ->
  sifreem (glue csix) ->
  match_invs (Bcctx ge sp rs1 m1) csix rs2 ->
  match_invs (Bcctx ge sp rs1 m2) csix rs2.

Lemma clobbered_compat_sifreem csi res: clobbered_compat csi res -> sifreem csi.

Lemma clobbered_compat_sifreem_remove csi res:
  clobbered_compat csi res -> sifreem (csi_remove res csi).

Local Hint Resolve clobbered_compat_sifreem clobbered_compat_sifreem_remove: core.

Lemma clobbered_compat_matchsi_preserv ge sp rs1 rs2 m1 csi res:
  clobbered_compat csi res ->
  match_si (Bcctx ge sp rs1 m1) (csi_remove res csi) rs2 ->
  forall v m2, match_si (Bcctx ge sp (rs1#res <- v) m2) csi (rs2#res <- v).

Local Hint Resolve clobbered_compat_matchsi_preserv: core.

Lemma clobbered_compat_matchinvs_preserv ge sp rs1 rs2 m1 (csix: invariants) res:
  clobbered_compat (history csix) res ->
  clobbered_compat (glue csix) res ->
  match_invs (Bcctx ge sp rs1 m1) (csix_remove res csix) rs2 ->
  forall v m2, match_invs (Bcctx ge sp (rs1#res <- v) m2) csix (rs2#res <- v).

A theory of build_frame and eqlive_reg

Definition build_frame {A} (si: reg -> option A) (r: reg): Prop := alive (si r).

Lemma build_frame_intro {A} (si: reg -> option A) r sv: si r = Some sv -> build_frame si r.

Local Hint Unfold build_frame: core.
Local Hint Resolve build_frame_intro: core.

Definition eqlive_reg (frame: reg -> Prop) (rs1 rs2: regset): Prop :=
 forall r, (frame r) -> rs1#r = rs2#r.

Lemma match_si_eqlive ctx si rs1 rs2:
  match_si ctx si rs1 ->
  eqlive_reg (build_frame si) rs1 rs2 ->
  match_si ctx si rs2.
Local Hint Resolve match_si_eqlive: core.

Lemma match_invs_eqlive ctx csix rs1 rs2:
  match_invs ctx csix rs1 ->
  eqlive_reg (build_frame csix) rs1 rs2 ->
  match_invs ctx csix rs2.

Lemma eqlive_reg_update (frame: reg -> Prop) rs1 rs2 r v:
  eqlive_reg (fun r1 => r1 <> r /\ frame r1) rs1 rs2 ->
  eqlive_reg frame (rs1 # r <- v) (rs2 # r <- v).

Lemma eqlive_reg_update_gso frame rs1 rs2 res r: forall v : val,
  eqlive_reg frame rs1 # res <- v rs2 # res <- v ->
  res <> r -> frame r ->
  rs1 # r = rs2 # r.

Lemma eqlive_reg_monotonic (frame1 frame2: reg -> Prop) rs1 rs2:
  eqlive_reg frame2 rs1 rs2 -> (forall r, frame1 r -> frame2 r) -> eqlive_reg frame1 rs1 rs2.

Lemma eqlive_reg_list (frame: reg -> Prop) args rs1 rs2:
  eqlive_reg frame rs1 rs2 -> (forall r, List.In r args -> (frame r)) -> rs1##args = rs2##args.

Lemma eqlive_reg_refl frame rs: eqlive_reg frame rs rs.
Global Hint Resolve eqlive_reg_refl: core.

Lemma eqlive_reg_trans frame rs1 rs2 rs3:
  eqlive_reg frame rs1 rs2 -> eqlive_reg frame rs2 rs3 -> eqlive_reg frame rs1 rs3.

Lemma find_function_eqlive ge frame ros rs1 rs2:
  eqlive_reg frame rs1 rs2 ->
  (forall r, ros = inl r -> frame r) ->
  find_function ge ros rs1 = find_function ge ros rs2.

Inductive eqlive_stackframes: stackframe -> stackframe -> Prop :=
  | eqlive_stackframes_intro res f sp pc rs1 rs2
      (EQUIV: forall v, eqlive_reg (build_frame (f.(fn_gm) pc)) (rs1 # res <- v) (rs2 # res <- v)):
       eqlive_stackframes (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2).

Inductive eqlive_states: state -> state -> Prop :=
  | eqlive_states_intro
      st1 st2 f sp pc rs1 rs2 m bc
      (STACKS: list_forall2 eqlive_stackframes st1 st2)
      (EQUIV: eqlive_reg (build_frame (f.(fn_gm) pc)) rs1 rs2):
      eqlive_states (State st1 f sp pc rs1 m bc) (State st2 f sp pc rs2 m bc)
  | eqlive_states_call st1 st2 f args m bc
      (STACKS: list_forall2 eqlive_stackframes st1 st2):
      eqlive_states (Callstate st1 f args m bc) (Callstate st2 f args m bc)
  | eqlive_states_return st1 st2 v m bc
      (STACKS: list_forall2 eqlive_stackframes st1 st2):
      eqlive_states (Returnstate st1 v m bc) (Returnstate st2 v m bc).

Local Hint Constructors eqlive_stackframes eqlive_states: core.

Lemma eqlive_stackframes_refl stf: eqlive_stackframes stf stf.
Global Hint Resolve eqlive_stackframes_refl: core.

Lemma eqlive_stack_refl stk: list_forall2 eqlive_stackframes stk stk.
Global Hint Resolve eqlive_stack_refl: core.

Lemma eqlive_states_refl s: eqlive_states s s.

Lemma eqlive_stackframes_trans stf1 stf2:
  eqlive_stackframes stf1 stf2 ->
  forall stf3, eqlive_stackframes stf2 stf3 ->
  eqlive_stackframes stf1 stf3.

Lemma eqlive_stacks_trans stk1 stk2:
  list_forall2 eqlive_stackframes stk1 stk2 ->
  forall stk3, list_forall2 eqlive_stackframes stk2 stk3 ->
  list_forall2 eqlive_stackframes stk1 stk3.

Local Hint Resolve eqlive_stacks_trans: core.

Lemma eqlive_states_trans s1 s2:
  eqlive_states s1 s2 ->
  forall s3, eqlive_states s2 s3 ->
  eqlive_states s1 s3.

Auxiliary definitions on Builtins

Section EVAL_BUILTIN_SARG.

Variable ctx: iblock_common_context.
Variable m: mem.

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

Definition eval_builtin_sargs (al: list (builtin_arg sval)) (vl: list val) : Prop :=
  list_forall2 eval_builtin_sarg al vl.

End EVAL_BUILTIN_SARG.


Lemma eval_builtin_sarg_iff [A B : Type] ctx (fs : A -> option sval) (fb : A -> option B) (fv : B -> val)
  (arg : builtin_arg A) (sarg : builtin_arg sval) (barg : builtin_arg B) (m : mem) (v : val)
  (MATCH: forall (x : A) (y : B) (sv : sval),
            fs x = Some sv -> fb x = Some y ->
            eval_sval ctx sv = Some (fv y))
  (MAP0: map_builtin_arg_opt fs arg = Some sarg)
  (MAP1: map_builtin_arg_opt fb arg = Some barg):
  eval_builtin_sarg ctx m sarg v <-> eval_builtin_arg (cge ctx) fv (csp ctx) m barg v.


Lemma map_builtin_arg_opt_id A (f : A -> option A) b
  (FID: forall x, f x = Some x):
  map_builtin_arg_opt f b = Some b.

Lemma builtin_arg_opt_map_correct ctx rs m arg varg:
  eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg ->
  forall (sreg : reg -> option sval) (b: builtin_arg sval), map_builtin_arg_opt sreg arg = Some b ->
  match_sreg ctx sreg rs ->
  eval_builtin_sarg ctx m b varg.

Lemma builtin_arg_opt_map_exact arg:
  forall (sreg: reg -> option sval) b,
  map_builtin_arg_opt sreg arg = Some b ->
  forall ctx rs m varg, eval_builtin_sarg ctx m b varg ->
  match_sreg ctx sreg rs ->
  eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg.


Lemma map_builtin_arg_opt_all_Some A B (f : A -> option B) (g : A -> B) b
  (FSOME: forall x, f x = Some (g x)):
  map_builtin_arg_opt f b = Some (map_builtin_arg g b).

Lemma eval_builtin_sarg_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 ->
  eval_builtin_sarg ctx m (map_builtin_arg sreg arg) varg.

Lemma eval_builtin_sarg_exact ctx rs m sreg: forall arg varg,
  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
  eval_builtin_sarg ctx m (map_builtin_arg sreg arg) varg ->
  eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg.

Lemma eval_builtin_sargs_exact ctx rs m sreg: forall args vargs,
  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
  eval_builtin_sargs ctx m (map (map_builtin_arg sreg) args) vargs ->
  eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs.
Local Hint Resolve eval_builtin_sargs_exact: core.


Definition eval_builtin_sval ctx : builtin_arg sval -> option (builtin_arg val) :=
  map_builtin_arg_opt (eval_sval ctx).

Definition eval_list_builtin_sval ctx : list (builtin_arg sval) -> option (list (builtin_arg val)) :=
  map_opt (eval_builtin_sval ctx).


Lemma eval_builtin_sval_arg ctx bs:
  forall ba m v,
  eval_builtin_sval ctx bs = Some ba ->
  eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v ->
  eval_builtin_sarg ctx m bs v.

Lemma eval_builtin_sarg_sval ctx m v: forall bs,
  eval_builtin_sarg ctx m bs v ->
  exists ba,
    eval_builtin_sval ctx bs = Some ba
    /\ eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v.

Lemma eval_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 ->
  eval_builtin_sargs ctx m lbs v.

Lemma eval_builtin_sargs_sval ctx m lv: forall lbs,
  eval_builtin_sargs 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.

Lemma eval_builtin_sval_correct ctx m: forall bs1 v bs2,
  eval_builtin_sarg ctx m bs1 v ->
  (eval_builtin_sval ctx bs1) = (eval_builtin_sval ctx bs2) ->
  eval_builtin_sarg ctx m bs2 v.

Lemma eval_list_builtin_sval_correct ctx m vargs: forall lbs1,
  eval_builtin_sargs ctx m lbs1 vargs ->
  forall lbs2, (eval_list_builtin_sval ctx lbs1) = (eval_list_builtin_sval ctx lbs2) ->
  eval_builtin_sargs ctx m lbs2 vargs.

Symbolic (final) value of a block

Inductive sfval :=
  | Sgoto (pc: exit)
  | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:exit)
  | 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.

Record iblock_function_context := Bfctx {
  cf: function;
  cc:> iblock_common_context
}.

Import ListNotations.
Local Open Scope list_scope.

Inductive sem_sfval ctx stk bc: sfval -> regset -> mem -> trace -> state -> Prop :=
  | exec_Sgoto pc rs m:
      sem_sfval ctx stk bc (Sgoto pc) rs m E0 (State stk (cf ctx) (csp ctx) pc rs m bc)
  | exec_Sreturn pstk osv rs m m' bc' v:
      (csp ctx) = (Vptr pstk Ptrofs.zero) ->
      Mem.free m pstk 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 stk bc (Sreturn osv) rs m
         E0 (Returnstate stk v m' bc')
  | exec_Scall rs m sig svos lsv args res pc fd bc':
      sfind_function ctx svos = Some fd ->
      funsig fd = sig ->
      eval_list_sval ctx lsv = Some args ->
      sem_sfval ctx stk bc (Scall sig svos lsv res pc) rs m
        E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc rs::stk) fd args m bc')
  | exec_Stailcall pstk rs m sig svos args fd m' bc' lsv:
      sfind_function ctx svos = Some fd ->
      funsig fd = sig ->
      (csp ctx) = Vptr pstk Ptrofs.zero ->
      Mem.free m pstk 0 (cf ctx).(fn_stacksize) = Some m' ->
      eval_list_sval ctx lsv = Some args ->
      sem_sfval ctx stk bc (Stailcall sig svos lsv) rs m
        E0 (Callstate stk fd args m' bc')
  | exec_Sbuiltin m' bc' rs m vres res pc t sargs ef vargs:
      eval_builtin_sargs ctx m sargs vargs ->
      external_call ef (cge ctx) vargs m t vres m' ->
      sem_sfval ctx stk bc (Sbuiltin ef sargs res pc) rs m
        t (State stk (cf ctx) (csp ctx) pc (regmap_setres res vres rs) m' bc')
  | 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 stk bc (Sjumptable sv tbl) rs m
        E0 (State stk (cf ctx) (csp ctx) pc' rs m bc)
.

Preservation properties under a simu_proof_context

Record simu_proof_context := Sctx {
  sge1: BTL.genv;
  sge2: BTL.genv;
  sge_match: forall s, Genv.find_symbol sge1 s = Genv.find_symbol sge2 s;
  ssp: val;
  srs0: regset;
  smbc: mem * option block_classification
}.

Definition sm0 ctx : mem := fst (smbc ctx).

Definition bcctx1 (ctx: simu_proof_context) := Bcctx ctx.(sge1) ctx.(ssp) ctx.(srs0) ctx.(smbc).
Definition bcctx2 (ctx: simu_proof_context) := Bcctx ctx.(sge2) ctx.(ssp) ctx.(srs0) ctx.(smbc).

Section SymbValPreserved.

Hypothesis ctx: simu_proof_context.
Local Hint Resolve sge_match: core.

Lemma eval_sval_preserved sv:
  eval_sval (bcctx1 ctx) sv = eval_sval (bcctx2 ctx) sv.

Lemma list_sval_eval_preserved lsv:
  eval_list_sval (bcctx1 ctx) lsv = eval_list_sval (bcctx2 ctx) lsv.

Lemma smem_eval_preserved sm:
  eval_smem (bcctx1 ctx) sm = eval_smem (bcctx2 ctx) sm.

Lemma eval_builtin_sval_preserved sv:
  eval_builtin_sval (bcctx1 ctx) sv = eval_builtin_sval (bcctx2 ctx) sv.

Lemma eval_list_builtin_sval_preserved lsv:
  eval_list_builtin_sval (bcctx1 ctx) lsv = eval_list_builtin_sval (bcctx2 ctx) lsv.

Lemma eval_scondition_preserved cond lsv:
  eval_scondition (bcctx1 ctx) cond lsv = eval_scondition (bcctx2 ctx) cond lsv.

Lemma match_sreg_preserved sreg rs:
  match_sreg (bcctx1 ctx) sreg rs -> match_sreg (bcctx2 ctx) sreg rs.
Local Hint Resolve match_sreg_preserved: core.

Lemma match_si_preserved si rs:
  match_si (bcctx1 ctx) si rs -> match_si (bcctx2 ctx) si rs.
Local Hint Resolve match_si_preserved: core.

Lemma match_invs_preserved csix rs:
  match_invs (bcctx1 ctx) csix rs -> match_invs (bcctx2 ctx) csix rs.

Hypothesis senv_preserved_BTL: Senv.equiv (sge1 ctx) (sge2 ctx).

Lemma senv_find_symbol_preserved id:
  Senv.find_symbol (sge1 ctx) id = Senv.find_symbol (sge2 ctx) id.

Lemma senv_symbol_address_preserved id ofs:
  Senv.symbol_address (sge1 ctx) id ofs = Senv.symbol_address (sge2 ctx) id ofs.

Lemma eval_builtin_sarg_preserved m: forall bs varg,
  eval_builtin_sarg (bcctx1 ctx) m bs varg ->
  eval_builtin_sarg (bcctx2 ctx) m bs varg.

Lemma eval_builtin_sargs_preserved m lbs vargs:
  eval_builtin_sargs (bcctx1 ctx) m lbs vargs ->
  eval_builtin_sargs (bcctx2 ctx) m lbs vargs.

End SymbValPreserved.

Syntax and Semantics of symbolic internal states

Record sistate :=
  { sis_pre: iblock_common_context -> Prop;
    sis_sreg:> reg -> option sval;
    sis_smem: smem;
    sis_pre_preserved: forall pctx, sis_pre (bcctx1 pctx) <-> sis_pre (bcctx2 pctx)
  }.

Record sistate_eq ctx (si0 si1 : sistate) : Prop := {
    EQ_SIS_PRE: si0.(sis_pre) ctx <-> si1.(sis_pre) ctx;
    EQ_SIS_SREG: forall (r : reg), optsv_simu ctx (si0.(sis_sreg) r) (si1.(sis_sreg) r);
    EQ_SIS_SMEM: smem_equiv ctx (si0.(sis_smem)) (si1.(sis_smem))
  }.

Global Instance sistate_Equivalence {ctx : iblock_common_context} : Equivalence (sistate_eq ctx).

Lemma sreg_ok_morph [ctx si0 si1]:
  sistate_eq ctx si0 si1 ->
  sreg_ok ctx si0 <-> sreg_ok ctx si1.


Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop :=
  sis.(sis_pre) ctx
  /\ eval_smem ctx sis.(sis_smem) = Some m
  /\ match_sreg ctx sis rs
.

Local Hint Resolve match_sreg_preserved: core.

Lemma sem_sistate_preserved ctx sis rs m:
  sem_sistate (bcctx1 ctx) sis rs m -> sem_sistate (bcctx2 ctx) sis rs m.

Fixpoint lmap_sv {A} (sreg: A -> option sval) (l: list A): option list_sval :=
  match l with
  | nil => Some (fSnil)
  | r::l' =>
     SOME sv <- sreg r IN
     SOME lsv <- lmap_sv sreg l' IN
     Some (fScons sv lsv)
  end.

Definition bamap_opt {A B}:
  (builtin_arg A -> option (builtin_arg B)) -> list (builtin_arg A) -> option (list (builtin_arg B)) :=
  map_opt.

Lemma eval_lmap_sv ctx sreg l rs:
  match_sreg ctx sreg rs ->
  forall lsv, lmap_sv sreg l = Some lsv ->
  eval_list_sval ctx lsv = Some (rs ## l).

Lemma lmap_sv_TRIV_alive args sis
  (TRIV: forall r, build_frame sis r)
  :alive (lmap_sv sis args).
Local Hint Resolve lmap_sv_TRIV_alive: core.

Lemma eval_bamap_opt_correct ctx rs m args vargs:
  eval_builtin_args (cge ctx) (fun r : reg => rs # r)
    (csp ctx) m args vargs ->
  forall sis l,
    bamap_opt (map_builtin_arg_opt sis) args = Some l ->
    match_sreg ctx sis rs ->
  eval_builtin_sargs ctx m l vargs.

Lemma eval_bamap_opt_exact ctx m l vargs:
  eval_builtin_sargs ctx m l vargs ->
  forall sis rs args,
    bamap_opt (map_builtin_arg_opt sis) args = Some l ->
    match_sreg ctx sis rs ->
  eval_builtin_args (cge ctx) (fun r : positive => rs # r)
    (csp ctx) m args vargs.

Lemma builtin_arg_opt_map_TRIV_alive (A: Type) (sis: reg -> option A) args
  (TRIVFRAME : forall r : reg, build_frame sis r)
  (LBMAP: bamap_opt (map_builtin_arg_opt sis) args = None)
  :False.

Symbolic execution of final step

Definition sum_left_optmap {A B C} (f : A -> option B) (x : A + C): option (B + C) :=
  match x with
  | inl y => SOME r <- f y IN Some (inl r)
  | inr z => Some (inr z)
  end.

Definition sexec_final_sfv (i: final) (sreg: reg -> option sval): option sfval :=
  match i with
  | Bgoto pc => Some (Sgoto pc)
  | Bcall sig ros args res pc =>
    SOME svos <- sum_left_optmap sreg ros IN
    SOME sargs <- lmap_sv sreg args IN
    Some (Scall sig svos sargs res pc)
  | Btailcall sig ros args =>
    SOME svos <- sum_left_optmap sreg ros IN
    SOME sargs <- lmap_sv sreg args IN
    Some (Stailcall sig svos sargs)
  | Bbuiltin ef args res pc =>
    SOME sargs <- bamap_opt (map_builtin_arg_opt sreg) args IN
    Some (Sbuiltin ef sargs res pc)
  | Breturn None => Some (Sreturn None)
  | Breturn (Some r) =>
    SOME sv <- sreg r IN
    Some (Sreturn (Some sv))
  | Bjumptable reg tbl =>
    SOME sv <- sreg reg IN
    Some (Sjumptable sv tbl)
  end.

Local Hint Constructors sem_sfval: core.

Lemma sexec_final_sfv_correct (ctx: iblock_function_context) stk bc i sis t rs m s sfv:
  sem_sistate ctx sis rs m ->
  final_step (cge ctx) stk (cf ctx) (csp ctx) rs m bc i t s ->
  sexec_final_sfv i sis = Some sfv ->
  sem_sfval ctx stk bc sfv rs m t s.

Lemma sexec_final_sfv_TRIV_alive i sis
  (TRIVFRAME: forall r, build_frame sis r)
  :alive (sexec_final_sfv i sis).
Local Hint Resolve sexec_final_sfv_TRIV_alive: core.

Local Hint Constructors final_step: core.

Lemma sexec_final_sfv_exact (ctx: iblock_function_context) stk bc i sis t rs m s sfv:
  sem_sistate ctx sis rs m ->
  sexec_final_sfv i sis = Some sfv ->
  sem_sfval ctx stk bc sfv rs m t s
  -> final_step (cge ctx) stk (cf ctx) (csp ctx) rs m bc i t s.

Record sis_ok ctx (sis: sistate): Prop := {
  OK_PRE: sis.(sis_pre) ctx;
  OK_SMEM: eval_smem ctx sis.(sis_smem) <> None;
  OK_SREG: sreg_ok ctx sis
}.

Lemma sis_ok_morph [ctx si0 si1]:
  sistate_eq ctx si0 si1 ->
  sis_ok ctx si0 <-> sis_ok ctx si1.

Lemma sis_ok_preserved ctx sis:
  sis_ok (bcctx1 ctx) sis <-> sis_ok (bcctx2 ctx) sis.

Lemma sem_sis_ok ctx sis rs m:
  sem_sistate ctx sis rs m -> sis_ok ctx sis.

Program Definition set_sreg (r:reg) (sv:sval) (sis:sistate): sistate :=
  {| sis_pre:=(fun ctx =>
      (forall rsv, sis r = Some rsv -> eval_sval ctx rsv <> None) /\
      (sis.(sis_pre) ctx));
     sis_sreg:=fun y => if Pos.eq_dec r y then Some sv else sis y;
     sis_smem:= sis.(sis_smem)|}.

Lemma set_sreg_correct ctx dst sv sis (rs rs': regset) m:
  sem_sistate ctx sis rs m ->
  (eval_sval ctx sv = Some rs' # dst) ->
  (forall r, build_frame sis r -> r <> dst -> rs'#r = rs#r) ->
  sem_sistate ctx (set_sreg dst sv sis) rs' m.

Lemma set_sreg_TRIV_alive ctx dst sv sis rs m
  (SIS: sem_sistate ctx sis rs m)
  (TRIVFRAME: forall r, build_frame sis r)
  :forall r, build_frame (set_sreg dst sv sis) r.

Lemma ok_set_sreg ctx r sv sis:
  sis_ok ctx (set_sreg r sv sis)
  <-> (sis_ok ctx sis /\ eval_sval ctx sv <> None).


Program Definition set_smem (sm:smem) (sis:sistate): sistate :=
  {| sis_pre:=(fun ctx => eval_smem ctx sis.(sis_smem) <> None /\ (sis.(sis_pre) ctx));
     sis_sreg:= sis.(sis_sreg);
     sis_smem:= sm |}.

Lemma set_smem_correct ctx sm sis rs m m':
  sem_sistate ctx sis rs m ->
  (eval_smem ctx sm = Some m') ->
  sem_sistate ctx (set_smem sm sis) rs m'.

symbolic execution of basic instructions

Definition sexec_op op args dst (sis: sistate): option sistate :=
   SOME args <- lmap_sv sis args IN
   Some (set_sreg dst (fSop op args) sis).

Lemma sexec_op_TRIV_alive ctx op args dst sis rs m
  (SIS: sem_sistate ctx sis rs m)
  (TRIVFRAME: forall r, build_frame sis r)
  :exists sis', sexec_op op args dst sis = Some sis' /\ forall r, build_frame sis' r.

Local Hint Resolve valid_pointer_preserv: core.
Lemma sexec_op_correct ctx op args dst sis sis' rs m v
 (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = Some v)
 (SIS: sem_sistate ctx sis rs m)
 :sexec_op op args dst sis = Some sis' -> sem_sistate ctx sis' (rs#dst <- v) m.

Definition sexec_load trap chunk addr args aaddr dst (sis: sistate): option sistate :=
   SOME args <- lmap_sv sis args IN
   Some (set_sreg dst (fSload sis.(sis_smem) trap chunk addr args aaddr) sis).

Lemma sexec_load_TRIV_alive ctx trap chunk addr args aaddr dst sis rs m
  (SIS: sem_sistate ctx sis rs m)
  (TRIVFRAME: forall r, build_frame sis r)
  :exists sis', sexec_load trap chunk addr args aaddr dst sis = Some sis' /\ forall r, build_frame sis' r.

Lemma sexec_load_correct ctx chunk addr args aaddr dst sis sis' rs m v trap
 (HLOAD: has_loaded (cge ctx) (csp ctx) (ctx_bc ctx) rs m chunk addr args aaddr v trap)
 (SIS: sem_sistate ctx sis rs m)
 : (sexec_load trap chunk addr args aaddr dst sis = Some sis') ->
   (sem_sistate ctx sis' (rs#dst <- v) m).

Definition sexec_store chunk addr args sinfo src (sis: sistate): option sistate :=
   SOME args <- lmap_sv sis args IN
   SOME src <- sis src IN
   Some (set_smem (fSstore sis.(sis_smem) chunk addr args sinfo src) sis).

Lemma sexec_store_TRIV_alive sis chunk addr args sinfo src ctx rs m
  (SIS: sem_sistate ctx sis rs m)
  (TRIVFRAME: forall r, build_frame sis r)
  :exists sis', sexec_store chunk addr args sinfo src sis = Some sis'
   /\ forall r, build_frame sis' r.

Lemma sexec_store_correct ctx chunk addr args sinfo src sis sis' rs m m' a
  (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a)
  (VMATCH: vmatch_opt (ctx_bc ctx) a (store_aaddr sinfo))
  (STORE: Mem.storev chunk m a (rs # src) = Some m')
  (SIS: sem_sistate ctx sis rs m)
  :sexec_store chunk addr args sinfo src sis = Some sis' -> sem_sistate ctx sis' rs m'.

Lemma eval_scondition_eq ctx cond args sis rs m lsv
  (SIS : sem_sistate ctx sis rs m)
  (ARGS: lmap_sv sis args = Some lsv)
  :eval_scondition ctx cond lsv = eval_condition cond rs ## args m.

symbolic execution of blocks

Inductive pstate (S : Type) :=
  | Sfinal (sis: S) (sfv: sfval)
  | Scond (cond: condition) (args: list_sval) (ifso ifnot: pstate S)
  | Sabort
 .
Arguments Sfinal {_}.
Arguments Scond {_}.
Arguments Sabort {_}.

Definition sstate := pstate sistate.


Record poutcome (istate : Type) := sout {
   _sis: istate;
   _sfv: sfval;
}.
Arguments sout {_}.
Arguments _sis [_].
Arguments _sfv [_].


Definition soutcome := poutcome sistate.

Fixpoint get_soutcome [S] ctx (ss:pstate S): option (poutcome S) :=
  match ss with
  | Sfinal sis sfv => Some (sout sis sfv)
  | Scond cond args ifso ifnot =>
     SOME b <- eval_scondition ctx cond args IN
     get_soutcome ctx (if b then ifso else ifnot)
  | Sabort => None
  end.

Definition sfv_frame f sfv: reg -> Prop :=
  match sfv with
  | Sgoto pc => build_frame (f.(fn_gm) pc)
  | Sreturn _ | Stailcall _ _ _ => fun r => False
  | Scall _ _ _ res pc => fun r => r <> res /\ build_frame (f.(fn_gm) pc) r
  | Sjumptable _ tbl => fun r => exists pc, List.In pc tbl /\ build_frame (f.(fn_gm) pc) r
  | Sbuiltin _ _ bres pc => fun r => (forall res, reg_builtin_res bres = Some res -> r <> res)
                                                  /\ build_frame (f.(fn_gm) pc) r
  end.

Definition triv_frame (f: function) (sfv: sfval) (r: reg):= True.

Inductive sem_sstate (SVFF: function -> sfval -> reg -> Prop)
  (ctx: iblock_function_context) stk bc t cs: sstate -> Prop :=
  | sem_Sfinal sis sfv rs m
     (SIS: sem_sistate ctx sis rs m)
     (LIVEOK: forall r, SVFF (cf ctx) sfv r -> build_frame sis r)
     (SFV: sem_sfval ctx stk bc sfv rs m t cs)
     : sem_sstate SVFF ctx stk bc t cs (Sfinal sis sfv)
  | sem_Scond b cond args ifso ifnot
     (SEVAL: eval_scondition ctx cond args = Some b)
     (SELECT: sem_sstate SVFF ctx stk bc t cs (if b then ifso else ifnot))
     : sem_sstate SVFF ctx stk bc t cs (Scond cond args ifso ifnot)
  .

Lemma sem_sstate_run SVFF ctx stk bc ss t cs:
  sem_sstate SVFF ctx stk bc t cs ss ->
  exists sis sfv rs m,
    get_soutcome ctx ss = Some (sout sis sfv)
    /\ sem_sistate ctx sis rs m
    /\ (forall r, SVFF (cf ctx) sfv r -> build_frame sis r)
    /\ sem_sfval ctx stk bc sfv rs m t cs.

Local Hint Resolve sem_Sfinal: core.

Lemma run_sem_sstate (SVFF: function -> sfval -> reg -> Prop)
  (ctx: iblock_function_context) ss sis sfv:
  get_soutcome ctx ss = Some (sout sis sfv) ->
  forall rs m stk bc cs t,
  sem_sistate ctx sis rs m ->
  (forall r, SVFF (cf ctx) sfv r -> build_frame sis r) ->
  sem_sfval ctx stk bc sfv rs m t cs ->
  sem_sstate SVFF ctx stk bc t cs ss.

Notation "'STBIND' X <- A 'IN' B" := (match A with Some X => B | None => Sabort end)
         (at level 200, X name, A at level 100, B at level 200)
         : option_monad_scope.

Fixpoint sexec_rec ib (sis:sistate) (k: sistate -> sstate): sstate :=
  match ib with
  | BF fin _ =>
    STBIND sfv <- sexec_final_sfv fin sis IN
    Sfinal sis sfv
  | Bnop _ => k sis
  | Bop op args res _ =>
     STBIND sis' <- sexec_op op args res sis IN
     k sis'
  | Bload trap chunk addr args aaddr dst _ =>
     STBIND sis' <- sexec_load trap chunk addr args aaddr dst sis IN
     k sis'
  | Bstore chunk addr args sinfo src _ =>
     STBIND sis' <- sexec_store chunk addr args sinfo src sis IN
     k sis'
  | Bseq ib1 ib2 =>
      sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k)
  | Bcond cond args ifso ifnot _ =>
      let ifso := sexec_rec ifso sis k in
      let ifnot := sexec_rec ifnot sis k in
      STBIND args <- lmap_sv sis args IN
      Scond cond args ifso ifnot
  end
  .

Definition sexec ib sinit := sexec_rec ib sinit (fun _ => Sabort).

Local Hint Constructors sem_sstate: core.

Local Hint Resolve sexec_op_correct sexec_final_sfv_correct
  sexec_load_correct sexec_store_correct: core.

Lemma intro_False_sem_sstate SVFF ctx stk bc t cs ss: False -> sem_sstate SVFF ctx stk bc t cs ss.
Local Hint Resolve intro_False_sem_sstate: core.

Lemma sexec_rec_correct (ctx: iblock_function_context) stk bc t s ib rs m rs1 m1 ofin
  (ISTEP: iblock_istep (cge ctx) (csp ctx) (ctx_bc ctx) rs m ib rs1 m1 ofin): forall sis k
  (SIS: sem_sistate ctx sis rs m)
  (TRIVFRAME: forall r, build_frame sis r)
  (CONT: match ofin with
         | None => forall sis', sem_sistate ctx sis' rs1 m1 ->
             (forall r, build_frame sis' r) -> sem_sstate triv_frame ctx stk bc t s (k sis')
         | Some fin => final_step (cge ctx) stk (cf ctx) (csp ctx) rs1 m1 bc fin t s
         end),
  sem_sstate triv_frame ctx stk bc t s (sexec_rec ib sis k).

Theorem sexec_correct (strict : bool) (ctx: iblock_function_context) sinit bc stk ib t s
  (CTX_BC: ctx_bc ctx = ASSERT strict IN Some bc):
  iblock_step strict (cge ctx) stk (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) bc ib t s ->
  sem_sistate ctx sinit (crs0 ctx) (cm0 ctx) ->
  (forall r : reg, build_frame sinit r) ->
  sem_sstate triv_frame ctx stk bc t s (sexec ib sinit).

Lemma sem_sistate_determ ctx sis rs1 m1 rs2 m2:
  sem_sistate ctx sis rs1 m1 ->
  sem_sistate ctx sis rs2 m2 ->
     (eqlive_reg (build_frame sis) rs2 rs1)
  /\ m1 = m2.


Local Hint Constructors eqlive_stackframes list_forall2: core.
Local Hint Resolve eqlive_reg_update eqlive_reg_monotonic list_nth_z_in: core.

Lemma sem_sfval_equiv rs1 rs2 ctx stk bc sfv m t s:
  sem_sfval ctx stk bc sfv rs1 m t s ->
  (eqlive_reg (sfv_frame (cf ctx) sfv) rs1 rs2) ->
  exists s', sem_sfval ctx stk bc sfv rs2 m t s' /\ eqlive_states s s'.



Definition abort_sistate ctx (sis: sistate): Prop :=
  ~(sis.(sis_pre) ctx)
  \/ eval_smem ctx sis.(sis_smem) = None
  \/ exists r sv, sis r = Some sv /\ eval_sval ctx sv = None.

Lemma sem_sistate_exclude_abort ctx sis rs m:
  sem_sistate ctx sis rs m ->
  abort_sistate ctx sis ->
  False.

Lemma set_sreg_preserv_abort ctx sv dst sis:
  abort_sistate ctx sis ->
  abort_sistate ctx (set_sreg dst sv sis).

Lemma sexec_op_preserv_abort ctx op args dest sis sis':
  abort_sistate ctx sis ->
  sexec_op op args dest sis = Some sis' ->
  abort_sistate ctx sis'.

Lemma sexec_load_preserv_abort ctx chunk addr args aaddr dest sis sis' trap:
  abort_sistate ctx sis ->
  sexec_load trap chunk addr args aaddr dest sis = Some sis' ->
  abort_sistate ctx sis'.

Lemma set_smem_preserv_abort ctx sm sis:
  abort_sistate ctx sis ->
  abort_sistate ctx (set_smem sm sis).

Lemma sexec_store_preserv_abort ctx chunk addr args sinfo src sis sis':
  abort_sistate ctx sis ->
  sexec_store chunk addr args sinfo src sis = Some sis' ->
  abort_sistate ctx sis'.

Lemma sem_sstate_Sabort SVFF ctx stk bc t s:
   sem_sstate SVFF ctx stk bc t s Sabort -> False.


Section REC_EXACT_PROOF.

Local Hint Resolve sexec_op_preserv_abort sexec_load_preserv_abort
  sexec_store_preserv_abort sem_sistate_exclude_abort sem_sstate_Sabort: core.

Lemma sexec_exclude_abort SVFF ctx stk bc ib t s1: forall sis k
  (SEXEC: sem_sstate SVFF ctx stk bc t s1 (sexec_rec ib sis k))
  (CONT: forall sis', sem_sstate SVFF ctx stk bc t s1 (k sis') -> (abort_sistate ctx sis') -> False)
  (ABORT: abort_sistate ctx sis),
  False.

Lemma set_sreg_abort ctx dst sv sis rs m:
  sem_sistate ctx sis rs m ->
  eval_sval ctx sv = None ->
  abort_sistate ctx (set_sreg dst sv sis).

Lemma sexec_op_abort ctx sis op args dest sis' rs m
  (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = None)
  (SIS: sem_sistate ctx sis rs m)
  :(sexec_op op args dest sis=Some sis') -> abort_sistate ctx sis'.

Lemma sexec_load_TRAP_abort ctx chunk addr args aaddr dst sis sis' rs m
  (EVAL: forall a,
           eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a ->
           vmatch_opt (ctx_bc ctx) a aaddr ->
         Mem.loadv chunk m a = None)
  (SIS: sem_sistate ctx sis rs m)
  :(sexec_load TRAP chunk addr args aaddr dst sis = Some sis') -> abort_sistate ctx sis'.

Lemma set_smem_abort ctx sm sis rs m:
  sem_sistate ctx sis rs m ->
  eval_smem ctx sm = None ->
  abort_sistate ctx (set_smem sm sis).

Lemma sexec_store_abort ctx chunk addr args sinfo src sis sis' rs m
  (EVAL: forall a,
           eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a ->
           vmatch_opt (ctx_bc ctx) a (store_aaddr sinfo) ->
         Mem.storev chunk m a (rs # src) = None)
  (SIS: sem_sistate ctx sis rs m)
  :sexec_store chunk addr args sinfo src sis = Some sis' -> abort_sistate ctx sis'.

Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort sexec_final_sfv_exact: core.

Lemma sexec_rec_exact ctx stk bc ib t s1: forall sis k
  (SEXEC: sem_sstate sfv_frame ctx stk bc t s1 (sexec_rec ib sis k))
  rs m
  (SIS: sem_sistate ctx sis rs m)
  (CONT: forall sis', sem_sstate sfv_frame ctx stk bc t s1 (k sis') ->
  (abort_sistate ctx sis') -> False),
     match iblock_istep_run (cge ctx) (csp ctx) (ctx_bc ctx) ib rs m with
     | Some (out rs' m' (Some fin)) =>
        exists s2, final_step (cge ctx) stk (cf ctx) (csp ctx) rs' m' bc fin t s2
                   /\ eqlive_states s1 s2
     | Some (out rs' m' None) => exists sis', (sem_sstate sfv_frame ctx stk bc t s1 (k sis'))
                                              /\ (sem_sistate ctx sis' rs' m')
     | None => False
     end.

Theorem sexec_exact (strict:bool) (ctx:iblock_function_context) stk bc ib t s1 sinit rs m
  (CTX_BC: ctx_bc ctx = ASSERT strict IN Some bc):
  sem_sistate ctx sinit rs m ->
  sem_sstate sfv_frame ctx stk bc t s1 (sexec ib sinit) ->
  exists s2, iblock_step strict (cge ctx) stk (cf ctx) (csp ctx) rs m bc ib t s2
             /\ eqlive_states s1 s2.

End REC_EXACT_PROOF.

Simulation properties on internal states

Inductive svident_simu ctx: (sval + ident) -> (sval + ident) -> Prop :=
  | Sleft_simu sv1 sv2
      (SIMU: sval_equiv ctx sv1 sv2)
      :svident_simu ctx (inl sv1) (inl sv2)
  | Sright_simu id1 id2
      (IDSIMU: id1 = id2)
      :svident_simu ctx (inr id1) (inr id2)
  .

Definition bargs_simu ctx (args1 args2: list (builtin_arg sval)): Prop :=
  eval_list_builtin_sval ctx args1 = eval_list_builtin_sval ctx args2.

Inductive sfv_simu ctx: sfval -> sfval -> Prop :=
  | Sgoto_simu pc: sfv_simu ctx (Sgoto pc) (Sgoto pc)
  | Scall_simu sig ros1 ros2 args1 args2 r pc
      (SVID: svident_simu ctx ros1 ros2)
      (ARGS: eval_list_sval ctx args1 = eval_list_sval ctx args2)
      :sfv_simu ctx (Scall sig ros1 args1 r pc) (Scall sig ros2 args2 r pc)
  | Stailcall_simu sig ros1 ros2 args1 args2
      (SVID: svident_simu ctx ros1 ros2)
      (ARGS: eval_list_sval ctx args1 = eval_list_sval ctx args2)
      :sfv_simu ctx (Stailcall sig ros1 args1) (Stailcall sig ros2 args2)
  | Sbuiltin_simu ef lba1 lba2 br pc
      (BARGS: bargs_simu ctx lba1 lba2)
      :sfv_simu ctx (Sbuiltin ef lba1 br pc) (Sbuiltin ef lba2 br pc)
  | Sjumptable_simu sv1 sv2 lpc
      (VAL: eval_sval ctx sv1 = eval_sval ctx sv2)
      :sfv_simu ctx (Sjumptable sv1 lpc) (Sjumptable sv2 lpc)
  | simu_Sreturn osv1 osv2
      (OPT:optsv_simu ctx osv1 osv2)
      :sfv_simu ctx (Sreturn osv1) (Sreturn osv2)
.

Definition sistate_simu ctx (sis1 sis2:sistate): Prop :=
  forall rs1 m, sem_sistate ctx sis1 rs1 m ->
  exists rs2, sem_sistate ctx sis2 rs2 m
  /\ eqlive_reg (build_frame sis1) rs1 rs2.

Applying symbolic invariants

Fixpoint sv_subst (substm: smem) (subst: reg -> option sval) (sv: sval): sval :=
  match sv with
  | Sinput r _ =>
      match subst r with
      | Some sv' => sv'
      | None => fSinput r
      end
  | Sop op lsv _ =>
     let lsv' := lsv_subst substm subst lsv in
     fSop op lsv'
  | Sfoldr op lsv sv0 _ =>
     let lsv' := lsv_subst substm subst lsv in
     let sv0' := sv_subst substm subst sv0 in
     fSfoldr op lsv' sv0'
  | Sload sm trap chunk addr lsv aaddr _ =>
     let sm' := sm_subst substm subst sm in
     let lsv' := lsv_subst substm subst lsv in
     fSload sm' trap chunk addr lsv' aaddr
  end
with lsv_subst (substm: smem) (subst: reg -> option sval) (lsv0: list_sval): list_sval :=
  match lsv0 with
  | Snil _ => fSnil
  | Scons sv lsv _ =>
    let sv' := sv_subst substm subst sv in
    let lsv' := lsv_subst substm subst lsv in
    fScons sv' lsv'
  end
with sm_subst substm (subst: reg -> option sval) (sm0: smem): smem :=
  match sm0 with
  | Sinit _ => substm
  | Sstore sm chunk addr lsv sinfo sv _ =>
     let sm' := sm_subst substm subst sm in
     let lsv' := lsv_subst substm subst lsv in
     let sv' := sv_subst substm subst sv in
     fSstore sm' chunk addr lsv' sinfo sv'
  end.

Lemma sv_subst_correct rs m ctx substm subst sv:
  (eval_smem ctx substm = Some m) ->
  (forall r, eval_osv ctx (subst r) = Some (rs#r)) ->
  eval_sval ctx (sv_subst substm subst sv) = eval_sval (Bcctx (cge ctx) (csp ctx) rs (m, ctx_bc ctx)) sv.

Lemma sv_subst_ext_equiv sv: forall sm sis,
  sv_subst sm (fun r => Some (ext sis r)) sv = sv_subst sm sis sv.

Definition eval_subst_si ctx (sis:sistate) := eval_map_sreg ctx (sv_subst sis.(sis_smem) sis).

Lemma eval_subst_si_correct ctx sis (si:fpasv) sv r:
  si r = Some sv ->
  (eval_subst_si ctx sis si)#r =
       match eval_sval ctx (sv_subst sis.(sis_smem) sis sv) with
       | Some v => v
       | None => (crs0 ctx)#r
       end.
Proof eval_map_sreg_correct_some ctx (sv_subst sis.(sis_smem) sis) si sv r.

Program Definition sis_empty: sistate :=
  {| sis_pre := fun _ => True;
     sis_sreg := fun r => Some (fSinput r);
     sis_smem := fSinit
|}.

Lemma sis_ok_empty ctx:
  sis_ok ctx sis_empty.
Global Hint Resolve sis_ok_empty: sempty.

Lemma sv_subst_sis_empty ctx sv:
  eval_sval ctx (sv_subst fSinit sis_empty sv) = eval_sval ctx sv.
Global Hint Resolve sv_subst_sis_empty: sempty.
Global Hint Rewrite sv_subst_sis_empty: sempty.

Definition si_ok_subst (sis: sistate) (si: fpasv) ctx: Prop :=
  forall sv, List.In sv (fpa_ok si) -> eval_sval ctx (sv_subst (sis_smem sis) sis sv) <> None.

Lemma si_ok_empty ctx:
  si_ok ctx si_empty.

Lemma si_ok_subst_empty ctx sis:
  si_ok_subst sis si_empty ctx.

Lemma si_ok_subst_sis_empty_si_ok ctx si:
  si_ok_subst sis_empty si ctx ->
  si_ok ctx si.
Global Hint Resolve si_ok_empty si_ok_subst_empty si_ok_subst_sis_empty_si_ok: sempty.

Lemma si_ok_subst_hd lseq: forall ctx r sv (si: fpasv) sis
  (OK_SUBST: si_ok_subst sis (exec_seq lseq (si_set r sv si)) ctx),
  si_ok_subst sis (si_set r sv si) ctx.

Definition ir_subst_si (sis: sistate) (si: fpasv) (ir: ireg): option sval :=
  if ir.(force_input) then sis ir else Some (sv_subst (sis_smem sis) sis (ext si ir)).


Lemma lsv_subst_sis_empty args: forall ctx si,
  list_sval_equiv ctx (lsv_subst (sis_smem sis_empty) sis_empty (lsvof (ext si) args))
    (lsvof (ext si) args).
Global Hint Resolve lsv_subst_sis_empty: sempty.
Global Hint Rewrite lsv_subst_sis_empty: sempty.

Lemma ir_subst_si_sv_subst sis si ir sv:
  ir_subst_si sis si ir = Some sv ->
  sv = sv_subst (sis_smem sis) sis (ir_subst (ext si) ir).

Lemma lmap_sv_lsv_subst args: forall ctx l (si: fpasv) sis,
  lmap_sv (ir_subst_si sis si) args = Some l ->
  list_sval_equiv ctx (lsv_subst (sis_smem sis) sis (lsvof (ext si) args)) l.

Lemma lmap_sv_input_subst args: forall (sis: sistate) (si: fpasv),
  lmap_sv sis args =
  lmap_sv (ir_subst_si sis si) (ir_input_of args).

Lemma eval_ir_subst_si_ok_nofail sis si ctx ir sv
  (SIS_OK: sis_ok ctx sis)
  (SI_OK : si_ok_subst sis si ctx)
  (SUBST : ir_subst_si sis si ir = Some sv):
  alive (eval_sval ctx sv).

Lemma eval_lmap_sv_input_nofail (lr: list reg): forall ctx sis si lsv
  (SOK: sis_ok ctx sis)
  (LMAP: lmap_sv (ir_subst_si sis si) (ir_input_of lr) = Some lsv),
  eval_list_sval ctx lsv = None -> False.

Program Definition tr_sis (sis: sistate) (si: fpasv) (sis_input_init: bool): sistate :=
  {| sis_pre := fun ctx => sis.(sis_pre) ctx
                        /\ sreg_ok ctx sis
                        /\ si_ok_subst sis si ctx;
     sis_sreg := fun r => match si r with
                          | Some sv => Some (sv_subst sis.(sis_smem) sis sv)
                          | None => if sis_input_init then Some (fSinput r) else None
                          end;
     sis_smem := sis.(sis_smem) |}.

Lemma tr_sis_morph [ctx sis fp0 fp1 sinit]:
  fpa_eq fp0 fp1 ->
  sistate_eq ctx (tr_sis sis fp0 sinit) (tr_sis sis fp1 sinit).

Lemma tr_sis_okpreserv ctx sis si sinit:
  sis_ok ctx (tr_sis sis si sinit) -> sis_ok ctx sis.

Lemma tr_sis_ok_indep_sinit ctx sis si:
  sis_ok ctx (tr_sis sis si true) <-> sis_ok ctx (tr_sis sis si false).

Definition tr_sis_ok ctx sis (si: fpasv): Prop :=
  sis_ok ctx sis -> si_ok_subst sis si ctx.

Lemma ok_tr_sis ctx sis (si: fpasv) sinit
  (SI_DONT_TRAP: tr_sis_ok ctx sis si)
  :sis_ok ctx (tr_sis sis si sinit) <-> sis_ok ctx sis.

Lemma tr_sis_correct sis (si: fpasv) ctx rs m
  (SIS: sem_sistate ctx sis rs m)
  (TRIVFRAME: forall r, build_frame sis r)
  (SI_DONT_TRAP: tr_sis_ok ctx sis si)
  :sem_sistate ctx (tr_sis sis si false) (eval_subst_si ctx sis si) m
    /\ match_si (Bcctx (cge ctx) (csp ctx) rs (m, ctx_bc ctx)) si (eval_subst_si ctx sis si).

Operations on two sistate

Section TwoStatesOp.

Definition sis_get_ireg (sis0 sis1 : sistate) (r : ireg) : option sval :=
  if r.(force_input) then sis0 r else sis1 r.

Lemma sis_get_ireg_nofail ctx sis0 sis1 r sv
  (SOK0 : sis_ok ctx sis0)
  (SOK1 : sis_ok ctx sis1)
  (GET: sis_get_ireg sis0 sis1 r = Some sv):
  alive (eval_sval ctx sv).

Lemma sis_get_ireg_lmap_nofail ctx sis0 sis1 rs lsv
  (SOK0 : sis_ok ctx sis0)
  (SOK1 : sis_ok ctx sis1)
  (GET: lmap_sv (sis_get_ireg sis0 sis1) rs = Some lsv):
  alive (eval_list_sval ctx lsv).

Definition sis_set_rop (r : reg) (rop : root_op) (lir : list ireg) (sis0 sis1 : sistate): option sistate :=
  SOME lsv <- lmap_sv (sis_get_ireg sis0 sis1) lir IN
  Some (set_sreg r (root_apply rop lsv sis0.(sis_smem)) sis1).

Definition sis_get_ival (sis0 sis1 : sistate) (iv : ival) : option sval :=
  match iv with
  | Ireg ir => sis_get_ireg sis0 sis1 ir
  | Iop rop args => SOME lsv <- lmap_sv (sis_get_ireg sis0 sis1) args IN
                    Some (root_apply rop lsv sis0.(sis_smem))
  end.

Definition sis_set_ival (r : reg) (iv : ival) (sis0 sis1 : sistate): option sistate :=
  SOME sv <- sis_get_ival sis0 sis1 iv IN
  Some (set_sreg r sv sis1).

Fixpoint sis_set_seq (l : list (reg*ival)) (sis0 sis1 : sistate): option sistate :=
  match l with
  | nil => Some sis1
  | (r, iv) :: l =>
      SOME sis2 <- sis_set_ival r iv sis0 sis1 IN
      sis_set_seq l sis0 sis2
  end.

Lemma sis_set_seq_okpreserv ctx l sis0 sis1 sis2:
  sis_set_seq l sis0 sis1 = Some sis2 ->
  sis_ok ctx sis2 -> sis_ok ctx sis1.

End TwoStatesOp.

Source symbolic state builder and register/memory set functions

Section InvariantApplication.

  Variable csix : invariants.
  Variable ctx : iblock_common_context.


Definition sis_history := tr_sis sis_empty (history csix) true.

Lemma sv_subst_pre_history sv
  (MSreg : match_sreg ctx (history csix) (crs0 ctx))
  :eval_sval ctx (sv_subst fSinit sis_history sv) = eval_sval ctx sv.


Definition sis_target :=
  let sis_H := sis_history in
  tr_sis sis_H (glue csix) false.

Lemma sis_target_ok_sis_history:
  sis_ok ctx sis_target -> sis_ok ctx sis_history.

Lemma sis_target_correct rs:
  match_invs ctx csix rs ->
  sem_sistate ctx sis_target rs (cm0 ctx).


Program Definition sis_source :=
  let sis_H := sis_history in
  let sis_HG := sis_target in
  {| sis_pre := sis_pre sis_HG; sis_sreg := sis_sreg sis_H; sis_smem := fSinit |}.

Lemma sis_source_ok_sis_target:
  sis_ok ctx sis_source <-> sis_ok ctx sis_target.

Lemma sis_source_ok_sis_history:
  sis_ok ctx sis_source -> sis_ok ctx sis_history.

Lemma sis_source_correct:
  match_si ctx (history csix) (crs0 ctx) ->
  si_ok ctx (glue csix) ->
  sem_sistate ctx sis_source (crs0 ctx) (cm0 ctx).

End InvariantApplication.


Definition symbolic_eq (ctx: iblock_common_context) sis (sv1 sv2: sval): bool :=
  match eval_sval ctx (sv_subst (sis_smem sis) sis sv1),
        eval_sval ctx (sv_subst (sis_smem sis) sis sv2) with
  | Some v1, Some v2 => Val.eq v1 v2
  | Some _, None | None, Some _ => false
  | None, None => true
  end.

Definition most_defined_sv (ctx: iblock_common_context) sis (sv1 sv2: sval): option sval :=
  if symbolic_eq ctx sis sv1 sv2 then Some sv2 else None.

Lemma most_defined_sv_preserved ctx sis:
  most_defined_sv (bcctx1 ctx) sis = most_defined_sv (bcctx2 ctx) sis.

Program Definition union2_si_gen (ctx: iblock_common_context) sis (si1 si2: fpasv):
  { res: option fpasv |
    match res with
    | Some si =>
       fpa_ok si = List.app (fpa_ok si1) (fpa_ok si2)
       /\ PTree.combine_mostdef (most_defined_sv ctx sis) (fpa_reg si1) (fpa_reg si2) = Some (fpa_reg si)
    | None =>
       PTree.combine_mostdef (most_defined_sv ctx sis) (fpa_reg si1) (fpa_reg si2) = None
    end } :=
   SOME pt <- PTree.combine_mostdef (most_defined_sv ctx sis) (fpa_reg si1) (fpa_reg si2) IN
   Some
    {| fpa_ok := List.app (fpa_ok si1) (fpa_ok si2);
       fpa_reg := pt |}.

Definition union2_si (ctx: iblock_common_context) sis (si1 si2: fpasv): option fpasv :=
  ` (union2_si_gen ctx sis si1 si2).

Lemma fpa_ok_union2_si ctx sis si1 si2 si:
  union2_si ctx sis si1 si2 = Some si ->
  fpa_ok si = List.app (fpa_ok si1) (fpa_ok si2).

Lemma fpa_reg_union2_si ctx sis si1 si2 si:
  union2_si ctx sis si1 si2 = Some si ->
  PTree.combine_mostdef (most_defined_sv ctx sis) (fpa_reg si1) (fpa_reg si2) = Some (fpa_reg si).

Fixpoint union_si (ctx: iblock_common_context) sis (lcsi: list csasv): option fpasv :=
  match lcsi with
  | nil => Some si_empty
  | csi :: l =>
      SOME si2 <- union_si ctx sis l IN
      union2_si ctx sis (siof csi) si2
  end.

Lemma union_si_single: forall ctx sis csi si,
  union_si ctx sis [csi] = Some si ->
  fpa_eq (siof csi) si.

Lemma fpa_ok_union_si (lcsi: list csasv): forall ctx sis csi sv si,
  In csi lcsi ->
  In sv (fpa_ok csi) ->
  union_si ctx sis lcsi = Some si ->
  In sv (fpa_ok si).

Ltac destruct_sir sir :=
  destruct sir eqn:SIR;
  [| exploit PTree.gcombine_mostdef_none_rev; eauto; simpl in *; intuition congruence ].

Lemma fpa_reg_union_si (lcsi: list csasv): forall ctx sis csi si r sv1
  (HIN: In csi lcsi)
  (UNION: union_si ctx sis lcsi = Some si)
  (CSIR: csi ! r = Some sv1),
  exists sv2, si r = Some sv2
      /\ eval_sval ctx (sv_subst (sis_smem sis) sis sv1) =
         eval_sval ctx (sv_subst (sis_smem sis) sis sv2).

Definition ctx_switch_prop ctx1 ctx2 :=
  ctx1 = ctx2 \/ (exists ctx, (ctx1 = bcctx1 ctx) /\ (ctx2 = bcctx2 ctx)).

Ltac destruct_ctx_sw hctx := destruct hctx as [CTXEQ|[ctx [HCTX1 HCTX2]]]; subst; auto.

Lemma match_sreg_union_si_H (lcsi: list csasv): forall
  ctx1 ctx2 sis rs m csi (si: fpasv)
  (HCTX: ctx2 = {| cge := cge ctx1; csp := csp ctx1; crs0 := rs; cmbc := (m, ctx_bc ctx1) |})
  (HIN: In csi lcsi)
  (UNION: union_si ctx1 sis lcsi = Some si)
  (SIS: sem_sistate ctx1 sis rs m)
  (LIVEOK: forall r : reg, build_frame sis r)
  (MATCH: match_sreg ctx2 si rs),
  match_sreg ctx2 csi rs.

Lemma match_sreg_union_si_G (lcsi: list csasv): forall
  ctx1 ctx2 sis rs rs0 m m0 bc pge tpge sp0 csi (si: fpasv) symbols_preserved_rev
  (HCTX1: ctx1 = {| sge1 := pge; sge2 := tpge; sge_match := symbols_preserved_rev;
                    ssp := sp0; srs0 := rs0; smbc := (m0, bc) |})
  (HCTX2: ctx2 = {| cge := pge; csp := sp0; crs0 := rs; cmbc := (m, bc) |})
  (HIN: In csi lcsi)
  (UNION: union_si (bcctx2 ctx1) sis lcsi = Some si)
  (SIS: sem_sistate (bcctx1 ctx1) sis rs m)
  (LIVEOK: forall r : reg, build_frame sis r)
  (MATCH: match_sreg ctx2 si (eval_subst_si (bcctx1 ctx1) sis si)),
  match_sreg ctx2 csi (eval_subst_si (bcctx1 ctx1) sis si).

Definition si_sfv (ctx: iblock_common_context) sis (gm: node -> csasv) sfv: option fpasv :=
  match sfv with
  | Sgoto pc => Some (siof (gm pc))
  | Scall sig svid args res pc =>
      if test_clobberable (gm pc) res then
        Some (siof (csi_remove res (gm pc)))
      else None
  | Sbuiltin ef args bres pc =>
      match reg_builtin_res bres with
      | Some r =>
          if test_clobberable (gm pc) r then
            Some (siof (csi_remove r (gm pc)))
          else None
      | None =>
          if test_csifreem (gm pc) then Some (siof (gm pc))
          else None
      end
  | Stailcall sig svid args => Some (si_empty)
  | Sreturn osv => Some (si_empty)
  | Sjumptable sv lpc => union_si ctx sis (List.map gm lpc)
  end.

Lemma si_sfv_morph ctx sis gm sfv0 sfv1:
  sfv_simu ctx sfv0 sfv1 ->
  si_sfv ctx sis gm sfv0 = si_sfv ctx sis gm sfv1.


Fixpoint tr_sstate (ctx: iblock_common_context) (gm: node -> csasv) ss: sstate :=
  match ss with
  | Sfinal sis sfv =>
      STBIND csi <- si_sfv ctx sis gm sfv IN
      Sfinal (tr_sis sis csi false) sfv
  | Scond cond args ifso ifnot =>
      let ifso' := tr_sstate ctx gm ifso in
      let ifnot' := tr_sstate ctx gm ifnot in
      Scond cond args ifso' ifnot'
  | Sabort => Sabort
  end.

Lemma get_soutcome_tr_sstate ctx gm ss sis sfv:
  get_soutcome ctx ss = Some (sout sis sfv) ->
  get_soutcome ctx (tr_sstate ctx gm ss)
    = option_map (fun si => sout (tr_sis sis si false) sfv) (si_sfv ctx sis gm sfv).

High-Level specification of the symbolic simulation test as predicate match_sexec_si

Definition symb_exec_ok ctx ss sis sfv :=
  get_soutcome ctx ss = Some (sout sis sfv) /\ sis_ok ctx sis.

Definition trss_ok ctx ss := exists sis sfv, symb_exec_ok ctx ss sis sfv.

Definition match_sexec_target ctx (sis1EI: sistate) sfv1EI (ss2IE: sstate): Prop :=
  exists sis2IE sfv2IE, get_soutcome ctx ss2IE = Some (sout sis2IE sfv2IE)
    /\ (forall r, build_frame sis1EI r -> build_frame sis2IE r)
    /\ sistate_simu ctx sis1EI sis2IE
    /\ (forall rs m, sem_sistate ctx sis1EI rs m -> sfv_simu ctx sfv1EI sfv2IE).

Definition match_sexec_live ctx (ss1EI ss2IE:sstate): Prop :=
  forall sis1EI sfv1EI, symb_exec_ok ctx ss1EI sis1EI sfv1EI ->
  match_sexec_target ctx sis1EI sfv1EI ss2IE.


Definition match_sexec_redundant ctx ss1EH sis1E: Prop :=
  forall sis1EH sfv1EH, get_soutcome ctx ss1EH = Some (sout sis1EH sfv1EH) ->
  sistate_simu ctx sis1EH sis1E.

Definition match_sexec_si ctx (gm: gluemap) ib1 ib2 pc: Prop := forall sis1E sfv1E,
  let ss1E := sexec ib1 (sis_source (gm pc)) in
  symb_exec_ok (bcctx1 ctx) ss1E sis1E sfv1E ->
  let ss1EH := tr_sstate (bcctx1 ctx) (fun pc => history (gm pc)) ss1E in
  let ss1EI := tr_sstate (bcctx2 ctx) (fun pc => glue (gm pc)) ss1E in
  trss_ok (bcctx1 ctx) ss1EH /\
  trss_ok (bcctx1 ctx) ss1EI /\
  match_sexec_redundant (bcctx1 ctx) ss1EH sis1E /\
  match_sexec_live (bcctx2 ctx) ss1EI (sexec ib2 (sis_target (gm pc))).


Definition match_sexec_live_ref ctx (gm: gluemap) (ss1E ss2IE:sstate): Prop :=
  forall sis1E sfv1E, symb_exec_ok (bcctx1 ctx) ss1E sis1E sfv1E ->
    exists ss1EH, tr_sstate (bcctx1 ctx) (fun pc => history (gm pc)) ss1E = ss1EH
    /\ trss_ok (bcctx1 ctx) ss1EH
      /\ exists ss1EI, tr_sstate (bcctx2 ctx) (fun pc => glue (gm pc)) ss1E = ss1EI
         /\ trss_ok (bcctx1 ctx) ss1EI
           /\ exists sis1EH sfv1EH, get_soutcome (bcctx1 ctx) ss1EH = Some (sout sis1EH sfv1EH)
              /\ sistate_simu (bcctx1 ctx) sis1EH sis1E
                /\ exists sis1EI sfv1EI, symb_exec_ok (bcctx2 ctx) ss1EI sis1EI sfv1EI
                   /\ match_sexec_target (bcctx2 ctx) sis1EI sfv1EI ss2IE.

Definition match_sexec_si_ref ctx (gm: gluemap) ib1 ib2 pc: Prop :=
  match_sexec_live_ref ctx gm (sexec ib1 (sis_source (gm pc))) (sexec ib2 (sis_target (gm pc))).

Definition instantiate_context (strict : bool) (P: simu_proof_context -> gluemap -> iblock -> iblock -> node -> Prop)
  gm ib1 ib2 pc: Prop := forall ctx, ctx_strict_reflect (snd (smbc ctx)) strict -> P ctx gm ib1 ib2 pc.

Theorem match_sexec_si_ref_imp ctx (gm: gluemap) ib1 ib2 pc:
  match_sexec_si_ref ctx gm ib1 ib2 pc ->
  match_sexec_si ctx gm ib1 ib2 pc.