Module BTL_Invariants


Definitions and Operations on Symbolic Values and Invariants

Require Import Coqlib Maps Floats.
Require Import Classes.RelationClasses.
Require Import AST.
Require Import Op Registers.
Require Import OptionMonad.
Require Export Impure.ImpHCons.
Require Import ValueDomain.
Require Import IntPromotionCommon.
Require Memtype.
Import HConsing.

Local Open Scope option_monad_scope.

Syntax of symbolic values


Additional informations attached to the stores. Used by the semantics (if strict) and the rewriting rules.
Inductive store_num_t :=
  | SNumNone
  | SNumInv (i : positive)
  | SNumSrc (i : positive).

Record store_info : Type := mk_store_info {
  store_num: store_num_t;
  store_aaddr: option aval;
}.

Definition set_store_num (n : store_num_t) (si : store_info) : store_info :=
  mk_store_info n si.(store_aaddr).

symbolic value
Inductive sval :=
  | Sinput (trg: bool) (r: reg) (hid: hashcode)
  | Sop (op:operation) (lsv: list_sval) (hid: hashcode)
  | Sfoldr (op:operation) (lsv: list_sval) (sv0: sval) (hid: hashcode)
  | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk)
      (addr:addressing) (lsv:list_sval) (hid: hashcode)
  | SmayUndef (cond : okclause) (sv : sval) (hid : hashcode)
list of symbolic values
with list_sval :=
  | Snil (hid: hashcode)
  | Scons (sv: sval) (lsv: list_sval) (hid: hashcode)
symbolic memory
with smem :=
  | Sinit (hid: hashcode)
  | Sstore (sm: smem) (chunk:memory_chunk)
      (addr:addressing) (lsv:list_sval) (sinfo: store_info) (srce: sval) (hid: hashcode)
symbolic clauses used to represent boolean conditions
with okclause :=
  | OKfalse (hid : hashcode)
  | OKalive (sv : sval) (hid : hashcode)
  | OKpromotableOp (op : operation) (prom : op_promotion_ceq) (sargs : list_sval) (hid : hashcode)
  | OKpromotableCond (cond : condition) (prom : cond_promotion_ceq) (sargs : list_sval) (hid : hashcode)
  | OKaddrMatch (addr : addressing) (lsv : list_sval) (av : aval) (hid : hashcode)
  | OKvalidAccess (perm : Memtype.permission) (chunk : memory_chunk)
      (addr : addressing) (lsv : list_sval) (hid : hashcode)
.

Definition fst_lsv lsv :=
  match lsv with
  | Snil _ => None
  | Scons sv _ _ => Some sv
  end.

"fake" smart-constructors using an unknown_hid instead of the one provided by hash-consing. These smart-constructors are those used in the abstract model of symbolic execution. They will also appear in the implementation of rewriting rules (in order to avoid hash-consing handling in proofs of rewriting rules) and in the invariants provided by oracles.

Definition fSinput (trg: bool) (r: reg) := Sinput trg r unknown_hid.
Definition fSop (op:operation) (lsv: list_sval) := Sop op lsv unknown_hid.
Definition fSfoldr (op:operation) (lsv: list_sval) (sv0: sval) := Sfoldr op lsv sv0 unknown_hid.
Definition fSload (sm: smem) (trap: trapping_mode)
  (chunk:memory_chunk) (addr:addressing) (lsv:list_sval)
 := Sload sm trap chunk addr lsv unknown_hid.
Definition fSmayUndef (cond : okclause) (sv : sval) := SmayUndef cond sv unknown_hid.

Definition fSnil := Snil unknown_hid.
Definition fScons (sv: sval) (lsv: list_sval) := Scons sv lsv unknown_hid.

Definition fSinit := Sinit unknown_hid.
Definition fSstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (sinfo:store_info) (srce: sval)
  := Sstore sm chunk addr lsv sinfo srce unknown_hid.

Definition fOKfalse
  := OKfalse unknown_hid.
Definition fOKpromotableOp (op : operation) (prom : op_promotion_ceq) (sargs : list_sval)
  := OKpromotableOp op prom sargs unknown_hid.
Definition fOKpromotableCond (cond : condition) (prom : cond_promotion_ceq) (sargs : list_sval)
  := OKpromotableCond cond prom sargs unknown_hid.
Definition fOKaddrMatch (addr : addressing) (lsv : list_sval) (av : aval)
  := OKaddrMatch addr lsv av unknown_hid.

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
with okclause_mut := Induction for okclause Sort Prop.

Combined Scheme sval_mut_comb from sval_mut, list_sval_mut, smem_mut, okclause_mut.


Fixpoint lsv_of_list (l : list sval) : list_sval :=
  match l with
  | nil => fSnil
  | x :: xs => fScons x (lsv_of_list xs)
  end.

Fixpoint list_of_lsv (l : list_sval) : list sval :=
  match l with
  | Snil _ => nil
  | Scons x xs _ => x :: list_of_lsv xs
  end.

Lemma l_lsv_l (l : list sval):
  list_of_lsv (lsv_of_list l) = l.
Proof.
  induction l; simpl; f_equal; auto.
Qed.

Fixpoint lsv_length (l : list_sval) : nat :=
  match l with
  | Snil _ => O
  | Scons _ l _ => S (lsv_length l)
  end.

Lemma lsv_length_eq l:
  lsv_length l = length (list_of_lsv l).
Proof.
  induction l; simpl; f_equal; auto.
Qed.


Representations and syntax of symbolic invariants


registers in invariant
Record ireg := { force_input: bool; regof:> reg }.

input r is the input value of r in the block; last r is the last value of the variable in the invariant
Definition input (r:reg) := {| force_input := true; regof := r |}.
Definition last (r:reg) := {| force_input := false; regof := r |}.

Definition ir_subst (subst: reg -> sval) (ir: ireg): sval :=
  if ir.(force_input) then fSinput false ir else subst ir.

operations in invariant
Inductive root_op: Type :=
  | Rop (op: operation)
  | Rload (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (aaddr: option aval)
  .

Definition fSmayUndef_opt (okc : option okclause) (sv : sval) : sval :=
  match okc with
  | Some okc => fSmayUndef okc sv
  | None => sv
  end.

root_apply builds the symbolic value corresponding to the application of a root_op operator.
Definition root_apply (o : root_op) (args : list_sval) (sm : smem): sval :=
  match o with
  | Rop op => fSop op args
  | Rload trap chunk addr aaddr =>
      fSmayUndef_opt
        (SOME aaddr <- aaddr IN Some (fOKaddrMatch addr args aaddr))
        (fSload sm trap chunk addr args)
  end.

values in invariant
Inductive ival: Type :=
  | Ireg (ir: ireg)
  | Iop (rop: root_op) (args: list ireg)
  .

Fixpoint lsvof subst (l: list ireg): list_sval :=
  match l with
  | nil => fSnil
  | ir::l => fScons (ir_subst subst ir) (lsvof subst l)
  end.

Definition ir_input_of : list reg -> list ireg := map input.
Definition ir_last_of : list reg -> list ireg := map last.
Definition ir_reg_of : list ireg -> list reg := map regof.

Definition rop_subst subst (rop: root_op) (lr: list ireg): sval :=
  let lsv := lsvof subst lr in
  root_apply rop (lsvof subst lr) fSinit.

Definition iv_subst subst (iv: ival): sval :=
  match iv with
  | Ireg ir => ir_subst subst ir
  | Iop rop args => rop_subst subst rop args
  end.

Definition svof iv := iv_subst (fSinput false) iv.
Coercion svof: ival >-> sval.


Inductive istore :=
  mk_istore (chunk:memory_chunk) (addr:addressing) (args:list reg) (sinfo: store_info) (src: reg).

Definition istore_subst (sm0 : smem) (st : istore) : smem :=
  let subst := fSinput true in
  match st with
  | mk_istore chk addr args sinfo src =>
      fSstore sm0 chk addr (lsv_of_list (map subst args)) sinfo (subst src)
  end.

Definition imem := list istore.

Definition imem_subst (im : imem) : smem :=
  fold_left istore_subst im fSinit.

FPASV is an "abstract" representation of symbolic invariants as "parallel assignments" of invariant values (into registers). In other words, such an invariants relates "output" variables in function of "input" variables and an "input" memory. Such invariant also express an implicit precondition on the "inputs" that the symbolic values do not trap.

Inductive is_input: sval -> Prop :=
  | is_input_intro r hid: is_input (Sinput false r hid).

Local Hint Resolve is_input_intro: core.

FPASV stands for "Finite Parallel Assignment of Symbolic Values". (the finiteness of fpa_reg is no longer ensured by its type, but it is finite in practice)
Record fpasv := {
  fpa_ok : list sval;
  fpa_reg :> reg -> option sval;
  fpa_wf : forall r sv, fpa_reg r = Some sv -> is_input sv \/ List.In sv fpa_ok
}.

Program Definition si_empty: fpasv := {|
  fpa_ok := nil;
  fpa_reg := fun _ => None;
|}.

Definition fset [A B : Type] (e : forall (x y : A), {x=y}+{x<>y}) (x : A) (y : B) (f : A -> B) : A -> B :=
  fun x' => if e x' x then y else f x'.

Lemma fset_gs [A B] e x y (f : A -> B):
  fset e x y f x = y.
Proof.
  unfold fset; case e; congruence.
Qed.

Lemma fset_go [A B] e x y (f : A -> B) x'
  (O : x' <> x):
  fset e x y f x' = f x'.
Proof.
  unfold fset; case e; congruence.
Qed.

Program Definition si_set (r: reg) (sv: sval) (si: fpasv): fpasv := {|
  fpa_ok := sv :: si.(fpa_ok);
  fpa_reg := fset Reg.eq r (Some sv) si.(fpa_reg);
|}.
Next Obligation.
  revert H; unfold fset.
  case Reg.eq as [->|].
  - injection 1 as <-; tauto.
  - intro SI_R. apply fpa_wf in SI_R. tauto.
Qed.

Local Open Scope option_monad_scope.

A more "compact" (and "dynamic") representation of symbolic invariants as: This is the (abstract) syntax of invariants for oracles. In the set of output registers, we distinguish those not defined in aseq (which thus satisfy r=fSinput r). Important remark: lazily, the simulation checker will consider that the set of register r such that r = fSinput r is those not defined in aseq. This means that an oracle should not put in aseq an assignment like r := input r. This may lead the simulation checker to reject the invariant while checking "only liveness" constraints. In the same spirit, at the return address of a "call/builtin" putting its result in r, the aseq should not contain any reference to r, even as an auxiliary variable when r is dead afterwards (i.e. not in outputs). This would complicate a bit test_seq_rclobberable to support this feature (and this does not seem very useful). Perhaps a good strategy for the oracle, is to use "fresh" names in the context for auxiliary variables (it would be easier for debugging).

CSASV stands for "Compact Sequence Assignments of Symbolic Values"
Record csasv := {
  aseq: list (reg * ival);
  outputs: Regset.t;
}.

Definition ext (si: reg -> option sval) (r: reg): sval :=
  match si r with
  | Some iv => iv
  | None => fSinput false r
  end.

Lemma ext_inv si r sv:
  ext si r = sv -> si r = Some sv \/ sv = fSinput false r.
Proof.
  unfold ext; autodestruct; intuition.
Qed.

Fixpoint exec_seq (l: list (reg*ival)) (si: fpasv): fpasv :=
  match l with
  | nil => si
  | (r,iv)::l => exec_seq l (si_set r (iv_subst (ext si) iv) si)
  end.

Definition restrict_alive [A B] (p : A -> bool) (f : A -> B) (x : A) : option B :=
  if p x then Some (f x) else None.

Lemma restrict_alive_Some [A B] p (f : A -> B) x y:
  restrict_alive p f x = Some y <-> f x = y /\ p x = true.
Proof.
  unfold restrict_alive; autodestruct; intuition.
Qed.

Program Definition si_restrict_alive (p : reg -> bool) (si : fpasv) : fpasv :=
  {|
    fpa_ok := fpa_ok si;
    fpa_reg := restrict_alive p (ext si);
  |}.
Next Obligation.
  apply restrict_alive_Some in H as (H & _).
  apply ext_inv in H as [H | ->]; eauto using fpa_wf, is_input_intro.
Qed.

Definition regset_in_dec (r : reg) (rs : Regset.t) :
  { Regset.In r rs } + { ~Regset.In r rs}.
Proof.
  case (in_dec Reg.eq r (Regset.elements rs)) as [H|H];
  rewrite <- RegsetIn_elements_equiv in H;
  [left|right]; exact H.
Defined.

Semantics of csasv as "abstract" symbolic invariants
Definition siof (csi: csasv): fpasv :=
  let si := exec_seq csi.(aseq) si_empty in
  si_restrict_alive (fun r => regset_in_dec r csi.(outputs)) si.
Coercion siof: csasv >-> fpasv.

Definition csi_empty: csasv := {| aseq:= nil; outputs := Regset.empty |}.

Lemma csi_gempty r: csi_empty r = None.
Proof.
  reflexivity.
Qed.

Definition csi_remove r (csi: csasv) : csasv :=
  {| aseq:= csi.(aseq); outputs := Regset.remove r csi.(outputs) |}.

Lemma csi_grs csi r: csi_remove r csi r = None.
Proof.
  simpl; unfold restrict_alive.
  rewrite proj_sumbool_is_false by (apply Regset.remove_1; eauto).
  reflexivity.
Qed.

Lemma csi_gro csi r1 r2 (NEQ : r1 <> r2):
  csi_remove r1 csi r2 = csi r2.
Proof.
  simpl; unfold restrict_alive.
  do 2 destruct regset_in_dec; first [reflexivity | exfalso; apply n; revert i].
  - apply Regset.remove_3.
  - apply Regset.remove_2; auto.
Qed.

Record invariants := {
  history : csasv;
  glue :> csasv;
  meminv : imem;
}.


Definition csix_empty : invariants := {| history := csi_empty; glue := csi_empty; meminv := nil |}.

Definition gluemap := PTree.t invariants.

Definition gm_empty: gluemap := (@PTree.empty _).

Definition gm_apply (gm: gluemap) (pc: positive) :=
  match gm!pc with
  | Some csix => csix
  | _ => csix_empty
  end.
Coercion gm_apply: gluemap >-> Funclass.

Definition csix_remove r (csix: invariants) : invariants :=
  {|
    history := csi_remove r (history csix);
    glue := csi_remove r (glue csix);
    meminv := meminv csix;
  |}.


A few syntactic properties on invariants that we need to check during the symbolic test



Definition only_liveness (si: fpasv): Prop :=
     (fpa_ok si) = nil
  /\ (forall r sv, si r = Some sv -> sv=fSinput false r).

Inductive only_live_input (r: reg): sval -> Prop :=
  | only_live_input_intro hid: only_live_input r (Sinput false r hid).

Fixpoint svdep (sv: sval) (trg: bool) (r: reg): Prop :=
  match sv with
  | Sinput trg' r' _ => trg = trg' /\ r = r'
  | Sop _ l _ =>
     lsvdep l trg r
  | Sfoldr _ lsv sv0 _ =>
     lsvdep lsv trg r \/ svdep sv0 trg r
  | Sload sm _ _ _ lsv _ =>
     smdep sm trg r \/ lsvdep lsv trg r
  | SmayUndef cond sv _ =>
      okclausedep cond trg r \/ svdep sv trg r
  end
with lsvdep (lsv: list_sval) trg r: Prop :=
  match lsv with
  | Snil _ => False
  | Scons sv lsv' _ =>
    svdep sv trg r \/ lsvdep lsv' trg r
  end
with smdep (sm: smem) trg r: Prop :=
  match sm with
  | Sinit _ => False
  | Sstore sm _ _ lsv _ srce _ =>
     smdep sm trg r \/ lsvdep lsv trg r \/ svdep srce trg r
  end
with okclausedep (okc : okclause) trg r: Prop :=
  match okc with
  | OKfalse _ => False
  | OKalive sv _ => svdep sv trg r
  | OKpromotableOp _ _ sargs _ | OKpromotableCond _ _ sargs _ => lsvdep sargs trg r
  | OKaddrMatch _ sargs _ _ | OKvalidAccess _ _ _ sargs _ => lsvdep sargs trg r
  end.

Definition svfree (sv: sval) (r:reg) :=
  forall trg, ~svdep sv trg r.

Definition lsvfree (lsv: list_sval) (r:reg) :=
  forall trg, ~lsvdep lsv trg r.

Fixpoint svfreem (sv: sval): Prop :=
  match sv with
  | Sinput _ _ _ => True
  | Sop op l _ =>
     op_depends_on_memory op = false
     /\ lsvfreem l
  | Sfoldr op l sv0 _ =>
     op_depends_on_memory op = false
     /\ lsvfreem l
     /\ svfreem sv0
  | Sload _ _ _ _ _ _ => False
  | SmayUndef cond sv _ =>
      okclausefreem cond /\ svfreem sv
  end
with lsvfreem (lsv: list_sval): Prop :=
  match lsv with
  | Snil _ => True
  | Scons sv lsv' _ =>
    svfreem sv /\ lsvfreem lsv'
  end
with okclausefreem (okc : okclause): Prop :=
  match okc with
  | OKfalse _ => True
  | OKalive sv _ => svfreem sv
  | OKpromotableOp _ _ _ _ | OKpromotableCond _ _ _ _ => False
  | OKaddrMatch _ _ _ _ | OKvalidAccess _ _ _ _ _ => False
  end.

Definition sv_trg_free (sv : sval): Prop :=
  forall r, ~svdep sv true r.

Definition si_trg_free (si: fpasv): Prop :=
  Forall (sv_trg_free) (fpa_ok si) /\
  forall r, if_Some (si r) sv_trg_free.

Definition sifree (si: fpasv) (res: reg): Prop :=
  (forall sv, List.In sv (fpa_ok si) -> svfree sv res)
  /\ (forall r sv, si r = Some sv -> only_live_input r sv \/ svfree sv res).

Definition sifreem (si: fpasv): Prop :=
  forall sv, List.In sv (fpa_ok si) -> svfreem sv.

Record clobbered_compat (csi: csasv) (res: reg): Prop := {
  res_is_free: sifree csi res;
  mem_is_free: sifreem csi;
  res_only_live: forall sv, csi res = Some sv -> sv = fSinput false res
}.


Lemma si_trg_free_ext si r
  (FREE : si_trg_free si):
  sv_trg_free (ext si r).
Proof.
  case FREE as (_ & FREE); specialize (FREE r).
  unfold ext; autodestruct.
  intros _ ? [C]; discriminate C.
Qed.

Lemma si_trg_free_lsv_ext si args r0
  (FREE : si_trg_free si):
  ~lsvdep (lsvof (ext si) args) true r0.
Proof.
  induction args; simpl; intuition.
  revert H0; unfold ir_subst; case force_input; simpl; intuition.
  eapply si_trg_free_ext; eauto.
Qed.

Lemma si_exec_seq_trg_free sq:
  forall si (FREE: si_trg_free si),
  si_trg_free (exec_seq sq si).
Proof.
  induction sq as [|(r,iv)]; simpl; do 2 intro; auto.
  apply IHsq.
  assert (SVF: sv_trg_free (iv_subst (ext si) iv)). {
    destruct iv; simpl; unfold ir_subst, rop_subst, root_apply;
    repeat autodestruct; simpl; intros;
    intros r0 DEP; simpl in DEP; decompose [Logic.and Logic.or] DEP;
    solve [ congruence
          | eapply si_trg_free_ext; eauto
          | eapply si_trg_free_lsv_ext; eauto ].
  }
  split.
  - constructor; apply (conj FREE SVF).
  - intro; simpl; unfold fset.
    destruct Reg.eq; apply (conj FREE SVF).
Qed.

Lemma si_restrict_alive_trg_free b si
  (FREE : si_trg_free si):
  si_trg_free (si_restrict_alive b si).
Proof.
  split. apply FREE.
  intro; simpl; unfold restrict_alive; autodestruct; simpl; trivial; intros.
  apply si_trg_free_ext; auto.
Qed.

Lemma siof_trg_free csi:
  si_trg_free (siof csi).
Proof.
  apply si_restrict_alive_trg_free, si_exec_seq_trg_free.
  do 2 constructor.
Qed.


Lemma imem_subst_src_free im r:
  ~smdep (imem_subst im) false r.
Proof.
  unfold imem_subst.
  assert (H : ~smdep fSinit false r) by intros []; revert H.
  generalize fSinit.
  induction im as [|[]]; simpl; auto.
  intros ? ?; apply IHim.
  intros [|[L|[]]]; auto; try congruence.
  revert L; clear; induction args; simpl; auto.
  intros [[]|]; congruence.
Qed.


Local Open Scope lazy_bool_scope.

Lemma andb_rew (a b: bool): (a &&& b) = true <-> (a=true /\ b=true).
Proof.
  destruct a; simpl; intuition congruence.
Qed.

Lemma negb_rew a: negb a = true <-> a = false.
Proof.
  destruct a; simpl; intuition congruence.
Qed.

Local Hint Rewrite andb_rew negb_rew Pos.eqb_neq Pos.eqb_eq: bools.

Ltac simplify_ir_subst :=
  simpl; unfold ir_subst, rop_subst, root_apply in *;
  repeat autodestruct; simpl in *;
  intros; autorewrite with bools in *;
  intuition (congruence || eauto).

Lemma iv_subst_preserv_lsvfreem (lr: list ireg): forall (subst: reg -> sval),
  (forall r, svfreem (subst r)) ->
  lsvfreem (lsvof subst lr).
Proof.
  induction lr; simplify_ir_subst.
Qed.
Local Hint Resolve iv_subst_preserv_lsvfreem: core.

Lemma iv_subst_preserv_freem (iv: ival): forall (subst: reg -> sval),
  svfreem iv ->
  (forall r, svfreem (subst r)) ->
  svfreem (iv_subst subst iv).
Proof.
  destruct iv; simplify_ir_subst.
Qed.

Lemma ext_preserv_freem si r:
  sifreem si -> svfreem (ext si r).
Proof.
  unfold ext, sifreem; intro OK_FREE.
  destruct (si r) as [sv|] eqn:X; simpl; eauto.
  apply fpa_wf in X as [[]|]; simpl; auto.
Qed.

Lemma sifreem_si_empty: sifreem si_empty.
Proof.
  intros sv. simpl. intuition.
Qed.

Functional checkers corresponding to the above properties.


Definition is_nil [A] (l : list A) : {l = nil}+{l <> nil}.
Proof.
  case l as [|]; [left|right]; congruence.
Defined.

Definition test_ivfreem (iv: ival): bool :=
  match iv with
  | Iop (Rop op) _ => negb (op_depends_on_memory op)
  | Iop (Rload _ _ _ _) _ => false
  | _ => true
  end.

Lemma lsvfreem_fSinput lr: lsvfreem (lsvof (fSinput false) lr).
Proof.
  induction lr; simplify_ir_subst.
Qed.
Local Hint Resolve lsvfreem_fSinput: core.

Lemma test_ivfreem_correct iv: test_ivfreem iv = true -> svfreem iv.
Proof.
  destruct iv; simplify_ir_subst.
Qed.

Fixpoint test_seqfreem (l: list (reg*ival)): bool :=
  match l with
  | nil => true
  | (_,iv)::l => test_ivfreem iv &&& test_seqfreem l
  end.

Local Hint Resolve sifreem_si_empty iv_subst_preserv_freem ext_preserv_freem: core.

Lemma test_seqfreem_correct (l: list (reg*ival)): forall (si: fpasv),
  sifreem si -> (test_seqfreem l = true -> sifreem (exec_seq l si)).
Proof.
  induction l as [|(r,sv) l]; simpl; auto.
  intros si FREEsi; autorewrite with bools.
  intros (TESTSV & TESTL).
  apply test_ivfreem_correct in TESTSV.
  intros r1 sv1.
  eapply IHl in TESTL; eauto. clear r1 sv1.
  intros sv1; simpl.
  intros [H|H]; subst; eauto.
Qed.

NB: test_csifreem is linear in the size of csi
Definition test_csifreem (csi: csasv): bool := test_seqfreem csi.(aseq).

Theorem test_csifreem_correct csi: test_csifreem csi = true -> sifreem csi.
Proof.
  unfold test_csifreem; intros SEQ.
  eapply (test_seqfreem_correct (aseq csi) si_empty) in SEQ; eauto.
Qed.

Fixpoint test_lirfree (lir: list ireg) r: bool :=
  match lir with
  | nil => true
  | iv::lir =>
      negb (Pos.eqb r (regof iv))
      &&& test_lirfree lir r
  end.

Lemma test_lirfree_correct lir r subst
  (SFREE: forall r', r <> r' -> svfree (subst r') r):
  test_lirfree lir r = true -> lsvfree (lsvof subst lir) r.
Proof.
  induction lir; simplify_ir_subst; intros ? []; simpl in *;
  solve [intuition | eapply SFREE; eauto | eapply H0; eauto].
Qed.
Local Hint Resolve test_lirfree_correct: core.

Definition test_ivfree iv (r:reg): bool :=
  match iv with
  | Ireg ir => negb (Pos.eqb r (regof ir))
  | Iop _ lir => test_lirfree lir r
  end.

Lemma test_ivfree_correct iv r subst
  (SFREE: forall r', r <> r' -> svfree (subst r') r):
  test_ivfree iv r = true -> svfree (iv_subst subst iv) r.
Proof.
  destruct iv; simplify_ir_subst;
  intro; simpl; intro DEP; decompose [Logic.or] DEP; subst;
  solve [intuition | eapply test_lirfree_correct; eauto].
Qed.

Fixpoint test_seq_rclobberable (l: list (reg*ival)) r: bool :=
  match l with
  | nil => true
  | (r',iv)::l =>
      negb (Pos.eqb r r')
      &&& test_ivfree iv r
      &&& test_seq_rclobberable l r
  end.

Lemma ext_preserv_free si r r':
  r <> r' ->
  sifree si r ->
  svfree (ext si r') r.
Proof.
  unfold ext, sifree.
  intros DIFF H.
  autodestruct.
  intros EQ.
  eapply H in EQ as [[]|]; auto.
  all:intros; intros ? []; auto.
Qed.

Local Hint Resolve test_ivfree_correct ext_preserv_free : core.

Lemma test_seq_rclobberable_correct (l: list (reg*ival)) r: forall (si: fpasv),
  sifree si r ->
  si r = None ->
  test_seq_rclobberable l r = true -> sifree (exec_seq l si) r /\ exec_seq l si r = None.
Proof.
  induction l as [|(r',sv) l]; simpl; auto.
  intros si SVFREE EQNONE1; autorewrite with bools.
  intros ((DIFF & TESTsv) & TESTl).
  eapply IHl; eauto.
  - generalize SVFREE; intros (SVF1 & SVF2).
    split; simpl.
    * intros sv0 [H|H]; subst; eauto.
    * intros r0 sv0; unfold fset; destruct Reg.eq as [->|];
      auto; try_simplify_someHyps.
  - simpl; rewrite fset_go; eauto.
Qed.

NB: test_rclobberable is linear in the size of csi
Lemma sifree_si_empty r: sifree si_empty r.
Proof.
  split; simpl; intuition.
Qed.
Local Hint Resolve sifree_si_empty: core.


Definition test_rclobberable (csi: csasv) r: bool := test_seq_rclobberable csi.(aseq) r.

Theorem test_rclobberable_only_liveness csi r sv:
  test_rclobberable csi r = true -> csi r = Some sv -> sv = fSinput false r.
Proof.
  unfold test_rclobberable; intros SEQ EQ.
  eapply (test_seq_rclobberable_correct (aseq csi) r si_empty) in SEQ; eauto.
  destruct SEQ as (_&EQNONE).
  simpl in EQ. apply restrict_alive_Some in EQ as (EQ & _).
  unfold ext in EQ; rewrite EQNONE in EQ.
  auto.
Qed.


Theorem test_rclobberable_sifree csi r:
  test_rclobberable csi r = true -> sifree csi r.
Proof.
  unfold test_rclobberable.
  intros SEQ.
  eapply (test_seq_rclobberable_correct (aseq csi) r si_empty) in SEQ; eauto.
  destruct SEQ as ((SIFREE1 & SIFREE2)&EQNONE).
  split; simpl; auto.
  intros r0 sv H.
  apply restrict_alive_Some in H as (H & _).
  apply ext_inv in H as [H | ->]; eauto using only_live_input_intro.
Qed.

Definition test_only_liveness (csi: csasv): bool :=
  match csi.(aseq) with
  | nil => true
  | _ => false
  end.

Theorem test_only_liveness_correct csi: test_only_liveness csi = true -> only_liveness csi.
Proof.
  unfold test_only_liveness. case csi as [[|] ?]; simpl. 2:congruence. intros _.
  split; simpl.
  - reflexivity.
  - intros r sv X.
    apply restrict_alive_Some in X as (<- & _).
    reflexivity.
Qed.

Definition test_clobberable (csi: csasv) (res: reg): bool
  := test_rclobberable csi res &&& test_csifreem csi.

Local Hint Resolve test_rclobberable_only_liveness test_rclobberable_sifree test_csifreem_correct: core.

Theorem test_clobberable_correct res csi:
  test_clobberable csi res = true -> clobbered_compat csi res.
Proof.
  unfold test_clobberable; autorewrite with bools.
  intuition; constructor; eauto.
Qed.