Skip to content

Use max list #1236

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Sep 26, 2025
Merged

Use max list #1236

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e3a6cb1
replace list_max by MAX_LIST in wordLang
ordinarymath Sep 12, 2025
04f078c
fix word_alloc for change
ordinarymath Sep 13, 2025
37ecb16
fix compiler/backend/proofs for changes
ordinarymath Sep 13, 2025
8394da2
fix cv_translation
ordinarymath Sep 22, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
65 changes: 25 additions & 40 deletions compiler/backend/proofs/data_to_word_memoryProofScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,45 +46,30 @@ Proof
Induct \\ fs [REPLICATE]
QED

Theorem list_max_leq_suff:
EVERY (\x. x <= b) ls ==> list_max ls <= b
Theorem MAX_LIST_sum_bound:
SUM ls <= MAX_LIST ls * LENGTH ls
Proof
Induct_on`ls` \\ rw[list_max_def]
QED

Theorem list_max_mem:
ls <> [] ==> MEM (list_max ls) ls
Proof
Induct_on`ls` \\ rw[list_max_def]
\\ Cases_on`ls` \\ fs[list_max_def]
QED

Theorem list_max_sum_bound:
SUM ls <= list_max ls * LENGTH ls
Proof
Induct_on`ls` \\ rw[list_max_def,ADD1,LEFT_ADD_DISTRIB]
Induct_on`ls` \\ rw[MAX_DEF,ADD1,LEFT_ADD_DISTRIB]
\\ match_mp_tac LESS_EQ_TRANS
\\ asm_exists_tac \\ simp[]
QED

Theorem list_max_bounded_elements:
!l1 l2. LIST_REL $<= l1 l2 ==> list_max l1 <= list_max l2
Theorem MAX_LIST_bounded_elements:
!l1 l2. LIST_REL $<= l1 l2 ==> MAX_LIST l1 <= MAX_LIST l2
Proof
Induct \\ rw[list_max_def] \\ res_tac \\ rw[list_max_def]
Induct \\ rw[MAX_DEF] \\ res_tac \\ rw[MAX_DEF]
QED

Theorem list_max_map:
∀f l. (∀x y. x < y ==> f x < f y) ==> list_max (MAP f l) = if NULL l then 0 else f (list_max l)
Theorem MAX_LIST_MAP:
∀f l. (∀x y. x < y ==> f x < f y) ==> MAX_LIST (MAP f l) = if NULL l then 0 else f (MAX_LIST l)
Proof
rpt strip_tac
\\ Induct_on`l` \\ rw[list_max_def,NULL_EQ]
\\ res_tac \\ fs[list_max_def] \\ rveq
\\ fs[NOT_LESS]
\\ Cases_on`l = []` \\ fs[list_max_def]
\\ Cases_on`h < list_max l` \\ fs[]
>- ( res_tac \\ fs[] )
\\ `h = list_max l` by fs[]
\\ fs[]
Induct_on`l` \\ rw[NULL_EQ] \\
`!a b. f (MAX a b) = MAX (f a) (f b)`
by (rpt gen_tac \\
Cases_on `a < b` >- (first_x_assum drule \\ simp[MAX_DEF]) \\
Cases_on `a = b` >- fs[] \\
`b < a` by fs[] >- (first_x_assum drule \\ simp[MAX_DEF])) \\
fs[]
QED

Theorem w2i_i2w_IMP:
Expand Down Expand Up @@ -9027,7 +9012,7 @@ Proof
QED

Definition v_depth_def:
(v_depth (Block _ _ ls) = (if NULL ls then 0 else 1) + list_max (MAP v_depth ls)) ∧
(v_depth (Block _ _ ls) = (if NULL ls then 0 else 1) + MAX_LIST (MAP v_depth ls)) ∧
(v_depth _ = 0n)
Termination
WF_REL_TAC`measure v_size` \\
Expand Down Expand Up @@ -9083,10 +9068,10 @@ Theorem memory_rel_depth_limit:
elements_list (MAP FST ls ++ (v::(MAP FST vars)))
Proof
ho_match_mp_tac v_ind
\\ rw[v_depth_def,LENGTH_NIL_SYM,NULL_EQ,list_max_def]
\\ rw[v_depth_def,LENGTH_NIL_SYM,NULL_EQ]
\\ fsrw_tac[ETA_ss][]
\\ `MEM (list_max (MAP v_depth l)) (MAP v_depth l)`
by ( match_mp_tac list_max_mem \\ rw[] )
\\ `MEM (MAX_LIST (MAP v_depth l)) (MAP v_depth l)`
by (match_mp_tac MAX_LIST_MEM \\ rw[] )
\\ fs[MEM_MAP,EVERY_MEM]
\\ qmatch_assum_rename_tac`MEM e l`
\\ first_x_assum(qspec_then`e`mp_tac) \\ simp[]
Expand Down Expand Up @@ -9182,7 +9167,7 @@ Theorem memory_rel_depth_size_limit:
⇒
vb_size v ≤ dimword(:'a) ** (v_depth v + 1)
Proof
ho_match_mp_tac v_ind \\ rw[vb_size_def,EXP,NULL_EQ,list_max_def]
ho_match_mp_tac v_ind \\ rw[vb_size_def,EXP,NULL_EQ]
\\ TRY ( fs[dimword_def] \\ NO_TAC )
>- (
rpt_drule memory_rel_Block_IMP
Expand All @@ -9194,8 +9179,8 @@ Proof
qspecl_then[`dimindex(:'a)`,`4`,`2`]mp_tac EXP_SUB
\\ impl_tac >- fs[good_dimindex_def]
\\ strip_tac \\ fs[X_LT_DIV] )
\\ `SUM (MAP vb_size l) <= list_max (MAP vb_size l) * LENGTH l`
by metis_tac[list_max_sum_bound,LENGTH_MAP]
\\ `SUM (MAP vb_size l) <= MAX_LIST (MAP vb_size l) * LENGTH l`
by metis_tac[MAX_LIST_sum_bound,LENGTH_MAP]
\\ `n < dimword(:'a) DIV 16`
by (
fs[memory_rel_def,word_ml_inv_def,bc_stack_ref_inv_def,abs_ml_inv_def]
Expand All @@ -9205,14 +9190,14 @@ Proof
\\ qexists_tac`SUM (MAP vb_size l) + dimword(:'a) DIV 8`
\\ conj_tac >- simp[]
\\ qabbrev_tac`f = λx. dimword(:'a) * dimword(:'a) ** x`
\\ `list_max (MAP vb_size l) <= list_max (MAP (f o v_depth) l)`
\\ `MAX_LIST (MAP vb_size l) <= MAX_LIST (MAP (f o v_depth) l)`
by (
match_mp_tac list_max_bounded_elements
match_mp_tac MAX_LIST_bounded_elements
\\ fs[LIST_REL_EL_EQN,EVERY_MEM,MEM_EL,EL_MAP,Abbr`f`,PULL_EXISTS]
\\ rw[] \\ first_x_assum (match_mp_tac o MP_CANON) \\ rw[]
\\ rpt_drule memory_rel_Block_MEM \\ rw[]
\\ metis_tac[CONS_APPEND] )
\\ Q.ISPECL_THEN[`f`,`MAP v_depth l`]mp_tac list_max_map
\\ Q.ISPECL_THEN[`f`,`MAP v_depth l`]mp_tac MAX_LIST_MAP
\\ simp[NULL_EQ,Abbr`f`]
\\ rewrite_tac[TWO,EXP,ONE]
\\ rewrite_tac[GSYM ONE,MULT_RIGHT_1]
Expand Down
119 changes: 42 additions & 77 deletions compiler/backend/proofs/word_allocProofScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7859,11 +7859,10 @@ Proof
full_simp_tac(srw_ss())[EVERY_MEM]>>srw_tac[][]>>res_tac>>
match_mp_tac every_var_exp_mono>>
HINT_EXISTS_TAC>>srw_tac[][]>>
qpat_abbrev_tac`ls':(num list) = MAP f ls`>>
Q.ISPECL_THEN [`ls'`] assume_tac list_max_max>>
full_simp_tac(srw_ss())[EVERY_MEM,Abbr`ls'`,MEM_MAP,PULL_EXISTS]>>
pop_assum(qspec_then`a` assume_tac)>>rev_full_simp_tac(srw_ss())[]>>
DECIDE_TAC
irule LE_TRANS >>
irule_at (Pos (el 2)) MAX_LIST_PROPERTY >>
simp[MEM_MAP,PULL_EXISTS] >>
first_x_assum (fn x => irule_at (Any) x >> first_x_assum irule)
QED

Triviality max_var_inst_max:
Expand All @@ -7877,86 +7876,52 @@ Proof
DECIDE_TAC
QED

Triviality MAX_DEF2:
MAX m n = (if n > m then n else m)
Proof
fs[MAX_DEF]
QED

Theorem max_var_max:
∀prog.
every_var (λx. x ≤ max_var prog) prog
Proof
Proof[exclude_simps = max3_def]
ho_match_mp_tac max_var_ind>>
rpt strip_tac >>
full_simp_tac(std_ss)[every_var_def,max_var_def]
>-
(Q.ISPECL_THEN [`MAP FST ls ++ MAP SND ls`] assume_tac list_max_max>>
rev_full_simp_tac(srw_ss())[] >> NO_TAC)
>- metis_tac[max_var_inst_max] >>
TRY
(match_mp_tac every_var_exp_mono>>
rpt strip_tac
>~ [`Call`]
>- (full_simp_tac(std_ss)[every_var_def,max_var_def,every_name_def] >>
`!x y z. max3 x y z = MAX x (MAX y z)` by simp[MAX_DEF,max3_def] >>
pop_assum (simp o single) >> rpt TOP_CASE_TAC >> fs[] >>
rpt strip_tac
>>~-([`EVERY`],
fs[EVERY_MEM] >> srw_tac[][] >>
every_drule MAX_LIST_PROPERTY >>
simp[])
>>~-([`max_var`],
srw_tac[][] >> match_mp_tac every_var_mono>>
first_x_assum (irule_at (Pos $ el 2)) >>
fs[]))
>~ [`If`]
>- (full_simp_tac(std_ss)[every_var_def,max_var_def,every_name_def] >>
`!x y z. max3 x y z = MAX x (MAX y z)` by simp[MAX_DEF,max3_def] >>
pop_assum (simp o single) >> TOP_CASE_TAC >> simp[every_var_imm_def] >>
(srw_tac[][] >> match_mp_tac every_var_mono>>
TRY(HINT_EXISTS_TAC)>>TRY(qexists_tac`λx. x ≤ max_var prog`)>>
srw_tac[][]>>
DECIDE_TAC)) >>

full_simp_tac(std_ss)[every_var_def,max_var_def,every_name_def] >>
`!x y z. max3 x y z = MAX x (MAX y z)` by simp[MAX_DEF,max3_def] >>
pop_assum (simp o single)
>~ [`max_var_inst`]
>- (metis_tac[max_var_inst_max])
>>~-([`max_var_exp`],
match_mp_tac every_var_exp_mono>>
qexists_tac`λx. x ≤ max_var_exp exp`>>
full_simp_tac(srw_ss())[max_var_exp_max]>>
DECIDE_TAC)
>- (
EVERY_CASE_TAC >> full_simp_tac(srw_ss())[] >>
TRY (full_simp_tac(srw_ss())[list_max_max,LET_THM] >> NO_TAC) >>
rpt strip_tac >> full_simp_tac(srw_ss())[EVERY_MEM,every_name_def] >>
rpt strip_tac >> LET_ELIM_TAC >> full_simp_tac(srw_ss())[] >>
TRY ( match_mp_tac every_var_mono>>
first_x_assum (irule_at (Pos last)) >>
rw[]) >>
TRY (
qmatch_asmsub_abbrev_tac `MEM _ ls` >>
Q.ISPECL_THEN [`ls`] assume_tac list_max_max>>
full_simp_tac(srw_ss())[EVERY_MEM] >>
first_x_assum drule_all >>
disch_tac >> rw[]) >>
UNABBREV_ALL_TAC >> EVERY_CASE_TAC >>
rw[] >> intLib.ARITH_TAC
)
>>~ [`max_var`]
>-(srw_tac[][] >> match_mp_tac every_var_mono>>
TRY(HINT_EXISTS_TAC)>>TRY(qexists_tac`λx. x ≤ max_var prog`)>>
srw_tac[][]>>
DECIDE_TAC)
>-(
Cases_on `ri` >> full_simp_tac(srw_ss())[every_var_imm_def] >>
LET_ELIM_TAC >> UNABBREV_ALL_TAC >>
TRY (intLib.ARITH_TAC) >>
rpt IF_CASES_TAC >> fs[] >>
match_mp_tac every_var_mono>>
first_x_assum (irule_at (Pos last)) >>
full_simp_tac (srw_ss())[] >>
intLib.ARITH_TAC)
>-((*This is ugly*)
fs[every_name_def] >>
fs[EVERY_MEM] >> rw[] >>
qmatch_asmsub_abbrev_tac `MEM x ls` >>
Q.ISPECL_THEN [`ls`] assume_tac list_max_max>>
fs[EVERY_MEM])
>-(fs[GSYM FOLDR_MAX_0_list_max])
>-(
fs[GSYM FOLDR_MAX_0_list_max] >>
fs[FOLDR_MAX_0_list_max] >>
fs[every_name_def] >>
fs[EVERY_MEM] >> rw[] >>
qmatch_asmsub_abbrev_tac `MEM x ls` >>
Q.ISPECL_THEN [`ls`] assume_tac list_max_max>>
fs[EVERY_MEM])
>-(
fs[GSYM FOLDR_MAX_0_list_max] >>
fs[FOLDR_MAX_0_list_max] >>
fs[every_name_def] >>
fs[EVERY_MEM] >> rw[] >>
qmatch_asmsub_abbrev_tac `MEM x ls` >>
Q.ISPECL_THEN [`ls`] assume_tac list_max_max>>
fs[EVERY_MEM])
>-(
fs[list_max_def] >>
IF_CASES_TAC >> fs[list_max_max] >>
Q.ISPECL_THEN [`ns`] assume_tac list_max_max>>
fs[EVERY_MEM] >> rw[] >> res_tac >> intLib.ARITH_TAC)
first_x_assum (irule_at (Pos $ el 2)) >>
fs[])
>>~-([`EVERY`],
fs[EVERY_MEM] >> srw_tac[][] >>
every_drule MAX_LIST_PROPERTY >>
simp[])
QED

Triviality limit_var_props:
Expand Down
Loading