summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--test/hol/Holmakefile4
-rw-r--r--test/hol/hoareScript.sml95
-rw-r--r--test/hol/state_monad_lemmasScript.sml25
-rw-r--r--test/hol/test_raw_addScript.sml248
4 files changed, 372 insertions, 0 deletions
diff --git a/test/hol/Holmakefile b/test/hol/Holmakefile
new file mode 100644
index 00000000..bc2ddc81
--- /dev/null
+++ b/test/hol/Holmakefile
@@ -0,0 +1,4 @@
+ifndef SAILDIR
+SAILDIR=../..
+endif
+INCLUDES = $(SAILDIR)/snapshots/hol4/sail/cheri $(SAILDIR)/snapshots/hol4/sail/lib/hol
diff --git a/test/hol/hoareScript.sml b/test/hol/hoareScript.sml
new file mode 100644
index 00000000..04d2560c
--- /dev/null
+++ b/test/hol/hoareScript.sml
@@ -0,0 +1,95 @@
+open HolKernel boolLib bossLib Parse pairTheory mp_then
+open state_monadTheory state_monad_lemmasTheory
+
+val _ = new_theory "hoare"
+
+(* Hoare logic, as in the Isabelle version *)
+
+val _ = type_abbrev("predS", ``:'regs sequential_state -> bool``);
+
+val PrePost_def = Define`
+ PrePost (P:'regs predS) (f:('regs, 'a, 'e)monadS) Q =
+ ∀s. P s ⇒ (∀r. r ∈ f s ⇒ Q (FST r) (SND r))`;
+
+val PrePostI = Q.store_thm("PrePostI",
+ `(∀s r s'. P s ∧ (r,s') ∈ f s ⇒ Q r s') ⇒ PrePost P f Q`,
+ rw[PrePost_def,FORALL_PROD] \\ res_tac);
+
+val PrePost_elim = Q.store_thm("PrePost_elim",
+ `PrePost P f Q ∧ P s ∧ (r, s') ∈ f s ⇒ Q r s'`,
+ rw[PrePost_def] \\ res_tac \\ fs[]);
+
+val PrePost_consequence = Q.store_thm("PrePost_consequence",
+ `PrePost X f Y ∧ (∀s. P s ⇒ X s) ∧ (∀v s. Y v s ⇒ Q v s) ⇒ PrePost P f Q`,
+ rw[PrePost_def] \\ ntac 3 res_tac);
+
+val PrePost_strengthen_pre = Q.store_thm("PrePost_strengthen_pre",
+ `PrePost X f Z ∧ (∀s. Y s ⇒ X s) ⇒ PrePost X f Z`,
+ metis_tac[PrePost_consequence]);
+
+val PrePost_weaken_post = Q.store_thm("PrePost_weaken_post",
+ `PrePost X f Y ∧ (∀v s. Y v s ⇒ Z v s) ⇒ PrePost X f Z`,
+ metis_tac[PrePost_consequence]);
+
+val PrePost_True_post = Q.store_thm("PrePost_True_post[simp]",
+ `PrePost P m (λ_ _. T)`, rw[PrePost_def]);
+
+val PrePost_any = Q.store_thm("PrePost_any",
+ `PrePost (λs. ∀r. r ∈ m s ⇒ Q (FST r) (SND r)) m Q`,
+ rw[PrePost_def]);
+
+val PrePost_returnS = Q.store_thm("PrePost_returnS",
+ `PrePost (P (Value x)) (returnS x) P`,
+ rw[PrePost_def, returnS_def]);
+
+val PrePost_bindS = Q.store_thm("PrePost_bindS",
+ `(∀s a s'. (Value a, s') ∈ m s ⇒ PrePost (R a) (f a) Q) ∧
+ PrePost P m (λr. case r of Value a => R a | Ex e => Q (Ex e))
+ ⇒
+ PrePost P (bindS m f) Q`,
+ strip_tac
+ \\ match_mp_tac PrePostI
+ \\ rw[]
+ \\ drule (GEN_ALL PrePost_elim)
+ \\ drule bindS_cases
+ \\ rw[]
+ \\ first_x_assum drule \\ strip_tac
+ \\ first_x_assum drule \\ strip_tac
+ \\ fs[]
+ \\ match_mp_tac (GEN_ALL PrePost_elim)
+ \\ metis_tac[]);
+
+val PrePost_bindS_ignore = Q.store_thm("PrePost_bindS_ignore",
+ `PrePost R f Q ∧ PrePost P m (λr. case r of Value a => R | Ex e => Q (Ex e)) ⇒
+ PrePost P (bindS m (λ_. f)) Q`,
+ strip_tac
+ \\ match_mp_tac (GEN_ALL PrePost_bindS)
+ \\ qexists_tac`λa. R` \\ simp[]);
+
+val PrePost_seqS = save_thm("PrePost_seqS",
+ PrePost_bindS_ignore
+ |> INST_TYPE[delta |-> oneSyntax.one_ty]
+ |> CONV_RULE(RAND_CONV(RATOR_CONV(RAND_CONV(REWR_CONV(GSYM seqS_def)))))
+ |> ONCE_REWRITE_RULE[CONJ_COMM]
+ |> GEN_ALL);
+
+val PrePost_bindS_unit = Q.store_thm("PrePost_bindS_unit",
+ `PrePost R (f ()) Q ∧ PrePost P m (λr. case r of Value a => R | Ex e => Q (Ex e))
+ ⇒ PrePost P (bindS m f) Q`,
+ strip_tac
+ \\ match_mp_tac (GEN_ALL PrePost_bindS)
+ \\ qexists_tac`λa. R` \\ simp[]);
+
+val PrePost_readS = Q.store_thm("PrePost_readS",
+ `PrePost (λs. P (Value (f s)) s) (readS f) P`,
+ rw[PrePost_def, readS_def, returnS_def]);
+
+val PrePost_updateS = Q.store_thm("PrePost_updateS",
+ `PrePost (λs. P (Value ()) (f s)) (updateS f) P`,
+ rw[PrePost_def, updateS_def, returnS_def]);
+
+val PrePostE_def = Define`
+ PrePostE P f Q E = PrePost P f (λv. case v of Value a => Q a | Ex e => E e)`;
+
+val _ = export_theory();
+
diff --git a/test/hol/state_monad_lemmasScript.sml b/test/hol/state_monad_lemmasScript.sml
new file mode 100644
index 00000000..b88fc2ab
--- /dev/null
+++ b/test/hol/state_monad_lemmasScript.sml
@@ -0,0 +1,25 @@
+open HolKernel boolLib bossLib Parse
+open state_monadTheory
+val _ = temp_tight_equality();
+
+val _ = new_theory "state_monad_lemmas";
+
+val () = monadsyntax.declare_monad("state_monad",
+ { bind = ``bindS``,
+ ignorebind = SOME ``seqS``,
+ unit = ``returnS``,
+ fail = SOME ``failS``,
+ choice = SOME ``chooseS``,
+ guard = SOME ``assert_expS`` });
+
+val bindS_cases = Q.store_thm("bindS_cases",
+ `(r, s') ∈ bindS m f s ⇒
+ (∃a a' s''. r = Value a ∧ (Value a', s'') ∈ m s ∧ (Value a, s') ∈ f a' s'') ∨
+ (∃e. r = Ex e ∧ (Ex e, s') ∈ m s) ∨
+ (∃e a s''. r = Ex e ∧ (Value a, s'') ∈ m s ∧ (Ex e, s') ∈ f a s'')`,
+ rw[bindS_def]
+ \\ Cases_on`r` \\ fs[]
+ \\ BasicProvers.EVERY_CASE_TAC \\ fs[]
+ \\ metis_tac[]);
+
+val _ = export_theory();
diff --git a/test/hol/test_raw_addScript.sml b/test/hol/test_raw_addScript.sml
new file mode 100644
index 00000000..eca6def7
--- /dev/null
+++ b/test/hol/test_raw_addScript.sml
@@ -0,0 +1,248 @@
+open HolKernel boolLib bossLib Parse
+open intLib bitLib wordsLib
+open sail_valuesAuxiliaryTheory state_monad_lemmasTheory
+open cheriTheory hoareTheory
+
+val _ = new_theory "test_raw_add";
+
+val _ = Globals.max_print_depth := 20;
+
+(* MIPS register names
+ ftp://www.linux-mips.org/pub/linux/mips/doc/ABI/MIPS-N32-ABI-Handbook.pdf
+ *)
+val gpr_names_def = Define`
+ gpr_names = [
+ "zero";
+ "at";
+ "v0"; "v1";
+ "a0"; "a1"; "a2"; "a3"; "a4"; "a5"; "a6"; "a7";
+ "t4"; "t5"; "t6"; "t7";
+ "s0"; "s1"; "s2"; "s3"; "s4"; "s5"; "s6"; "s7";
+ "t8"; "t9";
+ "kt0"; "kt1";
+ "gp";
+ "sp";
+ "s8";
+ "ra"]`;
+
+val install_code_def = Define`
+ install_code initialPC (code:word32 list) =
+ iteriS (λi c. MEMw_wrapper (initialPC + 4w*(i2w i)) 4 c) code`;
+
+val clocked_whileS_def = Define`
+ clocked_whileS clock vars cond body s =
+ if 0n < clock then
+ bindS (cond vars)
+ (λcond_val s'.
+ if cond_val then
+ bindS (body vars) (λvars' s''. clocked_whileS (clock-1) vars' cond body s'') s'
+ else returnS vars s') s
+ else
+ failS "timeout" s`;
+
+val install_and_run_def = Define`
+ install_and_run code clock =
+ seqS
+ (seqS (install_code 0x9000000040000000w code) (init_registers 0x9000000040000000w))
+ (clocked_whileS clock () (λunit_var. fetch_and_execute ()) (λunit_var. returnS ()))`;
+
+(* obtained from
+ objdump -d test_raw_add.elf
+ (with the cheri mips binutils version of objdump)
+
+test_raw_add.elf: file format elf64-bigmips
+
+Disassembly of section .text:
+
+9000000040000000 <start>:
+9000000040000000: 24130001 li s3,1
+9000000040000004: 24140002 li s4,2
+9000000040000008: 02742020 add a0,s3,s4
+900000004000000c: 240c0001 li t0,1
+9000000040000010: 24050002 li a1,2
+9000000040000014: 00ac2820 add a1,a1,t0
+9000000040000018: 240c0001 li t0,1
+900000004000001c: 24060002 li a2,2
+9000000040000020: 01863020 add a2,t0,a2
+9000000040000024: 24070001 li a3,1
+9000000040000028: 00e73820 add a3,a3,a3
+900000004000002c: 240c0001 li t0,1
+9000000040000030: 240d0002 li t1,2
+9000000040000034: 240e0003 li t2,3
+9000000040000038: 018d7820 add t3,t0,t1
+900000004000003c: 01ee4020 add a4,t3,t2
+9000000040000040: 240c0001 li t0,1
+9000000040000044: 240dffff li t1,-1
+9000000040000048: 018d4820 add a5,t0,t1
+900000004000004c: 240cffff li t0,-1
+9000000040000050: 240dffff li t1,-1
+9000000040000054: 018d5020 add a6,t0,t1
+9000000040000058: 240cffff li t0,-1
+900000004000005c: 240d0002 li t1,2
+9000000040000060: 018d5820 add a7,t0,t1
+9000000040000064: 240c0001 li t0,1
+9000000040000068: 240dfffe li t1,-2
+900000004000006c: 018d8020 add s0,t0,t1
+9000000040000070: 4082d000 mtc0 v0,$26
+ ...
+900000004000007c: 4082b800 mtc0 v0,$23
+
+9000000040000080 <end>:
+9000000040000080: 1000ffff b 9000000040000080 <end>
+9000000040000084: 00000000 nop
+*)
+
+
+val test_raw_add_insts_def = Define`test_raw_add_insts =
+ [0x24130001w:word32
+ ;0x24140002w
+ ;0x02742020w
+ ;0x240c0001w
+ ;0x24050002w
+ ;0x00ac2820w
+ ;0x240c0001w
+ ;0x24060002w
+ ;0x01863020w
+ ;0x24070001w
+ ;0x00e73820w
+ ;0x240c0001w
+ ;0x240d0002w
+ ;0x240e0003w
+ ;0x018d7820w
+ ;0x01ee4020w
+ ;0x240c0001w
+ ;0x240dffffw
+ ;0x018d4820w
+ ;0x240cffffw
+ ;0x240dffffw
+ ;0x018d5020w
+ ;0x240cffffw
+ ;0x240d0002w
+ ;0x018d5820w
+ ;0x240c0001w
+ ;0x240dfffew
+ ;0x018d8020w
+ ;0x4082d000w]`;
+
+fun check_name n =
+ EVAL ``EL ^(numSyntax.term_of_int n) gpr_names``;
+
+val test_raw_add_post_def = Define`
+ test_raw_add_post s = (
+ bindS (rGPR 19w) (λs3. (* check_name 19 *)
+ seqS (assert_expS (s3 = 1w) "add modified first input") (
+ bindS (rGPR 20w) (λs4. (* check_name 20 *)
+ seqS (assert_expS (s4 = 2w) "add modified second input") (
+ bindS (rGPR 04w) (λa0. (* check_name 04 *)
+ seqS (assert_expS (a0 = 3w) "add failed") (
+ bindS (rGPR 05w) (λa1. (* check_name 05 *)
+ seqS (assert_expS (a1 = 3w) "add into first input failed") (
+ bindS (rGPR 06w) (λa2. (* check_name 06 *)
+ seqS (assert_expS (a2 = 3w) "add into second input failed") (
+ bindS (rGPR 07w) (λa3. (* check_name 07 *)
+ seqS (assert_expS (a3 = 2w) "add into both inputs failed") (
+ bindS (rGPR 08w) (λa4. (* check_name 08 *)
+ seqS (assert_expS (a4 = 6w) "add-to-add pipeline failed") (
+ bindS (rGPR 09w) (λa5. (* check_name 09 *)
+ seqS (assert_expS (a5 = 0w) "positive plus negative to zero failed") (
+ bindS (rGPR 10w) (λa6. (* check_name 10 *)
+ seqS (assert_expS (a6 = 0xfffffffffffffffew) "negative plus negative to negative failed") (
+ bindS (rGPR 11w) (λa7. (* check_name 11 *)
+ seqS (assert_expS (a7 = 1w) "negative plus positive to positive failed") (
+ bindS (rGPR 16w) (λs0. (* check_name 16 *)
+ (assert_expS (s0 = 0xffffffffffffffffw) "positive plus negative to negative failed")))))))))))))))))))))) s
+ = {(Value (),s)})`;
+
+(*
+
+val decoded_insts1 =
+ listLib.MAP_CONV EVAL ``MAP decode ^(rhs(concl test_raw_add_insts_def))``
+
+val (SOME_is, oty) = decoded_insts1 |> concl |> rhs |> listSyntax.dest_list
+val asts = map rand SOME_is
+val ls2 = listLib.MAP_CONV EVAL ``MAP SOME ^(listSyntax.mk_list(asts,optionSyntax.dest_option oty))``;
+val test_raw_add_asts_def = Define`
+ test_raw_add_asts = ^(rand(lhs(concl ls2)))`;
+
+val decoded_insts = TRANS decoded_insts1 (SYM ls2)
+ |> ONCE_REWRITE_RULE[GSYM test_raw_add_insts_def, GSYM test_raw_add_asts_def]
+*)
+
+val test_raw_add_thm = Q.store_thm("test_raw_add_thm",
+ `PrePost
+ (λ_. T)
+ (install_and_run test_raw_add_insts 100000)
+ (λ_ s. test_raw_add_post s)`,
+(*
+ rw[install_and_run_def]
+ \\ match_mp_tac PrePost_seqS
+ \\ simp[]
+ \\ qmatch_goalsub_abbrev_tac`install_code initPC`
+ \\ qexists_tac`λs. code_installed initPC test_raw_add_insts s ∧
+ init_registers_post s`
+ \\ conj_tac
+ >- (
+ match_mp_tac PrePost_seqS \\ simp[]
+ \\ qexists_tac`code_installed initPC test_raw_add_insts`
+ \\ conj_tac
+ >- cheat
+ \\ cheat )
+ fetch_and_execute_def
+*)
+cheat);
+
+(*
+val cs = wordsLib.words_compset();
+val () = computeLib.extend_compset [
+ computeLib.Extenders [
+ intReduce.add_int_compset
+ ],
+ (* sail stuff *)
+ computeLib.Defs [
+ sail_valuesTheory.nat_of_int_def,
+ sail_operators_mwordsTheory.subrange_vec_dec_def
+ ],
+ (* cheri/mips model *)
+ computeLib.Defs [
+ decode_def
+ ],
+ (* addition test *)
+ computeLib.Defs [
+ test_raw_add_insts_def
+ ]
+] cs;
+
+computeLib.CBV_CONV cs ``decode (EL 1 test_raw_add_insts)``
+
+val th1 = EVAL ``THE (decode (EL 1 test_raw_add_insts))``
+
+val s1 = EVAL ``init_cp0_state () (init_state (regs:regstate) o1 seed)``
+
+val th2 = ``execute ^(rhs(concl th1)) ^s1``
+ |> SIMP_CONV(srw_ss())[execute_def]
+ |> SIMP_RULE(srw_ss())[execute_ADDIU_def]
+
+f"bindS"
+type_of ``execute ast ``
+f"init_state"
+execute_ADDIU_def
+type_of``OPTION_BIND``
+tyabbrev_info"M"
+val (_, execute_rng) = dom_rng (type_of``execute``)
+val (mdom, mrng) = dom_rng execute_rng
+val state_ty = ``:regstate sequential_state``
+dest_thy_type state_ty
+TypeBase.fields_of state_ty
+disable_tyabbrev_printing"rel"
+dest_type``:unit M``
+
+f"vec_of_bits"
+f"of_bits_fail"
+f"maybe_failw"
+f"nat_of_int"
+f"just_list"
+f"sfunpow"
+show_assums := true
+*)
+
+val _ = export_theory ();
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-13 07:32:01 +0000