Merge pull request #865 from CakeML/Iced_cake

Add floating-point optimizer based on Icing
CakeML · May 24, 2022 · 7c4f5d1 · 7c4f5d1
2 parents a986431 + 8b37aa7
commit 7c4f5d1
Show file tree

Hide file tree

Showing 221 changed files with 47,389 additions and 1,538 deletions.
diff --git a/.gitignore b/.gitignore
@@ -75,4 +75,8 @@ compiler/benchmarks/sml/polyc_*
 compiler/benchmarks/sml/sml_*
 compiler/benchmarks/*.dat
 compiler/benchmarks/*.eps
+
+#sexp files generated by Icing
+icing/examples/output/*/*.sexp.cml
+icing/examples/*_data_prog.txt
 .DS_Store
diff --git a/README.md b/README.md
@@ -63,6 +63,10 @@ particular:
 - a list of how CakeML differs from SML and OCaml, and,
 - a number of small CakeML code examples.
 
+[icing](icing):
+Main implementation directory for the RealCake development, presented in
+"Verified Compilation and Optimization of Floating-Point Programs"
+
 [misc](misc):
 Auxiliary files providing glue between a standard HOL installation
 and what we want to use for CakeML development.

diff --git a/basis/TextIOProofScript.sml b/basis/TextIOProofScript.sml
@@ -824,7 +824,7 @@ val instream_buffered_inv_def = Define `
       bactive = TAKE (w-r) (DROP r bcontent))`;
       (*(bactive = [] <=> r = w))*)
 
-Overload TypeStamp_InstreamBuffered = “TypeStamp "InstreamBuffered" 12”;
+Overload TypeStamp_InstreamBuffered = “TypeStamp "InstreamBuffered" 35”;
 
 val INSTREAM_BUFFERED_def = Define `
   INSTREAM_BUFFERED bactive is =

diff --git a/basis/basisProgScript.sml b/basis/basisProgScript.sml
@@ -14,7 +14,7 @@ val eval_thm = let
   val state = get_ml_prog_state () |> ml_progLib.get_state
   val goal = list_mk_icomb (prim_mk_const {Thy="ml_prog", Name="eval_rel"},
     [state, env, print_e, state, mk_var ("x", v_ty)])
-  val lemma = goal |> (EVAL THENC SIMP_CONV(srw_ss())[])
+  val lemma = goal |> (EVAL THENC SIMP_CONV(srw_ss())[semanticPrimitivesTheory.state_component_equality])
   val v_thm = prove(mk_imp(lemma |> concl |> rand, goal),
     rpt strip_tac \\ rveq \\ match_mp_tac(#2(EQ_IMP_RULE lemma))
     \\ asm_simp_tac bool_ss [])

diff --git a/candle/prover/ast_extrasScript.sml b/candle/prover/ast_extrasScript.sml
@@ -48,6 +48,9 @@ Definition every_exp_def[simp]:
   (every_exp f (Lannot e l) <=>
     f (Lannot e l) /\
     every_exp f e) /\
+  (every_exp f (FpOptimise sc e) <=>
+    f (FpOptimise sc e) /\
+    every_exp f e) /\
   (every_exp f e <=> f e)
 Termination
   WF_REL_TAC `measure (exp_size o SND)`
@@ -131,7 +134,8 @@ Definition freevars_def[simp]:
                                        {Short fn; Short vn}) f)) ∪
        (freevars x DIFF set (MAP (Short o FST) f))) ∧
   freevars (Tannot x t) = freevars x ∧
-  freevars (Lannot x l) = freevars x
+  freevars (Lannot x l) = freevars x ∧
+  freevars (FpOptimise sc e) = freevars e
 Termination
   wf_rel_tac ‘measure exp_size’
 End
@@ -148,4 +152,3 @@ Definition do_partial_app_def:
 End
 
 val _ = export_theory ();
-
diff --git a/candle/prover/candle_basis_evaluateScript.sml b/candle/prover/candle_basis_evaluateScript.sml
@@ -209,19 +209,38 @@ Theorem evaluate_basis_v_ok_App:
   ^(get_goal "App")
 Proof
   rw [evaluate_def]
+  \\ Cases_on ‘getOpClass op’
   \\ gvs [CaseEqs ["bool", "option", "prod", "semanticPrimitives$result"], SF SFY_ss]
-  \\ gvs [do_app_cases, Boolv_def]
-  \\ rw [v_ok_def]
+  >- (Cases_on ‘op’ \\ gs[])
+  >- (Cases_on ‘op’ \\ gs[])
+  >- (Cases_on ‘op’ \\ gs[])
+  >- (Cases_on ‘op’ \\ gs[])
   >- (
-    gvs [store_alloc_def, post_state_ok_def]
-    \\ strip_tac
-    \\ first_x_assum (drule_all_then assume_tac) \\ gs []
-  )
-  >- (
-    irule v_ok_v_to_list
-    \\ first_assum (irule_at Any)
-    \\ first_x_assum irule \\ gs []
-    \\ gs [post_state_ok_def])
+    gvs [do_app_cases, Boolv_def]
+    \\ rw [v_ok_def]
+    >- (
+      gvs [store_alloc_def, post_state_ok_def]
+      \\ strip_tac
+      \\ first_x_assum (drule_all_then assume_tac) \\ gs []
+    )
+    >- (
+      irule v_ok_v_to_list
+      \\ first_assum (irule_at Any)
+      \\ first_x_assum irule \\ gs []
+      \\ gs [post_state_ok_def]))
+  >- (Cases_on ‘op’ \\ gs[])
+  >- (Cases_on ‘op’ \\ gs[])
+QED
+
+Theorem evaluate_basis_v_ok_FpOptimise:
+  ^(get_goal "FpOptimise")
+Proof
+  rw [evaluate_def]
+  \\ gvs [CaseEqs ["bool", "option", "prod", "semanticPrimitives$result"], SF SFY_ss]
+  >- (irule EVERY_v_ok_do_fpoptimise \\ first_assum irule \\ gs[simple_exp_def])
+  >- (Cases_on ‘e'’ \\ gs[] \\ first_assum irule \\ gs[simple_exp_def])
+  >- (irule EVERY_v_ok_do_fpoptimise \\ first_assum irule \\ gs[simple_exp_def])
+  >- (Cases_on ‘e'’ \\ gs[] \\ first_assum irule \\ gs[simple_exp_def])
 QED
 
 Theorem evaluate_basis_v_ok_decs_Nil:
@@ -377,6 +396,7 @@ Proof
   \\ rewrite_tac [evaluate_basis_v_ok_Nil, evaluate_basis_v_ok_Cons,
                   evaluate_basis_v_ok_Lit, evaluate_basis_v_ok_Con,
                   evaluate_basis_v_ok_Var, evaluate_basis_v_ok_App,
+                  evaluate_basis_v_ok_FpOptimise,
                   evaluate_basis_v_ok_decs_Nil,
                   evaluate_basis_v_ok_decs_Cons,
                   evaluate_basis_v_ok_decs_Dlet,

diff --git a/candle/prover/candle_prover_evaluateScript.sml b/candle/prover/candle_prover_evaluateScript.sml
@@ -405,7 +405,7 @@ Proof
     \\ gvs [v_ok_def, store_alloc_def, EVERY_EL, LLOOKUP_EQ_EL]
     \\ first_assum (irule_at Any) \\ gs []
     \\ rw [EL_APPEND_EQN] \\ gs [NOT_LESS, LESS_OR_EQ, ref_ok_def]
-    >- (
+    \\ TRY (
       gs [kernel_loc_ok_def, LLOOKUP_EQ_EL, EL_APPEND_EQN]
       \\ first_x_assum (drule_then strip_assume_tac)
       \\ rw [] \\ gs [SF SFY_ss])
@@ -558,6 +558,22 @@ Proof
     \\ first_assum (irule_at Any)
     \\ simp [v_ok_def])
   \\ Cases_on ‘∃cmp. op = FP_cmp cmp’ \\ gs []
+  >- (
+    rw [do_app_cases] \\ gs [SF SFY_ss]
+    \\ first_assum (irule_at Any)
+    \\ simp [Boolv_def]
+    \\ rw [v_ok_def])
+  \\ Cases_on ‘∃bop. op = Real_bop bop’ \\ gs []
+  >- (
+    rw [do_app_cases] \\ gs [SF SFY_ss]
+    \\ first_assum (irule_at Any)
+    \\ simp [v_ok_def])
+  \\ Cases_on ‘∃uop. op = Real_uop uop’ \\ gs []
+  >- (
+    rw [do_app_cases] \\ gs [SF SFY_ss]
+    \\ first_assum (irule_at Any)
+    \\ simp [v_ok_def])
+  \\ Cases_on ‘∃cmp. op = Real_cmp cmp’ \\ gs []
   >- (
     rw [do_app_cases] \\ gs [SF SFY_ss]
     \\ first_assum (irule_at Any)
@@ -617,22 +633,64 @@ Proof
     \\ rw [EL_APPEND_EQN] \\ gs [NOT_LESS, LESS_OR_EQ, ref_ok_def]
     \\ first_x_assum (drule_then assume_tac)
     \\ drule kernel_loc_ok_LENGTH \\ gs [])
+  \\ Cases_on ‘op = FpFromWord’ \\ gs[]
+  >- (
+    rw[do_app_cases] \\ gs [SF SFY_ss]
+    \\ first_assum (irule_at Any)
+    \\ simp [v_ok_def])
+  \\ Cases_on ‘op = FpToWord’ \\ gs[]
+  >- (
+    rw[do_app_cases] \\ gs [SF SFY_ss]
+    \\ first_assum (irule_at Any)
+    \\ simp [v_ok_def])
+  \\ Cases_on ‘op = RealFromFP’ \\ gs[]
+  >- (
+    rw[do_app_cases] \\ gs [SF SFY_ss]
+    \\ first_assum (irule_at Any)
+    \\ simp [v_ok_def])
   \\ Cases_on ‘op’ \\ gs []
 QED
 
 Theorem evaluate_v_ok_Op:
   op ≠ Opapp ∧ op ≠ Eval ⇒ ^(get_goal "App")
 Proof
-  rw [evaluate_def]
-  \\ gvs [AllCaseEqs()]
-  \\ first_x_assum (drule_all_then strip_assume_tac) \\ gs [state_ok_def]
-  \\ rename1 ‘EVERY (v_ok ctxt1)’
-  \\ qexists_tac ‘ctxt1’ \\ gs []
-  \\ drule do_app_ok \\ gs []
-  \\ disch_then drule_all \\ simp []
-  \\ strip_tac \\ gs []
-  \\ rpt CASE_TAC \\ gs []
-  \\ first_assum (irule_at Any) \\ gs []
+  rw [evaluate_def] \\ Cases_on ‘getOpClass op’ \\ gs[]
+  >~ [‘EvalOp’] >- (Cases_on ‘op’ \\ gs[])
+  >~ [‘FunApp’] >- (Cases_on ‘op’ \\ gs[])
+  >~ [‘Simple’] >- (
+    gvs [AllCaseEqs()]
+    \\ first_x_assum (drule_all_then strip_assume_tac) \\ gs [state_ok_def]
+    \\ rename1 ‘EVERY (v_ok ctxt1)’
+    \\ qexists_tac ‘ctxt1’ \\ gs []
+    \\ drule do_app_ok \\ gs []
+    \\ disch_then drule_all \\ simp []
+    \\ strip_tac \\ gs []
+    \\ rpt CASE_TAC \\ gs []
+    \\ first_assum (irule_at Any) \\ gs [])
+  >~ [‘Icing’] >- (
+    gvs [AllCaseEqs()]
+    \\ first_x_assum (drule_all_then strip_assume_tac) \\ gs [state_ok_def]
+    \\ rename1 ‘EVERY (v_ok ctxt1)’
+    \\ qexists_tac ‘ctxt1’ \\ gs [astTheory.isFpBool_def]
+    \\ drule do_app_ok \\ gs []
+    \\ disch_then drule_all \\ simp []
+    \\ strip_tac \\ gs []
+    \\ rpt CASE_TAC \\ gs[do_fprw_def] \\ rveq
+    \\ first_assum (irule_at Any)
+    \\ gs [shift_fp_opts_def, Boolv_def,
+           CaseEqs["option","semanticPrimitives$result","list", "v"]]
+    \\ rveq \\ gs[v_ok_def]
+    \\ COND_CASES_TAC \\ gs[v_ok_def])
+  >~ [‘Reals’] >- (
+    gvs [AllCaseEqs()]
+    \\ first_x_assum (drule_all_then strip_assume_tac) \\ gs [state_ok_def]
+    \\ rename1 ‘EVERY (v_ok ctxt1)’
+    \\ qexists_tac ‘ctxt1’ \\ gs [shift_fp_opts_def]
+    \\ drule do_app_ok \\ gs []
+    \\ disch_then drule_all \\ simp []
+    \\ strip_tac \\ gs []
+    \\ rpt CASE_TAC \\ gs []
+    \\ first_assum (irule_at Any) \\ gs [])
 QED
 
 Theorem evaluate_v_ok_Opapp:
@@ -823,6 +881,125 @@ Proof
   rw [evaluate_def]
 QED
 
+Theorem STRING_TYPE_do_fpoptimise:
+  STRING_TYPE m v ⇒
+  do_fpoptimise annot [v] = [v]
+Proof
+  Cases_on ‘m’
+  \\ gs[ml_translatorTheory.STRING_TYPE_def, do_fpoptimise_def]
+QED
+
+Theorem LIST_TYPE_TYPE_TYPE_do_fpoptimise:
+  ∀ l v annot.
+    (∀ ty v. MEM ty l ⇒ TYPE_TYPE ty v ⇒ do_fpoptimise annot [v] = [v]) ∧
+    LIST_TYPE TYPE_TYPE l v ⇒
+    do_fpoptimise annot [v] = [v]
+Proof
+  Induct_on ‘l’ \\ rw[ml_translatorTheory.LIST_TYPE_def]
+  \\ gs [do_fpoptimise_def]
+  \\ last_x_assum irule \\ metis_tac[]
+QED
+
+Theorem TYPE_TYPE_do_fpoptimise:
+  ∀ ty v. TYPE_TYPE ty v ⇒ do_fpoptimise annot [v] = [v]
+Proof
+  ho_match_mp_tac TYPE_TYPE_ind \\ rw[TYPE_TYPE_def]
+  \\ gs[do_fpoptimise_def]
+  \\ imp_res_tac STRING_TYPE_do_fpoptimise \\ gs[]
+  \\ drule LIST_TYPE_TYPE_TYPE_do_fpoptimise \\ gs[]
+QED
+
+Theorem TERM_TYPE_do_fpoptimise:
+  ∀ v ty. TERM_TYPE ty v ⇒ do_fpoptimise annot [v] = [v]
+Proof
+  Induct_on ‘ty’ \\ rw[TERM_TYPE_def] \\ res_tac \\ gs[do_fpoptimise_def]
+  \\ imp_res_tac TYPE_TYPE_do_fpoptimise
+  \\ imp_res_tac STRING_TYPE_do_fpoptimise \\ gs []
+QED
+
+Theorem LIST_TYPE_TERM_TYPE_do_fpoptimise:
+  ∀ l v annot. LIST_TYPE TERM_TYPE l v ⇒ do_fpoptimise annot [v] = [v]
+Proof
+  Induct_on ‘l’ \\ gs[ml_translatorTheory.LIST_TYPE_def, do_fpoptimise_def]
+  \\ rpt strip_tac \\ rveq
+  \\ imp_res_tac TERM_TYPE_do_fpoptimise
+  \\ gs[do_fpoptimise_def]
+QED
+
+Theorem THM_TYPE_do_fpoptimise:
+  ∀ v ty. THM_TYPE ty v ⇒ do_fpoptimise annot [v] = [v]
+Proof
+  Induct_on ‘ty’ \\ rw [THM_TYPE_def]
+  \\ imp_res_tac TERM_TYPE_do_fpoptimise
+  \\ imp_res_tac LIST_TYPE_TERM_TYPE_do_fpoptimise
+  \\ gs [do_fpoptimise_def]
+QED
+
+Theorem inferred_do_fpoptimise:
+  ∀ ctxt v.
+    inferred ctxt v ⇒
+    ∀ xs vs annot.
+      v = Conv (SOME xs) vs ⇒
+      inferred ctxt (Conv (SOME xs) (do_fpoptimise annot vs))
+Proof
+  ho_match_mp_tac inferred_ind \\ rw[]
+  >- gs[kernel_funs_def]
+  >- (imp_res_tac TYPE_TYPE_do_fpoptimise \\ gs [do_fpoptimise_def]
+      \\ gs[inferred_cases, SF SFY_ss])
+  >- (imp_res_tac TERM_TYPE_do_fpoptimise \\ gs [do_fpoptimise_def]
+      \\ gs [inferred_cases, SF SFY_ss])
+  >- (imp_res_tac THM_TYPE_do_fpoptimise \\ gs [do_fpoptimise_def]
+      \\ gs [inferred_cases, SF SFY_ss])
+QED
+
+Theorem EVERY_v_ok_do_fpoptimise:
+  ∀ annot vs ctxt.
+    EVERY (v_ok ctxt) vs ⇒
+    EVERY (v_ok ctxt) (do_fpoptimise annot vs)
+Proof
+  ho_match_mp_tac do_fpoptimise_ind \\ rpt conj_tac
+  \\ gs[do_fpoptimise_def, v_ok_def] \\ rpt strip_tac
+  \\ gs[] \\ Cases_on ‘st’ \\ gs[]
+  \\ imp_res_tac kernel_vals_Conv \\ simp[]
+  \\ qpat_x_assum ‘kernel_vals _ _’ $ assume_tac o SIMP_RULE std_ss [Once v_ok_cases]
+  \\ gs[]
+  >- (simp [Once v_ok_cases]
+      \\ drule inferred_do_fpoptimise \\ gs[])
+  \\ Cases_on ‘f’ \\ gs[do_partial_app_def, CaseEq"exp"]
+QED
+
+Theorem evaluate_v_ok_FpOptimise:
+  ^(get_goal "FpOptimise")
+Proof
+  rw[evaluate_def] \\ gvs [AllCaseEqs()]
+  \\ ‘st with fp_state := st.fp_state = st’ by gs [state_component_equality]
+  \\ gvs []
+  >- (
+    last_x_assum drule \\ gs[safe_exp_def, state_ok_def]
+    \\ strip_tac \\ gs[]
+    \\ first_assum $ irule_at Any \\ gs[] \\ conj_tac
+    >- metis_tac[]
+    \\ irule EVERY_v_ok_do_fpoptimise \\ gs[])
+  >- (last_x_assum drule \\ gs[safe_exp_def, state_ok_def])
+  >- (
+    ‘state_ok ctxt (st with fp_state := st.fp_state with canOpt := FPScope annot)’
+    by (gs[state_ok_def] \\ metis_tac[])
+    \\ last_x_assum drule \\ gs[safe_exp_def]
+    \\ strip_tac \\ gs[]
+    \\ ‘state_ok ctxt'' (st' with fp_state := st'.fp_state with canOpt := st.fp_state.canOpt)’
+      by (gs[state_ok_def] \\ metis_tac[])
+    \\ first_assum $ irule_at Any  \\ gs[]
+    \\ irule EVERY_v_ok_do_fpoptimise \\ gs[])
+  >- (
+    ‘state_ok ctxt (st with fp_state := st.fp_state with canOpt := FPScope annot)’
+    by (gs[state_ok_def] \\ metis_tac[])
+    \\ last_x_assum drule \\ gs[safe_exp_def]
+    \\ strip_tac \\ gs[]
+    \\ Cases_on ‘e'’ \\ gs[]
+    \\ first_assum $ irule_at Any  \\ gs[]
+    \\ gs[state_ok_def] \\ metis_tac[])
+QED
+
 Theorem evaluate_v_ok_pmatch_Nil:
   ^(get_goal "[]:(pat # exp) list")
 Proof
@@ -1032,6 +1209,7 @@ Proof
                   evaluate_v_ok_If, evaluate_v_ok_Mat,
                   evaluate_v_ok_Let, evaluate_v_ok_Letrec,
                   evaluate_v_ok_Tannot, evaluate_v_ok_Lannot,
+                  evaluate_v_ok_FpOptimise,
                   evaluate_v_ok_pmatch_Nil, evaluate_v_ok_pmatch_Cons,
                   evaluate_v_ok_decs_Nil, evaluate_v_ok_decs_Cons,
                   evaluate_v_ok_decs_Dlet, evaluate_v_ok_decs_Dletrec,

diff --git a/candle/prover/candle_prover_invScript.sml b/candle/prover/candle_prover_invScript.sml
@@ -111,6 +111,15 @@ Inductive v_ok:
 [~Lit:]
   (∀ctxt lit.
      v_ok ctxt (Litv lit)) ∧
+[~FP_WordTree:]
+  (∀ ctxt fp.
+     v_ok ctxt (FP_WordTree fp)) ∧
+[~FP_BoolTree:]
+  (∀ ctxt fp.
+     v_ok ctxt (FP_BoolTree fp)) ∧
+[~Real:]
+  (∀ ctxt r.
+     v_ok ctxt (Real r)) ∧
 [~Loc:]
   (∀ctxt loc.
      loc ∉ kernel_locs ⇒
@@ -169,6 +178,9 @@ Theorem v_ok_def =
    “v_ok ctxt (Recclosure env f n)”,
    “v_ok ctxt (Vectorv vs)”,
    “v_ok ctxt (Litv lit)”,
+   “v_ok ctxt (FP_WordTree fp)”,
+   “v_ok ctxt (FP_BoolTree fp)”,
+   “v_ok ctxt (Real r)”,
    “v_ok ctxt (Loc loc)”,
    “v_ok ctxt (Env env ns)”]
   |> map (SIMP_CONV (srw_ss()) [Once v_ok_cases])