1 2open HolKernel Parse boolLib bossLib; 3open realTheory finite_mapTheory machine_ieeeTheory; 4 5val _ = new_theory "daisy"; 6 7val _ = Datatype ` X = Var string | Const string ` 8val _ = Datatype ` F = Add F F | Sub F F | Uminus F 9 | Mul F F | Div F F | Sqrt F | X X ` 10val _ = Datatype ` C = LessEq F F | Less F F 11 | GreaterEq F F | Greater F F ` 12val _ = Datatype ` B = Let string F B | Exp F ` 13val _ = Datatype ` D = If C D D | Simple B) ` 14val _ = Datatype ` S = Conj S S | Disj S S | Not S | Cons C ` 15val _ = Datatype ` A = Err string string | Assert S ` 16val _ = Datatype ` L = Rec B | NonRec D` 17val _ = Datatype ` P = Func (string list) (* inputs/outputs *) 18 (A list) (* requires *) 19 L (* body *)` 20 21val _ = Datatype ` ops = <| less : 'a -> 'a -> bool 22 ; less_eq : 'a -> 'a -> bool 23 ; greater : 'a -> 'a -> bool 24 ; greater_eq : 'a -> 'a -> bool 25 ; add : 'a -> 'a -> 'a 26 ; uminus : 'a -> 'a 27 ; sub : 'a -> 'a -> 'a 28 ; mul : 'a -> 'a -> 'a 29 ; div : 'a -> 'a -> 'a 30 ; sqrt : 'a -> 'a 31 ; to_real : 'a -> float_value 32 ; from_real : real -> 'a option 33 ; parse : string -> 'a 34 |>` 35 36val eval_X_def = Define ` 37 (eval_X c env (Var v) = env ' v) /\ 38 (eval_X c env (Const str) = c.parse str)` 39 40val eval_F_def = Define ` 41 (eval_F c env (X x) = eval_X c env x) /\ 42 (eval_F c env (Add f1 f2) = c.add (eval_F c env f1) (eval_F c env f2)) /\ 43 (eval_F c env (Div f1 f2) = c.div (eval_F c env f1) (eval_F c env f2))` 44 45val eval_C_def = Define ` 46 (eval_C c env (LessEq f1 f2) = c.less_eq (eval_F c env f1) (eval_F c env f2))` 47 48val eval_B_def = Define ` 49 (eval_B c env (Let v f b) = eval_B c (env |+ (v,eval_F c env f)) b) /\ 50 (eval_B c env (Exp f) = (eval_F c env f,env))` 51 52val eval_D_def = Define ` 53 (eval_D c env (Simple b) = eval_B c env b)` 54 55val eval_S_def = Define ` 56 (eval_S c env (Cons x) = eval_C c env x)` 57 58val eval_A_def = Define ` 59 (eval_A c env (Err _ _) = T (* checked elsewhere *)) /\ 60 (eval_A c env (Assert s) = eval_S c env s)` 61 62val has_lower_bound_def = Define ` 63 (has_lower_bound v (Assert (Cons (LessEq (X (Const r)) (X (Var w))))::rest) = 64 ((w = v) \/ has_lower_bound v rest)) /\ 65 (has_lower_bound v (Assert (Cons (Less (X (Const r)) (X (Var w))))::rest) = 66 ((w = v) \/ has_lower_bound v rest)) /\ 67 (has_lower_bound v _ = F) (* not complete *)` 68 69val has_upper_bound_def = Define ` 70 (has_upper_bound v [] = F) /\ 71 (has_upper_bound v (Assert (Cons (LessEq (X (Var w)) (X (Const r))))::rest) = 72 ((w = v) \/ has_upper_bound v rest)) /\ 73 (has_upper_bound v (Assert (Cons (Less (X (Var w)) (X (Const r))))::rest) = 74 ((w = v) \/ has_upper_bound v rest)) /\ 75 (has_upper_bound v _ = F) (* not complete *)` 76 77val req_holds_def = Define ` 78 req_holds reqs env <=> 79 FEVERY (\(v,r). has_lower_bound v reqs /\ has_upper_bound v reqs) env` 80 81val eval_P_def = Define ` 82 eval_P c inputs (Func args requires body) (n:num) = 83 if req_holds requires inputs then 84 case body of 85 | NonRec d => SOME [FST (eval_D c inputs d)] 86 | Rec b => 87 if n = 0 then 88 SOME (MAP (\v. inputs ' v) args) 89 else 90 let (_,env) = eval_B c inputs b in 91 eval_P c env (Func args requires body) (n-1) 92 else NONE` 93 94(* real configuration *) 95 96val real_conf = Define ` 97 real_conf = <| less := (<):real -> real -> bool 98 ; less_eq := (<=) 99 ; add := (+) 100 ; uminus := (\r. 0-r) 101 ; sub := (-) 102 ; mul := $* 103 ; div := (/) 104 ; sqrt := sqrt 105 ; to_real := Float (* unnecessary *) 106 ; from_real := SOME (* unnecessary *) 107 ; parse := ARB |>` 108 109(* floating pointt configurations *) 110 111val fp32_conf = Define ` 112 fp32_conf = <| less := fp32_lessThan 113 ; less_eq := fp32_lessEqual 114 ; greater := fp32_greaterThan 115 ; greater_eq := fp32_greaterEqual 116 ; add := fp32_add roundTiesToEven 117 ; uminus := fp32_negate 118 ; sub := fp32_sub roundTiesToEven 119 ; mul := fp32_mul roundTiesToEven 120 ; div := fp32_div roundTiesToEven 121 ; sqrt := fp32_sqrt roundTiesToEven 122 ; parse := ARB 123 ; to_real := fp32_to_real 124 ; from_real := \r. let w = real_to_fp32 roundTiesToEven r in 125 case fp32_to_real w of 126 | Float _ => SOME w 127 | _ => NONE |>` 128 129val fp64_conf = Define ` 130 fp64_conf = <| less := fp64_lessThan 131 ; less_eq := fp64_lessEqual 132 ; greater := fp64_greaterThan 133 ; greater_eq := fp64_greaterEqual 134 ; add := fp64_add roundTiesToEven 135 ; uminus := fp64_negate 136 ; sub := fp64_sub roundTiesToEven 137 ; mul := fp64_mul roundTiesToEven 138 ; div := fp64_div roundTiesToEven 139 ; sqrt := fp64_sqrt roundTiesToEven 140 ; parse := ARB 141 ; to_real := fp64_to_real 142 ; from_real := \r. let w = real_to_fp64 roundTiesToEven r in 143 case fp64_to_real w of 144 | Float _ => SOME w 145 | _ => NONE |>` 146 147(* correctness provided by Rosa *) 148 149val inputs_ok_def = Define ` 150 inputs_ok c inputs fp_inputs reqs = 151 (FDOM inputs = FDOM fp_inputs) /\ 152 EVERY (eval_A real_conf inputs) reqs /\ 153 (* each Err requirement must be satisfied *) 154 (���v i. MEM (Err v i) reqs ==> 155 ���fp r r'. (FLOOKUP inputs v = SOME r) /\ 156 (FLOOKUP fp_inputs v = SOME fp) /\ 157 (c.to_real fp = Float r') /\ 158 abs (r - r') <= real_conf.parse i) /\ 159 (* each variable without an Err-requirement must be the closes fp *) 160 ���v r. (FLOOKUP inputs v = SOME r) /\ (���i. ~(MEM (Err v i) reqs)) ==> 161 ���fp. (FLOOKUP fp_inputs v = SOME fp) /\ 162 (c.from_real r = SOME fp)` 163 164val distance_def = Define ` 165 distance c r fp (i,b,e) <=> 166 ���r'. (c.to_real fp = Float r') /\ 167 abs (r - r') <= real_conf.parse i /\ 168 real_conf.parse b <= r' /\ r' <= real_conf.parse e` 169 170val every3_def = Define ` 171 (every3 p [] [] [] = T) /\ 172 (every3 p (x::xs) (y::ys) (z::zs) = p x y z /\ every3 p xs ys zs)`; 173 174val rosa_correctness_def = Define ` 175 rosa_correctness fp_conf func limit ensures = 176 case func of Func args reqs _ => 177 ���inputs res fp_inputs. 178 (eval_P real_conf inputs func limit = SOME res) /\ 179 inputs_ok fp_conf inputs fp_inputs reqs ==> 180 ���fp_res. 181 (eval_P fp_conf fp_inputs func limit = SOME fp_res) /\ 182 every3 (distance fp_conf) res fp_res ensures` 183 184(* pretty printing used by daisyLib *) 185 186val _ = Define ` 187 (x_str (Var str) = str) /\ (x_str (Const str) = str) ` 188 189val _ = Define ` 190 (f_str (Add f1 f2) = "(" ++ f_str f1 ++ " + " ++ f_str f2 ++ ")") /\ 191 (f_str (X x) = x_str x)` 192 193val _ = Define ` 194 (c_str (LessEq f1 f2) = "(" ++ f_str f1 ++ " <= " ++ f_str f2 ++ ")") ` 195 196val _ = Define ` 197 (b_str (Let v f b) = "val " ++ v ++ " = " ++ f_str f ++ "\n") /\ 198 (b_str (Exp f) = f_str f ++ "\n")` 199 200val _ = Define ` 201 (d_str (Simple b) = b_str b)` 202 203val _ = Define ` 204 (s_str (Conj s1 s2) = "(" ++ s_str s1 ++ " && " ++ s_str s2 ++ ")") /\ 205 (s_str (Not s1) = "!(" ++ s_str s1 ++ ")") /\ 206 (s_str (Cons c) = "(" ++ c_str c ++ ")")` 207 208val _ = Define ` 209 (a_str (Err v i) = "(" ++ v ++ " +/- " ++ i ++ ")") /\ 210 (a_str (Assert s) = "(" ++ s_str s ++ ")")` 211 212val _ = Define ` 213 (l_str (NonRec d) = d_str d)` 214 215val sep_str_def = Define ` 216 (sep_str sep [] = "") /\ 217 (sep_str sep [x] = x) /\ 218 (sep_str sep (x::xs) = x ++ sep ++ sep_str sep xs) ` 219 220val _ = Define ` 221 (p_str name (Func args reqs l) = 222 "import daisy.lang._\n" ++ 223 "import Real._\n" ++ 224 "object Program {\n" ++ 225 "def " ++ name ++ "(" ++ 226 sep_str ", " (MAP (\v. v ++ ": Real") args) ++ "):Real = {\n" ++ 227 "require(" ++ sep_str " && " (MAP a_str reqs) ++ ")\n" ++ 228 l_str l ++ "}\n}")` 229 230val _ = export_theory(); 231