diff --git a/Holmakefile b/Holmakefile index 6d4ccb0ea..2104105c0 100644 --- a/Holmakefile +++ b/Holmakefile @@ -1,6 +1,6 @@ CLINE_OPTIONS = -r -INCLUDES = $(HOLBADIR)/src/aux \ +INCLUDES = $(HOLBADIR)/src/extra \ $(HOLBADIR)/src/shared \ $(HOLBADIR)/src/shared/HolSmt \ $(HOLBADIR)/src/shared/sml-simplejson \ diff --git a/README.md b/README.md index 4a4590533..8591c2960 100644 --- a/README.md +++ b/README.md @@ -72,37 +72,40 @@ cd examples ${HOLBA_HOLMAKE} ``` -## Directories and organization - -``` -├─ doc: Documentation material -├─ examples: Showcasing HolBA -│ ├─ aes: lifting + WP of AES on ARMv8 and for Cortex-M0 -│ ├─ bsl-wp-smt: Small BIR example programs to test simplified BIR generation, WP propagation and SMT interface -│ ├─ nic: NIC formalization -│ ├─ tutorial: End-to-end tutorial of simple ARMv8 examples -├─ scripts: CI and installation scripts -└─ src - ├─ aux: Non-HolBA-specific theories and libraries - ├─ shared: Libraries shared between tools - ├─ theory - │ ├─ abstract-hoare-logic: Abstract Hoare-style logic for unstructured code - │ ├─ bir: Core BIR language - │ ├─ bir-support: Extensions and supporting theories for BIR - │ ├─ models: Additional machine models - │ └─ tools: Theories for the tool libraries in src/tools - └─ tools - ├─ backlifter: Gets ISA-level contracts from BIR contracts - ├─ cfg: Control Flow Graph utilities - ├─ comp: Composition of contracts - ├─ exec: Concrete execution - ├─ lifter: Transpiler from binary to BIR - ├─ pass: Passification utility - ├─ scamv: Abstract side channel model validation framework - └─ wp: Weakest precondition propagation -``` - -### Tools status +## Library organization + +### Directory structure + +- `doc`: Documentation about HolBA and BIR +- `examples`: Applications of HolBA + - `aes`: lifting + WP of an AES block cipher implementation on ARMv8 and Cortex-M0 + - `bsl-wp-smt`: Small BIR example programs to test simplified BIR generation, WP propagation and SMT interface + - `ijr`: Theory and examples related to indirect jumps + - `nic`: Network interface controller formalization + - `riscv`: Examples of specifying and verifying RISC-V programs + - `tutorial`: End-to-end tutorial of simple ARMv8 example programs +- `scripts`: CI and installation scripts +- `src`: Library sources + - `extra`: General theories and libraries + - `shared`: Libraries shared between tools + - `theory`: Domain-specific theories + - `bir`: Core BIR language + - `bir-support`: Extensions and supporting theories for BIR + - `models`: Additional machine models + - `program_logic`: Abstract Hoare-style logic for unstructured code + - `tools`: Theories for the tool libraries in `src/tools` + - `tools`: Domain-specific libraries + - `backlifter`: Utilities for obtaining ISA-level contracts from BIR contracts + - `cfg`: Control flow graph utilities + - `comp`: Composition of contracts + - `compute`: Utilities for using `cv_compute` in HOL4 + - `exec`: Concrete execution + - `lifter`: Translation from binary ISA code to BIR + - `pass`: Passification utility + - `scamv`: Abstract side channel model validation framework + - `wp`: Weakest precondition propagation + +### Tool status - `tools/backlifter`: * Proof-producing diff --git a/examples/aes/wp/aesWpExport.sml b/examples/aes/wp/aesWpExport.sml index 921866a4d..a96635c15 100644 --- a/examples/aes/wp/aesWpExport.sml +++ b/examples/aes/wp/aesWpExport.sml @@ -7,7 +7,7 @@ open bir_typing_progTheory; open bir_envTheory; open bir_exp_substitutionsTheory; open bir_bool_expTheory; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; open bir_valuesTheory; open bir_expTheory; open bir_program_env_orderTheory; diff --git a/examples/ijr/contractTransferScript.sml b/examples/ijr/contractTransferScript.sml index c5d35f285..7f7078d6b 100644 --- a/examples/ijr/contractTransferScript.sml +++ b/examples/ijr/contractTransferScript.sml @@ -4,10 +4,10 @@ open listTheory pred_setTheory pred_setSimps; open bir_programTheory bir_htTheory bir_program_multistep_propsTheory; open HolBACoreSimps; -open bir_wm_instTheory bir_auxiliaryTheory; +open bir_wm_instTheory holba_auxiliaryTheory; open abstract_simp_hoare_logicTheory abstract_hoare_logicTheory; open abstract_hoare_logicSimps bir_program_env_orderTheory bir_env_oldTheory; -open bir_auxiliaryLib; +open holba_auxiliaryLib; open resolutionTheory simulationTheory simulationFailTheory; diff --git a/examples/ijr/resolveFullyScript.sml b/examples/ijr/resolveFullyScript.sml index 6ac582058..869de1e67 100644 --- a/examples/ijr/resolveFullyScript.sml +++ b/examples/ijr/resolveFullyScript.sml @@ -61,7 +61,7 @@ CASE_TAC >- ( FULL_SIMP_TAC (list_ss++bir_TYPES_ss) [fresh_label_def, direct_jump_target_def, bir_get_current_block_def, bir_block_pc_def, bir_get_program_block_info_by_label_def] >> -SIMP_TAC std_ss [Once bir_auxiliaryTheory.INDEX_FIND_INDEX_CHANGE] >> +SIMP_TAC std_ss [Once holba_auxiliaryTheory.INDEX_FIND_INDEX_CHANGE] >> Q.PAT_X_ASSUM ‘∀l'' bl. _’ (MP_TAC o Q.SPECL [‘l'’, ‘bl’]) >> EVERY_CASE_TAC >> FULL_SIMP_TAC std_ss [] >> diff --git a/examples/ijr/resolveScript.sml b/examples/ijr/resolveScript.sml index 3362db2c6..11e334550 100644 --- a/examples/ijr/resolveScript.sml +++ b/examples/ijr/resolveScript.sml @@ -38,7 +38,7 @@ REPEAT GEN_TAC >- ( SIMP_TAC list_ss [] >> ASM_SIMP_TAC arith_ss [INDEX_FIND_def] >> REPEAT STRIP_TAC >> -MP_TAC (Q.SPECL [‘SUC n’, ‘n'’, ‘P’, ‘(xs ++ ys)’, ‘x’] bir_auxiliaryTheory.INDEX_FIND_PRE) >> +MP_TAC (Q.SPECL [‘SUC n’, ‘n'’, ‘P’, ‘(xs ++ ys)’, ‘x’] holba_auxiliaryTheory.INDEX_FIND_PRE) >> ASM_SIMP_TAC std_ss [] QED diff --git a/examples/ijr/simulationFailScript.sml b/examples/ijr/simulationFailScript.sml index ce244f7d9..f36ea6eee 100644 --- a/examples/ijr/simulationFailScript.sml +++ b/examples/ijr/simulationFailScript.sml @@ -3,7 +3,7 @@ open HolKernel Parse boolLib bossLib; open listTheory pred_setSimps; open bir_programTheory bir_expTheory bir_exp_immTheory bir_typing_expTheory; -open bir_valuesTheory bir_auxiliaryTheory +open bir_valuesTheory holba_auxiliaryTheory open bir_program_blocksTheory bir_program_multistep_propsTheory; open HolBACoreSimps; diff --git a/examples/riscv/common/bir_symbLib.sml b/examples/riscv/common/bir_symbLib.sml index 47a0b60ab..b5ce33260 100644 --- a/examples/riscv/common/bir_symbLib.sml +++ b/examples/riscv/common/bir_symbLib.sml @@ -24,15 +24,15 @@ fun bir_symb_analysis bprog_tm birs_state_init_lbl bsst_status := BST_Running; bsst_pcond := ^birs_pcond |>``; - val timer_symbanalysis = bir_miscLib.timer_start 0; - val timer_symbanalysis_last = ref (bir_miscLib.timer_start 0); + val timer_symbanalysis = holba_miscLib.timer_start 0; + val timer_symbanalysis_last = ref (holba_miscLib.timer_start 0); val birs_rule_STEP_thm = birs_rule_STEP_prog_fun (bir_prog_has_no_halt_fun bprog_tm); val birs_rule_SUBST_thm = birs_rule_SUBST_prog_fun bprog_tm; val birs_post_step_fun = (fn t => ( - bir_miscLib.timer_stop (fn delta_s => print ("running since " ^ delta_s ^ "\n")) timer_symbanalysis; - bir_miscLib.timer_stop (fn delta_s => print ("time since last step " ^ delta_s ^ "\n")) (!timer_symbanalysis_last); - timer_symbanalysis_last := bir_miscLib.timer_start 0; + holba_miscLib.timer_stop (fn delta_s => print ("running since " ^ delta_s ^ "\n")) timer_symbanalysis; + holba_miscLib.timer_stop (fn delta_s => print ("time since last step " ^ delta_s ^ "\n")) (!timer_symbanalysis_last); + timer_symbanalysis_last := holba_miscLib.timer_start 0; (*print_term ((last o pairSyntax.strip_pair o snd o dest_comb o concl) t);*) t)) o birs_rule_SUBST_trysimp_fun birs_rule_SUBST_thm o @@ -56,12 +56,12 @@ fun bir_symb_analysis bprog_tm birs_state_init_lbl birs_rule_STEP_SEQ_fun (birs_rule_SUBST_thm, birs_rule_STEP_SEQ_thm)); val _ = print "now reducing it to one sound structure\n"; - val timer = bir_miscLib.timer_start 0; + val timer = holba_miscLib.timer_start 0; val result = exec_until (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec) single_step_A_thm birs_end_lbls handle e => (Profile.print_profile_results (Profile.results ()); raise e); - val _ = bir_miscLib.timer_stop + val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; (* @@ -81,7 +81,7 @@ fun bir_symb_analysis_thm bir_prog_def init_addr_def end_addr_defs bspec_pre_def birenvtyl_def = let val _ = print "\n======\n > bir_symb_analysis_thm started\n"; - val timer = bir_miscLib.timer_start 0; + val timer = holba_miscLib.timer_start 0; val bprog_tm = (fst o dest_eq o concl) bir_prog_def; val init_addr_tm = (snd o dest_eq o concl) init_addr_def; val birs_state_init_lbl_tm = @@ -106,7 +106,7 @@ fun bir_symb_analysis_thm bir_prog_def val symb_analysis_thm = bir_symb_analysis bprog_tm birs_state_init_lbl_tm birs_state_end_tm_lbls birs_env_tm birs_pcond_tm; - val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > bir_symb_analysis_thm took " ^ delta_s ^ "\n")) timer; + val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > bir_symb_analysis_thm took " ^ delta_s ^ "\n")) timer; val symb_analysis_fix_thm = REWRITE_RULE [GSYM birs_env_thm] symb_analysis_thm; in (bsysprecond_thm, symb_analysis_fix_thm) diff --git a/examples/riscv/perftest/simpstress.sml b/examples/riscv/perftest/simpstress.sml index 62c193b54..5d4eab4b6 100644 --- a/examples/riscv/perftest/simpstress.sml +++ b/examples/riscv/perftest/simpstress.sml @@ -7078,12 +7078,12 @@ val bprog_tm = (fst o dest_eq o concl) bir_aespart_prog_def; val birs_rule_STEP_thm = birs_rule_STEP_prog_fun (bir_prog_has_no_halt_fun bprog_tm); val birs_rule_SUBST_thm = birs_rule_SUBST_prog_fun bprog_tm; - val timer_symbanalysis_last = ref (bir_miscLib.timer_start 0); + val timer_symbanalysis_last = ref (holba_miscLib.timer_start 0); val birs_post_step_fun = (fn t => ( - bir_miscLib.timer_stop (fn delta_s => print ("time since last step " ^ delta_s ^ "\n")) (!timer_symbanalysis_last); - timer_symbanalysis_last := bir_miscLib.timer_start 0; + holba_miscLib.timer_stop (fn delta_s => print ("time since last step " ^ delta_s ^ "\n")) (!timer_symbanalysis_last); + timer_symbanalysis_last := holba_miscLib.timer_start 0; (*print_term ((last o pairSyntax.strip_pair o snd o dest_comb o concl) t);*) t)) o birs_rule_SUBST_trysimp_fun birs_rule_SUBST_thm o @@ -7097,7 +7097,7 @@ val bprog_tm = (fst o dest_eq o concl) bir_aespart_prog_def; (* ================================================================================= *) (* - val timer_symbanalysis_last = ref (bir_miscLib.timer_start 0); + val timer_symbanalysis_last = ref (holba_miscLib.timer_start 0); val _ = birs_rule_STEP_fun_spec state2; *) @@ -7120,7 +7120,7 @@ val _ = print "\n"; val _ = Profile.print_profile_results (Profile.results ()); (* -val teststring = bir_fileLib.read_from_file "/home/andreas/data/hol/HolBA_symbexec/examples/riscv/perftest/tempdir/smtquery_2024-08-08_11-38-51_253062_nil"; +val teststring = holba_fileLib.read_from_file "/home/andreas/data/hol/HolBA_symbexec/examples/riscv/perftest/tempdir/smtquery_2024-08-08_11-38-51_253062_nil"; val z3bin = "/home/andreas/data/hol/HolBA_opt/z3-4.8.4/bin/z3"; diff --git a/examples/tutorial/7-composition/mutrec_compositionScript.sml b/examples/tutorial/7-composition/mutrec_compositionScript.sml index 4f57fb838..13b6ffc7b 100644 --- a/examples/tutorial/7-composition/mutrec_compositionScript.sml +++ b/examples/tutorial/7-composition/mutrec_compositionScript.sml @@ -10,7 +10,7 @@ open bir_prog_mutrecTheory; open mutrec_wpTheory; open mutrec_smtTheory; -open bir_auxiliaryLib; +open holba_auxiliaryLib; open HolBACoreSimps; open HolBASimps; diff --git a/examples/tutorial/support2/bir_symb2_execScript.sml b/examples/tutorial/support2/bir_symb2_execScript.sml index 1530f9a3b..c638baab0 100644 --- a/examples/tutorial/support2/bir_symb2_execScript.sml +++ b/examples/tutorial/support2/bir_symb2_execScript.sml @@ -2,7 +2,7 @@ (* app load ["HolKernel", "Parse", "boolLib" ,"bossLib"]; app load ["wordsTheory", "bitstringTheory"]; -app load ["bir_auxiliaryTheory", "bir_immTheory", "bir_valuesTheory"]; +app load ["holba_auxiliaryTheory", "bir_immTheory", "bir_valuesTheory"]; app load ["bir_symb2_envTheory"]; app load ["bir_programTheory", "bir_expTheory", "bir_envTheory"]; app load ["llistTheory", "wordsLib"]; @@ -10,7 +10,7 @@ app load ["llistTheory", "wordsLib"]; open HolKernel Parse boolLib bossLib; open wordsTheory bitstringTheory; -open bir_auxiliaryTheory bir_immTheory bir_valuesTheory; +open holba_auxiliaryTheory bir_immTheory bir_valuesTheory; open bir_envTheory; open bir_expTheory; open bir_programTheory; diff --git a/src/aux/Holmakefile b/src/extra/Holmakefile similarity index 100% rename from src/aux/Holmakefile rename to src/extra/Holmakefile diff --git a/src/aux/bir_auxiliaryLib.sig b/src/extra/holba_auxiliaryLib.sig similarity index 92% rename from src/aux/bir_auxiliaryLib.sig rename to src/extra/holba_auxiliaryLib.sig index c796ea653..83f4b0b4f 100644 --- a/src/aux/bir_auxiliaryLib.sig +++ b/src/extra/holba_auxiliaryLib.sig @@ -1,4 +1,4 @@ -signature bir_auxiliaryLib = +signature holba_auxiliaryLib = sig include Abbrev type simpset = simpLib.simpset diff --git a/src/aux/bir_auxiliaryLib.sml b/src/extra/holba_auxiliaryLib.sml similarity index 95% rename from src/aux/bir_auxiliaryLib.sml rename to src/extra/holba_auxiliaryLib.sml index b25d884ee..4839e59ac 100644 --- a/src/aux/bir_auxiliaryLib.sml +++ b/src/extra/holba_auxiliaryLib.sml @@ -1,4 +1,4 @@ -structure bir_auxiliaryLib :> bir_auxiliaryLib = +structure holba_auxiliaryLib :> holba_auxiliaryLib = struct open HolKernel boolLib liteLib simpLib Parse bossLib; diff --git a/src/aux/bir_auxiliaryScript.sml b/src/extra/holba_auxiliaryScript.sml similarity index 99% rename from src/aux/bir_auxiliaryScript.sml rename to src/extra/holba_auxiliaryScript.sml index 73e2a04dc..5a223c24a 100644 --- a/src/aux/bir_auxiliaryScript.sml +++ b/src/extra/holba_auxiliaryScript.sml @@ -1,11 +1,11 @@ open HolKernel Parse boolLib bossLib; -open bir_auxiliaryLib; +open holba_auxiliaryLib; open wordsTheory bitstringTheory ASCIInumbersTheory; open pred_setTheory; -val _ = new_theory "bir_auxiliary"; +val _ = new_theory "holba_auxiliary"; (* -------------------------------------------------------------------------- *) (* List lemmata *) diff --git a/src/extra/holba_eq_utilLib.sig b/src/extra/holba_eq_utilLib.sig new file mode 100644 index 000000000..4e39165cc --- /dev/null +++ b/src/extra/holba_eq_utilLib.sig @@ -0,0 +1,8 @@ +signature holba_eq_utilLib = +sig + val assoc_with : ('b * 'b -> bool) -> 'b -> ('b * 'a) list -> 'a; + + val rev_assoc_with : ('a * 'a -> bool) -> 'a -> ('b * 'a) list -> 'b; + + val mem_with : ('a * 'a -> bool) -> 'a -> 'a list -> bool; +end diff --git a/src/aux/bir_eq_utilLib.sml b/src/extra/holba_eq_utilLib.sml similarity index 87% rename from src/aux/bir_eq_utilLib.sml rename to src/extra/holba_eq_utilLib.sml index d7314ff81..c4f36eb9c 100644 --- a/src/aux/bir_eq_utilLib.sml +++ b/src/extra/holba_eq_utilLib.sml @@ -1,10 +1,10 @@ -structure bir_eq_utilLib = +structure holba_eq_utilLib :> holba_eq_utilLib = struct local open HolKernel Parse; - val ERR = mk_HOL_ERR "bir_eq_utilLib" + val ERR = mk_HOL_ERR "holba_eq_utilLib" in (* val assoc_with : ('b * 'b -> bool) -> 'b -> ('b * 'a) list -> 'a *) diff --git a/src/shared/bir_smtLib.sml b/src/shared/bir_smtLib.sml index 881a3879a..d59c7116e 100644 --- a/src/shared/bir_smtLib.sml +++ b/src/shared/bir_smtLib.sml @@ -3,8 +3,8 @@ struct local - open bir_fileLib; - open bir_exec_wrapLib; + open holba_fileLib; + open holba_exec_wrapLib; val ERR = Feedback.mk_HOL_ERR "bir_smtLib"; @@ -189,7 +189,7 @@ local open bir_valuesSyntax; open wordsSyntax; - open bir_fileLib; + open holba_fileLib; val ERR = Feedback.mk_HOL_ERR "bir_smtLib"; diff --git a/src/shared/examples/test-json.sml b/src/shared/examples/test-json.sml index 1b5210130..9c582d533 100644 --- a/src/shared/examples/test-json.sml +++ b/src/shared/examples/test-json.sml @@ -9,7 +9,7 @@ val _ = load "sml-simplejson/jsonparse"; *) fun readFile filename = - String.concat (bir_fileLib.read_file_lines filename); + String.concat (holba_fileLib.read_file_lines filename); fun parseJson input = let @@ -264,7 +264,7 @@ val jsonarg = Json.STRING (term_to_string t); val command = "./try_deserialize_serialize_json.py"; val operation = "test"; -val jsonback = bir_json_execLib.call_json_exec (command, ["-v", operation], jsonarg); +val jsonback = holba_json_execLib.call_json_exec (command, ["-v", operation], jsonarg); val stringback = case jsonback of Json.STRING s => s @@ -280,7 +280,7 @@ end val command = "./try_deserialize_serialize_json.py"; val operation = "wrong"; val jsonarg = Json.STRING ""; -val r = (bir_json_execLib.call_json_exec (command, ["-v", operation], jsonarg); true) +val r = (holba_json_execLib.call_json_exec (command, ["-v", operation], jsonarg); true) handle _ => false; val _ = if not r then () else diff --git a/src/shared/examples/test-z3_wrapper.sml b/src/shared/examples/test-z3_wrapper.sml index 1184da594..478ae10cd 100644 --- a/src/shared/examples/test-z3_wrapper.sml +++ b/src/shared/examples/test-z3_wrapper.sml @@ -85,14 +85,14 @@ val _ = List.map (fn (name, query, expected) => (* test of real input, comparison. it is quite rigid in terms of output requirement *) -open bir_fileLib; +open holba_fileLib; val filename = "z3_wrapper_test/z3_wrapper_input_z3_T5bnC5_sat"; val _ = print ("\n\n=============== >>> RUNNING TEST CASE FILE '" ^ filename ^ "'\n"); val expected_output = read_from_file (filename ^ "_expectedoutput"); -val output = bir_exec_wrapLib.get_exec_output ("../z3_wrapper.py " ^ filename); +val output = holba_exec_wrapLib.get_exec_output ("../z3_wrapper.py " ^ filename); val _ = if output = expected_output then () else ( print "=============== >>> TEST CASE FAILED\n"; diff --git a/src/shared/bir_exec_wrapLib.sml b/src/shared/holba_exec_wrapLib.sml similarity index 92% rename from src/shared/bir_exec_wrapLib.sml rename to src/shared/holba_exec_wrapLib.sml index df66d4fe5..e897c2312 100644 --- a/src/shared/bir_exec_wrapLib.sml +++ b/src/shared/holba_exec_wrapLib.sml @@ -1,10 +1,10 @@ -structure bir_exec_wrapLib = +structure holba_exec_wrapLib = struct local - val ERR = Feedback.mk_HOL_ERR "bir_exec_wrapLib" - val wrap_exn = Feedback.wrap_exn "bir_exec_wrapLib" + val ERR = Feedback.mk_HOL_ERR "holba_exec_wrapLib" + val wrap_exn = Feedback.wrap_exn "holba_exec_wrapLib" - open bir_fileLib; + open holba_fileLib; in diff --git a/src/shared/bir_fileLib.sml b/src/shared/holba_fileLib.sml similarity index 95% rename from src/shared/bir_fileLib.sml rename to src/shared/holba_fileLib.sml index 294e41bc1..e1184eb92 100644 --- a/src/shared/bir_fileLib.sml +++ b/src/shared/holba_fileLib.sml @@ -1,10 +1,10 @@ -structure bir_fileLib = +structure holba_fileLib = struct local - val ERR = Feedback.mk_HOL_ERR "bir_fileLib" - val wrap_exn = Feedback.wrap_exn "bir_fileLib" + val ERR = Feedback.mk_HOL_ERR "holba_fileLib" + val wrap_exn = Feedback.wrap_exn "holba_fileLib" - open bir_miscLib; + open holba_miscLib; in diff --git a/src/shared/bir_json_execLib.sml b/src/shared/holba_json_execLib.sml similarity index 94% rename from src/shared/bir_json_execLib.sml rename to src/shared/holba_json_execLib.sml index f6d5557f3..2bc24ff5d 100644 --- a/src/shared/bir_json_execLib.sml +++ b/src/shared/holba_json_execLib.sml @@ -1,8 +1,8 @@ -structure bir_json_execLib = +structure holba_json_execLib = struct local - val ERR = Feedback.mk_HOL_ERR "bir_json_execLib" - val wrap_exn = Feedback.wrap_exn "bir_json_execLib" + val ERR = Feedback.mk_HOL_ERR "holba_json_execLib" + val wrap_exn = Feedback.wrap_exn "holba_json_execLib" (* val cmd = "/usr/bin/echo"; @@ -93,8 +93,8 @@ in end; local - open bir_fileLib; - open bir_exec_wrapLib; + open holba_fileLib; + open holba_exec_wrapLib; fun call_json_exec_old command jsonarg = let diff --git a/src/shared/bir_miscLib.sml b/src/shared/holba_miscLib.sml similarity index 91% rename from src/shared/bir_miscLib.sml rename to src/shared/holba_miscLib.sml index f973e16ed..585f6d8c6 100644 --- a/src/shared/bir_miscLib.sml +++ b/src/shared/holba_miscLib.sml @@ -1,8 +1,8 @@ -structure bir_miscLib = +structure holba_miscLib = struct local - val ERR = Feedback.mk_HOL_ERR "bir_miscLib" - val wrap_exn = Feedback.wrap_exn "bir_miscLib" + val ERR = Feedback.mk_HOL_ERR "holba_miscLib" + val wrap_exn = Feedback.wrap_exn "holba_miscLib" open HolKernel boolLib liteLib simpLib Parse bossLib; diff --git a/src/theory/bir-support/Holmakefile b/src/theory/bir-support/Holmakefile index ae99a0dae..69a22510b 100644 --- a/src/theory/bir-support/Holmakefile +++ b/src/theory/bir-support/Holmakefile @@ -1,4 +1,5 @@ -INCLUDES = $(HOLBADIR)/src/theory/bir +INCLUDES = $(HOLBADIR)/src/extra \ + $(HOLBADIR)/src/theory/bir all: $(DEFAULT_TARGETS) selftest.exe .PHONY: all diff --git a/src/theory/bir-support/bir_bool_expScript.sml b/src/theory/bir-support/bir_bool_expScript.sml index 4db0315df..836cfbcd7 100644 --- a/src/theory/bir-support/bir_bool_expScript.sml +++ b/src/theory/bir-support/bir_bool_expScript.sml @@ -1,12 +1,12 @@ open HolKernel Parse boolLib bossLib; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; open bir_envTheory bir_valuesTheory; open bir_immTheory bir_typing_expTheory; open bir_exp_memTheory bir_expTheory; open bir_exp_immTheory; open HolBACoreSimps -open bir_auxiliaryLib; +open holba_auxiliaryLib; val _ = new_theory "bir_bool_exp"; diff --git a/src/theory/bir-support/bir_exp_equivScript.sml b/src/theory/bir-support/bir_exp_equivScript.sml index d05769200..fa11bbea5 100644 --- a/src/theory/bir-support/bir_exp_equivScript.sml +++ b/src/theory/bir-support/bir_exp_equivScript.sml @@ -1,6 +1,6 @@ open HolKernel Parse boolLib bossLib; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; (* From /core: *) open bir_immTheory bir_expTheory bir_exp_immTheory diff --git a/src/theory/bir-support/bir_extra_expsScript.sml b/src/theory/bir-support/bir_extra_expsScript.sml index ac4b3d606..4f2fe05df 100644 --- a/src/theory/bir-support/bir_extra_expsScript.sml +++ b/src/theory/bir-support/bir_extra_expsScript.sml @@ -1685,7 +1685,7 @@ REPEAT STRIP_TAC >> Cases_on `w2` >> ASM_SIMP_TAC (arith_ss++wordsLib.SIZES_ss) [ word_ror_bv_def, word_lsl_bv_def, - word_lsr_def, w2n_n2w, bir_auxiliaryTheory.word_sub_n2w, + word_lsr_def, w2n_n2w, holba_auxiliaryTheory.word_sub_n2w, WORD_AND_EXP_SUB1] >> `n' MOD 2 ** n <= 2 ** n` by METIS_TAC[ bitTheory.MOD_2EXP_LT, arithmeticTheory.LESS_IMP_LESS_OR_EQ] >> @@ -1711,7 +1711,7 @@ ASM_SIMP_TAC arith_ss [fcpTheory.FCP_BETA, word_lsl_def, word_lsr_def, Cases_on `i + n' MOD 2 ** n < 2 ** n` >> ( ASM_SIMP_TAC arith_ss [] ) >> -ASM_SIMP_TAC arith_ss [bir_auxiliaryTheory.MOD_ADD_EQ_SUB] +ASM_SIMP_TAC arith_ss [holba_auxiliaryTheory.MOD_ADD_EQ_SUB] QED @@ -1800,7 +1800,7 @@ ASM_SIMP_TAC (arith_ss++wordsLib.SIZES_ss) [ REPEAT STRIP_TAC >> Cases_on `i + n < dimindex (:'a)` >> ASM_SIMP_TAC arith_ss [] >> Cases_on `n = dimindex (:'a)` >> ( - ASM_SIMP_TAC arith_ss [bir_auxiliaryTheory.MOD_ADD_EQ_SUB, + ASM_SIMP_TAC arith_ss [holba_auxiliaryTheory.MOD_ADD_EQ_SUB, arithmeticTheory.ADD_MODULUS] ) QED @@ -1893,7 +1893,7 @@ REPEAT STRIP_TAC >> Cases_on `w2` >> ASM_SIMP_TAC (arith_ss++wordsLib.SIZES_ss) [ word_rol_bv_def, word_lsl_bv_def, - word_lsr_def, w2n_n2w, bir_auxiliaryTheory.word_sub_n2w, + word_lsr_def, w2n_n2w, holba_auxiliaryTheory.word_sub_n2w, WORD_AND_EXP_SUB1] >> `n' MOD 2 ** n <= 2 ** n` by METIS_TAC[ bitTheory.MOD_2EXP_LT, arithmeticTheory.LESS_IMP_LESS_OR_EQ] >> @@ -1921,7 +1921,7 @@ Cases_on `n' MOD 2 ** n <= i` >> ( ASM_SIMP_TAC std_ss [arithmeticTheory.ADD_MODULUS] >> ASM_SIMP_TAC arith_ss [] ) >> -ASM_SIMP_TAC arith_ss [bir_auxiliaryTheory.MOD_ADD_EQ_SUB] +ASM_SIMP_TAC arith_ss [holba_auxiliaryTheory.MOD_ADD_EQ_SUB] QED @@ -2014,7 +2014,7 @@ Cases_on `n <= i` >- ( ) >> ASM_SIMP_TAC arith_ss [] >> Cases_on `n = dimindex (:'a)` >> ( - ASM_SIMP_TAC arith_ss [bir_auxiliaryTheory.MOD_ADD_EQ_SUB, + ASM_SIMP_TAC arith_ss [holba_auxiliaryTheory.MOD_ADD_EQ_SUB, arithmeticTheory.ADD_MODULUS] ) QED diff --git a/src/theory/bir-support/bir_interval_expScript.sml b/src/theory/bir-support/bir_interval_expScript.sml index 8584d99f5..a005d2051 100644 --- a/src/theory/bir-support/bir_interval_expScript.sml +++ b/src/theory/bir-support/bir_interval_expScript.sml @@ -1,6 +1,6 @@ open HolKernel Parse boolLib bossLib; open bir_immTheory bir_expTheory -open bir_nzcv_expTheory bir_auxiliaryTheory +open bir_nzcv_expTheory holba_auxiliaryTheory open HolBACoreSimps open bir_expTheory bir_typing_expTheory bir_valuesTheory open wordsTheory diff --git a/src/theory/bir-support/bir_nzcv_expScript.sml b/src/theory/bir-support/bir_nzcv_expScript.sml index b7e378de2..4471bba33 100644 --- a/src/theory/bir-support/bir_nzcv_expScript.sml +++ b/src/theory/bir-support/bir_nzcv_expScript.sml @@ -152,7 +152,7 @@ Theorem nzcv_BIR_ADD_C_CARRY_DEF: !w1 w2. nzcv_BIR_ADD_C w1 w2 = awc_BIR_C w1 w2 F Proof SIMP_TAC arith_ss [nzcv_BIR_ADD_C_def, add_with_carry_def, LET_THM, - bir_auxiliaryTheory.BIT_ADD_WORD_CARRY, w2n_n2w, ZERO_LT_dimword, + holba_auxiliaryTheory.BIT_ADD_WORD_CARRY, w2n_n2w, ZERO_LT_dimword, awc_BIR_C_def] QED diff --git a/src/theory/bir-support/bir_program_blocksScript.sml b/src/theory/bir-support/bir_program_blocksScript.sml index 7c8e65465..aa4173c6b 100644 --- a/src/theory/bir-support/bir_program_blocksScript.sml +++ b/src/theory/bir-support/bir_program_blocksScript.sml @@ -1,5 +1,5 @@ open HolKernel Parse boolLib bossLib; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; open bir_expTheory bir_programTheory HolBACoreSimps open bir_program_valid_stateTheory bir_program_terminationTheory; open bir_program_multistep_propsTheory; diff --git a/src/theory/bir-support/bir_program_labelsScript.sml b/src/theory/bir-support/bir_program_labelsScript.sml index 4c31d0eff..1c21ff037 100644 --- a/src/theory/bir-support/bir_program_labelsScript.sml +++ b/src/theory/bir-support/bir_program_labelsScript.sml @@ -241,7 +241,7 @@ End Theorem INDEX_OF_b2s_STRCAT[local]: !b s. INDEX_OF #"_" (STRCAT (b2s b) (STRING #"_" s)) = SOME (LENGTH (b2s b)) Proof -SIMP_TAC (list_ss++QI_ss) [INDEX_OF_def, bir_auxiliaryTheory.INDEX_FIND_EQ_SOME] >> +SIMP_TAC (list_ss++QI_ss) [INDEX_OF_def, holba_auxiliaryTheory.INDEX_FIND_EQ_SOME] >> SIMP_TAC list_ss [rich_listTheory.EL_APPEND1, rich_listTheory.EL_APPEND2] >> REPEAT STRIP_TAC >> `MEM #"_" (b2s b)` by METIS_TAC[MEM_EL] >> @@ -267,7 +267,7 @@ REPEAT STRIP_TAC >> EQ_TAC >> REPEAT STRIP_TAC >- ( ASM_REWRITE_TAC[listTheory.APPEND_11] >> FULL_SIMP_TAC (std_ss++QI_ss) [INDEX_OF_def, - bir_auxiliaryTheory.INDEX_FIND_EQ_SOME] >> + holba_auxiliaryTheory.INDEX_FIND_EQ_SOME] >> REPEAT BasicProvers.VAR_EQ_TAC >> ASM_SIMP_TAC list_ss [rich_listTheory.DROP_CONS_EL] ) diff --git a/src/theory/bir-support/bir_program_multistep_propsScript.sml b/src/theory/bir-support/bir_program_multistep_propsScript.sml index 72a8b957b..48183fd1d 100644 --- a/src/theory/bir-support/bir_program_multistep_propsScript.sml +++ b/src/theory/bir-support/bir_program_multistep_propsScript.sml @@ -1,16 +1,14 @@ open HolKernel Parse boolLib bossLib; -open bir_auxiliaryLib; +open holba_auxiliaryLib; open wordsTheory bitstringTheory; -open bir_auxiliaryTheory bir_immTheory bir_valuesTheory; +open holba_auxiliaryTheory bir_immTheory bir_valuesTheory; open bir_exp_immTheory bir_exp_memTheory bir_envTheory; open bir_expTheory bir_programTheory; open bir_program_valid_stateTheory; open llistTheory wordsLib pred_setTheory; -open HolBACoreSimps - -open bir_auxiliaryTheory; +open HolBACoreSimps; val _ = new_theory "bir_program_multistep_props"; diff --git a/src/theory/bir-support/bir_program_no_assumeScript.sml b/src/theory/bir-support/bir_program_no_assumeScript.sml index 20a91df6a..54eaaae29 100644 --- a/src/theory/bir-support/bir_program_no_assumeScript.sml +++ b/src/theory/bir-support/bir_program_no_assumeScript.sml @@ -2,7 +2,7 @@ open HolKernel Parse boolLib bossLib; (* bir *) open bir_programTheory; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; open HolBACoreSimps; (* bir-support *) diff --git a/src/theory/bir-support/bir_program_no_observeScript.sml b/src/theory/bir-support/bir_program_no_observeScript.sml index e1983252b..3b510e5ba 100644 --- a/src/theory/bir-support/bir_program_no_observeScript.sml +++ b/src/theory/bir-support/bir_program_no_observeScript.sml @@ -1,5 +1,5 @@ open HolKernel Parse boolLib bossLib; -open bir_auxiliaryTheory +open holba_auxiliaryTheory open bir_programTheory bir_program_valid_stateTheory HolBACoreSimps; open bir_program_blocksTheory bir_program_multistep_propsTheory; diff --git a/src/theory/bir-support/bir_program_terminationScript.sml b/src/theory/bir-support/bir_program_terminationScript.sml index 9a0093937..beb5c0677 100644 --- a/src/theory/bir-support/bir_program_terminationScript.sml +++ b/src/theory/bir-support/bir_program_terminationScript.sml @@ -1,7 +1,7 @@ open HolKernel Parse boolLib bossLib; -open bir_auxiliaryLib; +open holba_auxiliaryLib; open bir_programTheory bir_program_valid_stateTheory HolBACoreSimps; -open bir_program_multistep_propsTheory bir_auxiliaryTheory +open bir_program_multistep_propsTheory holba_auxiliaryTheory open bir_typing_expTheory bir_envTheory open bir_typing_progTheory open bir_valuesTheory bir_immTheory diff --git a/src/theory/bir-support/bir_program_valid_stateScript.sml b/src/theory/bir-support/bir_program_valid_stateScript.sml index b49d5d7ff..93aeeedbe 100644 --- a/src/theory/bir-support/bir_program_valid_stateScript.sml +++ b/src/theory/bir-support/bir_program_valid_stateScript.sml @@ -1,5 +1,5 @@ open HolKernel Parse boolLib bossLib; -open bir_auxiliaryTheory +open holba_auxiliaryTheory open bir_envTheory bir_valuesTheory open bir_programTheory HolBACoreSimps; diff --git a/src/theory/bir-support/bir_subprogramScript.sml b/src/theory/bir-support/bir_subprogramScript.sml index 8b82327fa..6cc2d28bf 100644 --- a/src/theory/bir-support/bir_subprogramScript.sml +++ b/src/theory/bir-support/bir_subprogramScript.sml @@ -1,7 +1,7 @@ open HolKernel Parse boolLib bossLib; open listTheory open bir_programTheory bir_program_valid_stateTheory HolBACoreSimps; -open bir_program_multistep_propsTheory bir_auxiliaryTheory +open bir_program_multistep_propsTheory holba_auxiliaryTheory open bir_valuesTheory bir_immTheory bir_program_valid_stateTheory open bir_program_terminationTheory bir_typing_progTheory open bir_program_multistep_propsTheory; diff --git a/src/theory/bir-support/bir_update_blockScript.sml b/src/theory/bir-support/bir_update_blockScript.sml index 9a73d8cd3..f1df6d833 100644 --- a/src/theory/bir-support/bir_update_blockScript.sml +++ b/src/theory/bir-support/bir_update_blockScript.sml @@ -4,7 +4,7 @@ open stringTheory finite_mapTheory pred_setTheory open bir_envTheory listTheory open bir_programTheory bir_valuesTheory open bir_typing_expTheory -open bir_auxiliaryTheory bir_expTheory +open holba_auxiliaryTheory bir_expTheory open bir_bool_expTheory bir_program_env_orderTheory open bir_temp_varsTheory bir_program_varsTheory open bir_program_terminationTheory diff --git a/src/theory/bir/HolBACoreSimps.sml b/src/theory/bir/HolBACoreSimps.sml index 4d6110785..0a2989f57 100644 --- a/src/theory/bir/HolBACoreSimps.sml +++ b/src/theory/bir/HolBACoreSimps.sml @@ -2,7 +2,7 @@ structure HolBACoreSimps :> HolBACoreSimps = struct open HolKernel boolLib liteLib simpLib Parse bossLib; -open bir_auxiliaryTheory bir_immTheory bir_valuesTheory; +open holba_auxiliaryTheory bir_immTheory bir_valuesTheory; open bir_exp_immTheory bir_exp_memTheory bir_envTheory; open bir_expTheory bir_programTheory bir_typing_progTheory; open bir_typing_expTheory; diff --git a/src/theory/bir/Holmakefile b/src/theory/bir/Holmakefile index f06001dc9..7e8a16700 100644 --- a/src/theory/bir/Holmakefile +++ b/src/theory/bir/Holmakefile @@ -1,4 +1,4 @@ -INCLUDES = $(HOLBADIR)/src/aux +INCLUDES = $(HOLBADIR)/src/extra all: $(DEFAULT_TARGETS) selftest.exe .PHONY: all diff --git a/src/theory/bir/bir_envScript.sml b/src/theory/bir/bir_envScript.sml index 7e9b6889d..8b9d42a88 100644 --- a/src/theory/bir/bir_envScript.sml +++ b/src/theory/bir/bir_envScript.sml @@ -1,7 +1,7 @@ open HolKernel Parse boolLib bossLib; open wordsTheory bitstringTheory; open combinTheory pred_setTheory; -open bir_auxiliaryTheory bir_immTheory bir_valuesTheory; +open holba_auxiliaryTheory bir_immTheory bir_valuesTheory; val _ = new_theory "bir_env"; diff --git a/src/theory/bir/bir_env_oldScript.sml b/src/theory/bir/bir_env_oldScript.sml index efd7603f0..cd98a6c65 100644 --- a/src/theory/bir/bir_env_oldScript.sml +++ b/src/theory/bir/bir_env_oldScript.sml @@ -1,7 +1,7 @@ open HolKernel Parse boolLib bossLib; open wordsTheory bitstringTheory; open combinTheory pred_setTheory; -open bir_auxiliaryTheory bir_immTheory bir_valuesTheory; +open holba_auxiliaryTheory bir_immTheory bir_valuesTheory; open bir_envTheory; diff --git a/src/theory/bir/bir_expScript.sml b/src/theory/bir/bir_expScript.sml index 32787ee5d..bdd45a71c 100644 --- a/src/theory/bir/bir_expScript.sml +++ b/src/theory/bir/bir_expScript.sml @@ -1,6 +1,6 @@ open HolKernel Parse boolLib bossLib; open wordsTheory bitstringTheory; -open bir_auxiliaryTheory bir_immTheory bir_valuesTheory; +open holba_auxiliaryTheory bir_immTheory bir_valuesTheory; open bir_exp_immTheory bir_exp_memTheory bir_envTheory; open finite_mapTheory; diff --git a/src/theory/bir/bir_exp_immScript.sml b/src/theory/bir/bir_exp_immScript.sml index aba9fcc1e..c903e42e4 100644 --- a/src/theory/bir/bir_exp_immScript.sml +++ b/src/theory/bir/bir_exp_immScript.sml @@ -1,6 +1,6 @@ open HolKernel Parse boolLib bossLib; open wordsTheory integer_wordTheory bitstringTheory; -open bir_auxiliaryTheory bir_immTheory bir_immSyntax; +open holba_auxiliaryTheory bir_immTheory bir_immSyntax; val _ = new_theory "bir_exp_imm"; diff --git a/src/theory/bir/bir_exp_memScript.sml b/src/theory/bir/bir_exp_memScript.sml index 130975044..229764006 100644 --- a/src/theory/bir/bir_exp_memScript.sml +++ b/src/theory/bir/bir_exp_memScript.sml @@ -1,6 +1,6 @@ open HolKernel Parse boolLib bossLib; open wordsTheory bitstringTheory; -open bir_auxiliaryTheory bir_immTheory bir_immSyntax; +open holba_auxiliaryTheory bir_immTheory bir_immSyntax; open finite_mapTheory; val _ = new_theory "bir_exp_mem"; diff --git a/src/theory/bir/bir_immScript.sml b/src/theory/bir/bir_immScript.sml index 3d577c63f..ce3ca7bae 100644 --- a/src/theory/bir/bir_immScript.sml +++ b/src/theory/bir/bir_immScript.sml @@ -1,6 +1,6 @@ open HolKernel Parse boolLib bossLib; open wordsTheory bitstringTheory pred_setTheory listTheory; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; val _ = new_theory "bir_imm"; diff --git a/src/theory/bir/bir_immSyntax.sml b/src/theory/bir/bir_immSyntax.sml index 792279590..589acf942 100644 --- a/src/theory/bir/bir_immSyntax.sml +++ b/src/theory/bir/bir_immSyntax.sml @@ -1,7 +1,7 @@ structure bir_immSyntax :> bir_immSyntax = struct -open HolKernel boolLib liteLib simpLib Parse bossLib bir_eq_utilLib; +open HolKernel boolLib liteLib simpLib Parse bossLib holba_eq_utilLib; open bir_immTheory; diff --git a/src/theory/bir/bir_programScript.sml b/src/theory/bir/bir_programScript.sml index 5b164cb23..08f110ead 100644 --- a/src/theory/bir/bir_programScript.sml +++ b/src/theory/bir/bir_programScript.sml @@ -1,6 +1,6 @@ open HolKernel Parse boolLib bossLib; open wordsTheory bitstringTheory; -open bir_auxiliaryTheory bir_immTheory bir_valuesTheory; +open holba_auxiliaryTheory bir_immTheory bir_valuesTheory; open bir_exp_immTheory bir_exp_memTheory bir_envTheory bir_env_oldTheory; open bir_expTheory; open llistTheory wordsLib; diff --git a/src/theory/bir/bir_typing_expScript.sml b/src/theory/bir/bir_typing_expScript.sml index 281738753..b54bb1f82 100644 --- a/src/theory/bir/bir_typing_expScript.sml +++ b/src/theory/bir/bir_typing_expScript.sml @@ -1,12 +1,12 @@ open HolKernel Parse boolLib bossLib; open wordsTheory bitstringTheory; open optionTheory; -open bir_auxiliaryTheory bir_immTheory bir_valuesTheory; +open holba_auxiliaryTheory bir_immTheory bir_valuesTheory; open bir_exp_immTheory bir_exp_memTheory bir_envTheory; open bir_expTheory finite_mapTheory open pred_setTheory; -open wordsLib bir_auxiliaryLib; +open wordsLib holba_auxiliaryLib; val _ = new_theory "bir_typing_exp"; diff --git a/src/theory/bir/bir_typing_progScript.sml b/src/theory/bir/bir_typing_progScript.sml index d9cccb00a..c3efa4bfd 100644 --- a/src/theory/bir/bir_typing_progScript.sml +++ b/src/theory/bir/bir_typing_progScript.sml @@ -1,6 +1,6 @@ open HolKernel Parse boolLib bossLib; open wordsTheory bitstringTheory; -open bir_auxiliaryTheory bir_immTheory bir_valuesTheory; +open holba_auxiliaryTheory bir_immTheory bir_valuesTheory; open bir_exp_immTheory bir_exp_memTheory bir_envTheory; open bir_expTheory bir_typing_expTheory bir_programTheory; open wordsLib pred_setTheory; diff --git a/src/theory/bir/bir_valuesScript.sml b/src/theory/bir/bir_valuesScript.sml index bb15ea870..8ade72576 100644 --- a/src/theory/bir/bir_valuesScript.sml +++ b/src/theory/bir/bir_valuesScript.sml @@ -1,7 +1,7 @@ open HolKernel Parse boolLib bossLib; open wordsTheory bitstringTheory listTheory pred_setTheory; open finite_mapTheory; -open bir_auxiliaryTheory bir_immTheory; +open holba_auxiliaryTheory bir_immTheory; val _ = new_theory "bir_values"; diff --git a/src/theory/bir/selftest.sml b/src/theory/bir/selftest.sml index 4216c21d0..e7e862a78 100644 --- a/src/theory/bir/selftest.sml +++ b/src/theory/bir/selftest.sml @@ -1,8 +1,7 @@ -open HolKernel Parse boolTheory boolLib pairTheory +open HolKernel Parse boolTheory boolLib pairTheory; -open HolKernel Parse boolLib bossLib; open wordsTheory bitstringTheory HolBACoreSimps; -open bir_auxiliaryTheory bir_immTheory bir_valuesTheory; +open holba_auxiliaryTheory bir_immTheory bir_valuesTheory; open bir_exp_immTheory bir_exp_memTheory bir_envTheory; open bir_expTheory bir_programTheory; open bir_typing_expTheory bir_typing_progTheory; diff --git a/src/theory/program_logic/Holmakefile b/src/theory/program_logic/Holmakefile index 81b544f00..cf9889f2c 100644 --- a/src/theory/program_logic/Holmakefile +++ b/src/theory/program_logic/Holmakefile @@ -1,4 +1,4 @@ -INCLUDES = $(HOLBADIR)/src/aux \ +INCLUDES = $(HOLBADIR)/src/extra \ $(HOLBADIR)/src/theory/bir all: $(DEFAULT_TARGETS) diff --git a/src/theory/program_logic/partial_program_logicScript.sml b/src/theory/program_logic/partial_program_logicScript.sml index f6f0bdefd..c65ea98b3 100644 --- a/src/theory/program_logic/partial_program_logicScript.sml +++ b/src/theory/program_logic/partial_program_logicScript.sml @@ -1,8 +1,8 @@ open HolKernel boolLib bossLib BasicProvers dep_rewrite prim_recTheory; -open bir_auxiliaryLib; +open holba_auxiliaryLib; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; open transition_systemTheory total_program_logicTheory; diff --git a/src/theory/program_logic/total_ext_program_logicScript.sml b/src/theory/program_logic/total_ext_program_logicScript.sml index e95c534ba..00bfe3673 100644 --- a/src/theory/program_logic/total_ext_program_logicScript.sml +++ b/src/theory/program_logic/total_ext_program_logicScript.sml @@ -1,8 +1,8 @@ open HolKernel Parse boolLib bossLib; open total_program_logicTheory; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; -open bir_auxiliaryLib; +open holba_auxiliaryLib; val _ = new_theory "total_ext_program_logic"; @@ -305,10 +305,10 @@ rpt strip_tac >> fs [t_ext_jgmt_def] >> strip_tac >- ( subgoal `il2 INTER el2 = {}` >- ( - irule bir_auxiliaryTheory.INTER_SUBSET_EMPTY_thm >> + irule INTER_SUBSET_EMPTY_thm >> Q.EXISTS_TAC `el1 UNION el2` >> fs [Once pred_setTheory.INTER_COMM] >> - irule bir_auxiliaryTheory.INTER_SUBSET_EMPTY_thm >> + irule INTER_SUBSET_EMPTY_thm >> Q.EXISTS_TAC `il1 UNION il2` >> fs [] ) >> diff --git a/src/theory/program_logic/total_program_logicScript.sml b/src/theory/program_logic/total_program_logicScript.sml index 9298d08f3..3310d9be4 100644 --- a/src/theory/program_logic/total_program_logicScript.sml +++ b/src/theory/program_logic/total_program_logicScript.sml @@ -1,8 +1,8 @@ open HolKernel Parse boolLib bossLib; -open bir_auxiliaryLib; +open holba_auxiliaryLib; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; open transition_systemTheory; diff --git a/src/theory/program_logic/transition_systemScript.sml b/src/theory/program_logic/transition_systemScript.sml index b50b5d16c..7166273bc 100644 --- a/src/theory/program_logic/transition_systemScript.sml +++ b/src/theory/program_logic/transition_systemScript.sml @@ -1,8 +1,8 @@ open HolKernel boolLib bossLib BasicProvers dep_rewrite; -open bir_auxiliaryLib; +open holba_auxiliaryLib; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; val _ = new_theory "transition_system"; diff --git a/src/theory/tools/backlifter/Holmakefile b/src/theory/tools/backlifter/Holmakefile index f8ae81b81..4d6823c10 100644 --- a/src/theory/tools/backlifter/Holmakefile +++ b/src/theory/tools/backlifter/Holmakefile @@ -1,4 +1,5 @@ -INCLUDES = $(HOLBADIR)/src/theory/bir \ +INCLUDES = $(HOLBADIR)/src/extra \ + $(HOLBADIR)/src/theory/bir \ $(HOLBADIR)/src/theory/bir-support \ $(HOLBADIR)/src/theory/program_logic \ $(HOLBADIR)/src/theory/models/l3mod \ diff --git a/src/theory/tools/backlifter/bir_arm8_backlifterScript.sml b/src/theory/tools/backlifter/bir_arm8_backlifterScript.sml index 48eecf940..f20b8a31b 100644 --- a/src/theory/tools/backlifter/bir_arm8_backlifterScript.sml +++ b/src/theory/tools/backlifter/bir_arm8_backlifterScript.sml @@ -4,7 +4,7 @@ open bir_immTheory; open bir_programTheory; open bir_tsTheory; open bir_program_multistep_propsTheory; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; (* From lifter: *) open bir_inst_liftingTheory; @@ -20,7 +20,7 @@ open HolBASimps; open HolBACoreSimps; open program_logicSimps; -open bir_auxiliaryLib; +open holba_auxiliaryLib; open m0_mod_stepLib; diff --git a/src/theory/tools/backlifter/bir_common_backlifterScript.sml b/src/theory/tools/backlifter/bir_common_backlifterScript.sml index 1d71eee19..86200174a 100644 --- a/src/theory/tools/backlifter/bir_common_backlifterScript.sml +++ b/src/theory/tools/backlifter/bir_common_backlifterScript.sml @@ -4,7 +4,7 @@ open bir_immTheory; open bir_programTheory; open bir_tsTheory; open bir_program_multistep_propsTheory; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; (* From lifter: *) open bir_inst_liftingTheory; @@ -18,7 +18,7 @@ open HolBASimps; open HolBACoreSimps; open program_logicSimps; -open bir_auxiliaryLib; +open holba_auxiliaryLib; open m0_mod_stepLib; diff --git a/src/theory/tools/backlifter/bir_riscv_backlifterScript.sml b/src/theory/tools/backlifter/bir_riscv_backlifterScript.sml index c0eda9580..a566ec229 100644 --- a/src/theory/tools/backlifter/bir_riscv_backlifterScript.sml +++ b/src/theory/tools/backlifter/bir_riscv_backlifterScript.sml @@ -4,7 +4,7 @@ open bir_immTheory; open bir_programTheory; open bir_tsTheory; open bir_program_multistep_propsTheory; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; (* From lifter: *) open bir_inst_liftingTheory; @@ -18,7 +18,7 @@ open HolBASimps; open HolBACoreSimps; open program_logicSimps; -open bir_auxiliaryLib; +open holba_auxiliaryLib; open m0_mod_stepLib; diff --git a/src/theory/tools/comp/Holmakefile b/src/theory/tools/comp/Holmakefile index a7fdb6cbe..4fc03496f 100644 --- a/src/theory/tools/comp/Holmakefile +++ b/src/theory/tools/comp/Holmakefile @@ -1,4 +1,5 @@ -INCLUDES = $(HOLBADIR)/src/theory/bir \ +INCLUDES = $(HOLBADIR)/src/extra \ + $(HOLBADIR)/src/theory/bir \ $(HOLBADIR)/src/theory/bir-support \ $(HOLBADIR)/src/theory/program_logic \ $(HOLBADIR)/src/theory/tools/wp diff --git a/src/theory/tools/comp/bir_tsScript.sml b/src/theory/tools/comp/bir_tsScript.sml index a51d2f2db..b61b57bc8 100644 --- a/src/theory/tools/comp/bir_tsScript.sml +++ b/src/theory/tools/comp/bir_tsScript.sml @@ -1,9 +1,9 @@ open HolKernel Parse boolLib bossLib; -open bir_auxiliaryLib; +open holba_auxiliaryLib; open bir_programTheory; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; open bir_program_multistep_propsTheory; open bir_program_blocksTheory; open bir_program_terminationTheory; diff --git a/src/theory/tools/lifter/Holmakefile b/src/theory/tools/lifter/Holmakefile index e26ec207b..0e856ccd6 100644 --- a/src/theory/tools/lifter/Holmakefile +++ b/src/theory/tools/lifter/Holmakefile @@ -5,6 +5,7 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \ $(HOLDIR)/examples/l3-machine-code/m0/step \ $(HOLDIR)/examples/l3-machine-code/riscv/model \ $(HOLDIR)/examples/l3-machine-code/riscv/step \ + $(HOLBADIR)/src/extra \ $(HOLBADIR)/src/theory/bir \ $(HOLBADIR)/src/theory/bir-support \ $(HOLBADIR)/src/theory/models/l3mod diff --git a/src/theory/tools/lifter/bir_arm8_extrasScript.sml b/src/theory/tools/lifter/bir_arm8_extrasScript.sml index 32c1bb4b1..dedc3ed50 100644 --- a/src/theory/tools/lifter/bir_arm8_extrasScript.sml +++ b/src/theory/tools/lifter/bir_arm8_extrasScript.sml @@ -361,7 +361,7 @@ REPEAT STRIP_TAC >> ASM_SIMP_TAC (list_ss++wordsLib.SIZES_ss++boolSimps.CONJ_ss) [word_shift_extract_def, word_or_def, fcpTheory.FCP_BETA, word_lsl_def, word_lsr_def, w2w] >> ASM_SIMP_TAC (list_ss++boolSimps.EQUIV_EXTRACT_ss) [rich_listTheory.LENGTH_BUTLASTN, - bir_auxiliaryTheory.testbit_el_iff, length_w2v, rich_listTheory.BUTLASTN_def, + holba_auxiliaryTheory.testbit_el_iff, length_w2v, rich_listTheory.BUTLASTN_def, listTheory.EL_REVERSE, GSYM arithmeticTheory.ADD1, rich_listTheory.LASTN_REVERSE, rich_listTheory.EL_TAKE] >> STRIP_TAC >> diff --git a/src/theory/tools/lifter/bir_exp_liftingScript.sml b/src/theory/tools/lifter/bir_exp_liftingScript.sml index 4e66ff268..d0424edb2 100644 --- a/src/theory/tools/lifter/bir_exp_liftingScript.sml +++ b/src/theory/tools/lifter/bir_exp_liftingScript.sml @@ -1,4 +1,5 @@ open HolKernel Parse boolLib bossLib; + open bir_expTheory HolBACoreSimps; open bir_typing_expTheory bir_valuesTheory open bir_envTheory bir_immTheory bir_exp_immTheory @@ -10,7 +11,7 @@ open bir_lifter_general_auxTheory open bir_extra_expsTheory open finite_mapTheory; open pred_setTheory; -open bir_auxiliaryLib; +open holba_auxiliaryLib; val _ = new_theory "bir_exp_lifting"; @@ -616,7 +617,7 @@ Theorem bir_is_lifted_imm_exp_LCAST0[local]: ^thm_t Proof SIMP_TAC (std_ss++holBACore_ss++wordsLib.WORD_ss) [bir_is_lifted_imm_exp_def, - bir_env_oldTheory.bir_env_vars_are_initialised_UNION, bir_auxiliaryTheory.sw2sw_w2w_downcast, + bir_env_oldTheory.bir_env_vars_are_initialised_UNION, holba_auxiliaryTheory.sw2sw_w2w_downcast, w2w_id] QED @@ -790,7 +791,7 @@ SIMP_TAC (std_ss++holBACore_ss++wordsLib.WORD_ss) [bir_is_lifted_imm_exp_def, ASM_SIMP_TAC std_ss [bir_load_from_mem_def, GSYM bitstringTheory.w2v_v2w, bitstringTheory.v2w_n2v, bir_load_bitstring_from_mmap_def, - w2bs_def, b2n_n2bs, n2w_w2n, bir_auxiliaryTheory.w2n_MOD_2EXP_ID] >> + w2bs_def, b2n_n2bs, n2w_w2n, holba_auxiliaryTheory.w2n_MOD_2EXP_ID] >> ASM_SIMP_TAC arith_ss [w2n_n2w, bir_mem_addr_def, GSYM wordsTheory.MOD_2EXP_DIMINDEX, wordsTheory.ZERO_LT_dimword, bir_load_mmap_MOD_dimword_thm, n2w_mod, bir_load_w2n_mf2mm_load_n2w_thm] QED diff --git a/src/theory/tools/lifter/bir_inst_liftingScript.sml b/src/theory/tools/lifter/bir_inst_liftingScript.sml index 9317d132b..e13a9e4d3 100644 --- a/src/theory/tools/lifter/bir_inst_liftingScript.sml +++ b/src/theory/tools/lifter/bir_inst_liftingScript.sml @@ -4,7 +4,7 @@ open bir_expTheory HolBACoreSimps; open bir_typing_expTheory bir_valuesTheory open bir_envTheory bir_immTheory bir_exp_immTheory open bir_immSyntax bir_programTheory wordsTheory -open bir_auxiliaryTheory +open holba_auxiliaryTheory open bir_exp_memTheory bir_bool_expTheory open bir_program_env_orderTheory open bir_program_blocksTheory diff --git a/src/theory/tools/lifter/bir_m0_extrasScript.sml b/src/theory/tools/lifter/bir_m0_extrasScript.sml index 5477f7699..27d9174da 100644 --- a/src/theory/tools/lifter/bir_m0_extrasScript.sml +++ b/src/theory/tools/lifter/bir_m0_extrasScript.sml @@ -219,7 +219,7 @@ Theorem m0_mem_store_half_BE_32: m0_mem_store_half_BE a (w2w w) mmap Proof SIMP_TAC (std_ss++wordsLib.SIZES_ss) [m0_mem_store_half_BE_def, - wordsTheory.word_bits_w2w, bir_auxiliaryTheory.word_extract_bits_w2w, + wordsTheory.word_bits_w2w, holba_auxiliaryTheory.word_extract_bits_w2w, w2w_REMOVE_FOLDS] QED @@ -231,7 +231,7 @@ Theorem m0_mem_store_half_LE_32: m0_mem_store_half_LE a (w2w w) mmap Proof SIMP_TAC (std_ss++wordsLib.SIZES_ss) [m0_mem_store_half_LE_def, - wordsTheory.word_bits_w2w, bir_auxiliaryTheory.word_extract_bits_w2w, + wordsTheory.word_bits_w2w, holba_auxiliaryTheory.word_extract_bits_w2w, w2w_REMOVE_FOLDS] QED @@ -474,7 +474,7 @@ ONCE_REWRITE_TAC [fcpTheory.CART_EQ] >> FULL_SIMP_TAC (arith_ss++boolSimps.EQUIV_EXTRACT_ss++wordsLib.SIZES_ss) [ word_and_def, fcpTheory.FCP_BETA, dimindex_lt_dimword, word_concat_def, w2w, - word_join_index, word_0, bir_auxiliaryTheory.word_extract_bits_w2w, + word_join_index, word_0, holba_auxiliaryTheory.word_extract_bits_w2w, word_bits_def, word_1comp_def, word_index] >> REPEAT STRIP_TAC >> `BIT i 1 = (0 = i)` by ( diff --git a/src/theory/tools/lifter/bir_nzcv_introsScript.sml b/src/theory/tools/lifter/bir_nzcv_introsScript.sml index d31895172..bfb3d0f75 100644 --- a/src/theory/tools/lifter/bir_nzcv_introsScript.sml +++ b/src/theory/tools/lifter/bir_nzcv_introsScript.sml @@ -650,7 +650,7 @@ Theorem lsrs_C_fold_M0: Proof Cases >> rename1 `n1 < dimword _` >> FULL_SIMP_TAC (arith_ss++wordsLib.SIZES_ss) [w2n_n2w, n2w_11, - word_ls_n2w, bir_auxiliaryTheory.word_sub_n2w] + word_ls_n2w, holba_auxiliaryTheory.word_sub_n2w] QED @@ -665,7 +665,7 @@ Theorem asrs_C_fold_M0: Proof Cases >> rename1 `n1 < dimword _` >> FULL_SIMP_TAC (arith_ss++wordsLib.SIZES_ss) [w2n_n2w, n2w_11, - word_ls_n2w, bir_auxiliaryTheory.word_sub_n2w, arithmeticTheory.MIN_DEF, + word_ls_n2w, holba_auxiliaryTheory.word_sub_n2w, arithmeticTheory.MIN_DEF, word_msb_def] >> REPEAT STRIP_TAC >> Cases_on `n1 <= 32` >> ASM_SIMP_TAC arith_ss [] @@ -681,7 +681,7 @@ Theorem lsls_C_fold_M0: Proof Cases >> rename1 `n1 < dimword _` >> FULL_SIMP_TAC (arith_ss++wordsLib.SIZES_ss) [w2n_n2w, n2w_11, - word_ls_n2w, bir_auxiliaryTheory.word_sub_n2w] >> + word_ls_n2w, holba_auxiliaryTheory.word_sub_n2w] >> Cases_on `n1 = 0` >> ASM_SIMP_TAC arith_ss [] >> ASM_SIMP_TAC (arith_ss++wordsLib.SIZES_ss) [word_lsl_def, diff --git a/src/theory/tools/symbexec/Holmakefile b/src/theory/tools/symbexec/Holmakefile index f22a29bd2..5042d416e 100644 --- a/src/theory/tools/symbexec/Holmakefile +++ b/src/theory/tools/symbexec/Holmakefile @@ -1,4 +1,4 @@ -INCLUDES = $(HOLBADIR)/src/aux \ +INCLUDES = $(HOLBADIR)/src/extra \ $(HOLBADIR)/src/theory/bir \ $(HOLBADIR)/src/theory/bir-support \ $(HOLBADIR)/src/theory/program_logic \ diff --git a/src/theory/tools/symbexec/symb_auxScript.sml b/src/theory/tools/symbexec/symb_auxScript.sml index 2898eabce..c614df71a 100644 --- a/src/theory/tools/symbexec/symb_auxScript.sml +++ b/src/theory/tools/symbexec/symb_auxScript.sml @@ -23,10 +23,10 @@ Theorem FUNPOW_OPT_SOME_thm: Proof GEN_TAC >> GEN_TAC >> STRIP_TAC >> Induct_on `n` >- ( - REWRITE_TAC [bir_auxiliaryTheory.FUNPOW_OPT_def, FUNPOW] + REWRITE_TAC [holba_auxiliaryTheory.FUNPOW_OPT_def, FUNPOW] ) >> - REWRITE_TAC [bir_auxiliaryTheory.FUNPOW_OPT_def, FUNPOW] >> - ASM_SIMP_TAC std_ss [GSYM bir_auxiliaryTheory.FUNPOW_OPT_def] + REWRITE_TAC [holba_auxiliaryTheory.FUNPOW_OPT_def, FUNPOW] >> + ASM_SIMP_TAC std_ss [GSYM holba_auxiliaryTheory.FUNPOW_OPT_def] QED val _ = export_theory(); diff --git a/src/theory/tools/symbexec/symb_rulesScript.sml b/src/theory/tools/symbexec/symb_rulesScript.sml index 9673bb5d7..d80d85703 100644 --- a/src/theory/tools/symbexec/symb_rulesScript.sml +++ b/src/theory/tools/symbexec/symb_rulesScript.sml @@ -142,7 +142,7 @@ Theorem symb_SEQ_interpr_dom_INTER_thm: ((symb_interpr_dom H1) INTER ((symb_interpr_dom H3) DIFF (symb_interpr_dom H2)) = EMPTY) Proof METIS_TAC [symb_minimal_interpretation_EQ_dom_thm, - symb_symbols_set_SUBSET_thm, bir_auxiliaryTheory.INTER_SUBSET_EMPTY_thm, SUBSET_of_DIFF_thm] + symb_symbols_set_SUBSET_thm, holba_auxiliaryTheory.INTER_SUBSET_EMPTY_thm, SUBSET_of_DIFF_thm] QED (* TODO: split this into two *) diff --git a/src/theory/tools/wp/bir_htScript.sml b/src/theory/tools/wp/bir_htScript.sml index 531368210..4ccb68cce 100644 --- a/src/theory/tools/wp/bir_htScript.sml +++ b/src/theory/tools/wp/bir_htScript.sml @@ -2,7 +2,7 @@ open HolKernel Parse boolLib bossLib; (* Theories from theory/bir: *) open bir_programTheory bir_typing_progTheory bir_envTheory - bir_auxiliaryTheory bir_valuesTheory bir_expTheory + holba_auxiliaryTheory bir_valuesTheory bir_expTheory bir_exp_immTheory bir_typing_expTheory bir_immTheory; (* Theories from theory/bir-support: *) diff --git a/src/theory/tools/wp/bir_wpScript.sml b/src/theory/tools/wp/bir_wpScript.sml index 31096f74c..cdd6f0bd8 100644 --- a/src/theory/tools/wp/bir_wpScript.sml +++ b/src/theory/tools/wp/bir_wpScript.sml @@ -2,7 +2,7 @@ open HolKernel Parse boolLib bossLib; (* Theories from theory/bir: *) open bir_programTheory bir_typing_progTheory bir_envTheory - bir_auxiliaryTheory bir_valuesTheory bir_expTheory + holba_auxiliaryTheory bir_valuesTheory bir_expTheory bir_exp_immTheory bir_typing_expTheory bir_immTheory; open bir_env_oldTheory; diff --git a/src/tools/cfg/bir_cfgLib.sml b/src/tools/cfg/bir_cfgLib.sml index 32dbd4b5c..43fee9743 100644 --- a/src/tools/cfg/bir_cfgLib.sml +++ b/src/tools/cfg/bir_cfgLib.sml @@ -215,7 +215,7 @@ in local - open bir_auxiliaryLib; + open holba_auxiliaryLib; open bir_immSyntax; open wordsSyntax; diff --git a/src/tools/cfg/bir_cfg_vizLib.sml b/src/tools/cfg/bir_cfg_vizLib.sml index 2ad43ffd2..8278fa3b4 100644 --- a/src/tools/cfg/bir_cfg_vizLib.sml +++ b/src/tools/cfg/bir_cfg_vizLib.sml @@ -10,7 +10,7 @@ open bir_programSyntax; open bir_cfgLib; - open bir_fileLib; + open holba_fileLib; open graphVizLib; (* error handling *) diff --git a/src/tools/comp/bir_compositionLib.sml b/src/tools/comp/bir_compositionLib.sml index db0730e9e..5af7a6c23 100644 --- a/src/tools/comp/bir_compositionLib.sml +++ b/src/tools/comp/bir_compositionLib.sml @@ -25,7 +25,7 @@ open bir_inst_liftingHelpersLib; open bslSyntax; open bir_wp_interfaceLib; - open bir_auxiliaryLib; + open holba_auxiliaryLib; open HolBACoreSimps; in @@ -744,7 +744,7 @@ open bir_inst_liftingHelpersLib; val spec_noteq_trans_impl1 = ISPECL [el 1 (get_labels_from_set_repr include_ending_label_set1), el 1 (get_labels_from_set_repr include_ending_label_set2)] - bir_auxiliaryTheory.noteq_trans_impl + holba_auxiliaryTheory.noteq_trans_impl val include_inter_lbls = (get_labels_from_set_repr include_ending_label_set1)@ (get_labels_from_set_repr include_ending_label_set2) val cases_on_x_lbls_tac = List.foldr (fn (lbl, st) => Cases_on `x = ^lbl` >> st) ALL_TAC include_inter_lbls diff --git a/src/tools/exec/bir_execLib.sml b/src/tools/exec/bir_execLib.sml index 03ce62d31..99579b760 100644 --- a/src/tools/exec/bir_execLib.sml +++ b/src/tools/exec/bir_execLib.sml @@ -3,7 +3,7 @@ struct open HolKernel boolLib liteLib simpLib Parse bossLib; - open bir_auxiliaryTheory; + open holba_auxiliaryTheory; open bir_program_multistep_propsTheory; open bir_programSyntax; open bir_envSyntax; diff --git a/src/tools/lifter/Holmakefile b/src/tools/lifter/Holmakefile index 96a0665a8..244f7e89c 100644 --- a/src/tools/lifter/Holmakefile +++ b/src/tools/lifter/Holmakefile @@ -5,7 +5,7 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \ $(HOLDIR)/examples/l3-machine-code/m0/step \ $(HOLDIR)/examples/l3-machine-code/riscv/model \ $(HOLDIR)/examples/l3-machine-code/riscv/step \ - $(HOLBADIR)/src/aux \ + $(HOLBADIR)/src/extra \ $(HOLBADIR)/src/theory/bir \ $(HOLBADIR)/src/theory/bir-support \ $(HOLBADIR)/src/theory/models/l3mod \ diff --git a/src/tools/lifter/bir_exp_liftingLib.sml b/src/tools/lifter/bir_exp_liftingLib.sml index 919ac55d2..77c67279c 100644 --- a/src/tools/lifter/bir_exp_liftingLib.sml +++ b/src/tools/lifter/bir_exp_liftingLib.sml @@ -441,7 +441,7 @@ fun bir_exp_lift_final thm = let fun gen_newname uvs c = let val v = mk_var ("e"^(int_to_string c), bir_expSyntax.bir_exp_t_ty) - in if (bir_eq_utilLib.mem_with (fn (a,b) => identical a b) v uvs) then gen_newname uvs (c + 1) else (v::uvs, c, v) end; + in if (holba_eq_utilLib.mem_with (fn (a,b) => identical a b) v uvs) then gen_newname uvs (c + 1) else (v::uvs, c, v) end; val (s, _, _) = foldl (fn (gv, (s, uvs, c)) => let val (uvs', c', v) = gen_newname uvs c diff --git a/src/tools/lifter/bir_inst_liftingLib.sml b/src/tools/lifter/bir_inst_liftingLib.sml index 834edd562..256dd6a20 100644 --- a/src/tools/lifter/bir_inst_liftingLib.sml +++ b/src/tools/lifter/bir_inst_liftingLib.sml @@ -347,7 +347,7 @@ fun get_patched_step_hex ms_v hex_code = val lifted_thms_raw = let val res = get_patched_step_hex ms_v hex_code val _ = assert (not o List.null) res - val _ = assert (List.all (fn thm => not (bir_eq_utilLib.mem_with (fn (a,b) => identical a b) F (hyp thm)))) res + val _ = assert (List.all (fn thm => not (holba_eq_utilLib.mem_with (fn (a,b) => identical a b) F (hyp thm)))) res in res end handle HOL_ERR _ => raise (bir_inst_liftingExn (hex_code, BILED_msg "bmr_step_hex failed")); @@ -369,11 +369,11 @@ fun get_patched_step_hex ms_v hex_code = val thm2 = foldl (uncurry DISCH) thm1 (List.filter disch_hyp_check (hyp thm1)) val thm3 = REWRITE_RULE [pc_thm, wordsTheory.word_add_n2w, wordsTheory.word_and_n2w, - wordsTheory.word_or_n2w, bir_auxiliaryTheory.word_sub_n2w, + wordsTheory.word_or_n2w, holba_auxiliaryTheory.word_sub_n2w, addressTheory.word_arith_lemma1, addressTheory.word_arith_lemma3, addressTheory.word_arith_lemma4, - addr_sz_dimword_THM, bir_auxiliaryTheory.align_n2w] thm2 handle UNCHANGED => thm2 + addr_sz_dimword_THM, holba_auxiliaryTheory.align_n2w] thm2 handle UNCHANGED => thm2 in thm3 end diff --git a/src/tools/lifter/bir_lifting_machinesLib_instances.sml b/src/tools/lifter/bir_lifting_machinesLib_instances.sml index a58e9e207..bfbea4e15 100644 --- a/src/tools/lifter/bir_lifting_machinesLib_instances.sml +++ b/src/tools/lifter/bir_lifting_machinesLib_instances.sml @@ -331,9 +331,9 @@ fun m0_step_hex' (endian_fl, sel_fl) = let val simp_conv = (SIMP_CONV (arith_ss++bitstringLib.v2w_n2w_ss++wordsLib.SIZES_ss) ((if endian_fl then m0_extra_FOLDS_BE else m0_extra_FOLDS_LE)::[nzcv_FOLDS_M0, - EQ_13w_EVAL, EQ_15w_EVAL, R_name_EVAL, bir_auxiliaryTheory.w2w_n2w, - m0_extra_FOLDS_GEN, Mode_Handler_INTRO, bir_auxiliaryTheory.align_aligned_add, - bir_auxiliaryTheory.align_aligned_sub, LowestSetBit_n2w, numeral_bitTheory.LOWEST_SET_BIT, + EQ_13w_EVAL, EQ_15w_EVAL, R_name_EVAL, holba_auxiliaryTheory.w2w_n2w, + m0_extra_FOLDS_GEN, Mode_Handler_INTRO, holba_auxiliaryTheory.align_aligned_add, + holba_auxiliaryTheory.align_aligned_sub, LowestSetBit_n2w, numeral_bitTheory.LOWEST_SET_BIT, alignmentTheory.aligned_numeric, alignmentTheory.align_aligned, wordsTheory.word_bit_n2w])); val compset_2 = reduceLib.num_compset (); @@ -500,9 +500,9 @@ fun m0_mod_step_hex' (endian_fl, sel_fl) = let val simp_conv = (SIMP_CONV (arith_ss++bitstringLib.v2w_n2w_ss++wordsLib.SIZES_ss) ((if endian_fl then m0_extra_FOLDS_BE else m0_extra_FOLDS_LE)::[nzcv_FOLDS_M0, - EQ_13w_EVAL, EQ_15w_EVAL, R_name_EVAL, bir_auxiliaryTheory.w2w_n2w, - m0_extra_FOLDS_GEN, Mode_Handler_INTRO, bir_auxiliaryTheory.align_aligned_add, - bir_auxiliaryTheory.align_aligned_sub, LowestSetBit_n2w, numeral_bitTheory.LOWEST_SET_BIT, + EQ_13w_EVAL, EQ_15w_EVAL, R_name_EVAL, holba_auxiliaryTheory.w2w_n2w, + m0_extra_FOLDS_GEN, Mode_Handler_INTRO, holba_auxiliaryTheory.align_aligned_add, + holba_auxiliaryTheory.align_aligned_sub, LowestSetBit_n2w, numeral_bitTheory.LOWEST_SET_BIT, alignmentTheory.aligned_numeric, alignmentTheory.align_aligned, wordsTheory.word_bit_n2w])); val compset_2 = reduceLib.num_compset (); diff --git a/src/tools/lifter/gcc_supportLib.sml b/src/tools/lifter/gcc_supportLib.sml index 17ca71fae..c656644a7 100644 --- a/src/tools/lifter/gcc_supportLib.sml +++ b/src/tools/lifter/gcc_supportLib.sml @@ -7,8 +7,8 @@ struct open bir_inst_liftingLibTypes; - open bir_auxiliaryLib; - open bir_fileLib; + open holba_auxiliaryLib; + open holba_fileLib; val ERR = mk_HOL_ERR "gcc_supportLib" diff --git a/src/tools/scamv/persistence/embexp_logsLib.sml b/src/tools/scamv/persistence/embexp_logsLib.sml index 9df3a94b9..b9d713422 100644 --- a/src/tools/scamv/persistence/embexp_logsLib.sml +++ b/src/tools/scamv/persistence/embexp_logsLib.sml @@ -4,7 +4,7 @@ local val ERR = Feedback.mk_HOL_ERR "embexp_logsLib" val wrap_exn = Feedback.wrap_exn "embexp_logsLib" - open bir_json_execLib; + open holba_json_execLib; open Json; in @@ -23,7 +23,7 @@ val embexp_logs_dir = val command = embexp_logs_dir ^ "/scripts/db-interface.py"; fun run_db_gen extra ops arg = - bir_json_execLib.call_json_exec (command, (if !is_testing then ["-t"] else [])@extra@[ops], arg); + holba_json_execLib.call_json_exec (command, (if !is_testing then ["-t"] else [])@extra@[ops], arg); fun run_db ops arg = run_db_gen [] ops arg; fun run_db_ro ops arg = run_db_gen ["-ro"] ops arg; diff --git a/src/tools/scamv/persistence/experimentsLib.sml b/src/tools/scamv/persistence/experimentsLib.sml index 915d9f6d2..6971d8edf 100644 --- a/src/tools/scamv/persistence/experimentsLib.sml +++ b/src/tools/scamv/persistence/experimentsLib.sml @@ -3,7 +3,7 @@ struct local open HolKernel Parse boolLib bossLib; - open bir_miscLib; + open holba_miscLib; (* error handling *) val libname = "experimentsLib" diff --git a/src/tools/scamv/persistence/persistenceLib.sml b/src/tools/scamv/persistence/persistenceLib.sml index 288aa42d8..bb08cb524 100644 --- a/src/tools/scamv/persistence/persistenceLib.sml +++ b/src/tools/scamv/persistence/persistenceLib.sml @@ -4,7 +4,7 @@ struct open HolKernel Parse boolLib bossLib; open bir_randLib; - open bir_miscLib; + open holba_miscLib; open holba_entryLib; @@ -54,7 +54,7 @@ struct (* prepare metadata for run *) (* write out git commit and git diff of current directory. *) (* so this code needs to be executed with the working directory in the holbarepo! *) - open bir_exec_wrapLib; + open holba_exec_wrapLib; val run_datestr = get_datestring(); val holba_diff = get_exec_output "git diff"; val holba_commit = get_exec_output "git rev-parse HEAD"; diff --git a/src/tools/scamv/persistence/t-test-logs.sml b/src/tools/scamv/persistence/t-test-logs.sml index 264a111c5..448ac1f61 100644 --- a/src/tools/scamv/persistence/t-test-logs.sml +++ b/src/tools/scamv/persistence/t-test-logs.sml @@ -71,7 +71,7 @@ fun fromJsonStr s = val command = embexp_logs_dir ^ "/scripts/db-interface.py"; fun run_db ops arg = - bir_json_execLib.call_json_exec (command, ["-t", ops], arg); + holba_json_execLib.call_json_exec (command, ["-t", ops], arg); val run_db_q = run_db "query"; fun run_db_q_table t = run_db_q ( diff --git a/src/tools/scamv/proggen/bir_gccLib.sml b/src/tools/scamv/proggen/bir_gccLib.sml index 6aca25f3e..c6825e16f 100644 --- a/src/tools/scamv/proggen/bir_gccLib.sml +++ b/src/tools/scamv/proggen/bir_gccLib.sml @@ -2,7 +2,7 @@ structure bir_gccLib :> bir_gccLib = struct local - open bir_fileLib; + open holba_fileLib; val libname = "bir_gccLib" val ERR = Feedback.mk_HOL_ERR libname diff --git a/src/tools/scamv/proggen/bir_prog_genLib.sml b/src/tools/scamv/proggen/bir_prog_genLib.sml index 65c5c6d1c..7d301efa5 100644 --- a/src/tools/scamv/proggen/bir_prog_genLib.sml +++ b/src/tools/scamv/proggen/bir_prog_genLib.sml @@ -20,7 +20,7 @@ struct open asm_genLib; open armv8_prefetch_genLib; - open bir_fileLib; + open holba_fileLib; open bir_randLib; (* error handling *) diff --git a/src/tools/scamv/proggen/bir_prog_gen_randLib.sml b/src/tools/scamv/proggen/bir_prog_gen_randLib.sml index 375267cdc..157f8654a 100644 --- a/src/tools/scamv/proggen/bir_prog_gen_randLib.sml +++ b/src/tools/scamv/proggen/bir_prog_gen_randLib.sml @@ -5,7 +5,7 @@ struct open arm8_progLib arm8AssemblerLib arm8; open bir_randLib; - open bir_miscLib; + open holba_miscLib; open regExLib; (* error handling *) diff --git a/src/tools/scamv/proggen/bir_prog_gen_sliceLib.sml b/src/tools/scamv/proggen/bir_prog_gen_sliceLib.sml index d59a4c1de..38de182e2 100644 --- a/src/tools/scamv/proggen/bir_prog_gen_sliceLib.sml +++ b/src/tools/scamv/proggen/bir_prog_gen_sliceLib.sml @@ -10,7 +10,7 @@ open arm8_progLib arm8AssemblerLib arm8; val wrap_exn = Feedback.wrap_exn libname open bir_randLib; -open bir_miscLib; +open holba_miscLib; fun remChars (c,s) = let fun rem [] = [] diff --git a/src/tools/scamv/symbexec/bir_angrLib.sml b/src/tools/scamv/symbexec/bir_angrLib.sml index 3f6517f24..335440d4e 100644 --- a/src/tools/scamv/symbexec/bir_angrLib.sml +++ b/src/tools/scamv/symbexec/bir_angrLib.sml @@ -34,7 +34,7 @@ val bir_program = ``BirProgram maxdepth, precondition, pd, envupdate_o *) fun symb_exec_program maxdepth precondition program pd envupdate_o = - let open bir_fileLib bir_exec_wrapLib; + let open holba_fileLib holba_exec_wrapLib; val bir_program_filename = get_tempfile "program" ".bir"; val _ = write_to_file bir_program_filename (term_to_string program); val python_script_filename = fence_insertion_repo_path ^ "/symbolic_execution.py"; diff --git a/src/tools/scamv/symbexec/bir_symb_execScript.sml b/src/tools/scamv/symbexec/bir_symb_execScript.sml index 3207bcff1..575a146fb 100644 --- a/src/tools/scamv/symbexec/bir_symb_execScript.sml +++ b/src/tools/scamv/symbexec/bir_symb_execScript.sml @@ -2,7 +2,7 @@ (* app load ["HolKernel", "Parse", "boolLib" ,"bossLib"]; app load ["wordsTheory", "bitstringTheory"]; -app load ["bir_auxiliaryTheory", "bir_immTheory", "bir_valuesTheory"]; +app load ["holba_auxiliaryTheory", "bir_immTheory", "bir_valuesTheory"]; app load ["bir_symb_envTheory"]; app load ["bir_programTheory", "bir_expTheory", "bir_envTheory"]; app load ["llistTheory", "wordsLib"]; @@ -10,7 +10,7 @@ app load ["llistTheory", "wordsLib"]; open HolKernel Parse boolLib bossLib; open wordsTheory bitstringTheory; -open bir_auxiliaryTheory bir_immTheory bir_valuesTheory; +open holba_auxiliaryTheory bir_immTheory bir_valuesTheory; open bir_envTheory; open bir_expTheory; open bir_programTheory; diff --git a/src/tools/symbexec/Holmakefile b/src/tools/symbexec/Holmakefile index 2b6244ecb..3e82dfdfb 100644 --- a/src/tools/symbexec/Holmakefile +++ b/src/tools/symbexec/Holmakefile @@ -1,4 +1,4 @@ -INCLUDES = $(HOLBADIR)/src/aux \ +INCLUDES = $(HOLBADIR)/src/extra \ $(HOLBADIR)/src/theory/bir \ $(HOLBADIR)/src/theory/bir-support \ $(HOLBADIR)/src/theory/program_logic \ diff --git a/src/tools/symbexec/birs_auxLib.sml b/src/tools/symbexec/birs_auxLib.sml index b98195ba3..fb29c8874 100644 --- a/src/tools/symbexec/birs_auxLib.sml +++ b/src/tools/symbexec/birs_auxLib.sml @@ -8,7 +8,7 @@ open HolKernel Parse boolLib bossLib; open birs_auxTheory; (* error handling *) - val libname = "bir_auxLib" + val libname = "birs_auxLib" val ERR = Feedback.mk_HOL_ERR libname val wrap_exn = Feedback.wrap_exn libname @@ -108,7 +108,7 @@ end (* local *) local open HolKernel Parse boolLib bossLib; - open bir_auxiliaryTheory; + open holba_auxiliaryTheory; open bir_programTheory; in diff --git a/src/tools/symbexec/birs_driveLib.sml b/src/tools/symbexec/birs_driveLib.sml index ef6778493..e39e88cc2 100644 --- a/src/tools/symbexec/birs_driveLib.sml +++ b/src/tools/symbexec/birs_driveLib.sml @@ -63,13 +63,13 @@ fun birs_rule_STEP_SEQ_fun_ (SUBST_thm, STEP_SEQ_thm) symbex_A_thm = val step2_thm = REWRITE_RULE [bir_symbTheory.birs_state_t_accessors, bir_symbTheory.birs_state_t_accfupds, combinTheory.K_THM] step1_thm; (* - val timer_exec_step_p3 = bir_miscLib.timer_start 0; + val timer_exec_step_p3 = holba_miscLib.timer_start 0; *) val step3_thm = CONV_RULE birs_exec_step_CONV_fun step2_thm; (* - val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n>>>>>> STEP_SEQ in " ^ delta_s ^ "\n")) timer_exec_step_p3; + val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n>>>>>> STEP_SEQ in " ^ delta_s ^ "\n")) timer_exec_step_p3; *) val step4_thm = (* (birs_rule_SUBST_trysimp_fun SUBST_thm o birs_rule_tryjustassert_fun true) *) step3_thm; in @@ -130,11 +130,11 @@ fun build_tree (STEP_fun_spec, SEQ_fun_spec, STEP_SEQ_fun_spec) symbex_A_thm sto (* val birs_state_mid = hd birs_states_mid; - val timer_exec_step_P1 = bir_miscLib.timer_start 0; + val timer_exec_step_P1 = holba_miscLib.timer_start 0; val single_step_B_thm = take_step birs_state_mid; - val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n>>> executed a whole step in " ^ delta_s ^ "\n")) timer_exec_step_P1; + val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n>>> executed a whole step in " ^ delta_s ^ "\n")) timer_exec_step_P1; *) - val timer_exec_step_P2 = bir_miscLib.timer_start 0; + val timer_exec_step_P2 = holba_miscLib.timer_start 0; (* (* TODO: derive freesymbols EMPTY from birs *) val (sys_B_tm, _, Pi_B_tm) = (symb_sound_struct_get_sysLPi_fun o concl) single_step_B_thm; @@ -148,7 +148,7 @@ fun build_tree (STEP_fun_spec, SEQ_fun_spec, STEP_SEQ_fun_spec) symbex_A_thm sto val bprog_composed_thm = SEQ_fun_spec symbex_A_thm single_step_B_thm (SOME freesymbols_B_thm); *) val bprog_composed_thm = STEP_SEQ_fun_spec symbex_A_thm; - val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n>>> FINISH took and sequentially composed a step in " ^ delta_s ^ "\n")) timer_exec_step_P2; + val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n>>> FINISH took and sequentially composed a step in " ^ delta_s ^ "\n")) timer_exec_step_P2; in build_tree (STEP_fun_spec, SEQ_fun_spec, STEP_SEQ_fun_spec) bprog_composed_thm stop_lbls diff --git a/src/tools/symbexec/birs_stepLib.sml b/src/tools/symbexec/birs_stepLib.sml index 7759aa457..438ec1b68 100644 --- a/src/tools/symbexec/birs_stepLib.sml +++ b/src/tools/symbexec/birs_stepLib.sml @@ -425,9 +425,9 @@ fun get_birs_state_size t = fun measure_fun s f v = let - val timer = bir_miscLib.timer_start 0; + val timer = holba_miscLib.timer_start 0; val res = f v; - val _ = bir_miscLib.timer_stop (fn delta_s => print (s ^ delta_s ^ "\n")) timer; + val _ = holba_miscLib.timer_stop (fn delta_s => print (s ^ delta_s ^ "\n")) timer; in res end; @@ -1113,10 +1113,10 @@ fun birs_exec_step_CONV_fun tm = (fn tm_i => let - val timer_exec_step = bir_miscLib.timer_start 0; + val timer_exec_step = holba_miscLib.timer_start 0; (* TODO: optimize *) val birs_exec_thm = birs_exec_step_CONV tm_i; - val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n>>>>>> executed step in " ^ delta_s ^ "\n")) timer_exec_step; + val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n>>>>>> executed step in " ^ delta_s ^ "\n")) timer_exec_step; in birs_exec_thm end) THENC @@ -1175,7 +1175,7 @@ fun birs_rule_STEP_fun_ birs_rule_STEP_thm bstate_tm = val birs_exec_thm = CONV_RULE (birs_exec_step_CONV_fun) (SPEC bstate_tm birs_rule_STEP_thm); - val timer_exec_step_p3 = bir_miscLib.timer_start 0; + val timer_exec_step_p3 = holba_miscLib.timer_start 0; (* TODO: optimize *) val single_step_prog_thm = REWRITE_RULE @@ -1183,7 +1183,7 @@ fun birs_rule_STEP_fun_ birs_rule_STEP_thm bstate_tm = bir_symbTheory.birs_state_t_accfupds, combinTheory.K_THM] birs_exec_thm; - val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n>>>>>> STEP in " ^ delta_s ^ "\n")) timer_exec_step_p3; + val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n>>>>>> STEP in " ^ delta_s ^ "\n")) timer_exec_step_p3; val _ = if symb_sound_struct_is_normform (concl single_step_prog_thm) then () else (print_term (concl single_step_prog_thm); @@ -1272,7 +1272,7 @@ fun birs_rule_tryjustassert_fun_ force_assert_justify single_step_prog_thm = case continue_thm_o_2 of SOME continue_thm => let - val timer_exec_step_p3 = bir_miscLib.timer_start 0; + val timer_exec_step_p3 = holba_miscLib.timer_start 0; val pcond_tm = (snd o dest_comb o snd o dest_comb o fst o dest_comb o concl) continue_thm; (*val _ = print_term pcond_tm;*) val pcond_is_contr = bir_check_unsat false pcond_tm; @@ -1286,7 +1286,7 @@ fun birs_rule_tryjustassert_fun_ force_assert_justify single_step_prog_thm = SOME (mk_oracle_thm "BIRS_CONTR_Z3" ([], mk_comb (birs_pcondinf_tm, pcond_tm))) else NONE; - val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n>>>>>> tryassert in " ^ delta_s ^ "\n")) timer_exec_step_p3; + val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n>>>>>> tryassert in " ^ delta_s ^ "\n")) timer_exec_step_p3; in (* val SOME pcond_thm = pcond_thm_o; *) case pcond_thm_o of @@ -1310,7 +1310,7 @@ fun birs_rule_tryprune_fun_ prune_thm single_step_prog_thm = case continue_thm_o_2 of SOME continue_thm => let - val timer_exec_step_p3 = bir_miscLib.timer_start 0; + val timer_exec_step_p3 = holba_miscLib.timer_start 0; val pcond_tm = (snd o dest_comb o snd o dest_comb o fst o dest_comb o concl) continue_thm; (* val _ = print_term pcond_tm; *) val pcond_is_contr = bir_check_unsat false pcond_tm; @@ -1320,7 +1320,7 @@ fun birs_rule_tryprune_fun_ prune_thm single_step_prog_thm = SOME (mk_oracle_thm "BIRS_CONTR_Z3" ([], mk_comb (birs_pcondinf_tm, pcond_tm))) else NONE; - val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n>>>>>> tryprune2 in " ^ delta_s ^ "\n")) timer_exec_step_p3; + val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n>>>>>> tryprune2 in " ^ delta_s ^ "\n")) timer_exec_step_p3; in case pcond_thm_o of SOME pcond_thm => @@ -1395,11 +1395,11 @@ fun birs_rule_SUBST_trysimp_fun_ birs_rule_SUBST_thm single_step_prog_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 timer_exec_step_p3 = bir_miscLib.timer_start 0; + val timer_exec_step_p3 = holba_miscLib.timer_start 0; val simp_t = birs_simpLib.birs_simp_repeat simp_tm; (* TODO: need to remove the following line later and enable the simp function above *) (*val simp_t_o = NONE;*) - val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n>>>>>> SUBST in " ^ delta_s ^ "\n")) timer_exec_step_p3; + 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; diff --git a/src/tools/symbexec/examples/analysis/bir_program_transf_exampleScript.sml b/src/tools/symbexec/examples/analysis/bir_program_transf_exampleScript.sml index 38242c527..fb38a728c 100644 --- a/src/tools/symbexec/examples/analysis/bir_program_transf_exampleScript.sml +++ b/src/tools/symbexec/examples/analysis/bir_program_transf_exampleScript.sml @@ -116,7 +116,7 @@ Proof `!A B. A INTER {B} = (EMPTY:bir_programcounter_t -> bool) <=> B NOTIN A` by ( REPEAT STRIP_TAC >> EQ_TAC >> ( - FULL_SIMP_TAC std_ss [bir_auxiliaryTheory.SING_DISJOINT_SING_NOT_IN_thm] + FULL_SIMP_TAC std_ss [holba_auxiliaryTheory.SING_DISJOINT_SING_NOT_IN_thm] ) >> REPEAT STRIP_TAC >> diff --git a/src/tools/symbexec/examples/analysis/exampleScript.sml b/src/tools/symbexec/examples/analysis/exampleScript.sml index 98e9eef15..916156098 100644 --- a/src/tools/symbexec/examples/analysis/exampleScript.sml +++ b/src/tools/symbexec/examples/analysis/exampleScript.sml @@ -86,9 +86,9 @@ val _ = print "done building the tree\n"; val _ = print "now reducing it to one sound structure\n"; -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; val result = exec_until (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec) single_step_A_thm birs_stop_lbls; -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; val _ = (print_term o concl) result; diff --git a/src/tools/symbexec/examples/analysis/motorfuncScript.sml b/src/tools/symbexec/examples/analysis/motorfuncScript.sml index dc4c9a9af..a0114de14 100644 --- a/src/tools/symbexec/examples/analysis/motorfuncScript.sml +++ b/src/tools/symbexec/examples/analysis/motorfuncScript.sml @@ -91,9 +91,9 @@ val _ = print "done building the tree\n"; val _ = print "now reducing it to one sound structure\n"; -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; val result = exec_until (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec) single_step_A_thm birs_stop_lbls; -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; val _ = (print_term o concl) result; diff --git a/src/tools/symbexec/examples/analysis/motorfunc_transfScript.sml b/src/tools/symbexec/examples/analysis/motorfunc_transfScript.sml index dda9b3c85..aeca2f61a 100644 --- a/src/tools/symbexec/examples/analysis/motorfunc_transfScript.sml +++ b/src/tools/symbexec/examples/analysis/motorfunc_transfScript.sml @@ -1,4 +1,3 @@ - open HolKernel Parse boolLib bossLib; open bir_symbTheory; @@ -26,13 +25,8 @@ open birs_auxTheory; open bir_program_transfTheory; val birs_state_ss = rewrites (type_rws ``:birs_state_t``); - - - val _ = new_theory "motorfunc_transf"; - - val bprog_def = motorfuncTheory.bprog_def; val bprog = (fst o dest_eq o concl) bprog_def; val bprog_tm = (fst o dest_eq o concl) bprog_def; @@ -616,7 +610,7 @@ Proof `!A B. A INTER {B} = (EMPTY:bir_programcounter_t -> bool) <=> B NOTIN A` by ( REPEAT STRIP_TAC >> EQ_TAC >> ( - FULL_SIMP_TAC std_ss [bir_auxiliaryTheory.SING_DISJOINT_SING_NOT_IN_thm] + FULL_SIMP_TAC std_ss [holba_auxiliaryTheory.SING_DISJOINT_SING_NOT_IN_thm] ) >> REPEAT STRIP_TAC >> diff --git a/src/tools/symbexec/examples/analysis/runningexampleScript.sml b/src/tools/symbexec/examples/analysis/runningexampleScript.sml index bb12c26d0..d3321df7a 100644 --- a/src/tools/symbexec/examples/analysis/runningexampleScript.sml +++ b/src/tools/symbexec/examples/analysis/runningexampleScript.sml @@ -91,9 +91,9 @@ val _ = print "done building the tree\n"; val _ = print "now reducing it to one sound structure\n"; -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; val result = exec_until (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec) single_step_A_thm birs_stop_lbls; -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; val _ = (print_term o concl) result; diff --git a/src/tools/symbexec/examples/analysis_modexp/modexpScript.sml b/src/tools/symbexec/examples/analysis_modexp/modexpScript.sml index ddc1e42ae..fa6e0faad 100644 --- a/src/tools/symbexec/examples/analysis_modexp/modexpScript.sml +++ b/src/tools/symbexec/examples/analysis_modexp/modexpScript.sml @@ -253,9 +253,9 @@ val result = birs_execute bprog_tm_ loop_skip_to_l10_state birs_stop_lbls_; (* compose everything, work with the tree structure (and the code in the function buildtree) *) (* -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; val _ = (print_term o concl) result; val _ = show_tags := true; diff --git a/src/tools/symbexec/examples/analysis_modexp/uidivmodScript.sml b/src/tools/symbexec/examples/analysis_modexp/uidivmodScript.sml index 1cf6f9d2d..d54e28eb0 100644 --- a/src/tools/symbexec/examples/analysis_modexp/uidivmodScript.sml +++ b/src/tools/symbexec/examples/analysis_modexp/uidivmodScript.sml @@ -101,9 +101,9 @@ fun birs_execute bprog_tm birs_state_init birs_stop_lbls = (* -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; val result = birs_execute bprog_tm_ birs_state_init_ birs_stop_lbls_ -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; *) diff --git a/src/tools/symbexec/examples/analysis_shortprogs/b16_00Script.sml b/src/tools/symbexec/examples/analysis_shortprogs/b16_00Script.sml index 75ab72ba1..b7b095cd4 100644 --- a/src/tools/symbexec/examples/analysis_shortprogs/b16_00Script.sml +++ b/src/tools/symbexec/examples/analysis_shortprogs/b16_00Script.sml @@ -86,9 +86,9 @@ val _ = print "done building the tree\n"; val _ = print "now reducing it to one sound structure\n"; -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; val result = exec_until (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec) single_step_A_thm birs_stop_lbls; -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; val _ = (print_term o concl) result; diff --git a/src/tools/symbexec/examples/analysis_shortprogs/b16_10Script.sml b/src/tools/symbexec/examples/analysis_shortprogs/b16_10Script.sml index 737546df9..5c1d75ec6 100644 --- a/src/tools/symbexec/examples/analysis_shortprogs/b16_10Script.sml +++ b/src/tools/symbexec/examples/analysis_shortprogs/b16_10Script.sml @@ -86,9 +86,9 @@ val _ = print "done building the tree\n"; val _ = print "now reducing it to one sound structure\n"; -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; val result = exec_until (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec) single_step_A_thm birs_stop_lbls; -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; val _ = (print_term o concl) result; diff --git a/src/tools/symbexec/examples/analysis_shortprogs/cmpbeqScript.sml b/src/tools/symbexec/examples/analysis_shortprogs/cmpbeqScript.sml index b0011ff6d..86a6e65bd 100644 --- a/src/tools/symbexec/examples/analysis_shortprogs/cmpbeqScript.sml +++ b/src/tools/symbexec/examples/analysis_shortprogs/cmpbeqScript.sml @@ -90,9 +90,9 @@ val _ = print "done building the tree\n"; val _ = print "now reducing it to one sound structure\n"; -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; val result = exec_until (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec) single_step_A_thm birs_stop_lbls; -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; val _ = (print_term o concl) result; diff --git a/src/tools/symbexec/examples/analysis_shortprogs/ldScript.sml b/src/tools/symbexec/examples/analysis_shortprogs/ldScript.sml index 70990efac..e12723ee2 100644 --- a/src/tools/symbexec/examples/analysis_shortprogs/ldScript.sml +++ b/src/tools/symbexec/examples/analysis_shortprogs/ldScript.sml @@ -90,9 +90,9 @@ val _ = print "done building the tree\n"; val _ = print "now reducing it to one sound structure\n"; -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; val result = exec_until (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec) single_step_A_thm birs_stop_lbls; -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; val _ = (print_term o concl) result; diff --git a/src/tools/symbexec/examples/analysis_shortprogs/ldldbr8Script.sml b/src/tools/symbexec/examples/analysis_shortprogs/ldldbr8Script.sml index ac0ca6ac0..d3332a902 100644 --- a/src/tools/symbexec/examples/analysis_shortprogs/ldldbr8Script.sml +++ b/src/tools/symbexec/examples/analysis_shortprogs/ldldbr8Script.sml @@ -90,9 +90,9 @@ val _ = print "done building the tree\n"; val _ = print "now reducing it to one sound structure\n"; -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; val result = exec_until (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec) single_step_A_thm birs_stop_lbls; -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; val _ = (print_term o concl) result; diff --git a/src/tools/symbexec/examples/analysis_shortprogs/ldnopScript.sml b/src/tools/symbexec/examples/analysis_shortprogs/ldnopScript.sml index cef24dfbf..93b3177bf 100644 --- a/src/tools/symbexec/examples/analysis_shortprogs/ldnopScript.sml +++ b/src/tools/symbexec/examples/analysis_shortprogs/ldnopScript.sml @@ -90,9 +90,9 @@ val _ = print "done building the tree\n"; val _ = print "now reducing it to one sound structure\n"; -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; val result = exec_until (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec) single_step_A_thm birs_stop_lbls; -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; val _ = (print_term o concl) result; diff --git a/src/tools/symbexec/examples/analysis_shortprogs/nopsubaddScript.sml b/src/tools/symbexec/examples/analysis_shortprogs/nopsubaddScript.sml index 3b6d6a895..36866e43b 100644 --- a/src/tools/symbexec/examples/analysis_shortprogs/nopsubaddScript.sml +++ b/src/tools/symbexec/examples/analysis_shortprogs/nopsubaddScript.sml @@ -86,9 +86,9 @@ val _ = print "done building the tree\n"; val _ = print "now reducing it to one sound structure\n"; -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; val result = exec_until (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec) single_step_A_thm birs_stop_lbls; -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; val _ = (print_term o concl) result; diff --git a/src/tools/symbexec/examples/analysis_shortprogs/stScript.sml b/src/tools/symbexec/examples/analysis_shortprogs/stScript.sml index a76ed2ec9..d85fb5e69 100644 --- a/src/tools/symbexec/examples/analysis_shortprogs/stScript.sml +++ b/src/tools/symbexec/examples/analysis_shortprogs/stScript.sml @@ -90,9 +90,9 @@ val _ = print "done building the tree\n"; val _ = print "now reducing it to one sound structure\n"; -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; val result = exec_until (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec) single_step_A_thm birs_stop_lbls; -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; val _ = (print_term o concl) result; diff --git a/src/tools/symbexec/examples/common/Holmakefile b/src/tools/symbexec/examples/common/Holmakefile index ebcad9a9c..826ba26f0 100644 --- a/src/tools/symbexec/examples/common/Holmakefile +++ b/src/tools/symbexec/examples/common/Holmakefile @@ -1,4 +1,5 @@ -INCLUDES = $(HOLBADIR)/src/theory/bir-support \ +INCLUDES = $(HOLBADIR)/src/extra \ + $(HOLBADIR)/src/theory/bir-support \ $(HOLBADIR)/src/tools/symbexec \ $(HOLBADIR)/src/theory/tools/lifter \ $(HOLBADIR)/src/theory/tools/comp diff --git a/src/tools/symbexec/examples/common/bir_program_transfScript.sml b/src/tools/symbexec/examples/common/bir_program_transfScript.sml index 7e19649b2..bf44431b8 100644 --- a/src/tools/symbexec/examples/common/bir_program_transfScript.sml +++ b/src/tools/symbexec/examples/common/bir_program_transfScript.sml @@ -1,4 +1,3 @@ - open HolKernel Parse boolLib bossLib; open pred_setTheory; @@ -1119,7 +1118,7 @@ ASSUME_TAC (ISPECL [``r:('c, 'd, 'b) bir_lifting_machine_rec_t``, ``mu:'c word_i ``mms:(('c word)# ('d word) list) list``, ``p:'a bir_program_t``] bir_inst_liftingTheory.bir_is_lifted_prog_MULTI_STEP_EXEC) >> REV_FULL_SIMP_TAC std_ss [] >> -bir_auxiliaryLib.QSPECL_X_ASSUM ``!n ms bs. _`` [`n'`, `ms`, `bs`] >> +holba_auxiliaryLib.QSPECL_X_ASSUM ``!n ms bs. _`` [`n'`, `ms`, `bs`] >> REV_FULL_SIMP_TAC (std_ss++holBACore_ss) [bir_programTheory.bir_state_is_terminated_def] QED @@ -1432,7 +1431,7 @@ open bir_immTheory; open bir_programTheory; open bir_tsTheory; open bir_program_multistep_propsTheory; -open bir_auxiliaryTheory; +open holba_auxiliaryTheory; (* From lifter: *) open bir_inst_liftingTheory; @@ -1446,7 +1445,7 @@ open HolBASimps; open HolBACoreSimps; open program_logicSimps; -open bir_auxiliaryLib; +open holba_auxiliaryLib; in (* TODO: copied and adjusted *) @@ -1984,11 +1983,11 @@ Theorem m0_mod_SIM_m0_thm: (m0_mod_R ms' mms')) Proof Induct_on `n` >- ( - FULL_SIMP_TAC std_ss [bir_auxiliaryTheory.FUNPOW_OPT_REWRS] >> + FULL_SIMP_TAC std_ss [holba_auxiliaryTheory.FUNPOW_OPT_REWRS] >> METIS_TAC [] ) >> - FULL_SIMP_TAC std_ss [bir_auxiliaryTheory.FUNPOW_OPT_REWRS] >> + FULL_SIMP_TAC std_ss [holba_auxiliaryTheory.FUNPOW_OPT_REWRS] >> REPEAT STRIP_TAC >> Cases_on `NextStateM0_mod mms` >> ( diff --git a/src/tools/symbexec/examples/riscv/se_swapScript.sml b/src/tools/symbexec/examples/riscv/se_swapScript.sml index 73585ca4a..170aa0f55 100644 --- a/src/tools/symbexec/examples/riscv/se_swapScript.sml +++ b/src/tools/symbexec/examples/riscv/se_swapScript.sml @@ -122,9 +122,9 @@ val _ = print "done building the tree\n"; val _ = print "now reducing it to one sound structure\n"; -val timer = bir_miscLib.timer_start 0; +val timer = holba_miscLib.timer_start 0; val result = exec_until (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec) single_step_A_thm birs_stop_lbls; -val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; +val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer; val _ = (print_term o concl) result; diff --git a/src/tools/wp/bir_wpLib.sml b/src/tools/wp/bir_wpLib.sml index 54785ed58..b93efd6dc 100644 --- a/src/tools/wp/bir_wpLib.sml +++ b/src/tools/wp/bir_wpLib.sml @@ -36,7 +36,7 @@ open bir_inst_liftingHelpersLib; (* From /theory/bir *) open bir_programTheory bir_typing_progTheory bir_envTheory - bir_auxiliaryTheory bir_valuesTheory bir_expTheory + holba_auxiliaryTheory bir_valuesTheory bir_expTheory bir_exp_memTheory bir_immTheory; open bir_immSyntax bir_expSyntax; diff --git a/src/tools/wp/examples/test-wp.sml b/src/tools/wp/examples/test-wp.sml index b319cf43c..e17c737c8 100644 --- a/src/tools/wp/examples/test-wp.sml +++ b/src/tools/wp/examples/test-wp.sml @@ -287,7 +287,7 @@ val wp_tests = *) ]; -val _ = bir_fileLib.makedir true "tempdir"; +val _ = holba_fileLib.makedir true "tempdir"; val _ = OS.FileSys.chDir "tempdir"; (*