Fixes for ffiname

CakeML · Jan 3, 2024 · d14bd87 · d14bd87
1 parent 691ccdc
commit d14bd87
Showing 1 changed file with 20 additions and 12 deletions.
diff --git a/examples/opentheory/compilation/ag32/proofs/readerProgProofScript.sml b/examples/opentheory/compilation/ag32/proofs/readerProgProofScript.sml
@@ -34,13 +34,13 @@ val LENGTH_data =
   |> (REWRITE_CONV[readerCompileTheory.data_def] THENC listLib.LENGTH_CONV)
 
 Overload reader_machine_config =
-  ``ag32_machine_config (THE config.lab_conf.ffi_names) (LENGTH code) (LENGTH data)``
+  ``ag32_machine_config (extcalls config.lab_conf.ffi_names) (LENGTH code) (LENGTH data)``
 
 Theorem target_state_rel_reader_start_asm_state:
    SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧
    LENGTH inp ≤ stdin_size ∧
-   is_ag32_init_state (init_memory code data (THE config.lab_conf.ffi_names) (cl,inp)) ms ⇒
-   ∃n. target_state_rel ag32_target (init_asm_state code data (THE config.lab_conf.ffi_names) (cl,inp)) (FUNPOW Next n ms) ∧
+   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) ∧
        ((FUNPOW Next n ms).io_events = ms.io_events) ∧
        (∀x. x ∉ (ag32_startup_addresses) ⇒
          ((FUNPOW Next n ms).MEM x = ms.MEM x))
@@ -49,8 +49,8 @@ Proof
   \\ drule (GEN_ALL init_asm_state_RTC_asm_step)
   \\ disch_then drule
   \\ simp_tac std_ss []
-  \\ disch_then(qspecl_then[`code`,`data`,`THE config.lab_conf.ffi_names`]mp_tac)
-  \\ impl_tac >- ( EVAL_TAC>> fs[ffi_names,LENGTH_data,LENGTH_code])
+  \\ disch_then(qspecl_then[`code`,`data`,`extcalls config.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)
   \\ rveq
@@ -78,20 +78,28 @@ val compile_correct_applied =
   |> Q.GEN`cbspace` |> Q.SPEC`0`
   |> Q.GEN`data_sp` |> Q.SPEC`0`
 
+Triviality to_MAP_ExtCall:
+  [ExtCall n] = MAP ExtCall [n] ∧
+  (ExtCall n::MAP ExtCall ns) = MAP ExtCall (n::ns)
+Proof
+  fs []
+QED
+
 Theorem reader_installed:
    SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧
    LENGTH inp ≤ stdin_size ∧
-   is_ag32_init_state (init_memory code data (THE config.lab_conf.ffi_names) (cl,inp)) ms0 ⇒
+   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
      (heap_regs ag32_backend_config.stack_conf.reg_names)
      (reader_machine_config) (FUNPOW Next (reader_startup_clock ms0 inp cl) ms0)
 Proof
-  rewrite_tac[ffi_names, THE_DEF]
+  rewrite_tac[ffi_names, extcalls_def]
   \\ strip_tac
+  \\ rewrite_tac [to_MAP_ExtCall]
   \\ irule ag32_installed
   \\ drule reader_startup_clock_def
   \\ disch_then drule
-  \\ rewrite_tac[ffi_names, THE_DEF]
+  \\ rewrite_tac[ffi_names, extcalls_def]
   \\ disch_then drule
   \\ strip_tac
   \\ simp[]
@@ -219,7 +227,7 @@ Theorem reader_ag32_next:
    LENGTH inp <= stdin_size /\
    wfcl cl /\
    (LENGTH cl = 1) /\
-   is_ag32_init_state (init_memory code data (THE config.lab_conf.ffi_names) (cl,inp)) ms0
+   is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms0
    ==>
    ?k1. !k. k1 <= k ==>
      let ms = FUNPOW Next k ms0 in
@@ -243,9 +251,9 @@ Proof
     \\ simp [stdin_fs_def, TextIOProofTheory.stdin_def])
   \\ strip_tac
   \\ irule ag32_next
-  \\ conj_tac >- simp [ffi_names]
-  \\ conj_tac >- (simp [ffi_names, LENGTH_code, LENGTH_data] \\ EVAL_TAC)
-  \\ conj_tac >- (simp [ffi_names] \\ EVAL_TAC)
+  \\ conj_tac >- simp [ffi_names, extcalls_def]
+  \\ conj_tac >- (simp [ffi_names, extcalls_def, LENGTH_code, LENGTH_data] \\ EVAL_TAC)
+  \\ conj_tac >- (simp [ffi_names, extcalls_def] \\ EVAL_TAC)
   \\ goal_assum (first_assum o mp_then Any mp_tac)
   \\ goal_assum (first_assum o mp_then Any mp_tac)
   \\ goal_assum (first_assum o mp_then Any mp_tac)