Merge pull request #906 from CakeML/candle-features

Candle: Kernel.compute and record syntax

candle/prover/Holmakefile

@@ -9,7 +9,8 @@ INCLUDES = ../../developers \
 	   ../standard/ml_kernel \
 	   ../standard/monadic \
 	   ../standard/semantics \
-	   ../standard/syntax
+	   ../standard/syntax \
+	   compute
 
 all: $(DEFAULT_TARGETS) README.md
 .PHONY: all

candle/prover/README.md

@@ -6,6 +6,9 @@ Useful predicates on the CakeML ast.
 [candle_basis_evaluateScript.sml](candle_basis_evaluateScript.sml):
 Proving that the basis program only produces v_ok values.
 
+[candle_kernelProgScript.sml](candle_kernelProgScript.sml):
+Adds Candle specific functions to the kernel module from ml_hol_kernel_funsProg
+
 [candle_kernel_funsScript.sml](candle_kernel_funsScript.sml):
 Prove that kernel functions maintain Candle prover's invariants
 
@@ -25,5 +28,8 @@ evaluate of Candle prover
 [candle_prover_semanticsScript.sml](candle_prover_semanticsScript.sml):
 Top-level soundness theorem for the Candle theorem prover.
 
+[compute](compute):
+A verified Candle compute primitive.
+
 [permsScript.sml](permsScript.sml):
 Permissions for CakeML values.

candle/prover/candle_basis_evaluateScript.sml

@@ -15,6 +15,15 @@ val _ = set_grammar_ancestry [
   "candle_prover_inv", "ast_extras", "evaluate", "namespaceProps", "perms",
   "semanticPrimitivesProps", "misc"];
 
+val _ = temp_send_to_back_overload "If"  {Name="If", Thy="compute_syntax"};
+val _ = temp_send_to_back_overload "App" {Name="App",Thy="compute_syntax"};
+val _ = temp_send_to_back_overload "Var" {Name="Var",Thy="compute_syntax"};
+val _ = temp_send_to_back_overload "Let" {Name="Let",Thy="compute_syntax"};
+val _ = temp_send_to_back_overload "If"  {Name="If", Thy="compute_exec"};
+val _ = temp_send_to_back_overload "App" {Name="App",Thy="compute_exec"};
+val _ = temp_send_to_back_overload "Var" {Name="Var",Thy="compute_exec"};
+val _ = temp_send_to_back_overload "Let" {Name="Let",Thy="compute_exec"};
+
 Definition simple_exp_def:
   simple_exp = every_exp $ λx.
     case x of

candle/standard/ml_kernel/candle_kernelProgScript.sml → candle/prover/candle_kernelProgScript.sml

@@ -5,10 +5,14 @@ open preamble;
 open ml_translatorLib ml_monad_translatorLib ml_progLib ml_hol_kernel_funsProgTheory;
 open basisFunctionsLib print_thmTheory;
 open (* lisp: *) lisp_parsingTheory lisp_valuesTheory lisp_printingTheory;
+open (* compute: *) compute_syntaxTheory compute_evalTheory computeTheory
+                    compute_pmatchTheory;
+open runtime_checkTheory runtime_checkLib;
 
 val _ = new_theory "candle_kernelProg";
 
-val _ = set_grammar_ancestry ["ml_hol_kernel_funsProg"];
+val _ = set_grammar_ancestry [ "ml_hol_kernel_funsProg", "compute"
+  ];
 
 val _ = m_translation_extends "ml_hol_kernel_funsProg"
 
@@ -71,6 +75,89 @@ val _ = (append_prog o process_topdecs) `
       #(kernel_ffi) str arr
     end;
 `
+(* compute primitive *)
+
+val _ = ml_prog_update open_local_block;
+
+val r = translate dest_num_PMATCH;
+val r = m_translate dest_numeral_PMATCH;
+val r = translate dest_numeral_opt_PMATCH;
+val r = translate list_dest_comb_def;
+val r = translate mapOption_def;
+val r = translate app_type_def;
+val r = translate dest_cexp_def;
+
+Theorem dest_cexp_side[local]:
+  ∀x. dest_cexp_side x
+Proof
+  ho_match_mp_tac dest_cexp_ind \\ rw []
+  \\ once_rewrite_tac [fetch "-" "dest_cexp_side_def"] \\ rw []
+QED
+
+val _ = update_precondition dest_cexp_side;
+
+val r = m_translate option_def;
+val r = m_translate check_def;
+val r = translate SAFEMOD_def;
+val r = translate SAFEDIV_def;
+val r = translate num2bit_def;
+val r = translate compute_execTheory.cv2term_def
+
+val r = compute_thms_def |> EVAL_RULE |> translate;
+
+val r = m_translate dest_binary_PMATCH;
+
+val r = check [‘ths’] compute_init_def |> translate;
+
+val r = m_translate check_var_def;
+
+val _ = use_mem_intro := true;
+val res = translate_no_ind check_cexp_closed_def;
+
+val ind_lemma = Q.prove(
+  `^(first is_forall (hyp res))`,
+  rpt gen_tac
+  \\ rpt (disch_then strip_assume_tac)
+  \\ match_mp_tac (latest_ind ())
+  \\ rpt strip_tac
+  \\ last_x_assum match_mp_tac
+  \\ rpt strip_tac
+  \\ fs [FORALL_PROD, GSYM ml_translatorTheory.MEMBER_INTRO])
+  |> update_precondition;
+val _ = use_mem_intro := false;
+
+val r = translate var_list_def;
+
+val r = translate const_list_def;
+val r = m_translate map_def;
+
+val _ = use_mem_intro := true;
+val r = m_translate check_consts_def;
+val r = m_translate check_eqn_def;
+val _ = use_mem_intro := false;
+
+val r = translate compute_default_clock; (* TODO _def *)
+val r = translate indexedListsTheory.findi_def
+val r = translate compute_execTheory.monop_def
+val r = translate compute_execTheory.to_num_def
+val r = translate compute_execTheory.cv_T_def
+val r = translate compute_execTheory.cv_F_def
+val r = translate compute_execTheory.binop_def
+val r = translate compute_execTheory.to_ce_def
+val r = translate compute_execTheory.compile_to_ce_def
+val r = translate compute_execTheory.build_funs_def
+val r = translate compute_execTheory.env_lookup_def
+
+val r = m_translate compute_execTheory.get_code_def
+val r = m_translate compute_execTheory.exec_def
+
+val _ = ml_prog_update open_local_in_block;
+
+val r = check [‘ths’,‘tm’] compute_add_def |> m_translate;
+val r = compute_def
+        |> SIMP_RULE(srw_ss()) [combinTheory.C_DEF]
+        |> check [‘ths’,‘ceqs’,‘tm’]
+        |> m_translate;
 
 val _ = ml_prog_update close_local_blocks;
 val _ = ml_prog_update (close_module NONE);

candle/prover/candle_kernel_funsScript.sml

@@ -6,7 +6,7 @@ open preamble helperLib;
 open semanticPrimitivesTheory semanticPrimitivesPropsTheory
      evaluateTheory namespacePropsTheory evaluatePropsTheory
      sptreeTheory holKernelProofTheory ml_hol_kernel_funsProgTheory
-     candle_kernel_permsTheory candle_kernelProgTheory;
+     candle_kernel_permsTheory candle_kernelProgTheory computeProofTheory;
 open permsTheory candle_kernel_valsTheory candle_prover_invTheory ast_extrasTheory;
 local open ml_progLib in end
 
@@ -469,7 +469,6 @@ Theorem inferred_ok:
       (∀vs. res = Rval vs ⇒ EVERY (v_ok ctxt') vs) ∧
       (∀v. res = Rerr (Rraise v) ⇒ v_ok ctxt' v)
 Proof
-
   rw [Once inferred_cases]
   >~ [‘TYPE ctxt ty’] >- (
     Cases_on ‘ty’ \\ gs [TYPE_TYPE_def, do_opapp_cases])
@@ -480,7 +479,8 @@ Proof
   \\ rename [‘f ∈ kernel_funs’]
   \\ Cases_on ‘f ∈ { call_type_subst_v; call_freesin_v; call_vfree_in_v;
                      call_variant_v; vsubst_v; inst_v; trans_v; abs_v; eq_mp_v;
-                     deduct_antisym_rule_v; inst_type_v; inst_1_v; trans_v }’ THEN1
+                     deduct_antisym_rule_v; inst_type_v; inst_1_v; trans_v;
+                     compute_add_v; compute_v }’ THEN1
    (gvs []
     \\ qpat_x_assum ‘do_opapp _ = _’ mp_tac
     \\ last_x_assum mp_tac
@@ -1508,11 +1508,7 @@ Proof
     \\ gvs[SF SFY_ss, THM_IMP_v_ok]
     \\ reverse conj_tac >- metis_tac[v_ok_APPEND, CONS_APPEND]
     \\ metis_tac[ref_ok_APPEND, CONS_APPEND])
-
   >~ [‘do_opapp [Kernel_print_thm_v; v]’] >- (
-
-
-
     drule_all Kernel_print_thm_v_head
     \\ strip_tac \\ gvs[]
     >- (first_assum $ irule_at Any \\ simp[])
@@ -1766,6 +1762,7 @@ Theorem kernel_vals_ok:
             (∀vs. res = Rval vs ⇒ EVERY (v_ok ctxt') vs) ∧
             (∀v. res = Rerr (Rraise v) ⇒ v_ok ctxt' v)
 Proof
+
   rw [Once v_ok_cases]
   >~ [‘inferred ctxt f’] >- (
     irule_at Any inferred_ok
@@ -2148,6 +2145,56 @@ Proof
     \\ imp_res_tac THM_IMP_v_ok \\ gvs []
     \\ rename [‘M_failure ff’] \\ Cases_on ‘ff’ \\ fs []
     \\ fs [HOL_EXN_TYPE_Fail_v_ok, SF SFY_ss])
+  \\ Cases_on ‘f = compute_add_v’ \\ gvs [] >- (
+    drule_all compute_add_v_head \\ strip_tac \\ gvs[]
+    >- (qexists_tac`ctxt` \\ fs[])
+    \\ rename1 ‘do_opapp [g; w]’
+    \\ assume_tac compute_add_v_thm
+    \\ fs[state_ok_def]
+    \\ drule_all_then strip_assume_tac v_ok_LIST_THM_TYPE_HEAD
+    \\ drule_all_then strip_assume_tac v_ok_TERM_TYPE_HEAD
+    \\ drule ArrowM2
+    \\ rpt(disch_then drule)
+    \\ simp[SF SFY_ss, TERM_TYPE_perms_ok, LIST_TYPE_THM_perms_ok]
+    \\ strip_tac \\ gvs[]
+    \\ qexists_tac ‘ctxt’ \\ simp[]
+    \\ drule_all_then assume_tac v_ok_TERM
+    \\ drule_all_then assume_tac v_ok_LIST_THM
+    \\ strip_tac
+    \\ drule_all_then strip_assume_tac compute_add_thm \\ rveq
+    >- ( first_assum $ irule_at $ Any \\ simp[SF SFY_ss] )
+    \\ Cases_on ‘r’ \\ gvs [THM_IMP_v_ok, SF SFY_ss]
+    \\ rename [‘M_failure ff’] \\ Cases_on ‘ff’ \\ fs []
+    \\ fs [HOL_EXN_TYPE_Fail_v_ok, SF SFY_ss])
+  \\ Cases_on ‘f = compute_v’ \\ gvs [] >- (
+
+    drule_all compute_v_head \\ strip_tac \\ gvs[]
+    >- (qexists_tac`ctxt` \\ fs[])
+    \\ rename1 ‘do_opapp [g; w]’
+    \\ assume_tac compute_v_thm
+    \\ fs[state_ok_def]
+    \\ ‘∃pq. PAIR_TYPE (LIST_TYPE THM_TYPE) (LIST_TYPE THM_TYPE) pq v’
+      by (irule_at Any v_ok_PAIR_TYPE_HEAD
+          \\ first_x_assum (irule_at Any)
+          \\ first_x_assum (irule_at Any)
+          \\ simp [v_ok_LIST_THM_TYPE_HEAD, SF SFY_ss])
+    \\ drule_all_then strip_assume_tac v_ok_TERM_TYPE_HEAD
+    \\ drule ArrowM2
+    \\ rpt(disch_then drule) \\ simp []
+    \\ Cases_on ‘pq’ \\ gs [ml_translatorTheory.PAIR_TYPE_def]
+    \\ simp [Once perms_ok_def, TERM_TYPE_perms_ok, LIST_TYPE_THM_perms_ok,
+             SF SFY_ss]
+    \\ strip_tac \\ gvs[]
+    \\ qexists_tac ‘ctxt’ \\ gs [v_ok_def]
+    \\ drule_all_then assume_tac v_ok_TERM
+    \\ imp_res_tac v_ok_LIST_THM \\ gs [SF SFY_ss]
+    \\ drule_all_then strip_assume_tac compute_thm \\ gvs []
+    \\ strip_tac
+    >- ( first_assum $ irule_at $ Any \\ simp[SF SFY_ss] )
+    \\ rename [‘compute _ _ _ = (res1,_)’]
+    \\ Cases_on ‘res1’ \\ gvs [THM_IMP_v_ok, SF SFY_ss]
+    \\ rename [‘M_failure ff’] \\ Cases_on ‘ff’ \\ fs []
+    \\ fs [HOL_EXN_TYPE_Fail_v_ok, SF SFY_ss])
   \\ qsuff_tac ‘∃v1 v2 x. f = Closure v1 v2 x ∧ ∀n w. x ≠ Fun n w’
   THEN1 (strip_tac \\ fs [do_partial_app_def,AllCaseEqs()])
   \\ fs [kernel_funs_def]