From 0222b445505a7a7b8e3c6bb1157913811759e8b9 Mon Sep 17 00:00:00 2001 From: Andreas Lindner Date: Mon, 14 Oct 2024 23:09:40 +0200 Subject: [PATCH] Small fixes and cleanup --- .../tools/symbexec/birs_rulesScript.sml | 74 ++++++++++++++++--- src/tools/symbexec/birs_composeLib.sml | 33 +++------ src/tools/symbexec/birs_execLib.sml | 52 +++++++++++-- src/tools/symbexec/birs_intervalLib.sml | 3 +- src/tools/symbexec/birs_utilsLib.sml | 26 +++++-- 5 files changed, 140 insertions(+), 48 deletions(-) diff --git a/src/theory/tools/symbexec/birs_rulesScript.sml b/src/theory/tools/symbexec/birs_rulesScript.sml index 74af91f24..b0b198f41 100644 --- a/src/theory/tools/symbexec/birs_rulesScript.sml +++ b/src/theory/tools/symbexec/birs_rulesScript.sml @@ -315,6 +315,29 @@ QED (* ******************************************************* *) (* SUBST rule *) (* ******************************************************* *) +Theorem symb_rule_SUBST_thm[local]: + !sr. +!sys L sys2 var symbexp symbexp' Pi. + (symb_symbols_f_sound sr) ==> + (symb_ARB_val_sound sr) ==> + + (symb_hl_step_in_L_sound sr (sys, L, sys2 INSERT Pi)) ==> + ((symb_symbst_store sys2) var = SOME symbexp) ==> + + (symb_simplification sr (symb_symbst_pcond sys2) symbexp symbexp') ==> + + (symb_hl_step_in_L_sound sr (sys, L, (symb_symbst_store_update var symbexp' sys2) INSERT (Pi DELETE sys2))) +Proof +REPEAT STRIP_TAC >> + +`!B.((sys2 INSERT Pi) DIFF {sys2}) UNION {B} = B INSERT (Pi DELETE sys2)` by ( + fs [] >> + METIS_TAC [INSERT_SING_UNION, UNION_COMM, DELETE_DEF] + ) >> + + METIS_TAC [symb_rulesTheory.symb_rule_SUBST_thm] +QED + Theorem symb_rule_SUBST_SING_thm[local]: !sr. !sys L sys2 var symbexp symbexp'. @@ -328,17 +351,23 @@ Theorem symb_rule_SUBST_SING_thm[local]: (symb_hl_step_in_L_sound sr (sys, L, {symb_symbst_store_update var symbexp' sys2})) Proof -REPEAT STRIP_TAC >> + REPEAT STRIP_TAC >> - `({sys2} DIFF {sys2}) UNION {symb_symbst_store_update var symbexp' sys2} = {symb_symbst_store_update var symbexp' sys2}` by ( - METIS_TAC [pred_setTheory.DIFF_EQ_EMPTY, pred_setTheory.UNION_EMPTY] - ) >> + METIS_TAC [symb_rule_SUBST_thm, EMPTY_DELETE] +QED - METIS_TAC [symb_rulesTheory.symb_rule_SUBST_thm] +(* TODO: move to bir_symbScript.sml *) +Theorem birs_symb_to_symbst_IMAGE_DELETE_thm: +!x s. + IMAGE birs_symb_to_symbst s DELETE birs_symb_to_symbst x = + IMAGE birs_symb_to_symbst (s DELETE x) +Proof + simp_tac std_ss [EXTENSION, IN_DELETE, IN_IMAGE] >> + metis_tac [birs_symb_to_symbst_EXISTS_thm, birs_symb_from_symbst_EXISTS_thm, birs_symb_to_from_symbst_thm] QED -Theorem birs_rule_SUBST_spec_thm: - !prog bs L bs2 bs2' lbl envl status pcond vn symbexp symbexp'. +Theorem birs_rule_SUBST_thm: + !prog bs L bs2 bs2' lbl envl status pcond vn symbexp symbexp' Pi. (bs2 = <|bsst_pc := lbl; bsst_environ := birs_gen_env ((vn, symbexp)::envl); @@ -349,19 +378,21 @@ Theorem birs_rule_SUBST_spec_thm: bsst_environ := birs_gen_env ((vn, symbexp')::envl); bsst_status := status; bsst_pcond := pcond|>) ==> - birs_symb_exec prog (bs, L, {bs2}) ==> + birs_symb_exec prog (bs, L, bs2 INSERT Pi) ==> birs_simplification pcond symbexp symbexp' ==> - birs_symb_exec prog (bs, L, {bs2'}) + birs_symb_exec prog (bs, L, bs2' INSERT (Pi DELETE bs2)) Proof - REWRITE_TAC [birs_symb_exec_def] >> + REWRITE_TAC [birs_symb_exec_def, IMAGE_INSERT] >> REPEAT STRIP_TAC >> ASSUME_TAC ( - (Q.SPECL [`birs_symb_to_symbst bs`, `L`, `birs_symb_to_symbst bs2`, `vn`, `symbexp`, `symbexp'`] o + (Q.SPECL [`birs_symb_to_symbst bs`, `L`, `birs_symb_to_symbst bs2`, `vn`, `symbexp`, `symbexp'`, `IMAGE birs_symb_to_symbst Pi`] o SIMP_RULE std_ss [bir_symb_soundTheory.birs_symb_ARB_val_sound_thm] o - MATCH_MP symb_rule_SUBST_SING_thm o + MATCH_MP symb_rule_SUBST_thm o Q.SPEC `prog`) bir_symb_soundTheory.birs_symb_symbols_f_sound_thm) >> + FULL_SIMP_TAC std_ss [birs_symb_to_symbst_IMAGE_DELETE_thm] >> + REV_FULL_SIMP_TAC (std_ss++birs_state_ss) [IMAGE_SING, birs_symb_to_symbst_def, symb_symbst_store_def, symb_symbst_pcond_def, bir_symb_simpTheory.birs_simplification_thm, @@ -369,6 +400,25 @@ Proof combinTheory.UPDATE_APPLY] QED +Theorem birs_rule_SUBST_spec_thm: + !prog bs L bs2 bs2' lbl envl status pcond vn symbexp symbexp'. + (bs2 = + <|bsst_pc := lbl; + bsst_environ := birs_gen_env ((vn, symbexp)::envl); + bsst_status := status; + bsst_pcond := pcond|>) ==> + (bs2' = + <|bsst_pc := lbl; + bsst_environ := birs_gen_env ((vn, symbexp')::envl); + bsst_status := status; + bsst_pcond := pcond|>) ==> + birs_symb_exec prog (bs, L, {bs2}) ==> + birs_simplification pcond symbexp symbexp' ==> + birs_symb_exec prog (bs, L, {bs2'}) +Proof + metis_tac [birs_rule_SUBST_thm, EMPTY_DELETE] +QED + diff --git a/src/tools/symbexec/birs_composeLib.sml b/src/tools/symbexec/birs_composeLib.sml index eb86ee9cd..4f5e6ddf1 100644 --- a/src/tools/symbexec/birs_composeLib.sml +++ b/src/tools/symbexec/birs_composeLib.sml @@ -9,6 +9,10 @@ local open birsSyntax; open birs_auxTheory; + + open aux_setLib; + open birs_utilsLib; + val birs_state_ss = rewrites (type_rws ``:birs_state_t``); (* error handling *) @@ -42,7 +46,7 @@ in (fn (al,g) => (print_term g; ([(al,g)], fn ([t]) => t))) >> (fn x => (print "starting to compute concrete set of free symbols\n"; ALL_TAC x)) >> *) - CONV_TAC (LAND_CONV (aux_setLib.varset_INTER_CONV)) >> + CONV_TAC (LAND_CONV (varset_INTER_CONV)) >> REWRITE_TAC [pred_setTheory.EMPTY_SUBSET] ); @@ -50,22 +54,6 @@ in freesymbols_thm end; - fun tidyup_birs_symb_exec_CONV stateset_conv labelset_conv tm = - let - val _ = if is_birs_symb_exec tm then () else - raise ERR "tidyup_birs_symb_exec_CONV" "cannot handle term"; - - val struct_CONV = - RAND_CONV; - fun Pi_CONV conv = - RAND_CONV (RAND_CONV conv); - fun L_CONV conv = - RAND_CONV (LAND_CONV conv); - in - (struct_CONV (Pi_CONV stateset_conv) THENC - struct_CONV (L_CONV labelset_conv)) tm - end; - (* val step_A_thm = single_step_A_thm; val step_B_thm = single_step_B_thm; @@ -86,14 +74,17 @@ in val _ = print "composed\n"; (* tidy up set operations to not accumulate (in both, post state set and label set) *) - val bprog_L_fixed_thm = CONV_RULE (tidyup_birs_symb_exec_CONV aux_setLib.birs_state_DIFF_UNION_CONV aux_setLib.labelset_UNION_CONV) bprog_composed_thm + val bprog_fixed_thm = CONV_RULE + (birs_Pi_CONV birs_state_DIFF_UNION_CONV THENC + birs_L_CONV labelset_UNION_CONV) + bprog_composed_thm handle e => (print "\n\n"; print_thm bprog_composed_thm; print "tidy up Pi and labelset failed\n"; raise e); - val _ = if symb_sound_struct_is_normform (concl bprog_L_fixed_thm) then () else - (print_term (concl bprog_L_fixed_thm); + val _ = if symb_sound_struct_is_normform (concl bprog_fixed_thm) then () else + (print_term (concl bprog_fixed_thm); raise ERR "birs_rule_SEQ_fun" "something is not right, the produced theorem is not evaluated enough"); in - bprog_L_fixed_thm + bprog_fixed_thm end; diff --git a/src/tools/symbexec/birs_execLib.sml b/src/tools/symbexec/birs_execLib.sml index 6a5a3fe25..979f5f679 100644 --- a/src/tools/symbexec/birs_execLib.sml +++ b/src/tools/symbexec/birs_execLib.sml @@ -255,20 +255,21 @@ fun birs_rule_SUBST_prog_fun bprog_tm = ``, cheat (* TODO: connect this with prep_thm from above *) );*) - val inst_thm = SIMP_RULE std_ss [] ((SPEC bprog_tm o INST_TYPE [Type.alpha |-> prog_type]) birs_rule_SUBST_spec_thm); + val inst_thm1 = SIMP_RULE std_ss [] ((SPEC bprog_tm o INST_TYPE [Type.alpha |-> prog_type]) birs_rule_SUBST_thm); + val inst_thm2 = SIMP_RULE std_ss [] ((SPEC bprog_tm o INST_TYPE [Type.alpha |-> prog_type]) birs_rule_SUBST_spec_thm); (*val _ = (print_term o concl) inst_thm;*) in - inst_thm + (inst_thm1,inst_thm2) end; (* -val single_step_prog_thm = result; +val thm = result; *) -fun birs_rule_SUBST_trysimp_fun birs_rule_SUBST_thm birs_simp_fun single_step_prog_thm = +fun birs_rule_SUBST_trysimp_SING_fun (_,birs_rule_SUBST_thm) birs_simp_fun thm = let val assignment_thm_o = - SOME (MATCH_MP birs_rule_SUBST_thm single_step_prog_thm) + SOME (MATCH_MP birs_rule_SUBST_thm thm) handle _ => NONE; val simp_t_o = Option.mapPartial (fn assignment_thm => @@ -286,9 +287,46 @@ fun birs_rule_SUBST_trysimp_fun birs_rule_SUBST_thm birs_simp_fun single_step_pr in case simp_t_o of SOME (simp_t, assignment_thm) => MATCH_MP assignment_thm simp_t - | NONE => single_step_prog_thm + | NONE => thm end; -val birs_rule_SUBST_trysimp_fun = fn x => Profile.profile "birs_rule_SUBST_trysimp_fun" (birs_rule_SUBST_trysimp_fun x); +val birs_rule_SUBST_trysimp_SING_fun = fn x => Profile.profile "birs_rule_SUBST_trysimp_SING_fun" (birs_rule_SUBST_trysimp_SING_fun x); + +fun birs_rule_SUBST_trysimp_first_fun (birs_rule_SUBST_thm,_) birs_simp_fun thm = + let + val assignment_thm_o = + SOME (MATCH_MP birs_rule_SUBST_thm thm) + handle _ => NONE; + + val simp_t_o = Option.mapPartial (fn assignment_thm => + let + val simp_tm = (fst o dest_imp o (*snd o strip_binder (SOME boolSyntax.universal) o*) concl o Q.SPEC `symbexp'`) assignment_thm; + (*val _ = print_term simp_tm;*) + val timer_exec_step_p3 = holba_miscLib.timer_start 0; + val simp_t = birs_simp_fun simp_tm; + (* TODO: need to remove the following line later and enable the simp function above *) + (*val simp_t_o = NONE;*) + val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n>>>>>> SUBST in " ^ delta_s ^ "\n")) timer_exec_step_p3; + in + SOME (simp_t, assignment_thm) + end) assignment_thm_o; + (* Pi is "bs2' INSERT (Pi DELETE bs2)"*) + val cleanup_Pi_conv = + let + open pred_setLib; + open aux_setLib; + in + RAND_CONV (DELETE_CONV birs_state_EQ_CONV) + end; + val cleanup_RULE = CONV_RULE (birs_utilsLib.birs_Pi_CONV cleanup_Pi_conv); + in + case simp_t_o of + SOME (simp_t, assignment_thm) => cleanup_RULE (MATCH_MP assignment_thm simp_t) + | NONE => thm + end; +val birs_rule_SUBST_trysimp_first_fun = fn x => Profile.profile "birs_rule_SUBST_trysimp_first_fun" (birs_rule_SUBST_trysimp_first_fun x); + +(* TODO: check if there is performance difference between this version and the one that applies the single item case, probably don't need special case... *) +fun birs_rule_SUBST_trysimp_fun x y = birs_utilsLib.birs_Pi_each_RULE (birs_rule_SUBST_trysimp_first_fun x y); end (* local *) diff --git a/src/tools/symbexec/birs_intervalLib.sml b/src/tools/symbexec/birs_intervalLib.sml index feda6ad6c..1d66743c4 100644 --- a/src/tools/symbexec/birs_intervalLib.sml +++ b/src/tools/symbexec/birs_intervalLib.sml @@ -198,7 +198,8 @@ in (* local *) val _ = print_term (hd refsymbs); *) val _ = if length refsymbs = 1 then () else - raise ERR "birs_intervals_Pi_first_unify_RULE::get_ref_symb" "unexpected"; + (print "\n\n"; print_term env_symbol; print_term intervaltm_; print "\n\n"; + raise ERR "birs_intervals_Pi_first_unify_RULE::get_ref_symb" "unexpected"); in hd refsymbs end; diff --git a/src/tools/symbexec/birs_utilsLib.sml b/src/tools/symbexec/birs_utilsLib.sml index f56ad6b98..b7941a2a4 100644 --- a/src/tools/symbexec/birs_utilsLib.sml +++ b/src/tools/symbexec/birs_utilsLib.sml @@ -326,6 +326,8 @@ in (* local *) RAND_CONV; fun sys_CONV conv = LAND_CONV conv; + fun L_CONV conv = + RAND_CONV (LAND_CONV conv); fun Pi_CONV conv = RAND_CONV (RAND_CONV conv); val first_CONV = @@ -335,11 +337,13 @@ in (* local *) local open pred_setSyntax; + open pred_setTheory; val rotate_first_INSERTs_thm = prove(`` !x1 x2 xs. (x1 INSERT x2 INSERT xs) = (x2 INSERT x1 INSERT xs) ``, - cheat + fs [EXTENSION] >> + metis_tac [] ); fun is_two_INSERTs tm = (is_insert tm) andalso ((is_insert o snd o dest_insert) tm); in @@ -351,8 +355,7 @@ in (* local *) val (x2_tm, xs_tm) = dest_insert x2xs_tm; val inst_thm = ISPECL [x1_tm, x2_tm, xs_tm] rotate_first_INSERTs_thm; in - (* TODO: the result of this should actually just be inst_thm *) - REWRITE_CONV [Once inst_thm] tm + inst_thm end; fun rotate_INSERTs_conv tm = @@ -364,8 +367,8 @@ in (* local *) (* apply state transformer to sys *) fun birs_sys_CONV conv tm = let - val _ = if symb_sound_struct_is_normform tm then () else - raise ERR "birs_sys_CONV" "term is not a standard birs_symb_exec"; + val _ = if is_birs_symb_exec tm then () else + raise ERR "birs_sys_CONV" "cannot handle term"; in (struct_CONV (sys_CONV conv)) tm end; @@ -373,12 +376,21 @@ in (* local *) (* apply state transformer to Pi *) fun birs_Pi_CONV conv tm = let - val _ = if symb_sound_struct_is_normform tm then () else - raise ERR "birs_Pi_CONV" "term is not a standard birs_symb_exec"; + val _ = if is_birs_symb_exec tm then () else + raise ERR "birs_Pi_CONV" "cannot handle term"; in (struct_CONV (Pi_CONV conv)) tm end; + (* apply state transformer to L *) + fun birs_L_CONV conv tm = + let + val _ = if is_birs_symb_exec tm then () else + raise ERR "birs_L_CONV" "cannot handle term"; + in + struct_CONV (L_CONV conv) tm + end; + (* apply state transformer to first state in Pi *) fun birs_Pi_first_CONV conv = birs_Pi_CONV (first_CONV conv);