Commit 74b182a2 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Update multiplication proofs

parent e6049050
This diff is collapsed.
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz.
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Require Import Flover.Infra.Ltacs Flover.Infra.RealSimps Flover.Typing.
Require Export Flover.IntervalArithQ Flover.IntervalArith Flover.ssaPrgs.
Definition validAffineBounds (e: Expr) (A: analysisResult) (P: precond)
(checkedExpressions: expressionAffineForms) (noiseCounter: nat): Option (expressionAffineForms, nat) :=
match e with
| _ => Some (checkedExpressions, 0)
end.
......@@ -13,9 +13,10 @@ Module FloverMap := FMapAVL.Make(legacy_OrderedQExps).
Module FloverMapFacts := OrdProperties (FloverMap).
Definition analysisResult :Type := FloverMap.t (intv * error).
Definition expressionAffineForms: Type := FloverMap.t (affine_form * nat).
(**
We treat a function mapping an expression arguing on fractions as value type
to pairs of intervals on rationals and rational errors as the analysis result
**)
(* Definition analysisResult :Type := exp Q -> intv * error. *)
\ No newline at end of file
(* Definition analysisResult :Type := exp Q -> intv * error. *)
......@@ -5,14 +5,14 @@ Require Export Coq.QArith.QArith.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
Definition RangeValidator e A P :=
(* if *)
validIntervalbounds e A P NatSet.empty.
(* then true
match validAffineBounds e A P NatSet.empty with
| Some (p, b) => b
| None => false
end.
else validAffineBounds e A P NatSet.empty *)
(*if*)
validIntervalbounds e A P NatSet.empty.
(*then true
match validAffineBounds e A P NatSet.empty with
| Some (p, b) => b
| None => false
end.
else validAffineBounds e A P NatSet.empty*)
Theorem RangeValidator_sound (f : exp Q) (A : analysisResult) (P : precond)
(E : env) (Gamma : nat -> option mType) :
......
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