WIP: Port to finite maps in Coq

coq/CertificateChecker.v

@@ -13,9 +13,11 @@ Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
 
 (** Certificate checking function **)
 Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
-  if (typeCheck e defVars (typeMap defVars e)) then
-    if (validIntervalbounds e absenv P NatSet.empty) && FPRangeValidator e absenv (typeMap defVars e) NatSet.empty
-    then (validErrorbound e (typeMap defVars e) absenv NatSet.empty)
+  let tMap := (typeMap defVars e (DaisyMap.empty mType)) in
+  if (typeCheck e defVars tMap)
+  then
+    if (validIntervalbounds e absenv P NatSet.empty) && FPRangeValidator e absenv tMap NatSet.empty
+    then (validErrorbound e tMap absenv NatSet.empty)
     else false
   else false.
 
@@ -27,19 +29,20 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (def
 Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVars:
   forall (E1 E2:env),
     approxEnv E1 defVars absenv (usedVars e) NatSet.empty E2 ->
-    (forall v, NatSet.mem v (Expressions.usedVars e) = true ->
+    (forall v, NatSet.In v (Expressions.usedVars e) ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
-    (forall v, (v) mem (usedVars e) = true ->
+    (forall v, NatSet.In v  (usedVars e) ->
           exists m : mType,
             defVars v = Some m) ->
     CertificateChecker e absenv P defVars = true ->
-   exists vR vF m,
-    eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
-    eval_exp E2 defVars (toRExp e) vF m /\
-    (forall vF m,
-        eval_exp E2 defVars (toRExp e) vF m ->
-        (Rabs (vR - vF) <= Q2R (snd (absenv e))))%R.
+    exists iv err vR vF m,
+      DaisyMap.find e absenv = Some (iv, err) /\
+      eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
+      eval_exp E2 defVars (toRExp e) vF m /\
+      (forall vF m,
+          eval_exp E2 defVars (toRExp e) vF m ->
+          (Rabs (vR - vF) <= Q2R err))%R.
 (**
    The proofs is a simple composition of the soundness proofs for the range
    validator and the error bound validator.
@@ -49,55 +52,52 @@ Proof.
   unfold CertificateChecker in certificate_valid.
   rewrite <- andb_lazy_alt in certificate_valid.
   andb_to_prop certificate_valid.
-  env_assert absenv e env_e.
-  destruct env_e as [iv [err absenv_eq]].
-  destruct iv as [ivlo ivhi].
-  rewrite absenv_eq; simpl.
   pose proof (NatSetProps.empty_union_2 (Expressions.usedVars e) NatSet.empty_spec) as union_empty.
   hnf in union_empty.
-  assert (forall v1, (v1) mem (Expressions.usedVars e ∪ NatSet.empty) = true ->
-                exists m0 : mType, defVars v1 = Some m0).
-  { intros; eapply types_defined.
-    rewrite NatSet.mem_spec in *.
-    rewrite <- union_empty; eauto. }
+  assert (dVars_range_valid NatSet.empty E1 absenv).
+  { unfold dVars_range_valid.
+    intros; set_tac. }
   assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
   { hnf; intros a in_empty.
     set_tac. }
+  assert (vars_typed (usedVars e ∪ NatSet.empty) defVars).
+  { unfold vars_typed. intros; apply types_defined. set_tac. destruct H1; set_tac.
+    split; try auto. hnf; intros; set_tac. }
   rename R into validFPRanges.
-  assert (forall v, (v) mem (NatSet.empty) = true -> exists vR :R, E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R).
-  { intros v v_in_empty.
-    rewrite NatSet.mem_spec in v_in_empty.
-    inversion v_in_empty. }
-  edestruct validIntervalbounds_sound as [vR [eval_real real_bounds_e]]; eauto.
-  destruct (validErrorbound_sound e P (typeMap defVars e) L approxE1E2 H0 eval_real R0 L1 H1 P_valid H absenv_eq) as [[vF [mF eval_float]] err_bounded]; auto.
-  exists vR; exists vF; exists mF; split; auto.
+  edestruct (validIntervalbounds_sound e (A:=absenv) (P:=P) (fVars:=usedVars e) (dVars:=NatSet.empty) (Gamma:=defVars) (E:=E1))
+    as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]]; eauto.
+  destruct iv_e as [elo ehi].
+  edestruct (validErrorbound_sound e (typeMap defVars e (DaisyMap.empty mType)) L approxE1E2 H0 eval_real R0 L1 H P_valid H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
+  exists (elo, ehi), err_e, vR, vF, mF; split; auto.
 Qed.
 
 Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
-  if (typeCheckCmd f defVars (typeMapCmd defVars f) && validSSA f (freeVars f))
+  let tMap := typeMapCmd defVars f (DaisyMap.empty mType) in
+  if (typeCheckCmd f defVars tMap && validSSA f (freeVars f))
   then
     if (validIntervalboundsCmd f absenv P NatSet.empty) &&
-       FPRangeValidatorCmd f absenv (typeMapCmd defVars f) NatSet.empty
-    then (validErrorboundCmd f (typeMapCmd defVars f) absenv NatSet.empty)
+       FPRangeValidatorCmd f absenv tMap NatSet.empty
+    then (validErrorboundCmd f tMap absenv NatSet.empty)
     else false
   else false.
 
 Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars:
   forall (E1 E2:env),
     approxEnv E1 defVars absenv (freeVars f) NatSet.empty E2 ->
-    (forall v, NatSet.mem v (freeVars f)= true ->
+    (forall v, NatSet.In v (freeVars f) ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
-    (forall v, (v) mem (freeVars f) = true ->
+    (forall v, NatSet.In v (freeVars f) ->
           exists m : mType,
             defVars v = Some m) ->
     CertificateCheckerCmd f absenv P defVars = true ->
-    exists vR vF m,
+    exists iv err vR vF m,
+      DaisyMap.find  (getRetExp f) absenv = Some (iv,err) /\
     bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\
     bstep (toRCmd f) E2 defVars vF m /\
     (forall vF m,
         bstep (toRCmd f) E2 defVars vF m ->
-        (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R).
+        (Rabs (vR - vF) <= Q2R (err))%R).
 (**
    The proofs is a simple composition of the soundness proofs for the range
    validator and the error bound validator.
@@ -109,32 +109,25 @@ Proof.
   andb_to_prop certificate_valid.
   apply validSSA_sound in R0.
   destruct R0 as [outVars ssa_f].
-  env_assert absenv (getRetExp f) env_f.
-  destruct env_f as [iv [err absenv_eq]].
-  destruct iv as [ivlo ivhi].
   assert (ssa f (freeVars f ∪ NatSet.empty) outVars) as ssa_valid.
   { eapply ssa_equal_set; try eauto.
     apply NatSetProps.empty_union_2.
     apply NatSet.empty_spec. }
   rename R into validFPRanges.
-  assert (forall v, (v) mem (NatSet.empty) = true ->
-               exists vR : R,
-                 E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) as no_dVars_valid.
-  { intros v v_in_empty.
-    set_tac. inversion v_in_empty. }
-  assert (forall v, (v) mem (freeVars f ∪ NatSet.empty) = true ->
-               exists m : mType, defVars v = Some m) as types_valid.
-  { intros v v_mem; apply types_defined.
-    set_tac. rewrite NatSet.union_spec in v_mem.
-    destruct v_mem; try auto.
-    inversion H. }
+  assert (dVars_range_valid NatSet.empty E1 absenv).
+  { unfold dVars_range_valid.
+    intros; set_tac. }
+  assert (vars_typed (freeVars f ∪ NatSet.empty) defVars).
+  { unfold vars_typed. intros; apply types_defined. set_tac.
+    destruct H0; set_tac. }
   assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
     as freeVars_contained by set_tac.
-  edestruct (validIntervalboundsCmd_sound) as [vR [eval_real bounded_real_f]] ; eauto.
-  rewrite absenv_eq; simpl.
+  edestruct (validIntervalboundsCmd_sound)
+    as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]]; eauto.
+  destruct iv as [f_lo f_hi].
   edestruct validErrorboundCmd_gives_eval as [vF [mF eval_float]]; eauto.
-  exists vR; exists vF; exists mF; split; try auto.
-  split; try auto.
+  exists (f_lo, f_hi), err, vR, vF, mF; split; try auto.
+  split; try auto; split; try auto.
   intros.
   eapply validErrorboundCmd_sound; eauto.
 Qed.
\ No newline at end of file

coq/Expressions.v

@@ -168,29 +168,19 @@ Lemma expEq_trans e f g:
 Proof.
   revert e f g; induction e;
     destruct f; intros g eq1 eq2;
-      destruct g; simpl in *; try congruence;
+      destruct g; cbn in *;
         try rewrite Nat.eqb_eq in *;
-        subst; try auto.
-  - andb_to_prop eq1;
-      andb_to_prop eq2.
-    rewrite mTypeEq_compat_eq in L, L0; subst.
-    rewrite mTypeEq_refl; simpl.
+        Daisy_compute; try congruence; type_conv; subst; try auto.
+  - rewrite mTypeEq_refl; simpl.
     rewrite Qeq_bool_iff in *; lra.
-  - andb_to_prop eq1;
-      andb_to_prop eq2.
-    rewrite unopEq_compat_eq in *; subst.
+  - rewrite unopEq_compat_eq in *; subst.
     rewrite unopEq_refl; simpl.
     eapply IHe; eauto.
-  - andb_to_prop eq1;
-      andb_to_prop eq2.
-    rewrite binopEq_compat_eq in *; subst.
+  - rewrite binopEq_compat_eq in *; subst.
     rewrite binopEq_refl; simpl.
     apply andb_true_iff.
     split; [eapply IHe1; eauto | eapply IHe2; eauto].
-  - andb_to_prop eq1;
-      andb_to_prop eq2.
-    rewrite mTypeEq_compat_eq in *; subst.
-    rewrite mTypeEq_refl; simpl.
+  - rewrite mTypeEq_refl; simpl.
     eapply IHe; eauto.
 Qed.
 

coq/Infra/Ltacs.v

@@ -55,20 +55,20 @@ Definition optionLift (X Y:Type) (v:option X) (f:X -> Y) (e:Y) :=
 Lemma optionLift_eq (X Y:Type) v (f:X -> Y) (e:Y):
   match v with |Some val => f val | None => e end = optionLift X Y v f e.
 Proof.
-  cbv; auto.
+  reflexivity.
 Qed.
 
 Lemma optionLift_cond X (a:bool) (b c :X):
   (if a then b else c) = match a with |true => b |false => c end.
 Proof.
-  cbv; auto.
+  reflexivity.
 Qed.
 
 Ltac remove_matches := rewrite optionLift_eq in *.
 
 Ltac remove_conds := rewrite <- andb_lazy_alt, optionLift_cond in *.
 
-Ltac match_factorize :=
+Ltac match_factorize_asm :=
   match goal with
   | [ H: ?t = ?u |- context [optionLift _ _ ?t _ _]]
     => rewrite H; cbn
@@ -76,6 +76,12 @@ Ltac match_factorize :=
     => rewrite H1 in H2; cbn in H2
   | [ H: context [optionLift _ _ ?t _ _] |- _ ]
     => destruct t eqn:?; cbn in H; try congruence
+  end.
+
+
+Ltac match_factorize :=
+  match_factorize_asm ||
+  match goal with
   | [ |- context [optionLift _ _ ?t _ _] ]
     => destruct t eqn:?; cbn; try congruence
   end.
@@ -104,9 +110,21 @@ Ltac bool_factorize :=
   | [H: _ = true |- _] => andb_to_prop H
   end.
 
+Ltac Daisy_compute_asm :=
+  repeat (
+      (try remove_conds;
+       try remove_matches;
+       repeat match_factorize_asm;
+       try pair_factorize) ||
+      bool_factorize).
+
 Ltac Daisy_compute :=
-  repeat
-    (match_simpl || bool_factorize).
+  repeat (
+      (try remove_conds;
+      try remove_matches;
+      repeat match_factorize;
+      try pair_factorize) ||
+      bool_factorize).
 
 (* Ltac destruct_if := *)
 (*   match goal with *)
@@ -133,4 +151,12 @@ Ltac Daisy_compute :=
 Tactic Notation "match_pat" open_constr(pat) tactic(t) :=
   match goal with
   | [H: ?ty |- _ ] => unify pat ty; t H
-  end.
\ No newline at end of file
+  end.
+
+Ltac telling_rewrite pat hyp :=
+  match goal with
+  | [H: context[pat] |- _ ] => rewrite hyp in H; constr:(H)
+  end.
+
+Tactic Notation "unify asm" open_constr(pat) hyp(H):=
+  telling_rewrite pat H.

coq/daisyParser.v

@@ -338,10 +338,10 @@ Definition parsePrecond (input :list Token) fuel :=
   | _ => None
   end.
 
-Definition defaultAbsenv:analysisResult := fun e => (mkIntv 0 0 ,0).
+Definition defaultAbsenv:analysisResult := DaisyMap.empty (intv * error).
 
 Definition updAbsenv (e:exp Q) (iv:intv) (err:Q) (A:analysisResult):=
-  fun e' => if expEq e e' then (iv, err) else A e'.
+  DaisyMap.add e  (iv, err) A.
 
 (** Abstract environment parser:
   The abstract environment should be encoded in the following format: