Require Import Coqlib AST Registers Maps.
Require Import Op OptionMonad.
Require Import BTL_SEtheory BTL_SEsimuref.
Require Import BTL_SEsimplify BTL_SEsimplifyproof.
Require Import BTL_SEsimplifyMem.
Import ValueDomain.
Import Notations.
Import HConsing.
Import SvalNotations.
Import ListNotations.

Local Open Scope list_scope.
Local Open Scope option_monad_scope.
Local Open Scope impure.

Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := RET tt.

Definition DEBUG (s: pstring): ?? unit := XDEBUG tt (fun _ => RET s).

Implementation of Data-structure use in Hash-consing

Definition sval_hash_eq (sv1 sv2: sval): ?? bool :=
  match sv1, sv2 with
  | Sinput trg1 r1 _, Sinput trg2 r2 _ =>
      DO b1 <~ struct_eq trg1 trg2;;
      if b1
      then struct_eq r1 r2
      else RET false
  | Sop op1 lsv1 _, Sop op2 lsv2 _ =>
     DO b1 <~ phys_eq lsv1 lsv2;;
     if b1
     then struct_eq op1 op2
     else RET false
  | Sload sm1 trap1 chk1 addr1 lsv1 _, Sload sm2 trap2 chk2 addr2 lsv2 _ =>
     DO b1 <~ phys_eq lsv1 lsv2;;
     DO b2 <~ phys_eq sm1 sm2;;
     DO b3 <~ struct_eq trap1 trap2;;
     DO b4 <~ struct_eq chk1 chk2;;
     if b1 && b2 && b3 && b4
     then struct_eq addr1 addr2
     else RET false
  | Sfoldr op1 lsv1 sv0_1 _, Sfoldr op2 lsv2 sv0_2 _ =>
      DO b1 <~ phys_eq lsv1 lsv2;;
      if b1 then
        DO b2 <~ phys_eq sv0_1 sv0_2;;
        if b2 then
          struct_eq op1 op2
        else RET false
      else RET false
  | SmayUndef c0 sv0 _, SmayUndef c1 sv1 _ =>
      DO b1 <~ phys_eq c0 c1;;
      if b1
      then phys_eq sv0 sv1
      else RET false
  | Sinput _ _ _,_ | Sop _ _ _,_ | Sload _ _ _ _ _ _,_
  | Sfoldr _ _ _ _,_ | SmayUndef _ _ _, _ => RET false
  end.

Lemma sval_hash_eq_correct x y:
  WHEN sval_hash_eq x y ~> b THEN
  b = true -> sval_set_hid x unknown_hid = sval_set_hid y unknown_hid.
Global Opaque sval_hash_eq.
Global Hint Resolve sval_hash_eq_correct: wlp.

Definition list_sval_hash_eq (lsv1 lsv2: list_sval): ?? bool :=
  match lsv1, lsv2 with
  | Snil _, Snil _ => RET true
  | Scons sv1 lsv1' _, Scons sv2 lsv2' _ =>
     DO b <~ phys_eq lsv1' lsv2';;
     if b
     then phys_eq sv1 sv2
     else RET false
  | Snil _,_ | Scons _ _ _, _=> RET false
  end.

Lemma list_sval_hash_eq_correct x y:
  WHEN list_sval_hash_eq x y ~> b THEN
  b = true -> list_sval_set_hid x unknown_hid = list_sval_set_hid y unknown_hid.
Global Opaque list_sval_hash_eq.
Global Hint Resolve list_sval_hash_eq_correct: wlp.

Definition smem_hash_eq (sm1 sm2: smem): ?? bool :=
  match sm1, sm2 with
  | Sinit _, Sinit _ => RET true
  | Sstore sm1 chk1 addr1 lsv1 sinfo1 sv1 _, Sstore sm2 chk2 addr2 lsv2 sinfo2 sv2 _ =>
     DO b1 <~ phys_eq lsv1 lsv2;;
     DO b2 <~ phys_eq sm1 sm2;;
     DO b3 <~ phys_eq sv1 sv2;;
     DO b4 <~ struct_eq chk1 chk2;;
     DO b5 <~ struct_eq sinfo1 sinfo2;;
     if b1 && b2 && b3 && b4 && b5
     then struct_eq addr1 addr2
     else RET false
  | Sinit _,_ | Sstore _ _ _ _ _ _ _, _ => RET false
  end.

Lemma smem_hash_eq_correct x y:
  WHEN smem_hash_eq x y ~> b THEN
  b = true -> smem_set_hid x unknown_hid = smem_set_hid y unknown_hid.
Global Opaque smem_hash_eq.
Global Hint Resolve smem_hash_eq_correct: wlp.

Definition okclause_hash_eq (c0 c1 : okclause): ??bool :=
  match c0, c1 with
  | OKfalse _, OKfalse _ =>
      RET true
  | OKalive sv0 _, OKalive sv1 _ =>
      phys_eq sv0 sv1
  | OKpromotableOp op0 prom0 args0 _, OKpromotableOp op1 prom1 args1 _ =>
      DO b0 <~ struct_eq op0 op1;;
      DO b1 <~ struct_eq prom0 prom1;;
      if b0 && b1
      then phys_eq args0 args1
      else RET false
  | OKpromotableCond cond0 prom0 args0 _, OKpromotableCond cond1 prom1 args1 _ =>
      DO b0 <~ struct_eq cond0 cond1;;
      DO b1 <~ struct_eq prom0 prom1;;
      if b0 && b1
      then phys_eq args0 args1
      else RET false
  | OKaddrMatch addr0 args0 aa0 _, OKaddrMatch addr1 args1 aa1 _ =>
      DO b0 <~ struct_eq addr0 addr1;;
      DO b1 <~ phys_eq args0 args1;;
      if b0 && b1
      then struct_eq aa0 aa1
      else RET false
  | OKvalidAccess perm0 chk0 addr0 args0 _, OKvalidAccess perm1 chk1 addr1 args1 _ =>
      DO b0 <~ struct_eq perm0 perm1;;
      DO b1 <~ struct_eq chk0 chk1;;
      DO b2 <~ struct_eq addr0 addr1;;
      if b0 && b1 && b2
      then phys_eq args0 args1
      else RET false
  | OKfalse _, _ | OKalive _ _, _ | OKpromotableOp _ _ _ _, _ | OKpromotableCond _ _ _ _, _
  | OKaddrMatch _ _ _ _, _ | OKvalidAccess _ _ _ _ _, _ => RET false
  end.

Lemma okclause_hash_eq_correct x y:
  WHEN okclause_hash_eq x y ~> b THEN b = true ->
  okclause_set_hid x unknown_hid = okclause_set_hid y unknown_hid.
Global Opaque okclause_hash_eq.
Global Hint Resolve okclause_hash_eq_correct: wlp.


Definition hSVAL: hashP sval := {| hash_eq := sval_hash_eq; get_hid:=sval_get_hid; set_hid:=sval_set_hid |}.
Definition hLSVAL: hashP list_sval := {| hash_eq := list_sval_hash_eq; get_hid:= list_sval_get_hid; set_hid:= list_sval_set_hid |}.
Definition hSMEM: hashP smem := {| hash_eq := smem_hash_eq; get_hid:= smem_get_hid; set_hid:= smem_set_hid |}.
Definition hOKCL: hashP okclause :=
  {| hash_eq := okclause_hash_eq; get_hid:= okclause_get_hid; set_hid:= okclause_set_hid |}.

Program Definition mk_okclause_hash_params: Dict.hash_params okclause :=
 {|
    Dict.test_eq := phys_eq;
    Dict.hashing := fun (okc : okclause) => RET (okclause_get_hid okc);
    Dict.log := fun okc =>
         DO ok_name <~ string_of_hashcode (okclause_get_hid okc);;
         println ("unexpected undef behavior of hashcode:" +; (CamlStr ok_name)) |}.

Implementation of symbolic execution

Record HashConsingFcts :=
  {
    hC_sval: hashinfo sval -> ?? sval;
    hC_list_sval: hashinfo list_sval -> ?? list_sval;
    hC_smem: hashinfo smem -> ?? smem;
    hC_okclause: hashinfo okclause -> ?? okclause;
  }.

Class HashConsingHyps HCF :=
  {
    hC_sval_correct: forall s,
      WHEN HCF.(hC_sval) s ~> s' THEN forall ctx,
      sval_equiv ctx (hdata s) s';

    hC_list_sval_correct: forall lh,
      WHEN HCF.(hC_list_sval) lh ~> lh' THEN forall ctx,
      list_sval_equiv ctx (hdata lh) lh';

    hC_smem_correct: forall hm,
      WHEN HCF.(hC_smem) hm ~> hm' THEN forall ctx,
      smem_equiv ctx (hdata hm) hm';
    
    hC_okclause_correct: forall ho,
      WHEN HCF.(hC_okclause) ho ~> ho' THEN forall ctx,
      eval_okclauseb ctx (hdata ho) = eval_okclauseb ctx ho';
  }.

Global Hint Resolve hC_sval_correct hC_list_sval_correct hC_smem_correct hC_okclause_correct: wlp.

Section SymbolicCommon.

  Context `{HCF : HashConsingFcts}.
  Context `{HC : HashConsingHyps HCF}.
  Context `{RRULES: rrules_set}.


Definition reg_hcode := 1.
Definition op_hcode := 2.
Definition foldr_hcode := 3.
Definition load_hcode := 4.
Definition mayundef_hcode := 5.
Definition undef_code := 6.

Definition hSinput_hcodes (trg: bool) (r: reg) :=
  DO hc <~ hash reg_hcode;;
  DO sv1 <~ hash trg;;
  DO sv2 <~ hash r;;
  RET [hc;sv1;sv2].
Extraction Inline hSinput_hcodes.

Definition hSop_hcodes (op:operation) (lsv: list_sval) :=
  DO hc <~ hash op_hcode;;
  DO sv <~ hash op;;
  RET [hc;sv;list_sval_get_hid lsv].
Extraction Inline hSop_hcodes.

Definition hSfoldr_hcodes (op: operation) (lsv: list_sval) (sv0: sval) :=
  DO hc <~ hash foldr_hcode;;
  DO sv <~ hash op;;
  RET [hc;sv;list_sval_get_hid lsv; sval_get_hid sv0].
Extraction Inline hSfoldr_hcodes.

Definition hSload_hcodes (sm: smem) (trap: trapping_mode) (chunk: memory_chunk)
  (addr: addressing) (lsv: list_sval):=
  DO hc <~ hash load_hcode;;
  DO sv1 <~ hash trap;;
  DO sv2 <~ hash chunk;;
  DO sv3 <~ hash addr;;
  RET [hc; smem_get_hid sm; sv1; sv2; sv3; list_sval_get_hid lsv].
Extraction Inline hSload_hcodes.

Definition hSstore_hcodes (sm: smem) (chunk: memory_chunk)
  (addr: addressing) (lsv: list_sval) (si : store_info) (srce: sval) :=
  DO sv1 <~ hash chunk;;
  DO sv2 <~ hash addr;;
  DO sv3 <~ hash si;;
  RET [smem_get_hid sm; sv1; sv2; list_sval_get_hid lsv; sv3; sval_get_hid srce].
Extraction Inline hSstore_hcodes.

Definition hSmayUndef_hcodes (okc : okclause) (sv : sval) :=
  DO hc <~ hash mayundef_hcode;;
  RET [hc; okclause_get_hid okc; sval_get_hid sv].

Definition okfalse_hcode := 1.
Definition okalive_hcode := 2.
Definition okpromotableop_hcode := 3.
Definition okpromotablecond_hcode := 4.
Definition okaddrmatch_hcode := 5.
Definition okvalidaccess_hcode := 6.

Definition hOKclause_hcodes (ok : okclause) : ?? list hashcode :=
  match ok with
  | OKfalse _ =>
      DO hc <~ hash okfalse_hcode;;
      RET [hc]
  | OKalive sv _ =>
      DO hc <~ hash okalive_hcode;;
      RET [hc; sval_get_hid sv]
  | OKpromotableOp op prom lsv _ =>
      DO hc <~ hash okpromotableop_hcode;;
      DO hc1 <~ hash op;;
      DO hc2 <~ hash prom;;
      RET [hc; hc1; hc2; list_sval_get_hid lsv]
  | OKpromotableCond cond prom lsv _ =>
      DO hc <~ hash okpromotablecond_hcode;;
      DO hc1 <~ hash cond;;
      DO hc2 <~ hash prom;;
      RET [hc; hc1; hc2; list_sval_get_hid lsv]
  | OKaddrMatch addr lsv av _ =>
      DO hc <~ hash okaddrmatch_hcode;;
      DO hc1 <~ hash av;;
      RET [hc; list_sval_get_hid lsv; hc1]
  | OKvalidAccess perm chk addr lsv _ =>
      DO hc <~ hash okvalidaccess_hcode;;
      DO hc1 <~ hash perm;;
      DO hc2 <~ hash chk;;
      DO hc3 <~ hash addr;;
      RET [hc; hc1; hc2; hc3; list_sval_get_hid lsv]
  end.


Definition hSnil (_: unit): ?? list_sval :=
  hC_list_sval HCF {| hdata := Snil unknown_hid; hcodes := nil |}.

Lemma hSnil_correct:
  WHEN hSnil() ~> sv THEN forall ctx,
  list_sval_equiv ctx sv (Snil unknown_hid).
Global Opaque hSnil.
Hint Resolve hSnil_correct: wlp.

Definition hScons (sv: sval) (lsv: list_sval): ?? list_sval :=
  hC_list_sval HCF
  {| hdata := Scons sv lsv unknown_hid; hcodes := [sval_get_hid sv; list_sval_get_hid lsv] |}.

Lemma hScons_correct sv1 lsv1:
  WHEN hScons sv1 lsv1 ~> lsv1' THEN forall ctx sv2 lsv2
  (ESVEQ: sval_equiv ctx sv1 sv2)
  (ELSVEQ: list_sval_equiv ctx lsv1 lsv2),
  list_sval_equiv ctx lsv1' (Scons sv2 lsv2 unknown_hid).
Global Opaque hScons.
Hint Resolve hScons_correct: wlp.

Definition hSinput (trg:bool) (r:reg): ?? sval :=
  DO sv <~ hSinput_hcodes trg r;;
  hC_sval HCF {| hdata:=Sinput trg r unknown_hid; hcodes :=sv; |}.

Lemma hSinput_correct trg r:
  WHEN hSinput trg r ~> sv THEN forall ctx,
  sval_equiv ctx sv (Sinput trg r unknown_hid).
Global Opaque hSinput.
Hint Resolve hSinput_correct: wlp.
  
Definition hSop (op:operation) (lsv: list_sval): ?? sval :=
  DO sv <~ hSop_hcodes op lsv;;
  hC_sval HCF {| hdata:=Sop op lsv unknown_hid; hcodes :=sv |}.

Lemma hSop_fSop_correct op lsv:
  WHEN hSop op lsv ~> sv THEN forall ctx,
  sval_equiv ctx sv (fSop op lsv).
Global Opaque hSop.
Hint Resolve hSop_fSop_correct: wlp_raw.

Lemma hSop_correct op lsv1:
  WHEN hSop op lsv1 ~> sv THEN forall ctx lsv2
  (ELSVEQ: list_sval_equiv ctx lsv1 lsv2),
  sval_equiv ctx sv (Sop op lsv2 unknown_hid).
Hint Resolve hSop_correct: wlp.

Definition hSfoldr (op: operation) (lsv: list_sval) (sv0: sval): ?? sval :=
  DO sv <~ hSfoldr_hcodes op lsv sv0;;
  hC_sval HCF {| hdata:=Sfoldr op lsv sv0 unknown_hid; hcodes := sv |}.

Lemma hSfoldr_correct op lsv1 sv0_1:
  WHEN hSfoldr op lsv1 sv0_1 ~> sv THEN forall ctx lsv2 sv0_2
  (ELSVEQ: list_sval_equiv ctx lsv1 lsv2)
  (ESVEQ: sval_equiv ctx sv0_1 sv0_2),
  sval_equiv ctx sv (Sfoldr op lsv2 sv0_2 unknown_hid).
Global Opaque hSfoldr.
Hint Resolve hSfoldr_correct: wlp.
  
Definition hSload (sm: smem) (trap: trapping_mode) (chunk: memory_chunk)
  (addr: addressing) (lsv: list_sval) : ?? sval :=
  DO sv <~ hSload_hcodes sm trap chunk addr lsv;;
  hC_sval HCF {| hdata := Sload sm trap chunk addr lsv unknown_hid; hcodes := sv |}.

Lemma hSload_correct sm1 trap chunk addr lsv1:
  WHEN hSload sm1 trap chunk addr lsv1 ~> sv THEN forall ctx lsv2 sm2
  (ELSVEQ: list_sval_equiv ctx lsv1 lsv2)
  (EMEQ: smem_equiv ctx sm1 sm2),
  sval_equiv ctx sv (Sload sm2 trap chunk addr lsv2 unknown_hid).
Global Opaque hSload.
Hint Resolve hSload_correct: wlp.

Definition hSmayUndef (okc: okclause) (sv : sval): ??sval :=
  DO hc <~ hSmayUndef_hcodes okc sv;;
  hC_sval HCF {| hdata := SmayUndef okc sv unknown_hid; hcodes := hc |}.

Lemma hSmayUndef_correct okc1 sv1:
  WHEN hSmayUndef okc1 sv1 ~> sv' THEN forall ctx okc2 sv2
  (OKEQ: eval_okclauseb ctx okc1 = eval_okclauseb ctx okc2)
  (SVEQ: sval_equiv ctx sv1 sv2),
  sval_equiv ctx sv' (SmayUndef okc2 sv2 unknown_hid).
Global Opaque hSmayUndef.
Hint Resolve hSmayUndef_correct: wlp.

Definition hSstore (sm: smem) (chunk: memory_chunk)
  (addr: addressing) (lsv: list_sval) (si : store_info) (srce: sval): ?? smem :=
  DO sv <~ hSstore_hcodes sm chunk addr lsv si srce;;
  hC_smem HCF {| hdata := Sstore sm chunk addr lsv si srce unknown_hid; hcodes := sv |}.

Lemma hSstore_correct sm1 chunk addr lsv1 si sv1:
  WHEN hSstore sm1 chunk addr lsv1 si sv1 ~> sm1' THEN forall ctx lsv2 sm2 sv2
  (ELSVEQ: list_sval_equiv ctx lsv1 lsv2)
  (EMEQ: smem_equiv ctx sm1 sm2)
  (ESVEQ: sval_equiv ctx sv1 sv2),
  smem_equiv ctx sm1' (Sstore sm2 chunk addr lsv2 si sv2 unknown_hid).
Global Opaque hSstore.
Hint Resolve hSstore_correct: wlp.

Definition okclause_eq (okc0 okc1 : okclause) : Prop :=
  forall ctx, eval_okclauseb ctx okc0 = eval_okclauseb ctx okc1.

Lemma okclause_eqP [ctx okc0 okc1]
  (H : okclause_eq okc0 okc1):
  eval_okclause ctx okc0 <-> eval_okclause ctx okc1.

Program Definition mk_hOKclause (okc0 : hashcode -> okclause)
  : ?? { okc : okclause | okclause_eq okc (okc0 unknown_hid) } :=
  DO hc <~ hOKclause_hcodes (okc0 unknown_hid);;
  DO res <~ mk_annot (hC_okclause HCF {| hdata := okc0 unknown_hid; hcodes := hc |});;
  RET (exist _ (`res) _).

Definition hOKfalse (_ : unit)
  := Eval cbv [mk_hOKclause hOKclause_hcodes] in mk_hOKclause OKfalse.
Definition hOKalive (sv : sval)
  := Eval cbv [mk_hOKclause hOKclause_hcodes] in mk_hOKclause (OKalive sv).
Definition hOKpromotableOp (op : operation) prom (sargs : list_sval)
  := Eval cbv [mk_hOKclause hOKclause_hcodes] in mk_hOKclause (OKpromotableOp op prom sargs).
Definition hOKpromotableCond (cond : condition) prom (sargs : list_sval)
  := Eval cbv [mk_hOKclause hOKclause_hcodes] in mk_hOKclause (OKpromotableCond cond prom sargs).
Definition hOKaddrMatch (addr : addressing) (lsv : list_sval) (av : aval)
  := Eval cbv [mk_hOKclause hOKclause_hcodes] in mk_hOKclause (OKaddrMatch addr lsv av).
Definition hOKvalidAccess (perm : Memtype.permission) (chunk : memory_chunk) (addr : addressing) (lsv : list_sval)
  := Eval cbv [mk_hOKclause hOKclause_hcodes] in mk_hOKclause (OKvalidAccess perm chunk addr lsv).
Global Opaque hOKfalse hOKalive hOKpromotableOp hOKpromotableCond hOKaddrMatch hOKvalidAccess.


Fixpoint fsval_proj sv: ?? sval :=
  DO b <~ phys_eq (sval_get_hid sv) unknown_hid;;
  if b then
    match sv with
    | Sinput trg r _ =>
        hSinput trg r
    | Sop op hl _ =>
        DO hl' <~ fsval_list_proj hl;;
        hSop op hl'
    | Sfoldr op hl hv _ =>
        DO hl' <~ fsval_list_proj hl;;
        DO hv' <~ fsval_proj hv;;
        hSfoldr op hl' hv'
    | Sload hm t chk addr hl _ =>
        DO hm' <~ fsmem_proj hm;;
        DO hl' <~ fsval_list_proj hl;;
        hSload hm' t chk addr hl'
    | SmayUndef okc sv hc =>
        DO okc' <~ fokclause_proj okc;;
        DO sv' <~ fsval_proj sv;;
        hSmayUndef okc' sv'
    end
  else RET sv
with fsval_list_proj sl: ?? list_sval :=
  match sl with
  | Snil hc =>
      DO b <~ phys_eq hc unknown_hid;;
      if b then hSnil()
      else RET sl
  | Scons sv hl hc =>
      DO b <~ phys_eq hc unknown_hid;;
      if b then
        DO sv' <~ fsval_proj sv;;
        DO hl' <~ fsval_list_proj hl;;
        hScons sv' hl'
      else RET sl
  end
with fsmem_proj sm: ??smem :=
  match sm with
  | Sinit hc =>
      RET sm
  | Sstore sm1 chk addr hl aaddr hv hc =>
      DO b <~ phys_eq hc unknown_hid;;
      if b then
        DO sm1' <~ fsmem_proj sm1;;
        DO hl' <~ fsval_list_proj hl;;
        DO hv' <~ fsval_proj hv;;
        hSstore sm1' chk addr hl' aaddr hv'
      else RET sm
  end
with fokclause_proj (c : okclause): ??okclause :=
  DO b <~ phys_eq (okclause_get_hid c) unknown_hid;;
  if b then
  match c with
  | OKfalse _ =>
      DO c' <~ hOKfalse ();;
      RET `c'
  | OKalive sv _ =>
      DO sv' <~ fsval_proj sv;;
      DO c' <~ hOKalive sv';;
      RET `c'
  | OKpromotableOp op prom lsv _ =>
      DO lsv' <~ fsval_list_proj lsv;;
      DO c' <~ hOKpromotableOp op prom lsv';;
      RET `c'
  | OKpromotableCond cond prom lsv _ =>
      DO lsv' <~ fsval_list_proj lsv;;
      DO c' <~ hOKpromotableCond cond prom lsv';;
      RET `c'
  | OKaddrMatch addr lsv aa _ =>
      DO lsv' <~ fsval_list_proj lsv;;
      DO c' <~ hOKaddrMatch addr lsv' aa;;
      RET `c'
  | OKvalidAccess perm chk addr lsv _ =>
      DO lsv' <~ fsval_list_proj lsv;;
      DO c' <~ hOKvalidAccess perm chk addr lsv';;
      RET `c'
  end
  else RET c .

Lemma fsval_proj_correct_comb ctx:
  (forall sv, WHEN fsval_proj sv ~> sv' THEN sval_equiv ctx sv sv') /\
  (forall lsv, WHEN fsval_list_proj lsv ~> lsv' THEN list_sval_equiv ctx lsv lsv') /\
  (forall sm, WHEN fsmem_proj sm ~> sm' THEN smem_equiv ctx sm sm') /\
  (forall okc, WHEN fokclause_proj okc ~> okc' THEN eval_okclauseb ctx okc = eval_okclauseb ctx okc').

Global Opaque fsval_proj fsval_list_proj fsmem_proj fokclause_proj.

Lemma fsval_proj_correct sv:
  WHEN fsval_proj sv ~> sv' THEN forall ctx,
  sval_equiv ctx sv sv'.

Lemma fsval_list_proj_correct lsv:
  WHEN fsval_list_proj lsv ~> lsv' THEN forall ctx,
  list_sval_equiv ctx lsv lsv'.

Lemma fsmem_proj_correct sm:
  WHEN fsmem_proj sm ~> sm' THEN forall ctx,
  smem_equiv ctx sm sm'.

Hint Resolve fsval_proj_correct fsval_list_proj_correct fsmem_proj_correct: wlp.

Lemma okclause_proj_correct ctx c:
  WHEN fokclause_proj c ~> c' THEN
  eval_okclause ctx c <-> eval_okclause ctx c'.

Fixpoint imp_map [A B] (f : A -> ??B) (l : list A) : ?? list B :=
  match l with
  | nil => RET nil
  | x :: xs => DO y <~ f x;;
               DO ys <~ imp_map f xs;;
               RET (y :: ys)
  end.

Lemma okclause_proj_list_correct ctx cs:
  WHEN imp_map fokclause_proj cs ~> cs' THEN
  Forall (eval_okclause ctx) cs <-> Forall (eval_okclause ctx) cs'.

Access of registers

Definition hrs_sreg_get (hrs: ristate) r: ?? sval :=
   match hrs.(ris_sreg)!r with
   | None =>
       match ris_input_init hrs with
       | Some trg => hSinput trg r
       | None => FAILWITH "hrs_sreg_get: dead variable"
       end
   | Some sv =>
RET sv
   end.

Lemma hrs_sreg_get_spec_ris hrs r:
  WHEN hrs_sreg_get hrs r ~> hsv THEN
  exists sv, hrs r = Some sv /\
    forall ctx, sval_equiv ctx hsv sv.
Global Opaque hrs_sreg_get.

Lemma hrs_sreg_get_spec hrs r:
  WHEN hrs_sreg_get hrs r ~> hsv THEN
  forall ctx sis
  (RR: ris_refines_ok ctx hrs sis),
  exists sv, sis r = Some sv /\ sval_equiv ctx hsv sv.

Lemma hrs_sreg_get_spec_alive ctx sis hrs r
  (RR : ris_refines_ok ctx hrs sis):
  WHEN hrs_sreg_get hrs r ~> hsv THEN
  exists sv, sis r = Some sv /\ sval_equiv ctx hsv sv /\ alive (eval_sval ctx hsv).

Hash-consed operations on ireg

Definition hrs_ir_get hrs hrs_old ir: ?? sval :=
  if force_input ir
  then hrs_sreg_get hrs_old (regof ir)
  else hrs_sreg_get hrs (regof ir).

Lemma hrs_ir_get_spec hrs hrs_old ir:
  WHEN hrs_ir_get hrs hrs_old ir ~> s THEN
  forall ctx sis0 sis1
  (RR0: ris_refines_ok ctx hrs_old sis0)
  (RR1: ris_refines_ok ctx hrs sis1),
  exists sv, sis_get_ireg sis0 sis1 ir = Some sv /\ sval_equiv ctx s sv.

Global Opaque hrs_ir_get.

Fixpoint hrs_lir_get hrs hrs_old (lir: list ireg): ?? list_sval :=
  match lir with
  | nil =>
      hSnil ()
  | ir::lir =>
      DO hlsv <~ hrs_lir_get hrs hrs_old lir;;
      DO sv <~ hrs_ir_get hrs hrs_old ir;;
      hScons sv hlsv
  end.

Lemma hrs_lir_get_spec [hrs hrs_old: ristate] [lir]
  :WHEN hrs_lir_get hrs hrs_old lir ~> hlsv THEN
  forall ctx (sis0 sis1: sistate)
  (RR0: ris_refines_ok ctx hrs_old sis0)
  (RR1: ris_refines_ok ctx hrs sis1),
  exists lsv',
    lmap_sv (sis_get_ireg sis0 sis1) lir = Some lsv' /\
    list_sval_equiv ctx hlsv lsv'.

Global Opaque hrs_lir_get.

Definition hrs_lr_get hrs (lr : list reg): ?? list_sval :=
  hrs_lir_get hrs hrs (ir_input_of lr).

Lemma hrs_lr_get_spec ctx sis hrs lr
  (RR : ris_refines_ok ctx hrs sis):
  WHEN hrs_lr_get hrs lr ~> hlsv THEN
  exists lsv,
    lmap_sv sis lr = Some lsv /\
    list_sval_equiv ctx hlsv lsv.

Lemma hrs_lr_get_spec_alive ctx sis hrs lr
  (RR : ris_refines_ok ctx hrs sis):
  WHEN hrs_lr_get hrs lr ~> hlsv THEN
  exists lsv,
    lmap_sv sis lr = Some lsv /\
    list_sval_equiv ctx hlsv lsv /\
    alive (eval_list_sval ctx hlsv).

Global Opaque hrs_lr_get.


Section OKset_IMP.

Program Definition okclause_eq_test (c0 c1 : okclause):
  ??{ forall ctx, eval_okclause ctx c0 <-> eval_okclause ctx c1 }+{True} :=
  DO b <~ mk_annot (okclause_hash_eq c0 c1);;
  if dec b then RET (left _) else RET (right _).

Program Fixpoint exists_forall_imp [A : Type] [P Q : A -> Prop] (t : forall (x : A), ??{P x }+{Q x}) (l : list A)
  : ??{Exists P l}+{Forall Q l} :=
  match l with
  | nil => RET (right _)
  | x :: xs =>
      DO b0 <~ t x;;
      if b0 then RET (left _)
      else DO b1 <~ exists_forall_imp t xs;;
           RET (if b1 then left _ else right _)
           
  end.

Local Transparent OKset.pred.

Program Definition okclause_in (c : okclause) (cs : OKset.t)
  : ??{ forall ctx, OKset.eval ctx cs -> eval_okclause ctx c }+{True} :=
  DO b <~ exists_forall_imp (okclause_eq_test c) cs;;
  RET (if b then left _ else right _).

Program Definition okset_incl (cs0 cs1 : OKset.t)
  : ??{ forall ctx, OKset.eval ctx cs1 -> OKset.eval ctx cs0 }+{True} :=
  DO b <~ exists_forall_imp (fun c =>
    DO b <~ okclause_in c cs1;;
    RET (Sumbool.sumbool_not _ _ b)) cs0;;
  RET (if b then right _ else left _).

Definition assert_okset_incl (cs0 cs1 : OKset.t) : ?? unit :=
  Sets.assert_list_incl mk_okclause_hash_params cs0 cs1.

Lemma assert_okset_incl_correct cs0 cs1:
  WHEN assert_okset_incl cs0 cs1 ~> _ THEN
  forall ctx, OKset.eval ctx cs1 -> OKset.eval ctx cs0.
Global Opaque assert_okset_incl.

End OKset_IMP.


Section Add_OKset.

Definition hrs_okset_union (m : se_mode) (hy : bool) (pre cs : OKset.t) : ?? OKset.t :=
  if se_ok_check m || (hy && se_ok_equiv m) then (
    DO bin <~ okset_incl cs pre;;
    if bin then RET pre
    else FAILWITH "hrs_rsv_set: adding potential failure"
  ) else
    RET (OKset.union cs pre).

Lemma hrs_okset_union_correct ctx m hy pre cs:
  WHEN hrs_okset_union m hy pre cs ~> s THEN
  OKset.eval ctx s <-> OKset.eval ctx pre /\ OKset.eval ctx cs.

Lemma hrs_okset_union_check ctx m hy pre cs
  (CH: se_ok_check m || (hy && se_ok_equiv m) = true):
  WHEN hrs_okset_union m hy pre cs ~> s THEN
  OKset.eval ctx s <-> OKset.eval ctx pre.

Global Opaque hrs_okset_union.

Definition hrs_add_okset (m : se_mode) (hy : bool) (hrs : ristate) (cs : OKset.t) : ?? ristate :=
  DO cs' <~ hrs_okset_union m hy (ris_pre hrs) cs;;
  RET (ris_pre_set hrs cs').

Lemma hrs_add_okset_impl ctx m hy hrs cs:
  WHEN hrs_add_okset m hy hrs cs ~> hrs1 THEN
  ris_ok ctx hrs1 -> OKset.eval ctx cs.

Lemma hrs_add_okset_rhy_correct m ctx hrs sis cs
  (RR : ris_refines_ok ctx hrs sis):
  WHEN hrs_add_okset m true hrs cs ~> hrs1 THEN
  ris_refines m ctx hrs1 sis.

Lemma hrs_add_okset_pre_correct m ctx hrs sis cs (pre : okpred)
  (RR : ris_refines_ok ctx hrs sis)
  (EQV : OKset.eval ctx cs <-> `pre ctx):
  WHEN hrs_add_okset m false hrs cs ~> hrs1 THEN
  ris_refines m ctx hrs1 (add_pre pre sis).

Lemma hrs_add_okset_rel m rcs hrs cs:
  WHEN hrs_add_okset m rcs hrs cs ~> hrs' THEN
  ris_rel m hrs hrs'.
Global Opaque hrs_add_okset.

End Add_OKset.


Section Stores.

Definition store_okset chk addr args sinfo
  : ?? OKset.t :=
  DO ok0 <~ hOKvalidAccess Memtype.Writable chk addr args;;
  DO ok1 <~ match store_aaddr sinfo with
            | Some av =>
                DO ok <~ hOKaddrMatch addr args av;;
                RET (OKset.singleton (`ok))
            | None =>
                RET OKset.empty
            end;;
  RET (OKset.union (OKset.singleton (`ok0)) ok1).

Lemma store_okset_correct ctx m chk addr args sinfo src
  (MALIVE : alive (eval_smem ctx m))
  (SALIVE : alive (eval_sval ctx src)):
  WHEN store_okset chk addr args sinfo ~> ok THEN
  OKset.eval ctx ok <-> alive (eval_smem ctx (fSstore m chk addr args sinfo src)).


Definition hrewrite_store (sm: smem)
  (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) sinfo (sv : sval)
  : ?? smem :=
  match rewrite_store RRULES sm chunk addr lsv sinfo sv with
  | Some fsv => fsmem_proj fsv
  | None => hSstore sm chunk addr lsv sinfo sv
  end.

Lemma hrewrite_store_correct ctx sm chunk addr lsv aaddr sv
  (AALIVE : alive (eval_list_sval ctx lsv))
  (VALIVE : alive (eval_sval ctx sv)):
  let sm1 := fSstore sm chunk addr lsv aaddr sv in
  forall (MALIVE : alive (eval_smem ctx sm1)),
  WHEN hrewrite_store sm chunk addr lsv aaddr sv ~> rew THEN
  smem_equiv ctx rew sm1.
Global Opaque hrewrite_store.


Definition hrs_set_store se_mode m chk addr args src sinfo (hrs : ristate): ?? ristate :=
  DO oks <~ store_okset chk addr args sinfo;;
  DO hm <~ hrewrite_store m chk addr args sinfo src;;
  DO h1 <~ hrs_add_okset se_mode false hrs oks;;
  RET (rset_smem hm h1).

Lemma hrs_set_store_spec ctx sis se_mode m chk addr args src sinfo hrs
  (RR : ris_refines_ok ctx hrs sis)
  (AALIVE : alive (eval_list_sval ctx args))
  (VALIVE : alive (eval_sval ctx src))
  (MALIVE : alive (eval_smem ctx m)):
  WHEN hrs_set_store se_mode m chk addr args src sinfo hrs ~> hrs' THEN
  let m1 := fSstore m chk addr args sinfo src in
  ris_refines se_mode ctx hrs' (set_smem m1 sis).

Lemma hrs_set_store_rel se_mode m chk addr args src sinfo hrs:
  WHEN hrs_set_store se_mode m chk addr args src sinfo hrs ~> rst THEN
  ris_rel se_mode hrs rst.
Global Opaque hrs_set_store.

End Stores.

Assignment of registers

Section Rewriting.

Definition hrewrite_load (sm: smem)
  (trap : trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) aaddr
  : ?? sval :=
  match rewrite_load RRULES sm trap chunk addr lsv aaddr with
  | Some fsv => fsval_proj fsv
  | None =>
      DO load <~ hSload sm trap chunk addr lsv;;
      match aaddr with
      | Some aaddr =>
          DO okc <~ hOKaddrMatch addr lsv aaddr;;
          hSmayUndef (`okc) load
      | None =>
          RET load
      end
  end.

Lemma hrewrite_load_correct sm trap chunk addr lsv aaddr:
  WHEN hrewrite_load sm trap chunk addr lsv aaddr ~> rew THEN
  forall ctx,
  alive (eval_smem ctx sm) ->
  sval_equiv ctx rew (root_apply (Rload trap chunk addr aaddr) lsv sm).
Global Opaque hrewrite_load.


Definition fst_lhsv_imp lhsv :=
  match lhsv with
  | Scons sv (Snil _) _ => RET sv
  | _ => FAILWITH "fst_lhsv_imp: move args bug - should never occur"
  end.

Lemma fst_lhsv_imp_correct (lhsv: list_sval): forall ctx v,
  WHEN fst_lhsv_imp lhsv ~> sv THEN forall
  (HEVAL: eval_list_sval ctx lhsv = Some [v]),
  eval_sval ctx sv = Some v.
Global Opaque fst_lhsv_imp.


Definition try_simplify_move (iinfo : option BTL.inst_info) : bool :=
  match RRULES with
  | RRpromotion => false
  | _ => true
  end.

Definition simplify (rsv: root_op) (lhsv: list_sval) (iinfo : option BTL.inst_info) (sm: smem)
  : ?? sval * OKset.t :=
  match rsv with
  | Rop op =>
      let lsv := list_of_lsv lhsv in
      match (ASSERT (try_simplify_move iinfo) IN is_move_operation op lsv) with
      | Some arg =>
          DO sv <~ fst_lhsv_imp lhsv;;
          RET (sv, OKset.empty)
      | None =>
        match rewrite_ops RRULES op lsv iinfo with
        | Some (fsv, pre) =>
            DO sv <~ fsval_proj fsv;;
            DO pre' <~ imp_map fokclause_proj pre;;
            RET (sv, OKset.of_list pre')
        | None =>
            DO sv <~ hSop op lhsv;;
            RET (sv, OKset.empty)
        end
      end
  | Rload _ chunk addr aaddr =>
      DO sv <~ hrewrite_load sm NOTRAP chunk addr lhsv aaddr;;
      RET (sv, OKset.empty)
  end.

Lemma load_alive_eq_NOTRAP ctx trap chk addr aa args sm:
  let sv0 := root_apply (Rload trap chk addr aa) args sm in
  let sv1 := root_apply (Rload NOTRAP chk addr aa) args sm in
  alive (eval_sval ctx sv0) ->
  sval_equiv ctx sv0 sv1.

Lemma simplify_spec ctx rsv lhsv iinfo sm:
  let sv0 := root_apply rsv lhsv sm in
  WHEN simplify rsv lhsv iinfo sm ~> res THEN
  let (sv1, pre) := res in
  forall
  (SEVAL: eval_sval ctx sv0 <> None)
  (PRE: OKset.eval ctx pre),
  sval_equiv ctx sv0 sv1.
Global Opaque simplify.

End Rewriting.

Definition hrs_rsv_eval_okset (m : se_mode) (rsv : root_op) (args : list_sval) (emem : smem)
  : ?? list okclause :=
  match rsv with
  | Rop op =>
      if is_trapping_op op || negb (Nat.eqb (lsv_length args) (args_of_operation op))
      then DO sv <~ hSop op args;;
           DO okc <~ hOKalive sv;;
           RET (OKset.singleton (`okc))
      else RET OKset.empty
  | Rload TRAP chk addr _ =>
      DO okc <~ hOKvalidAccess Memtype.Readable chk addr args;;
      RET (OKset.singleton (`okc))
  | Rload NOTRAP _ _ _ =>
      RET OKset.empty
  end.

Lemma fSmayUndef_opt_alive_iff ctx okc sv:
  alive (eval_sval ctx (fSmayUndef_opt okc sv)) <-> alive (eval_sval ctx sv).

Lemma hrs_rsv_eval_okset_correct ctx m rsv args emem
  (EMEM: alive (eval_smem ctx emem))
  (EARGS: alive (eval_list_sval ctx args)):
  WHEN hrs_rsv_eval_okset m rsv args emem ~> cs THEN
  alive (eval_sval ctx (root_apply rsv args emem)) <-> OKset.eval ctx cs.

Global Opaque hrs_rsv_eval_okset.

Definition hrs_rsv_set (m : se_mode) r (rsv : root_op) (lsv : list_sval) (iinfo : option BTL.inst_info)
                       (emem : smem) (hrs : ristate)
  : ?? ristate :=
  DO ecs <~ hrs_rsv_eval_okset m rsv lsv emem;;
  DO ok1 <~ hrs_okset_union m false (ris_pre hrs) ecs;;
  DO simp <~ simplify rsv lsv iinfo emem;;
  let (simp_sv, simp_hy) := simp in
  DO ok2 <~ hrs_okset_union m true ok1 simp_hy;;
  RET (ris_sreg_pre_set hrs (red_PTree_set r simp_sv hrs) ok2).

Lemma ris_set_reg_refines m ctx hrs sis r sv0 sv1 rok
  (RR: ris_refines_ok ctx hrs sis)
  (EQV: alive (eval_sval ctx sv1) -> Forall (eval_okclause ctx) rok -> sval_equiv ctx sv1 sv0)
  (OK_EQ: ok_equivp True (alive (eval_sval ctx sv1)) (OKset.eval ctx rok) m.(se_ok_equiv)):
  let hrs1 := ris_sreg_pre_set hrs (red_PTree_set r sv0 hrs) rok in
  let sis1 := set_sreg r sv1 sis in
  ris_refines m ctx hrs1 sis1.

Lemma hrs_rsv_set_spec m ctx sis r rop args iinfo emem hrs
  (RR: ris_refines_ok ctx hrs sis)
  (AARG : alive (eval_list_sval ctx args))
  (AMEM : alive (eval_smem ctx emem)):
  WHEN hrs_rsv_set m r rop args iinfo emem hrs ~> hrs' THEN
  ris_refines m ctx hrs' (set_sreg r (root_apply rop args emem) sis).

Lemma hrs_rsv_set_rel m dest rop args iinfo emem hrs:
  WHEN hrs_rsv_set m dest rop args iinfo emem hrs ~> rst THEN
  ris_rel m hrs rst.
Global Opaque hrs_rsv_set.

End SymbolicCommon.