fact: Fixpoint operationsExact {Tl T} (t: ArithExpr Tl T) : evalExprTypeRounded_list Tl -> _ := match t with | Int _ _ | BinFl _ _ | Var _ _ => fun l md => True | Op Tl' T' OP t1 t2 => fun l md => operationsExact t1 l md /\ operationsExact t2 l md /\ match T' return ArithExpr Tl' T' -> ArithExpr Tl' T' -> _ with | Integer => fun t1' t2' => - IZR (Int32.N / 2) <= IZR (ZOpToFunction OP (evalRounded t1' l md) (evalRounded t2' l md)) <= IZR (Int32.N / 2 - 1) | BinFloat => fun t1' t2' => Rabs (RrndOpToFunction OP md (evalRounded t1' l md) (evalRounded t2' l md)) <= Rrnd.maxval end t1 t2 | OpExact _ OP t1 t2 => fun l md => operationsExact t1 l md /\ operationsExact t2 l md /\ Rabs (ROpToFunction OP (evalRounded t1 l md) (evalRounded t2 l md)) <= Rrnd.maxval /\ RrndOpToFunction OP md (evalRounded t1 l md) (evalRounded t2 l md) = ROpToFunction OP (evalRounded t1 l md) (evalRounded t2 l md) | Fma _ t1 t2 t3 => fun l md => operationsExact t1 l md /\ operationsExact t2 l md /\ operationsExact t3 l md /\ Rabs (@Rrnd.fma md (evalRounded t1 l md) (evalRounded t2 l md) (evalRounded t3 l md)) <= Rrnd.maxval | FmaExact _ t1 t2 t3 => fun l md => operationsExact t1 l md /\ operationsExact t2 l md /\ operationsExact t3 l md /\ Rabs ((evalRounded t1 l md) * (evalRounded t2 l md) + (evalRounded t3 l md)) <= Rrnd.maxval /\ @Rrnd.fma md (evalRounded t1 l md) (evalRounded t2 l md) (evalRounded t3 l md) = (evalRounded t1 l md) * (evalRounded t2 l md) + (evalRounded t3 l md) | Nearbyint _ t => fun l md => operationsExact t l md | FastNearbyint _ t => fun l md => operationsExact t l md /\ -2251799813685248 <= evalRounded t l md <= 2251799813685247 | FastNearbyintToInt _ t => fun l md => operationsExact t l md /\ -2147483648 <= evalRounded t l md <= 2147483647 | TruncToInt _ t => fun l md => operationsExact t l md /\ (- Int32.N / 2 <= Ztrunc (evalRounded t l md) <= Int32.N / 2 - 1)%Z | FloatInj _ t => fun l md => operationsExact t l md /\ Rabs (IZR (evalRounded t l md)) <= Rpow2 53 | Sqrt _ _ t => fun l md => operationsExact t l md | ArrayAcc _ a t => fun l md => operationsExact t l md /\ (0 <= evalRounded t l md < Uint63.to_Z (PArray.length a))%Z | Let _ _ _ t1 t2 => fun l md => operationsExact t1 l md /\ operationsExact t2 (evalRounded t1 l md, l) md | Assert _ _ _ t | Postcond _ _ _ t => fun l md => operationsExact t l md end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)