simpler definition of reduce

2 files changed, 118 insertions, 44 deletions

diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
index 8ee04f44..43c70ae5 100644
--- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
+++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
@@ -1,5 +1,6 @@
 (** Syntax and Sequential Semantics of Abstract Basic Blocks.
 *)
+Require Import Setoid.
 Require Import ImpPrelude.
 
 Module Type PseudoRegisters.
@@ -303,50 +304,114 @@ Definition list_term_get_hid (l: list_term): hashcode :=
   end.
 
 
-Definition allvalid ge (l: list term) m := forall t, List.In t l -> term_eval ge t m <> None.
+Fixpoint allvalid ge (l: list term) m : Prop :=
+  match l with
+  | nil => True
+  | t::nil => term_eval ge t m <> None
+  | t::l' => term_eval ge t m <> None /\ allvalid ge l' m
+  end. 
+
+Lemma allvalid_extensionality ge (l: list term) m:
+  allvalid ge l m <-> (forall t, List.In t l -> term_eval ge t m <> None).
+Proof.
+  induction l as [|t l]; simpl; try (tauto).
+  destruct l.
+  - intuition (congruence || eauto).
+  - rewrite IHl; clear IHl. intuition (congruence || eauto).
+Qed.
 
-Record pseudo_term: Type := {
+Record pseudo_term: Type := intro_fail {
   mayfail: list term;
   effect: term
 }.
 
-Definition match_pseudo_term (t: term) (pt: pseudo_term) :=
+Definition match_pt (t: term) (pt: pseudo_term) :=
       (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m)
    /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1).
 
-Import ImpCore.Notations.
-Local Open Scope impure_scope.
+Lemma intro_fail_correct (l: list term) (t: term) :
+   (forall ge m, term_eval ge t m <> None <-> allvalid ge l m) -> match_pt t (intro_fail l t).
+Proof.
+  unfold match_pt; simpl; intros; intuition congruence.
+Qed.
+Hint Resolve intro_fail_correct: wlp.
 
-Record reduction (t:term):= {
-  result:> ?? pseudo_term;
-  result_correct: WHEN result ~> pt THEN match_pseudo_term t pt;
-}.
-Hint Resolve result_correct: wlp.
+Definition identity_fail (t: term):= intro_fail [t] t.
 
-Program Definition identity_reduce (t: term): reduction t := {| result := RET {| mayfail := [t]; effect := t |} |}.
-Obligation 1.
-  unfold match_pseudo_term, allvalid; wlp_simplify; congruence.
+Lemma identity_fail_correct (t: term): match_pt t (identity_fail t).
+Proof.
+  eapply intro_fail_correct; simpl; tauto.
 Qed.
-Global Opaque identity_reduce.
+Global Opaque identity_fail.
+Hint Resolve identity_fail_correct: wlp.
+
+Definition nofail (is_constant: op -> bool) (t: term):=
+    match t with
+    | Input x _ => intro_fail ([])%list t
+    | o @ [] => if is_constant o then (intro_fail ([])%list t) else (identity_fail t)
+    | _ => identity_fail t
+    end.
+
+Lemma nofail_correct (is_constant: op -> bool) t:
+ (forall ge o, is_constant o = true -> op_eval ge o nil <> None) -> match_pt t (nofail is_constant t).
+Proof.
+  destruct t; simpl.
+  + intros; eapply intro_fail_correct; simpl; intuition congruence.
+  + intros; destruct l; simpl; auto with wlp.
+    destruct (is_constant o) eqn:Heqo; simpl; intuition eauto with wlp.
+     eapply intro_fail_correct; simpl; intuition eauto with wlp.
+Qed.
+Global Opaque nofail.
+Hint Resolve nofail_correct: wlp.
 
-Program Definition failsafe_reduce (is_constant: op -> bool | forall ge o, is_constant o = true -> op_eval ge o nil <> None) (t: term) :=
-  match t with
-  | Input x _ => {| result := RET {| mayfail := []; effect := t |} |}
-  | o @ [] => match is_constant o with 
-              | true => {| result := RET {| mayfail := []; effect := t |} |}
-              | false => identity_reduce t
-              end
-  | _ => identity_reduce t
-  end.
-Obligation 1.
-  unfold match_pseudo_term, allvalid; simpl; wlp_simplify; congruence.
+Definition term_equiv t1 t2:= forall ge m, term_eval ge t1 m = term_eval ge t2 m.
+
+Global Instance term_equiv_Equivalence : Equivalence term_equiv.
+Proof.
+  split; intro x; unfold term_equiv; intros; eauto.
+  eapply eq_trans; eauto.
 Qed.
-Obligation 2.
-  unfold match_pseudo_term, allvalid; simpl; wlp_simplify.
+
+Lemma match_pt_term_equiv t1 t2 pt: term_equiv t1 t2 -> match_pt t1 pt -> match_pt t2 pt.
+Proof.
+  unfold match_pt, term_equiv.
+  intros H. intuition; try (erewrite <- H1 in * |- *; congruence).
+  erewrite <- H2; eauto; congruence.
 Qed.
-Obligation 3.
-  intuition congruence.
+Hint Resolve match_pt_term_equiv: wlp.
+
+Definition app_fail (l: list term) (pt: pseudo_term): pseudo_term :=
+  {| mayfail := List.rev_append l pt.(mayfail); effect := pt.(effect) |}.
+
+Lemma app_fail_correct l pt t1 t2: 
+  match_pt t1 pt -> 
+  match_pt t2 {| mayfail:=t1::l; effect:=t1 |} ->
+  match_pt t2 (app_fail l pt).
+Proof.
+  unfold match_pt in * |- *.
+  intros (XV & XE) (YV & YE).
+  split; intros ge m; try (simpl; auto; fail).
+  generalize (XV ge m) (YV ge m); rewrite !allvalid_extensionality; simpl. clear XV XE YV YE.
+  intuition subst.
+  + rewrite rev_append_rev, in_app_iff, <- in_rev in H3. destruct H3; eauto.
+  + eapply H3; eauto.
+    intros. intuition subst.
+    * eapply H2; eauto. intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff; auto.
+    * intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff, <- in_rev; auto.
 Qed.
+Hint Resolve app_fail_correct: wlp.
+Extraction Inline app_fail.
+Global Opaque app_fail.
+
+
+Import ImpCore.Notations.
+Local Open Scope impure_scope.
+
+Record reduction:= {
+  result:> term -> ?? pseudo_term;
+  result_correct: forall t, WHEN result t ~> pt THEN match_pt t pt;
+}.
+Hint Resolve result_correct: wlp.
 
 End Terms.
 
diff --git a/mppa_k1c/abstractbb/ImpSimuTest.v b/mppa_k1c/abstractbb/ImpSimuTest.v
index 13af4289..8f6b05b7 100644
--- a/mppa_k1c/abstractbb/ImpSimuTest.v
+++ b/mppa_k1c/abstractbb/ImpSimuTest.v
@@ -67,20 +67,20 @@ Declare Module CoreL: ISeqLanguage.
 Import CoreL.
 Import Terms.
 
-Parameter bblock_simu_test: (forall t : term, reduction t) -> bblock -> bblock -> ?? bool.
+Parameter bblock_simu_test: reduction -> bblock -> bblock -> ?? bool.
 
-Parameter bblock_simu_test_correct: forall (reduce: forall t, reduction t) (p1 p2 : bblock),
+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
-     : (forall t : term, reduction t) ->
+     : reduction ->
        (R.t -> ?? pstring) ->
        (op -> ?? pstring) -> bblock -> bblock -> ?? bool.
 
 Parameter verb_bblock_simu_test_correct: 
-   forall (reduce: forall t, reduction t)
+   forall reduce
           (string_of_name : R.t -> ?? pstring)
           (string_of_op : op -> ?? pstring) 
           (p1 p2 : bblock),
@@ -128,7 +128,7 @@ Module D:=ImpPrelude.Dict.
 
 Section SimuWithReduce.
 
-Variable reduce: forall t, reduction t.
+Variable reduce: reduction.
 
 Section CanonBuilding.
 
@@ -230,6 +230,8 @@ Qed.
 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 -> smem_eval ge hd x m = (smem_eval ge d x m)).
@@ -262,7 +264,7 @@ Proof.
     destruct (DM0 m) as (PRE & VALID0); clear DM0.
     assert (VALID1: allvalid ge hd.(hpre) m -> pre d ge m). { unfold smem_valid in PRE; tauto. }
     assert (VALID2: allvalid ge hd.(hpre) m -> forall x : Dict.R.t, smem_eval ge d x m <> None). { unfold smem_valid in PRE; tauto. }
-    unfold allvalid in * |- *; simpl.
+    rewrite !allvalid_extensionality in * |- *; simpl.
     intuition (subst; eauto).
     + eapply smem_valid_set_proof; eauto.
       erewrite <- EQT; eauto.
@@ -351,8 +353,10 @@ 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)).
 Proof.
   Local Hint Resolve eq_trans: localhint.
-  unfold allvalid; induction l as [|t l']; simpl; wlp_xsimplify ltac:(eauto with wlp).
-  intros REC ge m; rewrite REC; clear IHl' REC. intuition (subst; eauto with wlp localhint).
+  induction l as [|t l']; simpl; wlp_xsimplify ltac:(eauto with wlp).
+  - intros; rewrite! allvalid_extensionality; intuition eauto.
+  - intros REC ge m; rewrite REC; clear IHl' REC. rewrite !allvalid_extensionality.
+    simpl; intuition (subst; eauto with wlp localhint).
 Qed.
 (*Local Hint Resolve hterm_append_correct: wlp.*)
 Global Opaque hterm_append.
@@ -406,14 +410,14 @@ Proof.
   eapply equiv_hsmem_models; eauto; unfold equiv_hsmem; simpl. 
   destruct H as (VALID & EFFECT); split.
   - intros; rewrite APPEND, <- VALID.
-    unfold allvalid; simpl; intuition (subst; eauto).
+    rewrite !allvalid_extensionality in * |- *; simpl; intuition (subst; eauto).
   - intros m x0 ALLVALID; rewrite SMART.
     destruct (term_eval ge ht m) eqn: Hht.
     * case (R.eq_dec x x0).
       + intros; subst. unfold smem_eval; unfold smem_get; simpl. rewrite !Dict.set_spec_eq.
         erewrite LIFT, EFFECT; eauto.
       + intros; unfold smem_eval; unfold smem_get; simpl. rewrite !Dict.set_spec_diff; auto.
-    * destruct (ALLVALID ht); simpl; auto.
+    * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); simpl; auto.
 Qed.
 Local Hint Resolve hsmem_set_correct: wlp.
 Global Opaque hsmem_set.
@@ -520,11 +524,13 @@ Local Hint Resolve hbblock_smem_rec_correct: wlp.
 Definition hbblock_smem: bblock -> ?? hsmem
  := fun p => hbblock_smem_rec p {| hpre:= nil ; hpost := Dict.empty |}.
 
+Transparent allvalid.
+
 Lemma hbblock_smem_correct p:
   WHEN hbblock_smem p ~> hd THEN forall ge, smem_model ge (bblock_smem p) hd.
 Proof.
   unfold bblock_smem; wlp_simplify. eapply H. clear H.
-  unfold smem_model, smem_valid, smem_eval, allvalid, smem_eval, smem_get; simpl; intuition;
+  unfold smem_model, smem_valid, smem_eval, smem_get; simpl; intuition;
   rewrite !Dict.empty_spec in * |- *; simpl in * |- *; try congruence.
 Qed.
 Global Opaque hbblock_smem.
@@ -649,12 +655,14 @@ Obligation 1.
   destruct (H ge) as (EQPRE1&EQPOST1); destruct (H0 ge) as (EQPRE2&EQPOST2); clear H H0.
   apply bblock_smem_simu; auto.
   + intros m; rewrite <- EQPRE1, <- EQPRE2.
-    unfold incl, allvalid in * |- *; intuition eauto.
+    rewrite ! allvalid_extensionality.
+    unfold incl in * |- *; intuition eauto.
   + intros m0 x m1 VALID; rewrite <- EQPOST1, <- EQPOST2; auto.
     erewrite smem_eval_intro; eauto.
     erewrite <- EQPRE2; auto.
     erewrite <- EQPRE1 in VALID.
-    unfold incl, allvalid in * |- *; intuition eauto.
+    rewrite ! allvalid_extensionality in * |- *.
+    unfold incl in * |- *; intuition eauto.
 Qed.
 
 Theorem g_bblock_simu_test_correct p1 p2:
@@ -1011,9 +1019,10 @@ Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool :=
     DO cr <~ make_cref None;;
     DO hco_term <~ mk_annot (hCons hht);;
     DO hco_list <~ mk_annot (hCons hlht);;
-    DO result2 <~ g_bblock_simu_test 
+    DO result2 <~ g_bblock_simu_test
        (log_assign dict_info log1)
-       (log_new_term (msg_term cr))
+       (*fun _ _ => RET no_log_new_term*)  (* REM: too weak !! *)
+       (log_new_term (msg_term cr))        (* REM: too strong ?? *)
        (hlog log1 hco_term hco_list)
        (log_insert log2)
        hco_term _