fact: Fixpoint wellBehaved {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 => wellBehaved t1 l md /\ wellBehaved t2 l md /\ let P := 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 in match OP with | DIV => P /\ evalRounded t2 l md <> match T' with Integer => 0%Z | _ => 0 end | _ => P end | OpExact _ OP t1 t2 => fun l md => let P := wellBehaved t1 l md /\ wellBehaved 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) in match OP with | DIV => P /\ evalRounded t2 l md <> 0 |_ => P end | Fma _ t1 t2 t3 => fun l md => wellBehaved t1 l md /\ wellBehaved t2 l md /\ wellBehaved 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 => wellBehaved t1 l md /\ wellBehaved t2 l md /\ wellBehaved 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 => wellBehaved t l md | FastNearbyint _ t => fun l md => wellBehaved t l md /\ -2251799813685248 <= evalRounded t l md <= 2251799813685247 | FastNearbyintToInt _ t => fun l md => wellBehaved t l md /\ -2147483648 <= evalRounded t l md <= 2147483647 | TruncToInt _ t => fun l md => wellBehaved t l md /\ (- Int32.N / 2 <= Ztrunc (evalRounded t l md) <= Int32.N / 2 - 1)%Z | FloatInj _ t => fun l md => wellBehaved t l md /\ Rabs (IZR (evalRounded t l md)) <= Rpow2 53 | Sqrt Tl' T' t => fun l md => wellBehaved t l md /\ match T' return ArithExpr Tl' T' -> _ with | Integer => fun t' => 0 <= IZR (evalRounded t' l md) | _ => fun t' => 0 <= evalRounded t' l md end t | Let _ _ _ t1 t2 => fun l md => wellBehaved t1 l md /\ wellBehaved t2 (evalRounded t1 l md, l) md | ArrayAcc _ a t => fun l md => wellBehaved t l md /\ (0 <= evalRounded t l md < Uint63.to_Z (PArray.length a))%Z | Assert _ _ _ t | Postcond _ _ _ t => fun l md => wellBehaved t l md end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)