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