More work on in-logic compilation

Author: myreen

compiler/backend/ag32/proofs/ag32_configProofScript.sml

@@ -79,4 +79,63 @@ val ag32_compile_correct =
   |> DISCH_ALL
   |> curry save_thm"ag32_compile_correct";
 
+Theorem get_shmem_info_LENGTH:
+  ∀xs c l1 l2.
+    get_shmem_info xs c l1 l2 = (t1,t2) ∧ LENGTH l1 = LENGTH l2 ⇒
+    LENGTH t1 = LENGTH t2
+Proof
+  ho_match_mp_tac lab_to_targetTheory.get_shmem_info_ind \\ rw []
+  \\ gvs [lab_to_targetTheory.get_shmem_info_def]
+  \\ pairarg_tac \\ gvs []
+QED
+
+Triviality IMP_EVERY_list_add_if_fresh:
+  ∀xs x p. p x ∧ EVERY p xs ⇒ EVERY p (list_add_if_fresh x xs)
+Proof
+  Induct \\ gvs [lab_to_targetTheory.list_add_if_fresh_def] \\ rw []
+QED
+
+Theorem find_ffi_names_ExtCall:
+  ∀xs. EVERY (λx. ∃i. ExtCall i = x) (find_ffi_names xs)
+Proof
+  ho_match_mp_tac lab_to_targetTheory.find_ffi_names_ind
+  \\ rpt strip_tac
+  \\ asm_rewrite_tac [lab_to_targetTheory.find_ffi_names_def,EVERY_DEF]
+  \\ Cases_on ‘x’ \\ gvs []
+  \\ Cases_on ‘a’ \\ gvs []
+  \\ irule IMP_EVERY_list_add_if_fresh \\ gvs []
+QED
+
+Theorem MAP_ExtCall_ffinames:
+  ∀xs.
+    EVERY (λx. ∃i. ExtCall i = x) xs ⇒
+    xs = MAP ExtCall (ffinames_to_string_list xs)
+Proof
+  Induct \\ gvs [backendTheory.ffinames_to_string_list_def]
+  \\ Cases \\ gvs [backendTheory.ffinames_to_string_list_def]
+QED
+
+Theorem compile_imp_ffi_names:
+  backend$compile c p = SOME (b,d,c1) ∧
+  c1.lab_conf.shmem_extra = [] ∧ f ≠ [] ∧
+  c.lab_conf.ffi_names = NONE ∧
+  ffinames_to_string_list (the [] c1.lab_conf.ffi_names) = f ⇒
+  c1.lab_conf.ffi_names = SOME (MAP ExtCall f)
+Proof
+  Cases_on ‘c1.lab_conf.ffi_names’
+  \\ gvs [libTheory.the_def,backendTheory.ffinames_to_string_list_def]
+  \\ gvs [backendTheory.compile_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+  \\ gvs [oneline backendTheory.attach_bitmaps_def, AllCaseEqs()]
+  \\ strip_tac \\ gvs []
+  \\ gvs [lab_to_targetTheory.compile_def]
+  \\ gvs [lab_to_targetTheory.compile_lab_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+  \\ gvs [AllCaseEqs()]
+  \\ rpt (pairarg_tac \\ gvs [])
+  \\ drule get_shmem_info_LENGTH \\ gvs [] \\ rw []
+  \\ irule MAP_ExtCall_ffinames
+  \\ gvs [find_ffi_names_ExtCall]
+QED
+
 val _ = export_theory();

compiler/backend/cv_compute/backend_asmScript.sml

@@ -217,7 +217,10 @@ Definition attach_bitmaps_def:
      let syms = MAP (λ(n,p,l). (lookup_any n names «NOTFOUND»,p,l))
                     c'.inc_sec_pos_len
      in
-       SOME (code_bytes,data,ffi_names,syms,encode_backend_config $ c with
+       SOME (code_bytes, LENGTH code_bytes,
+             data, LENGTH data,
+             ffi_names, LENGTH c'.inc_shmem_extra,
+             syms, encode_backend_config $ c with
                <| inc_lab_conf := c'; inc_symbols := syms |>)) ∧
   attach_bitmaps names c bm NONE = NONE
 End
@@ -308,12 +311,16 @@ End
  *----------------------------------------------------------------*)
 
 Theorem from_lab_thm[local]:
-  from_lab asm_conf c names p bm = SOME (bytes,bm1,ffi_names,syms,conf_str) ⇒
+  from_lab asm_conf c names p bm =
+  SOME (bytes,bytes_len,bm1,bm1_len,ffi_names,shmem_len,syms,conf_str) ⇒
   ∃c1.
     backend$from_lab (inc_config_to_config asm_conf c) names p bm =
       SOME (bytes,bm1,c1) ∧
     ffi_names = ffinames_to_string_list (the [] c1.lab_conf.ffi_names) ∧
     syms = c1.symbols ∧
+    LENGTH bytes = bytes_len ∧
+    LENGTH bm1 = bm1_len ∧
+    LENGTH c1.lab_conf.shmem_extra = shmem_len ∧
     conf_str = encode_backend_config (config_to_inc_config c1)
 Proof
   gvs [from_lab_def,backendTheory.from_lab_def]
@@ -333,11 +340,15 @@ Proof
 QED
 
 Theorem from_stack_thm[local]:
-  from_stack asm_conf c names p bm = SOME (bytes,bm1,ffi_names,syms,conf_str) ⇒
+  from_stack asm_conf c names p bm =
+  SOME (bytes,bytes_len,bm1,bm1_len,ffi_names,shmem_len,syms,conf_str) ⇒
   ∃c1.
     backend$from_stack (inc_config_to_config asm_conf c) names p bm = SOME (bytes,bm1,c1) ∧
     ffi_names = ffinames_to_string_list (the [] c1.lab_conf.ffi_names) ∧
     syms = c1.symbols ∧
+    LENGTH bytes = bytes_len ∧
+    LENGTH bm1 = bm1_len ∧
+    LENGTH c1.lab_conf.shmem_extra = shmem_len ∧
     conf_str = encode_backend_config (config_to_inc_config c1)
 Proof
   gvs [from_stack_def,backendTheory.from_stack_def] \\ rw []
@@ -367,11 +378,15 @@ Proof
 QED
 
 Theorem from_word_0_thm[local]:
-  from_word_0 asm_conf (c,p,names) = SOME (bytes,bm,ffi_names,syms,conf_str) ⇒
+  from_word_0 asm_conf (c,p,names) =
+  SOME (bytes,bytes_len,bm1,bm1_len,ffi_names,shmem_len,syms,conf_str) ⇒
   ∃c1.
-    backend$from_word_0 (inc_config_to_config asm_conf c) names p = SOME (bytes,bm,c1) ∧
+    backend$from_word_0 (inc_config_to_config asm_conf c) names p = SOME (bytes,bm1,c1) ∧
     ffi_names = ffinames_to_string_list (the [] c1.lab_conf.ffi_names) ∧
     syms = c1.symbols ∧
+    LENGTH bytes = bytes_len ∧
+    LENGTH bm1 = bm1_len ∧
+    LENGTH c1.lab_conf.shmem_extra = shmem_len ∧
     conf_str = encode_backend_config (config_to_inc_config c1)
 Proof
   gvs [from_word_0_def,from_word_def,AllCaseEqs()] \\ strip_tac \\ gvs []
@@ -474,11 +489,15 @@ QED
 
 Theorem compile_cake_thm:
   ∀asm_conf:'a asm_config.
-    compile_cake asm_conf c p = SOME (bytes,bm,ffi_names,syms,conf_str) ⇒
+    compile_cake asm_conf c p =
+    SOME (bytes,bytes_len,bm,bm_len,ffi_names,shmem_len,syms,conf_str) ⇒
     ∃c1.
       backend$compile (inc_config_to_config asm_conf c) p = SOME (bytes,bm,c1) ∧
       ffi_names = ffinames_to_string_list (the [] c1.lab_conf.ffi_names) ∧
       syms = c1.symbols ∧
+      LENGTH bytes = bytes_len ∧
+      LENGTH bm = bm_len ∧
+      LENGTH c1.lab_conf.shmem_extra = shmem_len ∧
       conf_str = encode_backend_config (config_to_inc_config c1)
 Proof
   rw [compile_cake_def]

compiler/backend/proofs/backendProofScript.sml

@@ -2706,7 +2706,7 @@ Proof
   \\ gs []
 QED
 
-Triviality compile_asm_config_eq:
+Theorem compile_asm_config_eq:
   compile (c : 'a config) prog = SOME (b,bm,c') ==>
   c'.lab_conf.asm_conf = c.lab_conf.asm_conf
 Proof

compiler/bootstrap/compilation/ag32/32/Holmakefile

@@ -1,6 +1,6 @@
 ARCH = ag32
 WORD_SIZE = 32
-INCLUDES = $(CAKEMLDIR)/semantics $(CAKEMLDIR)/basis ../../../..\
+INCLUDES = $(CAKEMLDIR)/semantics $(CAKEMLDIR)/basis $(CAKEMLDIR)/cv_translator ../../../..\
 					 ../../../../encoders/asm ../../../../encoders/$(ARCH)\
 					 ../../../../backend/$(ARCH) ../../../translation
 
@@ -18,3 +18,7 @@ cake-$(ARCH)-$(WORD_SIZE).tar.gz: cake.S basis_ffi.c Makefile
 	tar -chzf $@ --transform='s|^|cake-$(ARCH)-$(WORD_SIZE)/|' cake.S basis_ffi.c Makefile
 
 EXTRA_CLEANS = cake.S cake-$(ARCH)-$(WORD_SIZE).tar.gz
+
+ifdef POLY
+HOLHEAP = $(CAKEMLDIR)/cv_translator/cake_compile_heap
+endif

compiler/bootstrap/compilation/ag32/32/README.md

@@ -13,11 +13,3 @@ library, as a thin wrapper around the relevant system calls.
 [proofs](proofs):
 This directory contains the end-to-end correctness theorem for the
 32-bit version of the CakeML compiler.
-
-[to_dataBootstrapScript.sml](to_dataBootstrapScript.sml):
-Evaluate the 32-bit version of the compiler down to a DataLang
-program.
-
-[to_lab_ag32BootstrapScript.sml](to_lab_ag32BootstrapScript.sml):
-Evaluate the 32-bit version of the compiler down to a LabLang
-program (an assembly program).

compiler/bootstrap/compilation/ag32/32/ag32BootstrapScript.sml

@@ -2,17 +2,11 @@
   Evaluate the final part of the 32-bit version of the compiler
   into machine code for ag32, i.e. the Silver ISA.
 *)
-open preamble to_lab_ag32BootstrapTheory compilationLib
+open preamble compiler32ProgTheory eval_cake_compile_ag32Lib;
 
 val _ = new_theory "ag32Bootstrap";
 
-val () = ml_translatorLib.reset_translation();
-
-val bootstrap_thm =
-  compilationLib.cbv_to_bytes_ag32
-    stack_to_lab_thm lab_prog_def
-    "code" "data" "config" "cake.S";
-
-val cake_compiled = save_thm("cake_compiled", bootstrap_thm);
+Theorem compiler32_compiled =
+  eval_cake_compile_ag32 "" compiler32_prog_def "cake.S";
 
 val _ = export_theory();

compiler/bootstrap/compilation/ag32/32/proofs/ag32BootstrapProofScript.sml

@@ -9,17 +9,19 @@ open preamble
 
 val _ = new_theory"ag32BootstrapProof";
 
-val with_clos_conf_simp = prove(
-  ``(mc_init_ok (ag32_backend_config with <| clos_conf := z ; bvl_conf updated_by
+Triviality with_clos_conf_simp:
+    (mc_init_ok (ag32_backend_config with <| clos_conf := z ; bvl_conf updated_by
                     (λc. c with <|inline_size_limit := t1; exp_cut := t2|>) |>) =
      mc_init_ok ag32_backend_config) /\
     (x.max_app <> 0 /\ (case x.known_conf of NONE => T | SOME k => k.val_approx_spt = LN) ==>
      (backend_config_ok (ag32_backend_config with clos_conf := x) =
-      backend_config_ok ag32_backend_config))``,
+      backend_config_ok ag32_backend_config))
+Proof
   fs [mc_init_ok_def,FUN_EQ_THM,backend_config_ok_def]
-  \\ rw [] \\ eq_tac \\ rw [] \\ EVAL_TAC);
+  \\ rw [] \\ eq_tac \\ rw [] \\ EVAL_TAC
+QED
 
-Overload cake_config = “ag32Bootstrap$config”;
+Overload cake_config = “ag32Bootstrap$info”;
 
 Definition compiler_instance_def:
   compiler_instance =
@@ -43,7 +45,10 @@ QED
 Theorem cake_config_lab_conf_asm_conf:
   cake_config.lab_conf.asm_conf = ag32_config
 Proof
-  once_rewrite_tac [ag32BootstrapTheory.config_def] \\ EVAL_TAC
+  assume_tac $ cj 1 compiler32_compiled
+  \\ drule compile_asm_config_eq
+  \\ gvs [backendTheory.set_oracle_def]
+  \\ strip_tac \\ EVAL_TAC
 QED
 
 val cake_io_events_def = new_specification("cake_io_events_def",["cake_io_events"],
@@ -58,30 +63,38 @@ val cake_io_events_def = new_specification("cake_io_events_def",["cake_io_events
 val (cake_sem,cake_output) = cake_io_events_def |> SPEC_ALL |> UNDISCH |> CONJ_PAIR
 val (cake_not_fail,cake_sem_sing) = MATCH_MP semantics_prog_Terminate_not_Fail cake_sem |> CONJ_PAIR
 
-val ffi_names =
-  ``config.lab_conf.ffi_names``
-  |> (REWRITE_CONV[ag32BootstrapTheory.config_def] THENC EVAL);
-
-val LENGTH_code =
-  ``LENGTH code``
-  |> (REWRITE_CONV[ag32BootstrapTheory.code_def] THENC listLib.LENGTH_CONV);
+Theorem extcalls_ffi_names:
+  extcalls cake_config.lab_conf.ffi_names = ffis
+Proof
+  rewrite_tac [compiler32_compiled]
+  \\ qspec_tac (‘cake_config.lab_conf.ffi_names’,‘xs’) \\ Cases
+  \\ gvs [extcalls_def,backendTheory.ffinames_to_string_list_def,
+          libTheory.the_def]
+  \\ Induct_on ‘x’ \\ gvs []
+  \\ gvs [extcalls_def,backendTheory.ffinames_to_string_list_def,
+          libTheory.the_def]
+  \\ Cases
+  \\ gvs [extcalls_def,backendTheory.ffinames_to_string_list_def,
+          libTheory.the_def]
+QED
 
-val LENGTH_data =
-  ``LENGTH data``
-  |> (REWRITE_CONV[ag32BootstrapTheory.data_def] THENC listLib.LENGTH_CONV);
+val ffis = ffis_def |> CONV_RULE (RAND_CONV EVAL);
+val ffi_names = extcalls_ffi_names |> SRULE [ffis]
 
-val shmem =
-  ``config.lab_conf.shmem_extra``
-  |> (REWRITE_CONV[ag32BootstrapTheory.config_def] THENC EVAL);
+val LENGTH_code = “LENGTH code” |> SCONV [compiler32_compiled];
+val LENGTH_data = “LENGTH data” |> SCONV [compiler32_compiled];
+val shmem = “info.lab_conf.shmem_extra” |> SCONV [compiler32_compiled];
 
 Overload cake_machine_config =
-  ``ag32_machine_config (extcalls config.lab_conf.ffi_names) (LENGTH code) (LENGTH data)``
+  “ag32_machine_config (extcalls info.lab_conf.ffi_names) (LENGTH code) (LENGTH data)”
 
 Theorem target_state_rel_cake_start_asm_state:
    SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧
    LENGTH inp ≤ stdin_size ∧
-   is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms ⇒
-   ∃n. target_state_rel ag32_target (init_asm_state code data (extcalls config.lab_conf.ffi_names) (cl,inp)) (FUNPOW Next n ms) ∧
+   is_ag32_init_state (init_memory code data (extcalls info.lab_conf.ffi_names) (cl,inp)) ms ⇒
+   ∃n. target_state_rel ag32_target
+          (init_asm_state code data (extcalls info.lab_conf.ffi_names) (cl,inp))
+          (FUNPOW Next n ms) ∧
        ((FUNPOW Next n ms).io_events = ms.io_events) ∧
        (∀x. x ∉ (ag32_startup_addresses) ⇒
          ((FUNPOW Next n ms).MEM x = ms.MEM x))
@@ -90,7 +103,7 @@ Proof
   \\ drule (GEN_ALL init_asm_state_RTC_asm_step)
   \\ disch_then drule
   \\ simp_tac std_ss []
-  \\ disch_then(qspecl_then[`code`,`data`,`extcalls config.lab_conf.ffi_names`]mp_tac)
+  \\ disch_then(qspecl_then[`code`,`data`,`extcalls info.lab_conf.ffi_names`]mp_tac)
   \\ impl_tac >- ( EVAL_TAC>> fs[ffi_names,LENGTH_data,LENGTH_code,extcalls_def])
   \\ strip_tac
   \\ drule (GEN_ALL target_state_rel_ag32_init)
@@ -107,11 +120,12 @@ val cake_startup_clock_def =
   |> SIMP_RULE bool_ss [GSYM RIGHT_EXISTS_IMP_THM,SKOLEM_THM]);
 
 val compile_correct_applied =
-  MATCH_MP compile_correct_eval cake_compiled
-  |> SIMP_RULE(srw_ss())[LET_THM,ml_progTheory.init_state_env_thm,GSYM AND_IMP_INTRO,
-                         with_clos_conf_simp]
+  MATCH_MP compile_correct_eval (cj 1 compiler32_compiled)
+  |> SIMP_RULE(srw_ss())[LET_THM,ml_progTheory.init_state_env_thm,
+                         GSYM AND_IMP_INTRO,with_clos_conf_simp]
   |> Q.INST [‘ev’|->‘SOME compiler_instance’]
-  |> SIMP_RULE (srw_ss()) [add_eval_state_def,opt_eval_config_wf_def,compiler_instance_lemma]
+  |> SIMP_RULE (srw_ss()) [add_eval_state_def,opt_eval_config_wf_def,
+                           compiler_instance_lemma]
   |> C MATCH_MP cake_not_fail
   |> C MATCH_MP ag32_backend_config_ok
   |> REWRITE_RULE[cake_sem_sing,AND_IMP_INTRO]
@@ -131,16 +145,25 @@ Theorem cake_compiled_thm =
 Theorem cake_installed:
    SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧
    LENGTH inp ≤ stdin_size ∧
-   is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms0 ⇒
-   installed code 0 data 0 config.lab_conf.ffi_names
+   is_ag32_init_state (init_memory code data
+                         (extcalls info.lab_conf.ffi_names) (cl,inp)) ms0 ⇒
+   installed code 0 data 0 info.lab_conf.ffi_names
      (heap_regs ag32_backend_config.stack_conf.reg_names)
-     (cake_machine_config) config.lab_conf.shmem_extra
+     (cake_machine_config) info.lab_conf.shmem_extra
      (FUNPOW Next (cake_startup_clock ms0 inp cl) ms0)
 Proof
   rewrite_tac[ffi_names, extcalls_def, shmem]
   \\ strip_tac
   \\ qmatch_asmsub_abbrev_tac ‘init_memory _ _ ff’
-  \\ ‘^(ffi_names |> concl |> rand |> rand) = MAP ExtCall ff’ by simp [Abbr‘ff’]
+  \\ qmatch_goalsub_abbrev_tac ‘installed _ _ _ _ dd’
+  \\ ‘dd = SOME (MAP ExtCall ff)’ by
+   (unabbrev_all_tac
+    \\ assume_tac (cj 1 compiler32_compiled)
+    \\ drule ag32_configProofTheory.compile_imp_ffi_names
+    \\ gvs [compiler32_compiled]
+    \\ gvs [GSYM compiler32_compiled,ffis]
+    \\ simp [backendTheory.set_oracle_def,
+             ag32_configTheory.ag32_backend_config_def])
   \\ asm_rewrite_tac []
   \\ irule ag32_installed
   \\ unabbrev_all_tac
@@ -200,7 +223,8 @@ Proof
 QED
 
 Theorem FST_ALOOKUP_fastForwardFD_infds:
-   OPTION_MAP FST (ALOOKUP (fastForwardFD fs fd).infds fd') = OPTION_MAP FST (ALOOKUP fs.infds fd')
+   OPTION_MAP FST (ALOOKUP (fastForwardFD fs fd).infds fd') =
+   OPTION_MAP FST (ALOOKUP fs.infds fd')
 Proof
   rw[fsFFIPropsTheory.fastForwardFD_def]
   \\ Cases_on`ALOOKUP fs.infds fd` \\ simp[libTheory.the_def]
@@ -212,7 +236,8 @@ Proof
 QED
 
 Theorem FST_ALOOKUP_add_stdo_infds:
-   OPTION_MAP FST (ALOOKUP (add_stdo fd nm fs out).infds fd') = OPTION_MAP FST (ALOOKUP fs.infds fd')
+   OPTION_MAP FST (ALOOKUP (add_stdo fd nm fs out).infds fd') =
+   OPTION_MAP FST (ALOOKUP fs.infds fd')
 Proof
   mp_tac TextIOProofTheory.add_stdo_MAP_FST_infds
   \\ strip_tac
@@ -501,7 +526,7 @@ QED
 Theorem cake_ag32_next:
    SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧ wfcl cl ∧
    LENGTH inp ≤ stdin_size ∧
-   is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms0
+   is_ag32_init_state (init_memory code data (extcalls info.lab_conf.ffi_names) (cl,inp)) ms0
   ⇒
    ∃k1. ∀k. k1 ≤ k ⇒
      let ms = FUNPOW Next k ms0 in