Require Export Impure.ImpHCons. (* Import the Impure library. See https://github.com/boulme/ImpureDemo *)
Export Notations.
Import HConsing.

Require Import Coq.Bool.Bool.
Require Export SeqSimuTheory.
Require Import PArith.


Local Open Scope impure.

Import ListNotations.
Local Open Scope list_scope.


Definition FULL_DEBUG_DUMP : bool := false.

Interface of (impure) equality tests for operators

Module Type ImpParam.

Include LangParam.

Parameter op_eq: op -> op -> ?? bool.

Parameter op_eq_correct: forall o1 o2,
 WHEN op_eq o1 o2 ~> b THEN
  b=true -> o1 = o2.

End ImpParam.


Module Type ISeqLanguage.

Declare Module LP: ImpParam.

Include MkSeqLanguage LP.

End ISeqLanguage.

A generic dictinary on PseudoRegisters with an impure equality test

Module Type ImpDict.

Declare Module R: PseudoRegisters.

Parameter t: Type -> Type.

Parameter get: forall {A}, t A -> R.t -> option A.

Parameter set: forall {A}, t A -> R.t -> A -> t A.

Parameter set_spec_eq: forall A d x (v: A),
  get (set d x v) x = Some v.

Parameter set_spec_diff: forall A d x y (v: A),
  x <> y -> get (set d x v) y = get d y.

Parameter rem: forall {A}, t A -> R.t -> t A.

Parameter rem_spec_eq: forall A (d: t A) x,
  get (rem d x) x = None.

Parameter rem_spec_diff: forall A (d: t A) x y,
  x <> y -> get (rem d x) y = get d y.

Parameter empty: forall {A}, t A.

Parameter empty_spec: forall A x,
  get (empty (A:=A)) x = None.

Parameter eq_test: forall {A}, t A -> t A -> ?? bool.

Parameter eq_test_correct: forall A (SAFE: phys_eq_safe A) (d1 d2: t A),
 WHEN eq_test d1 d2 ~> b THEN
  b=true -> forall x, get d1 x = get d2 x.


Parameter not_eq_witness: forall {A}, t A -> t A -> ?? option R.t.

End ImpDict.

Specification of the provided tests

Module Type ImpSimuInterface.

Declare Module CoreL: ISeqLanguage.
Import CoreL.
Import Terms.

Parameter bblock_simu_test: reduction -> bblock -> bblock -> ?? bool.

Parameter bblock_simu_test_correct: forall reduce (p1 p2 : bblock),
    WHEN bblock_simu_test reduce p1 p2 ~> b
    THEN b = true -> forall ge : genv, bblock_simu ge p1 p2.

Parameter verb_bblock_simu_test
     : reduction ->
       (R.t -> ?? pstring) ->
       (op -> ?? pstring) -> bblock -> bblock -> ?? bool.

Parameter verb_bblock_simu_test_correct:
   forall reduce
          (string_of_name : R.t -> ?? pstring)
          (string_of_op : op -> ?? pstring)
          (p1 p2 : bblock),
    WHEN verb_bblock_simu_test reduce string_of_name string_of_op p1 p2 ~> b
    THEN b = true -> forall ge : genv, bblock_simu ge p1 p2.

End ImpSimuInterface.

Implementation of the provided tests

Module ImpSimu (L: ISeqLanguage) (Dict: ImpDict with Module R:=L.LP.R): ImpSimuInterface with Module CoreL := L.

Module CoreL:=L.

Module ST := SimuTheory L.

Import ST.
Import Terms.

Definition term_set_hid (t: term) (hid: hashcode): term :=
  match t with
  | Input x _ => Input x hid
  | App op l _ => App op l hid
  end.

Definition list_term_set_hid (l: list_term) (hid: hashcode): list_term :=
  match l with
  | LTnil _ => LTnil hid
  | LTcons t l' _ => LTcons t l' hid
  end.

Lemma term_eval_set_hid ge t hid m:
  term_eval ge (term_set_hid t hid) m = term_eval ge t m.

Lemma list_term_eval_set_hid ge l hid m:
  list_term_eval ge (list_term_set_hid l hid) m = list_term_eval ge l m.

Module D:=ImpPrelude.Dict.

Section SimuWithReduce.

Variable reduce: reduction.

Section CanonBuilding.

Variable hC_term: hashinfo term -> ?? term.
Hypothesis hC_term_correct: forall t, WHEN hC_term t ~> t' THEN forall ge m, term_eval ge (hdata t) m = term_eval ge t' m.

Variable hC_list_term: hashinfo list_term -> ?? list_term.
Hypothesis hC_list_term_correct: forall t, WHEN hC_list_term t ~> t' THEN forall ge m, list_term_eval ge (hdata t) m = list_term_eval ge t' m.


Local Open Scope positive.
Local Open Scope list_scope.

Definition hInput_hcodes (x:R.t) :=
   DO hc <~ hash 1;;
   DO hv <~ hash x;;
   RET [hc;hv].
Extraction Inline hInput_hcodes.

Definition hInput (x:R.t): ?? term :=
   DO hv <~ hInput_hcodes x;;
   hC_term {| hdata:=Input x unknown_hid; hcodes :=hv; |}.

Lemma hInput_correct x:
  WHEN hInput x ~> t THEN forall ge m, term_eval ge t m = Some (m x).
Global Opaque hInput.
Hint Resolve hInput_correct: wlp.

Definition hApp_hcodes (o:op) (l: list_term) :=
   DO hc <~ hash 2;;
   DO hv <~ hash o;;
   RET [hc;hv;list_term_get_hid l].
Extraction Inline hApp_hcodes.

Definition hApp (o:op) (l: list_term) : ?? term :=
   DO hv <~ hApp_hcodes o l;;
   hC_term {| hdata:=App o l unknown_hid; hcodes:=hv |}.

Lemma hApp_correct o l:
  WHEN hApp o l ~> t THEN forall ge m,
    term_eval ge t m = match list_term_eval ge l m with
                       | Some v => op_eval ge o v
                       | None => None
                       end.
Global Opaque hApp.
Hint Resolve hApp_correct: wlp.

Definition hLTnil (_: unit): ?? list_term :=
   hC_list_term {| hdata:=LTnil unknown_hid; hcodes := nil; |} .

Lemma hLTnil_correct x:
  WHEN hLTnil x ~> l THEN forall ge m, list_term_eval ge l m = Some nil.
Global Opaque hLTnil.
Hint Resolve hLTnil_correct: wlp.


Definition hLTcons (t: term) (l: list_term): ?? list_term :=
   hC_list_term {| hdata:=LTcons t l unknown_hid; hcodes := [term_get_hid t; list_term_get_hid l]; |}.

Lemma hLTcons_correct t l:
  WHEN hLTcons t l ~> l' THEN forall ge m,
     list_term_eval ge l' m = match term_eval ge t m, list_term_eval ge l m with
                              | Some v, Some lv => Some (v::lv)
                              | _, _ => None
                              end.
Global Opaque hLTcons.
Hint Resolve hLTcons_correct: wlp.


Record hsmem:= {hpre: list term; hpost:> Dict.t term}.

Definition hsmem_post_eval ge (hd: Dict.t term) x (m:mem) :=
   match Dict.get hd x with
   | None => Some (m x)
   | Some ht => term_eval ge ht m
   end.

Definition hsmem_get (d:hsmem) x: ?? term :=
   match Dict.get d x with
   | None => hInput x
   | Some t => RET t
   end.

Lemma hsmem_get_correct (d:hsmem) x:
  WHEN hsmem_get d x ~> t THEN forall ge m, term_eval ge t m = hsmem_post_eval ge d x m.
Global Opaque hsmem_get.
Hint Resolve hsmem_get_correct: wlp.

Local Opaque allvalid.

Definition smem_model ge (d: smem) (hd:hsmem): Prop :=
  (forall m, allvalid ge hd.(hpre) m <-> smem_valid ge d m)
  /\ (forall m x, smem_valid ge d m -> hsmem_post_eval ge hd x m = (ST.term_eval ge (d x) m)).

Lemma smem_model_smem_valid_alt ge d hd: smem_model ge d hd ->
 forall m x, smem_valid ge d m -> hsmem_post_eval ge hd x m <> None.

Lemma smem_model_allvalid_alt ge d hd: smem_model ge d hd ->
 forall m x, allvalid ge hd.(hpre) m -> hsmem_post_eval ge hd x m <> None.

Definition naive_set (hd:hsmem) x (t:term) :=
  {| hpre:= t::hd.(hpre); hpost:=Dict.set hd x t |}.

Lemma naive_set_correct hd x ht ge d t:
    smem_model ge d hd ->
    (forall m, smem_valid ge d m -> term_eval ge ht m = ST.term_eval ge t m) ->
    smem_model ge (smem_set d x t) (naive_set hd x ht).
Local Hint Resolve naive_set_correct: core.

Definition equiv_hsmem ge (hd1 hd2: hsmem) :=
      (forall m, allvalid ge hd1.(hpre) m <-> allvalid ge hd2.(hpre) m)
   /\ (forall m x, allvalid ge hd1.(hpre) m -> hsmem_post_eval ge hd1 x m = hsmem_post_eval ge hd2 x m).

Lemma equiv_smem_symmetry ge hd1 hd2:
  equiv_hsmem ge hd1 hd2 -> equiv_hsmem ge hd2 hd1.

Lemma equiv_hsmem_models ge hd1 hd2 d:
   smem_model ge d hd1 -> equiv_hsmem ge hd1 hd2 -> smem_model ge d hd2.

Variable log_assign: R.t -> term -> ?? unit.

Definition lift {A B} hid (x:A) (k: B -> ?? A) (y:B): ?? A :=
  DO b <~ phys_eq hid unknown_hid;;
  if b then k y else RET x.

Fixpoint hterm_lift (t: term): ?? term :=
  match t with
  | Input x hid => lift hid t hInput x
  | App o l hid =>
      lift hid t
       (fun l => DO lt <~ hlist_term_lift l;;
        hApp o lt) l
  end
with hlist_term_lift (l: list_term) {struct l}: ?? list_term :=
  match l with
  | LTnil hid => lift hid l hLTnil ()
  | LTcons t l' hid =>
     lift hid l
        (fun t => DO t <~ hterm_lift t;;
         DO lt <~ hlist_term_lift l';;
          hLTcons t lt) t
  end.

Lemma hterm_lift_correct t:
  WHEN hterm_lift t ~> ht THEN forall ge m, term_eval ge ht m = term_eval ge t m.
Local Hint Resolve hterm_lift_correct: wlp.
Global Opaque hterm_lift.

Variable log_new_hterm: term -> ?? unit.

Fixpoint hterm_append (l: list term) (lh: list term): ?? list term :=
  match l with
  | nil => RET lh
  | t::l' =>
     DO ht <~ hterm_lift t;;
     log_new_hterm ht;;
     hterm_append l' (ht::lh)
  end.

Lemma hterm_append_correct l: forall lh,
  WHEN hterm_append l lh ~> lh' THEN (forall ge m, allvalid ge lh' m <-> (allvalid ge l m /\ allvalid ge lh m)).
Global Opaque hterm_append.

Definition smart_set (hd:hsmem) x (ht:term) :=
     match ht with
     | Input y _ =>
       if R.eq_dec x y then
          RET (Dict.rem hd x)
       else (
          log_assign x ht;;
          RET (Dict.set hd x ht)
       )
     | _ =>
       log_assign x ht;;
       RET (Dict.set hd x ht)
     end.

Lemma smart_set_correct hd x ht:
  WHEN smart_set hd x ht ~> d THEN
    forall ge m y, hsmem_post_eval ge d y m = hsmem_post_eval ge (Dict.set hd x ht) y m.
Global Opaque smart_set.

Definition hsmem_set (hd:hsmem) x (t:term) :=
  DO pt <~ reduce t;;
  DO lht <~ hterm_append pt.(mayfail) hd.(hpre);;
  DO ht <~ hterm_lift pt.(effect);;
  log_new_hterm ht;;
  DO nd <~ smart_set hd x ht;;
  RET {| hpre := lht; hpost := nd |}.

Lemma hsmem_set_correct hd x ht:
  WHEN hsmem_set hd x ht ~> nhd THEN
    forall ge d t, smem_model ge d hd ->
    (forall m, smem_valid ge d m -> term_eval ge ht m = ST.term_eval ge t m) ->
    smem_model ge (smem_set d x t) nhd.
Local Hint Resolve hsmem_set_correct: wlp.
Global Opaque hsmem_set.


Fixpoint exp_hterm (e: exp) (hd hod: hsmem): ?? term :=
  match e with
  | PReg x => hsmem_get hd x
  | Op o le =>
     DO lt <~ list_exp_hterm le hd hod;;
     hApp o lt
  | Old e => exp_hterm e hod hod
  end
with list_exp_hterm (le: list_exp) (hd hod: hsmem): ?? list_term :=
  match le with
  | Enil => hLTnil tt
  | Econs e le' =>
     DO t <~ exp_hterm e hd hod;;
     DO lt <~ list_exp_hterm le' hd hod;;
     hLTcons t lt
  | LOld le => list_exp_hterm le hod hod
  end.

Lemma exp_hterm_correct_x ge e hod od:
   smem_model ge od hod ->
  forall hd d,
   smem_model ge d hd ->
  WHEN exp_hterm e hd hod ~> t THEN forall m, smem_valid ge d m -> smem_valid ge od m -> term_eval ge t m = ST.term_eval ge (exp_term e d od) m.
Global Opaque exp_hterm.

Lemma exp_hterm_correct e hd hod:
  WHEN exp_hterm e hd hod ~> t THEN forall ge od d m, smem_model ge od hod -> smem_model ge d hd -> smem_valid ge d m -> smem_valid ge od m -> term_eval ge t m = ST.term_eval ge (exp_term e d od) m.
Hint Resolve exp_hterm_correct: wlp.

Fixpoint hinst_smem (i: inst) (hd hod: hsmem): ?? hsmem :=
  match i with
  | nil => RET hd
  | (x, e)::i' =>
     DO ht <~ exp_hterm e hd hod;;
     DO nd <~ hsmem_set hd x ht;;
     hinst_smem i' nd hod
  end.

Lemma hinst_smem_correct i: forall hd hod,
  WHEN hinst_smem i hd hod ~> hd' THEN
    forall ge od d, smem_model ge od hod -> smem_model ge d hd -> (forall m, smem_valid ge d m -> smem_valid ge od m) -> smem_model ge (inst_smem i d od) hd'.
Global Opaque hinst_smem.
Local Hint Resolve hinst_smem_correct: wlp.

Variable log_new_inst: unit -> ?? unit.

Fixpoint bblock_hsmem_rec (p: bblock) (d: hsmem): ?? hsmem :=
  match p with
  | nil => RET d
  | i::p' =>
     log_new_inst tt;;
     DO d' <~ hinst_smem i d d;;
     bblock_hsmem_rec p' d'
  end.

Lemma bblock_hsmem_rec_correct p: forall hd,
  WHEN bblock_hsmem_rec p hd ~> hd' THEN forall ge d, smem_model ge d hd -> smem_model ge (bblock_smem_rec p d) hd'.
Global Opaque bblock_hsmem_rec.
Local Hint Resolve bblock_hsmem_rec_correct: wlp.

Definition hsmem_empty: hsmem := {| hpre:= nil ; hpost := Dict.empty |}.

Lemma hsmem_empty_correct ge: smem_model ge smem_empty hsmem_empty.

Definition bblock_hsmem: bblock -> ?? hsmem
 := fun p => bblock_hsmem_rec p hsmem_empty.

Lemma bblock_hsmem_correct p:
  WHEN bblock_hsmem p ~> hd THEN forall ge, smem_model ge (bblock_smem p) hd.
Global Opaque bblock_hsmem.

End CanonBuilding.


Definition term_hash_eq (ta tb: term): ?? bool :=
  match ta, tb with
  | Input xa _, Input xb _ =>
     if R.eq_dec xa xb
     then RET true
     else RET false
  | App oa lta _, App ob ltb _ =>
     DO b <~ op_eq oa ob ;;
     if b then phys_eq lta ltb
     else RET false
  | _,_ => RET false
  end.

Lemma term_hash_eq_correct: forall ta tb, WHEN term_hash_eq ta tb ~> b THEN b=true -> term_set_hid ta unknown_hid=term_set_hid tb unknown_hid.
Global Opaque term_hash_eq.
Hint Resolve term_hash_eq_correct: wlp.

Definition list_term_hash_eq (lta ltb: list_term): ?? bool :=
  match lta, ltb with
  | LTnil _, LTnil _ => RET true
  | LTcons ta lta _, LTcons tb ltb _ =>
      DO b <~ phys_eq ta tb ;;
     if b then phys_eq lta ltb
     else RET false
  | _,_ => RET false
  end.

Lemma list_term_hash_eq_correct: forall lta ltb, WHEN list_term_hash_eq lta ltb ~> b THEN b=true -> list_term_set_hid lta unknown_hid=list_term_set_hid ltb unknown_hid.
Global Opaque list_term_hash_eq.
Hint Resolve list_term_hash_eq_correct: wlp.

Lemma hsmem_post_eval_intro (d1 d2: hsmem):
  (forall x, Dict.get d1 x = Dict.get d2 x) -> (forall ge x m, hsmem_post_eval ge d1 x m = hsmem_post_eval ge d2 x m).

Local Hint Resolve bblock_hsmem_correct Dict.eq_test_correct: wlp.

Program Definition mk_hash_params (log: term -> ?? unit): Dict.hash_params term :=
 {|
    Dict.test_eq := phys_eq;
    Dict.hashing := fun (ht: term) => RET (term_get_hid ht);
    Dict.log := log |}.

Definition no_log_assign (x:R.t) (t:term): ?? unit := RET tt.
Definition no_log_new_term (t:term): ?? unit := RET tt.

Section Prog_Eq_Gen.

Variable log_assign: R.t -> term -> ?? unit.
Variable log_new_term: hashConsing term -> hashConsing list_term -> ??(term -> ?? unit).
Variable log_inst1: unit -> ?? unit.
Variable log_inst2: unit -> ?? unit.

Variable hco_term: hashConsing term.
Hypothesis hco_term_correct: forall t, WHEN hco_term.(hC) t ~> t' THEN forall ge m, term_eval ge (hdata t) m = term_eval ge t' m.

Variable hco_list: hashConsing list_term.
Hypothesis hco_list_correct: forall t, WHEN hco_list.(hC) t ~> t' THEN forall ge m, list_term_eval ge (hdata t) m = list_term_eval ge t' m.

Variable print_end_error: hsmem -> hsmem -> ?? unit.
Variable print_dump: (option pstring) -> ?? unit.

Variable check_failpreserv: bool.
Variable dbg_failpreserv: term -> ?? unit.

Program Definition g_bblock_simu_test (p1 p2: bblock): ?? bool :=
  DO failure_in_failpreserv <~ make_cref false;;
  DO r <~ (TRY
    DO d1 <~ bblock_hsmem hco_term.(hC) hco_list.(hC) log_assign no_log_new_term log_inst1 p1;;
    DO log_new_term <~ log_new_term hco_term hco_list;;
    DO d2 <~ bblock_hsmem hco_term.(hC) hco_list.(hC) no_log_assign log_new_term log_inst2 p2;;
    DO b <~ Dict.eq_test d1 d2 ;;
    if b then (
      (if check_failpreserv then
          let hp := mk_hash_params dbg_failpreserv in
          failure_in_failpreserv.(set)(true);;
          Sets.assert_list_incl hp d2.(hpre) d1.(hpre)
      else RET tt);;
      (if FULL_DEBUG_DUMP then
        print_dump None
      else RET tt);;
      RET check_failpreserv
    ) else (
      print_end_error d1 d2 ;;
      RET false
    )
  CATCH_FAIL s, _ =>
    DO b <~ failure_in_failpreserv.(get)();;
    if b then RET false
         else print_dump (Some s);; RET false
  ENSURE (fun b => b=true -> forall ge, bblock_simu ge p1 p2));;
  RET (`r).
Obligation 1.
  constructor 1; wlp_simplify; try congruence.
  destruct (H ge) as (EQPRE1&EQPOST1); destruct (H0 ge) as (EQPRE2&EQPOST2); clear H H0.
  apply bblock_smem_simu; auto. split.
  + intros m; rewrite <- EQPRE1, <- EQPRE2.
    rewrite ! allvalid_extensionality.
    unfold incl in * |- *; intuition eauto.
  + intros m0 x VALID; rewrite <- EQPOST1, <- EQPOST2; auto.
    erewrite hsmem_post_eval_intro; eauto.
    erewrite <- EQPRE2; auto.
    erewrite <- EQPRE1 in VALID.
    rewrite ! allvalid_extensionality in * |- *.
    unfold incl in * |- *; intuition eauto.
Qed.