From 7a4ed25a1c86b11f888c1dcbe99f988258bb9210 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Wed, 11 Oct 2023 11:17:28 +1100 Subject: [PATCH] Various fixes for theorem-rebind errors Now think that -t3 build goes through entirely. --- .../machine-code/graph/func_decompileLib.sml | 2 + .../machine-code/lisp/lisp_proofScript.sml | 16 +++++--- .../lisp-runtime/extract/lisp_extractLib.sml | 7 ++++ .../garbage-collector/stop_and_copyScript.sml | 40 +++++++++---------- .../implementation/lisp_codegenScript.sml | 8 ---- .../implementation/lisp_opsScript.sml | 13 ++++-- .../implementation/lisp_symbolsScript.sml | 6 --- 7 files changed, 47 insertions(+), 45 deletions(-) diff --git a/examples/machine-code/graph/func_decompileLib.sml b/examples/machine-code/graph/func_decompileLib.sml index 709fd158f0..d36cae4aac 100644 --- a/examples/machine-code/graph/func_decompileLib.sml +++ b/examples/machine-code/graph/func_decompileLib.sml @@ -10,6 +10,8 @@ open writerLib cond_cleanLib; val _ = max_print_depth := ~1; val _ = set_trace "Unicode" 0; +val new_definition = Feedback.trace ("Theory.allow_rebinds", 1) new_definition + local val export_fails = ref ([]:string list) in diff --git a/examples/machine-code/lisp/lisp_proofScript.sml b/examples/machine-code/lisp/lisp_proofScript.sml index a6c5907368..8acf28bcaa 100644 --- a/examples/machine-code/lisp/lisp_proofScript.sml +++ b/examples/machine-code/lisp/lisp_proofScript.sml @@ -35,12 +35,16 @@ val x2sexp_def = tDefine "x2sexp" ` val x2sexp = x2sexp_def |> CONJUNCTS |> map SPEC_ALL |> LIST_CONJ -val term2sexp_def = save_thm("func2sexp_def",save_thm("term2sexp_def",let - val term2sexp_deff = Define `term2sexp x = x2sexp (T,x,FunVar "nil")`; - val func2sexp_deff = Define `func2sexp y = x2sexp (F,Var "nil",y)`; - val th = Q.INST [`xx`|->`Var "nil"`,`yy`|->`FunVar "nil"`] x2sexp - val th = REWRITE_RULE [GSYM term2sexp_deff,GSYM func2sexp_deff] th - in th end)); +val term2sexp_def = save_thm( + "func2sexp_def[allow_rebind]", + save_thm( + "term2sexp_def[allow_rebind]", + let + val term2sexp_deff = Define `term2sexp x = x2sexp (T,x,FunVar "nil")`; + val func2sexp_deff = Define `func2sexp y = x2sexp (F,Var "nil",y)`; + val th = Q.INST [`xx`|->`Var "nil"`,`yy`|->`FunVar "nil"`] x2sexp + val th = REWRITE_RULE [GSYM term2sexp_deff,GSYM func2sexp_deff] th + in th end)); val zip_yz_lemma = prove( ``!xs ys zs x (stack:SExp) alist (l:num). diff --git a/examples/theorem-prover/lisp-runtime/extract/lisp_extractLib.sml b/examples/theorem-prover/lisp-runtime/extract/lisp_extractLib.sml index 9c0bdadb4e..7920ed1117 100644 --- a/examples/theorem-prover/lisp-runtime/extract/lisp_extractLib.sml +++ b/examples/theorem-prover/lisp-runtime/extract/lisp_extractLib.sml @@ -13,6 +13,7 @@ val op \\ = op THEN; val RW = REWRITE_RULE; val RW1 = ONCE_REWRITE_RULE; +fun allowing_rebinds f x = Feedback.trace ("Theory.allow_rebinds", 1) f x (* definitions *) @@ -41,6 +42,7 @@ fun new_def def_tm term_tac = let handle HOL_ERR _ => NONE) in (def,ind) end +val new_def = allowing_rebinds new_def (* ML equivalent of term datatype defined in lisp_semanticsTheory *) @@ -444,6 +446,8 @@ fun pure_extract name term_tac = let val _ = save_thm("R_ev_" ^ good_name,result) in def end; +val pure_extract = fn n => fn tac => allowing_rebinds (pure_extract n) tac + fun pure_extract_mutual_rec names term_tac = let val _ = print "extracting:" val _ = map (fn name => print (" " ^ name)) names @@ -858,6 +862,9 @@ fun impure_extract_aux name term_tac use_short_cut = let val _ = save_thm("R_ev_" ^ good_name,result) in def end; +val impure_extract_aux = + fn n => fn tac => fn b => allowing_rebinds (impure_extract_aux n tac) b + fun impure_extract name term_tac = impure_extract_aux name term_tac false diff --git a/examples/theorem-prover/lisp-runtime/garbage-collector/stop_and_copyScript.sml b/examples/theorem-prover/lisp-runtime/garbage-collector/stop_and_copyScript.sml index 7dd4df2442..263fbd9c51 100644 --- a/examples/theorem-prover/lisp-runtime/garbage-collector/stop_and_copyScript.sml +++ b/examples/theorem-prover/lisp-runtime/garbage-collector/stop_and_copyScript.sml @@ -416,27 +416,25 @@ val rel_gc_def = Define ` (* invariant *) -val (full_heap_rules,full_heap_ind,full_heap_cases) = - Hol_reln - `(!b m. full_heap b b m) /\ - (!b e m n xs d. - (m b = H_BLOCK (xs,n,d)) /\ EMP_RANGE (b+1,b+n+1) m /\ - full_heap (b+n+1) e m ==> full_heap b e m)`; - -val full_heap_ind = IndDefLib.derive_strong_induction(full_heap_rules,full_heap_ind); -val _ = save_thm("full_heap_ind",full_heap_ind); - -val (part_heap_rules,part_heap_ind,part_heap_cases) = - Hol_reln - `(!b m. part_heap b b m 0) /\ - (!b e m k. - ~(isBLOCK (m b)) /\ part_heap (b+1) e m k ==> part_heap b e m k) /\ - (!b e m n xs d k. - (m b = H_BLOCK (xs,n,d)) /\ EMP_RANGE (b+1,b+n+1) m /\ - part_heap (b+n+1) e m k ==> part_heap b e m (k+n+1))`; - -val part_heap_ind = IndDefLib.derive_strong_induction(part_heap_rules,part_heap_ind); -val _ = save_thm("part_heap_ind",part_heap_ind); +Inductive full_heap: + (!b m. full_heap b b m) /\ + (!b e m n xs d. + (m b = H_BLOCK (xs,n,d)) /\ EMP_RANGE (b+1,b+n+1) m /\ + full_heap (b+n+1) e m ==> full_heap b e m) +End + +val full_heap_ind = save_thm("full_heap_ind[allow_rebind]",full_heap_strongind); + +Inductive part_heap: + (!b m. part_heap b b m 0) /\ + (!b e m k. + ~(isBLOCK (m b)) /\ part_heap (b+1) e m k ==> part_heap b e m k) /\ + (!b e m n xs d k. + (m b = H_BLOCK (xs,n,d)) /\ EMP_RANGE (b+1,b+n+1) m /\ + part_heap (b+n+1) e m k ==> part_heap b e m (k+n+1)) +End + +val part_heap_ind = save_thm("part_heap_ind[allow_rebind]",part_heap_strongind); val ref_heap_mem_def = Define ` ref_heap_mem (h,f) m = diff --git a/examples/theorem-prover/lisp-runtime/implementation/lisp_codegenScript.sml b/examples/theorem-prover/lisp-runtime/implementation/lisp_codegenScript.sml index 6c9af4e05f..055eacb67e 100644 --- a/examples/theorem-prover/lisp-runtime/implementation/lisp_codegenScript.sml +++ b/examples/theorem-prover/lisp-runtime/implementation/lisp_codegenScript.sml @@ -374,14 +374,6 @@ val (mc_xbp_load_spec,mc_xbp_load_def) = basic_decompile_strings x64_tools "mc_x val BLAST_LEMMA = prove(``w << 2 !! 1w = w << 2 + 1w:word32``,blastLib.BBLAST_TAC); -val EL_UPDATE_NTH = store_thm("EL_UPDATE_NTH", - ``!xs n k x. EL n (UPDATE_NTH k x xs) = - if (k = n) /\ k < LENGTH xs then x else EL n xs``, - Induct \\ Cases_on `k` \\ SIMP_TAC std_ss [LENGTH,UPDATE_NTH_def] - THEN1 (Cases_on `n` \\ FULL_SIMP_TAC std_ss [EL,HD,TL] \\ FULL_SIMP_TAC std_ss [ADD1]) - \\ Cases_on `n'` \\ FULL_SIMP_TAC std_ss [EL,HD,TL] - \\ FULL_SIMP_TAC std_ss [ADD1]); - val UPDATE_NTH_1 = prove(``UPDATE_NTH 1 x (y1::y2::ys) = y1::x::ys``, EVAL_TAC); val mc_xbp_load_blast = blastLib.BBLAST_PROVE diff --git a/examples/theorem-prover/lisp-runtime/implementation/lisp_opsScript.sml b/examples/theorem-prover/lisp-runtime/implementation/lisp_opsScript.sml index 7b2a1a130f..384d191ecb 100644 --- a/examples/theorem-prover/lisp-runtime/implementation/lisp_opsScript.sml +++ b/examples/theorem-prover/lisp-runtime/implementation/lisp_opsScript.sml @@ -13,6 +13,7 @@ open progTheory set_sepTheory helperLib; open prog_x64Theory prog_x64Lib x64_encodeLib; open stop_and_copyTheory; +fun allowing_rebinds f x = Feedback.trace ("Theory.allow_rebinds", 1) f x infix \\ val op \\ = op THEN; val RW = REWRITE_RULE; @@ -83,7 +84,8 @@ val zLISP_INIT_def = Define ` zCODE_UNCHANGED cu dd d * cond (lisp_init (a1,a2,sl,sl1,e,ex,cs) io (df,f,dg,g,dd,d,sp,sa1,sa_len,ds))`; -val zLISP_raw = Define `zLISP = zLISP_ALT (\wsp wi we ds tw2. T)`; +Definition zLISP_raw: zLISP = zLISP_ALT (\wsp wi we ds tw2. T) +End val zLISP_def = SIMP_CONV std_ss [zLISP_ALT_def,zLISP_raw] ``zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)`` val _ = save_thm("zLISP_def",zLISP_def); @@ -644,9 +646,12 @@ fun X64_LISP_EQ_VAL n i = let val result = prove_spec th imp def pre_tm post_tm in save_lisp_thm("X64_LISP_EQ_VAL_" ^ int_to_string n ^ "_" ^ int_to_string i,result) end; +val X64_LISP_EQ_VAL = fn n => fn i => allowing_rebinds (X64_LISP_EQ_VAL n) i + val _ = map (X64_LISP_EQ_VAL 1) all_regs; val _ = map (X64_LISP_EQ_VAL 2) all_regs; val _ = map (X64_LISP_EQ_VAL 3) all_regs; +(* does 3 0 a second time *) val _ = map (fn n => X64_LISP_EQ_VAL n 0) [3,4,5,6,7,8,9,10,11,12,13,14,15]; (* eq *) @@ -864,7 +869,7 @@ val all_syms = ilist 0 lisp_inv_sym_tests; val _ = map (X64_LISP_SYM 0) all_regs; (* NIL *) val _ = map (X64_LISP_SYM 1) all_regs; (* T *) val _ = map (X64_LISP_SYM 2) all_regs; (* QUOTE *) -val _ = map (fn x => X64_LISP_SYM x 0) all_syms; +val _ = map (fn x => allowing_rebinds (X64_LISP_SYM x) 0) all_syms; (* error *) @@ -3015,8 +3020,8 @@ val X64_LISP_TEST_CF = let (* prove a few theorems which imply that the bytecode does the right thing *) -val X64_POP0 = SPEC_COMPOSE_RULE [X64_LISP_TOP 0,X64_LISP_POP] -val X64_POP1 = SPEC_COMPOSE_RULE [X64_LISP_TOP 1,X64_LISP_POP] +val X64_POP0 = SPEC_COMPOSE_RULE [allowing_rebinds X64_LISP_TOP 0,X64_LISP_POP] +val X64_POP1 = SPEC_COMPOSE_RULE [allowing_rebinds X64_LISP_TOP 1,X64_LISP_POP] val X64_LISP_SWAP1 = let val ((th,_,_),_) = x64_spec (x64_encode "xchg r8,r9") diff --git a/examples/theorem-prover/lisp-runtime/implementation/lisp_symbolsScript.sml b/examples/theorem-prover/lisp-runtime/implementation/lisp_symbolsScript.sml index e8c55b9d61..60c1963688 100644 --- a/examples/theorem-prover/lisp-runtime/implementation/lisp_symbolsScript.sml +++ b/examples/theorem-prover/lisp-runtime/implementation/lisp_symbolsScript.sml @@ -406,12 +406,6 @@ val IO_WRITE_APPEND = store_thm("IO_WRITE_APPEND", ``!io x1 x2. IO_WRITE (IO_WRITE io x1) x2 = IO_WRITE io (x1 ++ x2)``, Cases \\ ASM_SIMP_TAC std_ss [IO_WRITE_def,APPEND_ASSOC,MAP_APPEND]); -val zIO_def = Define ` - zIO (iow:word64,ior:word64,iod:word64,ioi:word64) (io:io_streams) = zR 2w 3w`; - -val zIO_R_def = Define ` - zIO_R (iow,ior,iod) io = SEP_EXISTS ioi. zR 1w ioi * zIO (iow,ior,iod,ioi) io`; - val null_term_str_def = Define ` null_term_str a df f str = ?p. (one_string a (str ++ [CHR 0]) * p) (fun2set (f,df)) /\