Skip to content

Commit 467af03

Browse files
myreenmyreen
committed
Get remaining files up-to-date for cv_compute eval of compiler
1 parent b4fb863 commit 467af03

File tree

17 files changed

+234
-173
lines changed

17 files changed

+234
-173
lines changed

‎compiler/inference/proofs/README.md

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,6 @@ Proves completeness of the type inferencer, i.e. if there is a type
99
for the program, then the type inferencer will find a type (the most
1010
general type).
1111

12-
[inferPropsScript.sml](inferPropsScript.sml):
13-
Various lemmas that are handy in the soundness and completeness
14-
proofs of the type inferencer.
15-
1612
[inferSoundScript.sml](inferSoundScript.sml):
1713
Proves soundness of the type inferencer: any type assignment
1814
produced by the type inferencer is a valid type for the program.

‎examples/compilation/ag32/helloCompileScript.sml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
(*
22
Compiles the hello example by evaluation inside the logic of HOL
33
*)
4-
open preamble helloProgTheory eval_cake_compile_x64Lib
4+
open preamble helloProgTheory eval_cake_compile_ag32Lib
55

66
val _ = new_theory "helloCompile"
77

88
Theorem hello_compiled =
9-
eval_cake_compile_x64 "" hello_prog_def "hello.S";
9+
eval_cake_compile_ag32 "" hello_prog_def "hello.S";
1010

1111
val _ = export_theory ();

‎examples/compilation/ag32/proofs/helloProofScript.sml

Lines changed: 42 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -20,30 +20,37 @@ val hello_io_events_def =
2020
val (hello_sem,hello_output) = hello_io_events_def |> SPEC_ALL |> UNDISCH |> CONJ_PAIR
2121
val (hello_not_fail,hello_sem_sing) = MATCH_MP semantics_prog_Terminate_not_Fail hello_sem |> CONJ_PAIR
2222

23-
val ffi_names =
24-
``config.lab_conf.ffi_names``
25-
|> (REWRITE_CONV[helloCompileTheory.config_def] THENC EVAL)
23+
val ffinames_to_string_list_def = backendTheory.ffinames_to_string_list_def;
2624

27-
val LENGTH_code =
28-
``LENGTH code``
29-
|> (REWRITE_CONV[helloCompileTheory.code_def] THENC listLib.LENGTH_CONV)
25+
Theorem extcalls_ffi_names:
26+
extcalls info.lab_conf.ffi_names = ffis
27+
Proof
28+
rewrite_tac [hello_compiled]
29+
\\ qspec_tac (‘info.lab_conf.ffi_names’,‘xs’) \\ Cases
30+
\\ gvs [extcalls_def,ffinames_to_string_list_def,libTheory.the_def]
31+
\\ Induct_on ‘x’
32+
\\ gvs [extcalls_def,ffinames_to_string_list_def,libTheory.the_def]
33+
\\ Cases \\ gvs [extcalls_def,ffinames_to_string_list_def,libTheory.the_def]
34+
QED
3035

31-
val LENGTH_data =
32-
``LENGTH data``
33-
|> (REWRITE_CONV[helloCompileTheory.data_def] THENC listLib.LENGTH_CONV)
36+
val ffis = ffis_def |> CONV_RULE (RAND_CONV EVAL);
37+
val ffi_names = extcalls_ffi_names |> SRULE [ffis]
3438

35-
val shmem =
36-
``config.lab_conf.shmem_extra``
37-
|> (REWRITE_CONV[helloCompileTheory.config_def] THENC EVAL)
39+
val LENGTH_code = “LENGTH code” |> SCONV [hello_compiled];
40+
val LENGTH_data = “LENGTH data” |> SCONV [hello_compiled];
41+
val shmem = “info.lab_conf.shmem_extra” |> SCONV [hello_compiled];
3842

3943
Overload hello_machine_config =
40-
``ag32_machine_config (extcalls config.lab_conf.ffi_names) (LENGTH code) (LENGTH data)``
44+
“ag32_machine_config (extcalls info.lab_conf.ffi_names) (LENGTH code) (LENGTH data)”
4145

4246
Theorem target_state_rel_hello_start_asm_state:
4347
SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧
4448
LENGTH inp ≤ stdin_size ∧
45-
is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms ⇒
46-
∃n. target_state_rel ag32_target (init_asm_state code data (extcalls config.lab_conf.ffi_names) (cl,inp)) (FUNPOW Next n ms) ∧
49+
is_ag32_init_state (init_memory code data (extcalls info.lab_conf.ffi_names)
50+
(cl,inp)) ms ⇒
51+
∃n. target_state_rel ag32_target
52+
(init_asm_state code data (extcalls info.lab_conf.ffi_names) (cl,inp))
53+
(FUNPOW Next n ms) ∧
4754
((FUNPOW Next n ms).io_events = ms.io_events) ∧
4855
(∀x. x ∉ (ag32_startup_addresses) ⇒
4956
((FUNPOW Next n ms).MEM x = ms.MEM x))
@@ -52,7 +59,7 @@ Proof
5259
\\ drule (GEN_ALL init_asm_state_RTC_asm_step)
5360
\\ disch_then drule
5461
\\ simp_tac std_ss []
55-
\\ disch_then(qspecl_then[`code`,`data`,`extcalls config.lab_conf.ffi_names`]mp_tac)
62+
\\ disch_then(qspecl_then[`code`,`data`,`extcalls info.lab_conf.ffi_names`]mp_tac)
5663
\\ impl_tac >- ( EVAL_TAC>> fs[ffi_names,LENGTH_data,LENGTH_code,extcalls_def,shmem])
5764
\\ strip_tac
5865
\\ drule (GEN_ALL target_state_rel_ag32_init)
@@ -70,7 +77,8 @@ val hello_startup_clock_def =
7077

7178
val compile_correct_applied =
7279
MATCH_MP compile_correct (cj 1 hello_compiled)
73-
|> SIMP_RULE(srw_ss())[LET_THM,ml_progTheory.init_state_env_thm,GSYM AND_IMP_INTRO]
80+
|> SIMP_RULE(srw_ss())[LET_THM,ml_progTheory.init_state_env_thm,
81+
GSYM AND_IMP_INTRO]
7482
|> C MATCH_MP hello_not_fail
7583
|> C MATCH_MP ag32_backend_config_ok
7684
|> REWRITE_RULE[hello_sem_sing,AND_IMP_INTRO]
@@ -81,29 +89,33 @@ val compile_correct_applied =
8189
|> Q.GEN`cbspace` |> Q.SPEC`0`
8290
|> Q.GEN`data_sp` |> Q.SPEC`0`
8391

84-
Triviality to_MAP_ExtCall:
85-
[ExtCall n] = MAP ExtCall [n] ∧
86-
(ExtCall n::MAP ExtCall ns) = MAP ExtCall (n::ns)
87-
Proof
88-
fs []
89-
QED
90-
9192
Theorem hello_installed:
9293
SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧
9394
LENGTH inp ≤ stdin_size ∧
94-
is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms0 ⇒
95-
installed code 0 data 0 config.lab_conf.ffi_names
95+
is_ag32_init_state (init_memory code data (extcalls info.lab_conf.ffi_names) (cl,inp)) ms0 ⇒
96+
installed code 0 data 0 info.lab_conf.ffi_names
9697
(heap_regs ag32_backend_config.stack_conf.reg_names)
97-
(hello_machine_config) config.lab_conf.shmem_extra
98+
(hello_machine_config) info.lab_conf.shmem_extra
9899
(FUNPOW Next (hello_startup_clock ms0 inp cl) ms0)
99100
Proof
100101
rewrite_tac[ffi_names, extcalls_def, shmem]
101102
\\ strip_tac
102-
\\ rewrite_tac [to_MAP_ExtCall]
103+
\\ qmatch_asmsub_abbrev_tac ‘init_memory _ _ ff’
104+
\\ qmatch_goalsub_abbrev_tac ‘installed _ _ _ _ dd’
105+
\\ ‘dd = SOME (MAP ExtCall ff)’ by
106+
(unabbrev_all_tac
107+
\\ assume_tac (cj 1 hello_compiled)
108+
\\ drule ag32_configProofTheory.compile_imp_ffi_names
109+
\\ gvs [hello_compiled]
110+
\\ gvs [GSYM hello_compiled,ffis]
111+
\\ simp [backendTheory.set_oracle_def,
112+
ag32_configTheory.ag32_backend_config_def])
113+
\\ asm_rewrite_tac []
103114
\\ irule ag32_installed
104115
\\ drule hello_startup_clock_def
105116
\\ disch_then drule
106117
\\ rewrite_tac[ffi_names, extcalls_def]
118+
\\ unabbrev_all_tac
107119
\\ disch_then drule
108120
\\ strip_tac
109121
\\ simp[]
@@ -161,7 +173,8 @@ QED
161173
Theorem hello_ag32_next:
162174
SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧ wfcl cl ∧
163175
LENGTH inp ≤ stdin_size ∧
164-
is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms0
176+
is_ag32_init_state (init_memory code data (extcalls info.lab_conf.ffi_names)
177+
(cl,inp)) ms0
165178
⇒
166179
∃k1. ∀k. k1 ≤ k ⇒
167180
let ms = FUNPOW Next k ms0 in

‎examples/compilation/ag32/proofs/sortProofScript.sml

Lines changed: 38 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -37,30 +37,34 @@ val sort_io_events_def =
3737
val (sort_sem,sort_output) = sort_io_events_def |> SPEC_ALL |> CONJ_PAIR
3838
val (sort_not_fail,sort_sem_sing) = MATCH_MP semantics_prog_Terminate_not_Fail sort_sem |> CONJ_PAIR
3939

40-
val ffi_names =
41-
``config.lab_conf.ffi_names``
42-
|> (REWRITE_CONV[sortCompileTheory.config_def] THENC EVAL)
40+
val ffinames_to_string_list_def = backendTheory.ffinames_to_string_list_def;
4341

44-
val LENGTH_code =
45-
``LENGTH code``
46-
|> (REWRITE_CONV[sortCompileTheory.code_def] THENC listLib.LENGTH_CONV)
42+
Theorem extcalls_ffi_names:
43+
extcalls info.lab_conf.ffi_names = ffis
44+
Proof
45+
rewrite_tac [sort_compiled]
46+
\\ qspec_tac (‘info.lab_conf.ffi_names’,‘xs’) \\ Cases
47+
\\ gvs [extcalls_def,ffinames_to_string_list_def,libTheory.the_def]
48+
\\ Induct_on ‘x’
49+
\\ gvs [extcalls_def,ffinames_to_string_list_def,libTheory.the_def]
50+
\\ Cases \\ gvs [extcalls_def,ffinames_to_string_list_def,libTheory.the_def]
51+
QED
4752

48-
val LENGTH_data =
49-
``LENGTH data``
50-
|> (REWRITE_CONV[sortCompileTheory.data_def] THENC listLib.LENGTH_CONV)
53+
val ffis = ffis_def |> CONV_RULE (RAND_CONV EVAL);
54+
val ffi_names = extcalls_ffi_names |> SRULE [ffis]
5155

52-
val shmem =
53-
``config.lab_conf.shmem_extra``
54-
|> (REWRITE_CONV[sortCompileTheory.config_def] THENC EVAL)
56+
val LENGTH_code = “LENGTH code” |> SCONV [sort_compiled];
57+
val LENGTH_data = “LENGTH data” |> SCONV [sort_compiled];
58+
val shmem = “info.lab_conf.shmem_extra” |> SCONV [sort_compiled];
5559

5660
Overload sort_machine_config =
57-
``ag32_machine_config (extcalls config.lab_conf.ffi_names) (LENGTH code) (LENGTH data)``
61+
“ag32_machine_config (extcalls info.lab_conf.ffi_names) (LENGTH code) (LENGTH data)”
5862

5963
Theorem target_state_rel_sort_start_asm_state:
6064
SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧
6165
LENGTH inp ≤ stdin_size ∧
62-
is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms ⇒
63-
∃n. target_state_rel ag32_target (init_asm_state code data (extcalls config.lab_conf.ffi_names) (cl,inp)) (FUNPOW Next n ms) ∧
66+
is_ag32_init_state (init_memory code data (extcalls info.lab_conf.ffi_names) (cl,inp)) ms ⇒
67+
∃n. target_state_rel ag32_target (init_asm_state code data (extcalls info.lab_conf.ffi_names) (cl,inp)) (FUNPOW Next n ms) ∧
6468
((FUNPOW Next n ms).io_events = ms.io_events) ∧
6569
(∀x. x ∉ (ag32_startup_addresses) ⇒
6670
((FUNPOW Next n ms).MEM x = ms.MEM x))
@@ -69,7 +73,7 @@ Proof
6973
\\ drule (GEN_ALL init_asm_state_RTC_asm_step)
7074
\\ disch_then drule
7175
\\ simp_tac std_ss []
72-
\\ disch_then(qspecl_then[`code`,`data`,`extcalls config.lab_conf.ffi_names`]mp_tac)
76+
\\ disch_then(qspecl_then[`code`,`data`,`extcalls info.lab_conf.ffi_names`]mp_tac)
7377
\\ impl_tac >- ( EVAL_TAC>> fs[ffi_names,LENGTH_data,LENGTH_code,extcalls_def])
7478
\\ strip_tac
7579
\\ drule (GEN_ALL target_state_rel_ag32_init)
@@ -87,7 +91,8 @@ val sort_startup_clock_def =
8791

8892
val compile_correct_applied =
8993
MATCH_MP compile_correct (cj 1 sort_compiled)
90-
|> SIMP_RULE(srw_ss())[LET_THM,ml_progTheory.init_state_env_thm,GSYM AND_IMP_INTRO]
94+
|> SIMP_RULE(srw_ss())[LET_THM,ml_progTheory.init_state_env_thm,
95+
GSYM AND_IMP_INTRO]
9196
|> C MATCH_MP sort_not_fail
9297
|> C MATCH_MP ag32_backend_config_ok
9398
|> REWRITE_RULE[sort_sem_sing,AND_IMP_INTRO]
@@ -98,29 +103,33 @@ val compile_correct_applied =
98103
|> Q.GEN`cbspace` |> Q.SPEC`0`
99104
|> Q.GEN`data_sp` |> Q.SPEC`0`
100105

101-
Triviality to_MAP_ExtCall:
102-
[ExtCall n] = MAP ExtCall [n] ∧
103-
(ExtCall n::MAP ExtCall ns) = MAP ExtCall (n::ns)
104-
Proof
105-
fs []
106-
QED
107-
108106
Theorem sort_installed:
109107
SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧
110108
LENGTH inp ≤ stdin_size ∧
111-
is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms0 ⇒
112-
installed code 0 data 0 config.lab_conf.ffi_names
109+
is_ag32_init_state (init_memory code data (extcalls info.lab_conf.ffi_names) (cl,inp)) ms0 ⇒
110+
installed code 0 data 0 info.lab_conf.ffi_names
113111
(heap_regs ag32_backend_config.stack_conf.reg_names)
114-
(sort_machine_config) config.lab_conf.shmem_extra
112+
(sort_machine_config) info.lab_conf.shmem_extra
115113
(FUNPOW Next (sort_startup_clock ms0 inp cl) ms0)
116114
Proof
117115
rewrite_tac[ffi_names, extcalls_def, shmem]
118116
\\ strip_tac
119-
\\ rewrite_tac [to_MAP_ExtCall]
117+
\\ qmatch_asmsub_abbrev_tac ‘init_memory _ _ ff’
118+
\\ qmatch_goalsub_abbrev_tac ‘installed _ _ _ _ dd’
119+
\\ ‘dd = SOME (MAP ExtCall ff)’ by
120+
(unabbrev_all_tac
121+
\\ assume_tac (cj 1 sort_compiled)
122+
\\ drule ag32_configProofTheory.compile_imp_ffi_names
123+
\\ gvs [sort_compiled]
124+
\\ gvs [GSYM sort_compiled,ffis]
125+
\\ simp [backendTheory.set_oracle_def,
126+
ag32_configTheory.ag32_backend_config_def])
127+
\\ asm_rewrite_tac []
120128
\\ irule ag32_installed
121129
\\ drule sort_startup_clock_def
122130
\\ disch_then drule
123131
\\ rewrite_tac[ffi_names, extcalls_def]
132+
\\ unabbrev_all_tac
124133
\\ disch_then drule
125134
\\ strip_tac
126135
\\ simp[]
@@ -186,7 +195,7 @@ QED
186195

187196
Theorem sort_ag32_next:
188197
LENGTH inp ≤ stdin_size ∧
189-
is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) ([strlit"sort"],inp)) ms0
198+
is_ag32_init_state (init_memory code data (extcalls info.lab_conf.ffi_names) ([strlit"sort"],inp)) ms0
190199
⇒
191200
∃k1. ∀k. k1 ≤ k ⇒
192201
let ms = FUNPOW Next k ms0 in

‎examples/compilation/ag32/proofs/wordcountProofScript.sml

Lines changed: 38 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -47,30 +47,34 @@ val wordcount_io_events_def =
4747
val (wordcount_sem,wordcount_output) = wordcount_io_events_def |> SPEC_ALL |> CONJ_PAIR
4848
val (wordcount_not_fail,wordcount_sem_sing) = MATCH_MP semantics_prog_Terminate_not_Fail wordcount_sem |> CONJ_PAIR
4949

50-
val ffi_names =
51-
``config.lab_conf.ffi_names``
52-
|> (REWRITE_CONV[wordcountCompileTheory.config_def] THENC EVAL)
50+
val ffinames_to_string_list_def = backendTheory.ffinames_to_string_list_def;
5351

54-
val LENGTH_code =
55-
``LENGTH code``
56-
|> (REWRITE_CONV[wordcountCompileTheory.code_def] THENC listLib.LENGTH_CONV)
52+
Theorem extcalls_ffi_names:
53+
extcalls info.lab_conf.ffi_names = ffis
54+
Proof
55+
rewrite_tac [wordcount_compiled]
56+
\\ qspec_tac (‘info.lab_conf.ffi_names’,‘xs’) \\ Cases
57+
\\ gvs [extcalls_def,ffinames_to_string_list_def,libTheory.the_def]
58+
\\ Induct_on ‘x’
59+
\\ gvs [extcalls_def,ffinames_to_string_list_def,libTheory.the_def]
60+
\\ Cases \\ gvs [extcalls_def,ffinames_to_string_list_def,libTheory.the_def]
61+
QED
5762

58-
val LENGTH_data =
59-
``LENGTH data``
60-
|> (REWRITE_CONV[wordcountCompileTheory.data_def] THENC listLib.LENGTH_CONV)
63+
val ffis = ffis_def |> CONV_RULE (RAND_CONV EVAL);
64+
val ffi_names = extcalls_ffi_names |> SRULE [ffis]
6165

62-
val shmem =
63-
``config.lab_conf.shmem_extra``
64-
|> (REWRITE_CONV[wordcountCompileTheory.config_def] THENC EVAL)
66+
val LENGTH_code = “LENGTH code” |> SCONV [wordcount_compiled];
67+
val LENGTH_data = “LENGTH data” |> SCONV [wordcount_compiled];
68+
val shmem = “info.lab_conf.shmem_extra” |> SCONV [wordcount_compiled];
6569

6670
Overload wordcount_machine_config =
67-
``ag32_machine_config (extcalls config.lab_conf.ffi_names) (LENGTH code) (LENGTH data)``
71+
“ag32_machine_config (extcalls info.lab_conf.ffi_names) (LENGTH code) (LENGTH data)”
6872

6973
Theorem target_state_rel_wordcount_start_asm_state:
7074
SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧
7175
LENGTH inp ≤ stdin_size ∧
72-
is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms ⇒
73-
∃n. target_state_rel ag32_target (init_asm_state code data (extcalls config.lab_conf.ffi_names) (cl,inp)) (FUNPOW Next n ms) ∧
76+
is_ag32_init_state (init_memory code data (extcalls info.lab_conf.ffi_names) (cl,inp)) ms ⇒
77+
∃n. target_state_rel ag32_target (init_asm_state code data (extcalls info.lab_conf.ffi_names) (cl,inp)) (FUNPOW Next n ms) ∧
7478
((FUNPOW Next n ms).io_events = ms.io_events) ∧
7579
(∀x. x ∉ (ag32_startup_addresses) ⇒
7680
((FUNPOW Next n ms).MEM x = ms.MEM x))
@@ -79,7 +83,7 @@ Proof
7983
\\ drule (GEN_ALL init_asm_state_RTC_asm_step)
8084
\\ disch_then drule
8185
\\ simp_tac std_ss []
82-
\\ disch_then(qspecl_then[`code`,`data`,`extcalls config.lab_conf.ffi_names`]mp_tac)
86+
\\ disch_then(qspecl_then[`code`,`data`,`extcalls info.lab_conf.ffi_names`]mp_tac)
8387
\\ impl_tac >- ( EVAL_TAC>> fs[ffi_names,LENGTH_data,LENGTH_code,extcalls_def])
8488
\\ strip_tac
8589
\\ drule (GEN_ALL target_state_rel_ag32_init)
@@ -97,7 +101,8 @@ val wordcount_startup_clock_def =
97101

98102
val wordcount_compile_correct_applied =
99103
MATCH_MP compile_correct (cj 1 wordcount_compiled)
100-
|> SIMP_RULE(srw_ss())[LET_THM,ml_progTheory.init_state_env_thm,GSYM AND_IMP_INTRO]
104+
|> SIMP_RULE(srw_ss())[LET_THM,ml_progTheory.init_state_env_thm,
105+
GSYM AND_IMP_INTRO]
101106
|> C MATCH_MP wordcount_not_fail
102107
|> C MATCH_MP ag32_backend_config_ok
103108
|> REWRITE_RULE[wordcount_sem_sing,AND_IMP_INTRO]
@@ -109,29 +114,33 @@ val wordcount_compile_correct_applied =
109114
|> Q.GEN`data_sp` |> Q.SPEC`0`
110115
|> curry save_thm "wordcount_compile_correct_applied";
111116

112-
Triviality to_MAP_ExtCall:
113-
[ExtCall n] = MAP ExtCall [n] ∧
114-
(ExtCall n::MAP ExtCall ns) = MAP ExtCall (n::ns)
115-
Proof
116-
fs []
117-
QED
118-
119117
Theorem wordcount_installed:
120118
SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧
121119
LENGTH inp ≤ stdin_size ∧
122-
is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms0 ⇒
123-
installed code 0 data 0 config.lab_conf.ffi_names
120+
is_ag32_init_state (init_memory code data (extcalls info.lab_conf.ffi_names) (cl,inp)) ms0 ⇒
121+
installed code 0 data 0 info.lab_conf.ffi_names
124122
(heap_regs ag32_backend_config.stack_conf.reg_names)
125-
(wordcount_machine_config) config.lab_conf.shmem_extra
123+
(wordcount_machine_config) info.lab_conf.shmem_extra
126124
(FUNPOW Next (wordcount_startup_clock ms0 inp cl) ms0)
127125
Proof
128126
rewrite_tac[ffi_names, extcalls_def, shmem]
129127
\\ strip_tac
130-
\\ rewrite_tac [to_MAP_ExtCall]
128+
\\ qmatch_asmsub_abbrev_tac ‘init_memory _ _ ff’
129+
\\ qmatch_goalsub_abbrev_tac ‘installed _ _ _ _ dd’
130+
\\ ‘dd = SOME (MAP ExtCall ff)’ by
131+
(unabbrev_all_tac
132+
\\ assume_tac (cj 1 wordcount_compiled)
133+
\\ drule ag32_configProofTheory.compile_imp_ffi_names
134+
\\ gvs [wordcount_compiled]
135+
\\ gvs [GSYM wordcount_compiled,ffis]
136+
\\ simp [backendTheory.set_oracle_def,
137+
ag32_configTheory.ag32_backend_config_def])
138+
\\ asm_rewrite_tac []
131139
\\ irule ag32_installed
132140
\\ drule wordcount_startup_clock_def
133141
\\ disch_then drule
134142
\\ rewrite_tac[ffi_names, extcalls_def]
143+
\\ unabbrev_all_tac
135144
\\ disch_then drule
136145
\\ strip_tac
137146
\\ simp[]
@@ -195,7 +204,7 @@ QED
195204

196205
Theorem wordcount_ag32_next:
197206
LENGTH inp ≤ stdin_size ∧
198-
is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) ([strlit"wordcount"],inp)) ms0
207+
is_ag32_init_state (init_memory code data (extcalls info.lab_conf.ffi_names) ([strlit"wordcount"],inp)) ms0
199208
⇒
200209
∃k1. ∀k. k1 ≤ k ⇒
201210
let ms = FUNPOW Next k ms0 in

0 commit comments

Comments
 (0)