Commit c8dbdf1b authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix some bugs in certificate generation and make coq proofs compile

parent fbc09b0a
...@@ -2059,8 +2059,7 @@ Proof. ...@@ -2059,8 +2059,7 @@ Proof.
apply Qeq_eqR in R0; rewrite R0. apply Qeq_eqR in R0; rewrite R0.
simpl. simpl.
eapply valid_bounds_e; eauto. eapply valid_bounds_e; eauto.
- pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_intv) as env_approx_p. - simpl in valid_error.
simpl in valid_error.
destruct (absenv e1) as [[ivlo1 ivhi1] err1] eqn:absenv_e1; destruct (absenv e1) as [[ivlo1 ivhi1] err1] eqn:absenv_e1;
destruct (absenv e2) as [[ivlo2 ivhi2] err2] eqn:absenv_e2. destruct (absenv e2) as [[ivlo2 ivhi2] err2] eqn:absenv_e2.
subst; simpl in *. subst; simpl in *.
...@@ -2282,8 +2281,8 @@ Proof. ...@@ -2282,8 +2281,8 @@ Proof.
simpl. simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
split; try auto. } split; try auto. }
{ eapply test4 with (Gamma1 := updDefVars n M0 (toRMap defVars)); { eapply swap_Gamma_bstep with (Gamma1 := updDefVars n M0 (toRMap defVars));
eauto using test3. } eauto using Rmap_updVars_comm. }
{ intros v1 v1_mem. { intros v1 v1_mem.
unfold updEnv. unfold updEnv.
case_eq (v1 =? n); intros v1_eq. case_eq (v1 =? n); intros v1_eq.
...@@ -2410,8 +2409,8 @@ Proof. ...@@ -2410,8 +2409,8 @@ Proof.
simpl. simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
split; try auto. split; try auto.
+ eapply test4 with (Gamma1 := updDefVars n M0 (toRMap defVars)); + eapply swap_Gamma_bstep with (Gamma1 := updDefVars n M0 (toRMap defVars));
eauto using test3. eauto using Rmap_updVars_comm.
+ intros v1 v1_mem. + intros v1 v1_mem.
unfold updEnv. unfold updEnv.
case_eq (v1 =? n); intros v1_eq. case_eq (v1 =? n); intros v1_eq.
......
...@@ -474,7 +474,7 @@ Proof. ...@@ -474,7 +474,7 @@ Proof.
rewrite NatSet.union_spec, NatSet.add_spec in in_set. rewrite NatSet.union_spec, NatSet.add_spec in in_set.
destruct in_set as [P1 | [ P2 | P3]]; auto. destruct in_set as [P1 | [ P2 | P3]]; auto.
+ edestruct IHf as [vR [eval_f valid_bounds_f]]; try eauto. + edestruct IHf as [vR [eval_f valid_bounds_f]]; try eauto.
eapply ssa_equal_set. symmetry in H. apply H. apply H7. } eapply ssa_equal_set. symmetry in H. apply H. apply H7.
* intros v0 mem_v0. * intros v0 mem_v0.
unfold updEnv. unfold updEnv.
case_eq (v0 =? n); intros v0_eq. case_eq (v0 =? n); intros v0_eq.
...@@ -534,7 +534,7 @@ Proof. ...@@ -534,7 +534,7 @@ Proof.
rewrite NatSet.add_spec; auto. } rewrite NatSet.add_spec; auto. }
* simpl. exists vR; split; [econstructor; eauto | auto]. * simpl. exists vR; split; [econstructor; eauto | auto].
eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto. eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto.
intros n1; rewrite <- test3; auto. intros n1; erewrite Rmap_updVars_comm; eauto.
- unfold validIntervalboundsCmd in valid_bounds_f. - unfold validIntervalboundsCmd in valid_bounds_f.
pose proof (validIntervalbounds_sound e absenv P E Gamma valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e. pose proof (validIntervalbounds_sound e absenv P E Gamma valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
destruct valid_iv_e as [vR [eval_e valid_e]]; try auto. destruct valid_iv_e as [vR [eval_e valid_e]]; try auto.
......
...@@ -68,7 +68,7 @@ object CertificatePhase extends DaisyPhase { ...@@ -68,7 +68,7 @@ object CertificatePhase extends DaisyPhase {
fullCertificate ++= getPrelude(prover, "certificate_" + prg.id) fullCertificate ++= getPrelude(prover, "certificate_" + prg.id)
//Add some spacing for readability //Add some spacing for readability
//fullCertificate ++= "\n"; fullCertificate ++= "\n";
var num_of_functions = 0 var num_of_functions = 0
for (fnc <- prg.defs) if (!fnc.precondition.isEmpty && !fnc.body.isEmpty){ for (fnc <- prg.defs) if (!fnc.precondition.isEmpty && !fnc.body.isEmpty){
...@@ -546,7 +546,7 @@ object CertificatePhase extends DaisyPhase { ...@@ -546,7 +546,7 @@ object CertificatePhase extends DaisyPhase {
val errY = errorMap(Variable(y)).toFractionString.replace("/", "#") val errY = errorMap(Variable(y)).toFractionString.replace("/", "#")
val nameY = expressionNames(Variable(y)) val nameY = expressionNames(Variable(y))
conditional ( conditional (
s"( expEqBool e (Var Q ${identifierNums(y)}) )", s"( expEq e (Var Q ${identifierNums(y)}) )",
"(" + intvY + ", " + errY + ")", "(" + intvY + ", " + errY + ")",
gFun) gFun)
...@@ -590,7 +590,7 @@ object CertificatePhase extends DaisyPhase { ...@@ -590,7 +590,7 @@ object CertificatePhase extends DaisyPhase {
reporter.fatalError(s"Unsupported operation $e while generating absenv") reporter.fatalError(s"Unsupported operation $e while generating absenv")
} }
conditional ( conditional (
"( expEqBool e " + nameE + " )", "( expEq e " + nameE + " )",
"(" + intvE + ", " + errE + ")", "(" + intvE + ", " + errE + ")",
continuation) continuation)
} }
......
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