simplify shmem_extra in installed lemmas

CakeML · Mar 12, 2024 · d369d33 · d369d33
1 parent e61fd9a
commit d369d33
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 4 deletions.
diff --git a/examples/compilation/ag32/proofs/helloProofScript.sml b/examples/compilation/ag32/proofs/helloProofScript.sml
@@ -32,6 +32,10 @@ val LENGTH_data =
   ``LENGTH data``
   |> (REWRITE_CONV[helloCompileTheory.data_def] THENC listLib.LENGTH_CONV)
 
+val shmem =
+  ``config.lab_conf.shmem_extra``
+  |> (REWRITE_CONV[helloCompileTheory.config_def] THENC EVAL)
+
 Overload hello_machine_config =
   ``ag32_machine_config (extcalls config.lab_conf.ffi_names) (LENGTH code) (LENGTH data)``
 
@@ -49,7 +53,7 @@ Proof
   \\ disch_then drule
   \\ simp_tac std_ss []
   \\ 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])
+  \\ impl_tac >- ( EVAL_TAC>> fs[ffi_names,LENGTH_data,LENGTH_code,extcalls_def,shmem])
   \\ strip_tac
   \\ drule (GEN_ALL target_state_rel_ag32_init)
   \\ rveq
@@ -93,7 +97,7 @@ Theorem hello_installed:
      (hello_machine_config) config.lab_conf.shmem_extra
      (FUNPOW Next (hello_startup_clock ms0 inp cl) ms0)
 Proof
-  rewrite_tac[ffi_names, extcalls_def]
+  rewrite_tac[ffi_names, extcalls_def, shmem]
   \\ strip_tac
   \\ rewrite_tac [to_MAP_ExtCall]
   \\ irule ag32_installed

diff --git a/examples/compilation/ag32/proofs/sortProofScript.sml b/examples/compilation/ag32/proofs/sortProofScript.sml
@@ -49,6 +49,10 @@ val LENGTH_data =
   ``LENGTH data``
   |> (REWRITE_CONV[sortCompileTheory.data_def] THENC listLib.LENGTH_CONV)
 
+val shmem =
+  ``config.lab_conf.shmem_extra``
+  |> (REWRITE_CONV[sortCompileTheory.config_def] THENC EVAL)
+
 Overload sort_machine_config =
   ``ag32_machine_config (extcalls config.lab_conf.ffi_names) (LENGTH code) (LENGTH data)``
 
@@ -110,7 +114,7 @@ Theorem sort_installed:
      (sort_machine_config) config.lab_conf.shmem_extra
      (FUNPOW Next (sort_startup_clock ms0 inp cl) ms0)
 Proof
-  rewrite_tac[ffi_names, extcalls_def]
+  rewrite_tac[ffi_names, extcalls_def, shmem]
   \\ strip_tac
   \\ rewrite_tac [to_MAP_ExtCall]
   \\ irule ag32_installed

diff --git a/examples/compilation/ag32/proofs/wordcountProofScript.sml b/examples/compilation/ag32/proofs/wordcountProofScript.sml
@@ -59,6 +59,10 @@ val LENGTH_data =
   ``LENGTH data``
   |> (REWRITE_CONV[wordcountCompileTheory.data_def] THENC listLib.LENGTH_CONV)
 
+val shmem =
+  ``config.lab_conf.shmem_extra``
+  |> (REWRITE_CONV[wordcountCompileTheory.config_def] THENC EVAL)
+
 Overload wordcount_machine_config =
   ``ag32_machine_config (extcalls config.lab_conf.ffi_names) (LENGTH code) (LENGTH data)``
 
@@ -121,7 +125,7 @@ Theorem wordcount_installed:
      (wordcount_machine_config) config.lab_conf.shmem_extra
      (FUNPOW Next (wordcount_startup_clock ms0 inp cl) ms0)
 Proof
-  rewrite_tac[ffi_names, extcalls_def]
+  rewrite_tac[ffi_names, extcalls_def, shmem]
   \\ strip_tac
   \\ rewrite_tac [to_MAP_ExtCall]
   \\ irule ag32_installed