Commit 53984d19 authored by ='s avatar =

Adding support for unary minus; fixing certificate generation issues

parent 5607882d
......@@ -27,7 +27,11 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy
else (Qleb (maxAbs intv * (meps m)) err)
|Const _ n =>
Qleb (maxAbs intv * (meps m)) err
|Unop _ _ => false
|Unop Neg e =>
if (validErrorbound e typeMap absenv dVars)
then Qeq_bool err (snd (absenv e))
else false
|Unop Inv e => false
|Binop b e1 e2 =>
if ((validErrorbound e1 typeMap absenv dVars) && (validErrorbound e2 typeMap absenv dVars))
then
......@@ -2062,7 +2066,30 @@ Proof.
rewrite absenv_eq in valid_error.
case_eq (Gamma (Unop u e)); intros; rewrite H in valid_error; [ | inversion valid_error ].
andb_to_prop valid_error.
inversion R.
destruct u; try congruence.
env_assert absenv e absenv_e.
destruct absenv_e as [iv [err_e absenv_e]].
rename R into valid_error.
andb_to_prop valid_error.
apply Qeq_bool_iff in R.
apply Qeq_eqR in R.
rewrite R.
destruct iv as [e_lo e_hi].
inversion eval_real; subst.
inversion eval_float; subst.
unfold evalUnop.
apply bound_flip_sub.
eapply IHe; eauto.
+ simpl in typing_ok.
rewrite H in typing_ok.
case_eq (Gamma e); intros; rewrite H0 in typing_ok; [ | inversion typing_ok ].
andb_to_prop typing_ok; auto.
+ simpl in valid_intv.
rewrite absenv_eq in valid_intv; andb_to_prop valid_intv.
auto.
+ instantiate (1 := e_hi).
instantiate (1 := e_lo).
rewrite absenv_e; auto.
- pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_intv) as env_approx_p.
assert (typing_copy := typing_ok).
assert (valid_error_copy := valid_error).
......@@ -2200,47 +2227,47 @@ Proof.
apply H0.
Qed.
Lemma validErrorbound_subset e tmap absenv dVars dVars':
validErrorbound e tmap absenv dVars = true ->
NatSet.Subset dVars dVars' ->
validErrorbound e tmap absenv dVars' = true.
Proof.
induction e; intros validBound_e_dV subset_dV; simpl in *; try auto.
- destruct (absenv (Var Q n)); simpl in *.
case_eq (tmap (Var Q n)); intros; rewrite H in validBound_e_dV; [ | inversion validBound_e_dV ].
andb_to_prop validBound_e_dV.
apply Is_true_eq_true; apply andb_prop_intro; split.
+ apply Is_true_eq_left in L; auto.
+ case_eq (NatSet.mem n dVars);
intros case_mem; rewrite case_mem in *; simpl in *.
* hnf in subset_dV.
rewrite NatSet.mem_spec in case_mem.
specialize (subset_dV n case_mem).
rewrite <- NatSet.mem_spec in subset_dV.
rewrite subset_dV.
apply Is_true_eq_left; auto.
* case_eq (NatSet.mem n dVars'); intros case_mem';
apply Is_true_eq_left; auto.
- destruct (absenv (Binop b e1 e2)); simpl in *.
case_eq (tmap (Binop b e1 e2)); intros; rewrite H in validBound_e_dV; [ | inversion validBound_e_dV ].
rewrite <- andb_lazy_alt in *.
andb_to_prop validBound_e_dV.
rewrite andb_true_iff; split; try auto.
destruct (absenv e1); destruct (absenv e2).
rewrite <- andb_lazy_alt.
rewrite andb_true_iff; split; try auto.
repeat (rewrite andb_true_iff; split); auto.
- destruct (absenv (Downcast m e)); simpl in *.
case_eq (tmap (Downcast m e)); intros; rewrite H in validBound_e_dV; [ | inversion validBound_e_dV ].
andb_to_prop validBound_e_dV.
rewrite <- andb_lazy_alt.
rewrite L; simpl.
destruct (absenv e); simpl in *.
apply andb_true_iff in R; destruct R.
apply andb_true_iff; split.
+ apply IHe; auto.
+ auto.
Qed.
(* Lemma validErrorbound_subset e tmap absenv dVars dVars': *)
(* validErrorbound e tmap absenv dVars = true -> *)
(* NatSet.Subset dVars dVars' -> *)
(* validErrorbound e tmap absenv dVars' = true. *)
(* Proof. *)
(* induction e; intros validBound_e_dV subset_dV; simpl in *; try auto. *)
(* - destruct (absenv (Var Q n)); simpl in *. *)
(* case_eq (tmap (Var Q n)); intros; rewrite H in validBound_e_dV; [ | inversion validBound_e_dV ]. *)
(* andb_to_prop validBound_e_dV. *)
(* apply Is_true_eq_true; apply andb_prop_intro; split. *)
(* + apply Is_true_eq_left in L; auto. *)
(* + case_eq (NatSet.mem n dVars); *)
(* intros case_mem; rewrite case_mem in *; simpl in *. *)
(* * hnf in subset_dV. *)
(* rewrite NatSet.mem_spec in case_mem. *)
(* specialize (subset_dV n case_mem). *)
(* rewrite <- NatSet.mem_spec in subset_dV. *)
(* rewrite subset_dV. *)
(* apply Is_true_eq_left; auto. *)
(* * case_eq (NatSet.mem n dVars'); intros case_mem'; *)
(* apply Is_true_eq_left; auto. *)
(* - destruct (absenv (Binop b e1 e2)); simpl in *. *)
(* case_eq (tmap (Binop b e1 e2)); intros; rewrite H in validBound_e_dV; [ | inversion validBound_e_dV ]. *)
(* rewrite <- andb_lazy_alt in *. *)
(* andb_to_prop validBound_e_dV. *)
(* rewrite andb_true_iff; split; try auto. *)
(* destruct (absenv e1); destruct (absenv e2). *)
(* rewrite <- andb_lazy_alt. *)
(* rewrite andb_true_iff; split; try auto. *)
(* repeat (rewrite andb_true_iff; split); auto. *)
(* - destruct (absenv (Downcast m e)); simpl in *. *)
(* case_eq (tmap (Downcast m e)); intros; rewrite H in validBound_e_dV; [ | inversion validBound_e_dV ]. *)
(* andb_to_prop validBound_e_dV. *)
(* rewrite <- andb_lazy_alt. *)
(* rewrite L; simpl. *)
(* destruct (absenv e); simpl in *. *)
(* apply andb_true_iff in R; destruct R. *)
(* apply andb_true_iff; split. *)
(* + apply IHe; auto. *)
(* + auto. *)
(* Qed. *)
Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
......
......@@ -11,6 +11,7 @@ import utils.Interval
import utils.Rational
import utils.FinitePrecision._
import analysis.SpecsProcessingPhase
import lang.TreeOps.allVariablesOf
object CertificatePhase extends DaisyPhase {
......@@ -75,6 +76,9 @@ object CertificatePhase extends DaisyPhase {
case Some (pre) =>
//the definitions for the whole expression
val (theDefinitions, lastGenName) = getCmd(theBody.get,precision(fnc.id),constPrecision, reporter,prv)
// generate the mapping from variable ids to variable types
val (defVars, defVarsName) =
getDefVars(fnc, precision(fnc.id), reporter, prv)
//generate the precondition
val (thePreconditionFunction, functionName) =
getPrecondFunction(pre, fnc.id.toString, reporter, prv)
......@@ -82,10 +86,10 @@ object CertificatePhase extends DaisyPhase {
val (analysisResultText, analysisResultName) =
getAbsEnvDef(theBody.get, errorMap, rangeMap, precision(fnc.id), fnc.id.toString, prv, reporter)
//generate the final evaluation statement
val functionCall = getComputeExpr(lastGenName,analysisResultName,functionName,fnc.id.toString,prv)
val functionCall = getComputeExpr(lastGenName,analysisResultName,functionName,defVarsName, fnc.id.toString,prv)
//val functionCall = getAllComputeExps(theBody.get, analysisResultName, functionName, prv)
//compose the strings
val textWithoutFCall = theDefinitions + "\n\n" + thePreconditionFunction + "\n\n" + analysisResultText
val textWithoutFCall = theDefinitions + "\n\n" + defVars + "\n\n" + thePreconditionFunction + "\n\n" + analysisResultText
val certificateText =
if (prv == "hol-light")
textWithoutFCall + "\n\n" + "let theRewrites = [thePrecondition;absenv;" + holLightExpList(theBody.get) + "];;" + "\n" + functionCall + "\nexit(0);;"
......@@ -133,12 +137,11 @@ object CertificatePhase extends DaisyPhase {
}
}
private def coqVariable(vname:Identifier, id:Int, precision:Precision, reporter:Reporter) :(String, String) =
private def coqVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
//FIXME: Ugly Hack to get disjoint names for multiple function encodings with same variable names:
val freshId = nextFreshVariable()
val prec = coqPrecision(precision, reporter)
val theExpr = s"Definition ExpVar$vname$freshId :exp Q := Var Q $prec $id.\n"
val theExpr = s"Definition ExpVar$vname$freshId :exp Q := Var Q $id.\n"
(theExpr,s"ExpVar$vname$freshId")
}
......@@ -243,8 +246,10 @@ object CertificatePhase extends DaisyPhase {
reporter.fatalError("Unsupported value")
}
private def coqDowncast(nameOp:String, prec:Precision, reporter:Reporter) :(String, String) =
(s"Definition Downcast$nameOp :exp Q := Downcast ${coqPrecision(prec, reporter)} $nameOp.\n", s"Downcast$nameOp")
private def coqDowncast(nameOp:String, prec:Precision, reporter:Reporter) :(String, String) = {
val name = s"Downcast${coqPrecision(prec, reporter)}$nameOp"
(s"Definition $name :exp Q := Downcast ${coqPrecision(prec, reporter)} $nameOp.\n", name)
}
private def coqUMin (e:Expr, nameOp:String, reporter:Reporter) :(String, String) =
(s"Definition UMin${nameOp} :exp Q := Unop Neg $nameOp.\n", s"UMin${nameOp}")
......@@ -269,7 +274,7 @@ object CertificatePhase extends DaisyPhase {
identifierNums += (id -> varId)
val (definition, name) =
if (prv == "coq"){
coqVariable (id, varId, precision(id), reporter)
coqVariable (id, varId, reporter)
}else if (prv == "hol4"){
hol4Variable (id, varId, reporter)
}else {
......@@ -400,7 +405,7 @@ object CertificatePhase extends DaisyPhase {
identifierNums += (x -> varId)
val (varDef, varName) =
if (prv == "coq"){
coqVariable (x, varId, precision(x), reporter)
coqVariable (x, varId, reporter)
}else{
hol4Variable (x, varId, reporter)
}
......@@ -466,6 +471,26 @@ object CertificatePhase extends DaisyPhase {
(theFunction, s"thePrecondition_${fName}")
}
private def getDefVars(fnc:FunDef, precMap:Map[Identifier, Precision], reporter:Reporter, prv:String) : (String, String) = {
if (prv == "coq")
coqDefVars(fnc, precMap, reporter)
else
reporter.fatalError("Mixed precision certificate generation only supported in coq")
}
private def coqDefVars (fnc:FunDef, precMap:Map[Identifier, Precision], reporter:Reporter) : (String, String) =
{
val fName = fnc.id.toString
var theFunction = s"Definition defVars_$fName :(nat -> option mType) := fun n =>\n"
for (variable <- allVariablesOf(fnc.body.get)) {
theFunction += s"if n =? ${identifierNums(variable)} then Some ${coqPrecision(precMap(variable), reporter)} else "
}
theFunction += "None."
(theFunction, s"defVars_$fName")
}
private def hol4Precondition (ranges:Map [Identifier, (Rational, Rational)],fName:String) :(String, String) =
{
var theFunction = s"val thePrecondition_${fName}_def = Define ` \n thePrecondition${fName} (n:num):interval = \n"
......@@ -520,7 +545,7 @@ object CertificatePhase extends DaisyPhase {
val errY = errorMap(Variable (y)).toFractionString.replace("/","#")
val nameY = expressionNames(Variable(y))
conditional (
s"( expEqBool e (Var Q $prec ${identifierNums(y)}) )",
s"( expEqBool e (Var Q ${identifierNums(y)}) )",
"(" + intvY + ", " + errY + ")",
gFun)
......@@ -701,10 +726,10 @@ object CertificatePhase extends DaisyPhase {
holLightAbsEnv(e, errorMap, rangeMap, "((&0,&1),&1)") + "`;;",
"absenv")
private def getComputeExpr (lastGenName:String, analysisResultName:String,precondName:String, fName:String, prover:String) :String=
private def getComputeExpr (lastGenName:String, analysisResultName:String,precondName:String,defVarsName:String, fName:String, prover:String) :String=
if (prover == "coq")
s"Theorem ErrorBound_${fName}_Sound :\n CertificateCheckerCmd " + lastGenName + " " +
analysisResultName + " " + precondName + " = true.\n" +
analysisResultName + " " + precondName + " " + defVarsName + " = true.\n" +
"Proof.\n cbv; auto.\nQed."
else if (prover == "hol4")
"val _ = store_thm (\"" + s"ErrorBound_${fName}_Sound" + "\",\n ``CertificateCheckerCmd " +
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment