Skip to content

Commit

Permalink
Merge pull request #791 from CakeML/lpr_opt
Browse files Browse the repository at this point in the history 
Optimize LPR checker
  • Loading branch information
@myreen
myreen authored Sep 29, 2020
2 parents 63791af + 26dcb39 commit 018eec6
Show file tree
Hide file tree
Showing 5 changed files with 303 additions and 81 deletions.
190 changes: 167 additions & 23 deletions examples/lpr_checker/array/lpr_arrayProgScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,13 +15,6 @@ val _ = translation_extends"UnsafeProg";
val _ = register_type``:lprstep``;
val _ = register_type``:'a spt``;

val _ = translate mk_BS_def;
val _ = translate mk_BN_def;
val _ = translate delete_def;
val _ = translate lookup_def;
val _ = translate lrnext_def;
val _ = translate foldi_def;
val _ = translate toAList_def;
val _ = translate insert_def;

(* TODO: make sure these get inlined! *)
Expand Down Expand Up @@ -484,11 +477,13 @@ val _ = translate flip_def;
val _ = translate (delete_literals_def |> SIMP_RULE (srw_ss()) [MEMBER_INTRO]);
val _ = translate overlap_assignment_def;

val _ = translate overlap_assignment_def;

val check_RAT_arr = process_topdecs`
fun check_RAT_arr lno fml carr np c ik i ci =
(
if List.member np ci then
case lookup_1 i ik of
case Alist.lookup ik i of
None => raise Fail (format_failure lno ("clause index has no reduction sequence: " ^ Int.toString i))
| Some is =>
case is of
Expand All @@ -508,7 +503,7 @@ Theorem check_RAT_arr_spec:
LIST_TYPE INT ci civ ∧
INT pp ppv ∧
(LIST_TYPE INT) c cv ∧
(SPTREE_SPT_TYPE (LIST_TYPE NUM)) ik ikv ∧
LIST_TYPE (PAIR_TYPE NUM (LIST_TYPE NUM)) ik ikv ∧
LIST_REL (OPTION_TYPE (LIST_TYPE INT)) fmlls fmllsv ∧
bounded_fml (LENGTH Clist) fmlls ∧
EVERY ($> (LENGTH Clist) ∘ index) c ∧
Expand All @@ -526,8 +521,7 @@ Theorem check_RAT_arr_spec:
))
(λe. ARRAY fmlv fmllsv * &(Fail_exn e ∧ check_RAT_list fmlls Clist pp c ik i ci = NONE)))
Proof
simp[check_RAT_list_def]>>
xcf "check_RAT_arr" (get_ml_prog_state ())>>
simp[check_RAT_list_def]>> xcf "check_RAT_arr" (get_ml_prog_state ())>>
fs[MEMBER_INTRO]>>
xlet_autop>>
reverse xif
Expand Down Expand Up @@ -600,7 +594,7 @@ QED
val check_PR_arr = process_topdecs`
fun check_PR_arr lno fml carr nw c ik i ci =
if check_overlap ci nw then
case lookup_1 i ik of
case Alist.lookup ik i of
None => if check_overlap ci (flip_1 nw) then () else raise Fail (format_failure lno ("clause index has no reduction sequence but is not satisfied by witness: " ^ Int.toString i))
| Some is =>
(case is of
Expand All @@ -618,7 +612,7 @@ Theorem check_PR_arr_spec:
LIST_TYPE INT ci civ ∧
(LIST_TYPE INT) w wv ∧
(LIST_TYPE INT) c cv ∧
(SPTREE_SPT_TYPE (LIST_TYPE NUM)) ik ikv ∧
LIST_TYPE (PAIR_TYPE NUM (LIST_TYPE NUM)) ik ikv ∧
LIST_REL (OPTION_TYPE (LIST_TYPE INT)) fmlls fmllsv ∧
bounded_fml (LENGTH Clist) fmlls ∧
EVERY ($> (LENGTH Clist) ∘ index) c ∧
Expand Down Expand Up @@ -922,7 +916,7 @@ Theorem every_check_RAT_inds_arr_spec:
LIST_TYPE NUM ls lsv ∧
INT pp ppv ∧
(LIST_TYPE INT) c cv ∧
(SPTREE_SPT_TYPE (LIST_TYPE NUM)) ik ikv ∧
LIST_TYPE (PAIR_TYPE NUM (LIST_TYPE NUM)) ik ikv ∧
NUM mini miniv ∧
LIST_TYPE NUM acc accv ∧
LIST_REL (OPTION_TYPE (LIST_TYPE INT)) fmlls fmllsv ∧
Expand Down Expand Up @@ -1012,7 +1006,7 @@ Theorem every_check_PR_inds_arr_spec:
LIST_TYPE NUM ls lsv ∧
(LIST_TYPE INT) w wv ∧
(LIST_TYPE INT) c cv ∧
(SPTREE_SPT_TYPE (LIST_TYPE NUM)) ik ikv ∧
LIST_TYPE (PAIR_TYPE NUM (LIST_TYPE NUM)) ik ikv ∧
NUM mini miniv ∧
LIST_TYPE NUM acc accv ∧
LIST_REL (OPTION_TYPE (LIST_TYPE INT)) fmlls fmllsv ∧
Expand Down Expand Up @@ -1109,7 +1103,7 @@ Theorem is_PR_arr_spec:
(LIST_TYPE INT) c cv ∧
OPTION_TYPE (LIST_TYPE INT) wopt woptv ∧
(LIST_TYPE NUM) i0 i0v ∧
(SPTREE_SPT_TYPE (LIST_TYPE NUM)) ik ikv ∧
LIST_TYPE (PAIR_TYPE NUM (LIST_TYPE NUM)) ik ikv ∧
LIST_REL (OPTION_TYPE (LIST_TYPE INT)) fmlls fmllsv ∧
LIST_REL (OPTION_TYPE NUM) earliest earliestv ∧
bounded_fml (LENGTH Clist) fmlls ∧
Expand Down Expand Up @@ -1410,6 +1404,153 @@ QED

val result = translate sorted_insert_def;

val check_earliest_arr = process_topdecs`
fun check_earliest_arr fml x old new is =
case is of
[] => True
| (i::is) =>
if i >= old then
(if i < new
then
(if Array.length fml <= i then check_earliest_arr fml x old new is
else
case Unsafe.sub fml i of
None => check_earliest_arr fml x old new is
| Some ci =>
not(List.member x ci) andalso check_earliest_arr fml x old new is)
else
check_earliest_arr fml x old new is)
else True` |> append_prog;

Theorem check_earliest_arr_spec:
∀is isv new newv old oldv x xv fmlls fmllsv fmlv.
LIST_REL (OPTION_TYPE (LIST_TYPE INT)) fmlls fmllsv ∧
INT x xv ∧
NUM old oldv ∧
NUM new newv ∧
LIST_TYPE NUM is isv
⇒
app (p : 'ffi ffi_proj)
^(fetch_v "check_earliest_arr" (get_ml_prog_state()))
[fmlv; xv; oldv; newv; isv]
(ARRAY fmlv fmllsv)
(POSTv v.
ARRAY fmlv fmllsv *
&(BOOL (check_earliest fmlls x old new is) v))
Proof
Induct>>xcf "check_earliest_arr" (get_ml_prog_state ())>>
fs[LIST_TYPE_def,check_earliest_def]
>- (
xmatch>>xcon>>
xsimpl)
>>
xmatch>>
rpt xlet_autop>>
reverse (Cases_on`h ≥ old`)>>fs[]
>- (
xif>>asm_exists_tac>>xsimpl>>
xcon>>xsimpl>>fs[])>>
xif>>asm_exists_tac>>fs[]>>
xlet_autop>>
reverse xif>>fs[]
>- (xapp>>xsimpl)>>
xlet_autop>>
xlet_autop>>
`LENGTH fmlls = LENGTH fmllsv` by
metis_tac[LIST_REL_LENGTH]>>
xif
>- (
simp[list_lookup_def]>>
xapp>>xsimpl)>>
xlet_autop>>
simp[list_lookup_def]>>
`OPTION_TYPE (LIST_TYPE INT) (EL h fmlls) (EL h fmllsv)` by fs[LIST_REL_EL_EQN]>>
TOP_CASE_TAC>>fs[OPTION_TYPE_def]
>-
(xmatch >> xapp>>xsimpl)>>
xmatch>>
xlet_autop>>
xlet_autop>>
xlog>>
IF_CASES_TAC>>fs[MEMBER_INTRO]>>xsimpl>>
xapp>>xsimpl
QED

val _ = translate list_min_aux_def;

val _ = translate list_min_def;

val hint_earliest_arr = process_topdecs`
fun hint_earliest_arr c w ik fml inds earr =
case w of
None =>
let val lm = list_min ik in
if lm = 0 then earr
else
let val p = safe_hd c
val ip = index (~p) in
if Array.length earr <= ip then earr
else
(case Unsafe.sub earr ip of
None => earr
| Some mini =>
if check_earliest_arr fml (~p) mini lm inds
then
resize_update_arr (Some lm) ip earr
else
earr)
end
end
| Some u => earr` |> append_prog

Theorem hint_earliest_arr_spec:
LIST_TYPE INT c cv ∧
OPTION_TYPE (LIST_TYPE INT) w wv ∧
LIST_TYPE (PAIR_TYPE NUM (LIST_TYPE NUM)) ik ikv ∧
LIST_REL (OPTION_TYPE (LIST_TYPE INT)) fmlls fmllsv ∧
(LIST_TYPE NUM) ls lsv ∧
LIST_REL (OPTION_TYPE NUM) earliest earliestv
⇒
app (p : 'ffi ffi_proj)
^(fetch_v "hint_earliest_arr" (get_ml_prog_state()))
[cv; wv; ikv; fmlv; lsv; Earrv]
(ARRAY fmlv fmllsv * ARRAY Earrv earliestv)
(POSTv Earrv'.
ARRAY fmlv fmllsv *
SEP_EXISTS earliestv'.
ARRAY Earrv' earliestv' *
&(LIST_REL (OPTION_TYPE NUM) (hint_earliest c w ik fmlls ls earliest) earliestv'))
Proof
rw[]>>xcf "hint_earliest_arr" (get_ml_prog_state ())>>
fs[hint_earliest_def]>>
reverse TOP_CASE_TAC>>fs[OPTION_TYPE_def]>>xmatch
>- (xvar>>xsimpl)>>
rpt xlet_autop>>
xif
>- (xvar>>xsimpl)>>
rpt xlet_autop>>
simp[list_lookup_def]>>
`LENGTH earliest = LENGTH earliestv` by metis_tac[LIST_REL_LENGTH]>>
xif>>fs[]
>- (xvar>>xsimpl)>>
xlet_autop>>
`OPTION_TYPE NUM (EL (index (-safe_hd c)) earliest) (EL (index (-safe_hd c)) earliestv)` by fs[LIST_REL_EL_EQN]>>
TOP_CASE_TAC>>fs[OPTION_TYPE_def]>>
xmatch
>-
(xvar>>xsimpl)>>
rpt xlet_autop>>
reverse xif>>fs[]
>- (xvar>>xsimpl)>>
xlet_autop>>
xapp_spec (resize_update_arr_spec |> Q.GEN `vty` |> ISPEC ``NUM``)>>
xsimpl>>
asm_exists_tac>>simp[]>>
asm_exists_tac>>simp[]>>
qexists_tac`SOME (list_min ik)`>>
simp[OPTION_TYPE_def]
QED

val check_lpr_step_arr = process_topdecs`
fun check_lpr_step_arr lno step fml ls carr earr =
case step of
Expand All @@ -1418,6 +1559,7 @@ val check_lpr_step_arr = process_topdecs`
| Pr n c w i0 ik =>
let val p = safe_hd c
val carr = resize_carr c carr
val earr = hint_earliest_arr c w ik fml ls earr
val ls = is_PR_arr lno fml ls carr earr p c w i0 ik
val earr = update_earliest_arr earr n c in
(resize_update_arr (Some c) n fml, sorted_insert n ls, carr, earr)
Expand Down Expand Up @@ -1517,7 +1659,7 @@ Theorem check_lpr_step_arr_spec:
* (* v2 is the indexing list *)
&unwrap_TYPE (λa b. LIST_TYPE NUM (FST (SND a)) b) (check_lpr_step_list step fmlls ls Clist earliest) v2
)
(λe. ARRAY fmlv fmllsv * ARRAY Earrv earliestv * &(Fail_exn e ∧ check_lpr_step_list step fmlls ls Clist earliest = NONE)))
(λe. ARRAY fmlv fmllsv * (SEP_EXISTS Earrv earliestv. ARRAY Earrv earliestv) * &(Fail_exn e ∧ check_lpr_step_list step fmlls ls Clist earliest = NONE)))
Proof
rw[check_lpr_step_list_def]>>
xcf "check_lpr_step_arr" (get_ml_prog_state ())>>
Expand All @@ -1533,13 +1675,15 @@ Proof
xlet_auto
>- (xsimpl>>
metis_tac[bounded_fml_leq,LENGTH_resize_Clist,EVERY_index_resize_Clist])
>- (xsimpl>> rw[] >> simp[] >> metis_tac[])>>
>- (xsimpl>> rw[] >> simp[] >>
qexists_tac`Earrv'`>> qexists_tac`earliestv'`>>
xsimpl)>>
fs[unwrap_TYPE_def]>>
TOP_CASE_TAC>>fs[]>>
rpt xlet_autop>>
xlet`(POSTv resv.
W8ARRAY carrv Clist' *
ARRAY Earrv' earliestv' *
ARRAY Earrv'' earliestv'' *
SEP_EXISTS fmllsv'.
ARRAY resv fmllsv' *
&(LIST_REL (OPTION_TYPE (LIST_TYPE INT)) (resize_update_list fmlls NONE (SOME l) n) fmllsv'))`
Expand Down Expand Up @@ -1721,7 +1865,7 @@ Theorem parse_and_run_arr_spec:
)
) *
&unwrap_TYPE (λa b. LIST_TYPE NUM (FST (SND a)) b) (parse_and_run_list fmlls ls Clist earliest l) v2)
(λe. ARRAY fmlv fmllsv * ARRAY Earrv earliestv * &(Fail_exn e ∧ parse_and_run_list fmlls ls Clist earliest l = NONE)))
(λe. ARRAY fmlv fmllsv * (SEP_EXISTS Earrv' earliestv'. ARRAY Earrv' earliestv') * &(Fail_exn e ∧ parse_and_run_list fmlls ls Clist earliest l = NONE)))
Proof
rw[parse_and_run_list_def]>>
xcf "parse_and_run_arr" (get_ml_prog_state ())>>
Expand All @@ -1732,6 +1876,7 @@ Proof
rpt xlet_autop>>
xraise>>xsimpl>>
simp[unwrap_TYPE_def,Fail_exn_def]>>
qexists_tac`Earrv`>> qexists_tac`earliestv`>>xsimpl>>
metis_tac[])>>
xapp>>fs[]>>
metis_tac[]
Expand Down Expand Up @@ -1890,8 +2035,7 @@ Proof
\\ xmatch \\ fs []
\\ xlet_auto >- (
xsimpl>>simp[unwrap_TYPE_def]>>rw[]>>
asm_exists_tac>>simp[]>>rw[]>>fs[]>>
rfs[])
qexists_tac`x`>> qexists_tac`x'`>>xsimpl)
>- (
xsimpl>>
simp[parse_and_run_file_list_def]>>
Expand All @@ -1900,7 +2044,7 @@ Proof
qexists_tac ‘k’>>
qexists_tac`fmlv`>>qexists_tac`fmllsv`>>
xsimpl>>
qexists_tac`Earrv`>>qexists_tac`earliestv`>>
qexists_tac`x`>>qexists_tac`x'`>>
qexists_tac ‘lines’>>
xsimpl>>
metis_tac[])>>
Expand Down
Loading

0 comments on commit 018eec6

Please sign in to comment.