diff options
| -rw-r--r-- | backends/hol4/divDefExampleScript.sml | 7 | ||||
| -rw-r--r-- | backends/hol4/divDefLib.sml | 9 | ||||
| -rw-r--r-- | backends/hol4/divDefLibTestScript.sml | 3 | ||||
| -rw-r--r-- | backends/hol4/divDefNoFixLib.sml | 8 | ||||
| -rw-r--r-- | backends/hol4/divDefNoFixLibTestScript.sml | 7 | ||||
| -rw-r--r-- | backends/hol4/divDefScript.sml | 6 | ||||
| -rw-r--r-- | backends/hol4/ilistScript.sml | 4 | ||||
| -rw-r--r-- | backends/hol4/ilistTheory.sig | 2 | ||||
| -rw-r--r-- | backends/hol4/primitivesArithScript.sml | 3 | ||||
| -rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 3 | ||||
| -rw-r--r-- | backends/hol4/primitivesLib.sml | 5 | ||||
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 132 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 104 | ||||
| -rw-r--r-- | backends/hol4/testHashmapScript.sml | 1 |
14 files changed, 238 insertions, 56 deletions
diff --git a/backends/hol4/divDefExampleScript.sml b/backends/hol4/divDefExampleScript.sml index 338385ab..4a17977c 100644 --- a/backends/hol4/divDefExampleScript.sml +++ b/backends/hol4/divDefExampleScript.sml @@ -1,11 +1,6 @@ (* Manually written examples of how to use the fixed-point operator from divDefScript *) -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory - -open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory -open primitivesLib -open divDefTheory +open primitivesLib divDefTheory val _ = new_theory "divDefExample" diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml index 78e664e6..1e95b6c5 100644 --- a/backends/hol4/divDefLib.sml +++ b/backends/hol4/divDefLib.sml @@ -1,12 +1,7 @@ structure divDefLib :> divDefLib = struct -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory - -open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory -open primitivesLib -open divDefTheory +open primitivesBaseTacLib primitivesLib divDefTheory val dbg = ref false fun print_dbg s = if (!dbg) then print s else () @@ -907,7 +902,7 @@ fun DefineDiv (def_qt : term quotation) = (* Because [store_definition] overrides existing names, it seems that in practice we don't really need to delete the previous definitions (we still do it: it doesn't cost much). *) - val _ = map delete_binding thm_names + val _ = app delete_binding thm_names val _ = map store_definition (zip thm_names def_eqs) in def_eqs diff --git a/backends/hol4/divDefLibTestScript.sml b/backends/hol4/divDefLibTestScript.sml index f5df6139..2e6d56b6 100644 --- a/backends/hol4/divDefLibTestScript.sml +++ b/backends/hol4/divDefLibTestScript.sml @@ -1,6 +1,7 @@ (* Examples which use divDefLib.DefineDiv *) -open primitivesLib divDefLib +open HolKernel +open divDefLib val _ = new_theory "divDefLibTest" diff --git a/backends/hol4/divDefNoFixLib.sml b/backends/hol4/divDefNoFixLib.sml index 59319e6a..f7b9763d 100644 --- a/backends/hol4/divDefNoFixLib.sml +++ b/backends/hol4/divDefNoFixLib.sml @@ -3,11 +3,7 @@ structure divDefNoFixLib :> divDefNoFixLib = struct -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory - -open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory -open primitivesLib +open primitivesArithTheory primitivesBaseTacLib primitivesLib val case_result_same_eq = prove ( “!(r : 'a result). @@ -849,7 +845,7 @@ fun prove_termination_thms in (* Apply the theorem, prove the premise, and rewrite *) (prove_premise_then premise_tac assume_tac eq_th >> fs []) (asms, g) - end handle NotFound => all_tac (asms, g) + end handle Redblackmap.NotFound => all_tac (asms, g) | HOL_ERR _ => all_tac (asms, g) (* Getting the function name can also fail *) fun prove_one ((pred_tm, fun_eq_tm), pred_n_imp_pred_least_thm) : diff --git a/backends/hol4/divDefNoFixLibTestScript.sml b/backends/hol4/divDefNoFixLibTestScript.sml index b2a4d607..f613c327 100644 --- a/backends/hol4/divDefNoFixLibTestScript.sml +++ b/backends/hol4/divDefNoFixLibTestScript.sml @@ -1,8 +1,5 @@ -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory - -open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory -open primitivesLib divDefNoFixLib +open HolKernel +open divDefNoFixLib val _ = new_theory "divDefNoFixLibTest" diff --git a/backends/hol4/divDefScript.sml b/backends/hol4/divDefScript.sml index cc745e5d..8ef99530 100644 --- a/backends/hol4/divDefScript.sml +++ b/backends/hol4/divDefScript.sml @@ -7,11 +7,7 @@ how to use it. *) -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory - -open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory -open primitivesLib +open primitivesArithTheory primitivesBaseTacLib primitivesTheory primitivesLib val _ = new_theory "divDef" diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml index f382d95d..157b5c00 100644 --- a/backends/hol4/ilistScript.sml +++ b/backends/hol4/ilistScript.sml @@ -1,6 +1,4 @@ -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory - +open listTheory open primitivesArithTheory primitivesBaseTacLib (* The following theory contains alternative definitions of functions operating diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig index f155a328..21545b6e 100644 --- a/backends/hol4/ilistTheory.sig +++ b/backends/hol4/ilistTheory.sig @@ -20,8 +20,6 @@ sig (* [primitivesArith] Parent theory of "ilist" - [string] Parent theory of "ilist" - [index_def] Definition ⊢ ∀i x ls. diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml index b7b44b25..679ed2cd 100644 --- a/backends/hol4/primitivesArithScript.sml +++ b/backends/hol4/primitivesArithScript.sml @@ -1,5 +1,4 @@ -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory +open arithmeticTheory integerTheory open primitivesBaseTacLib val _ = new_theory "primitivesArith" diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml index 133f6a99..3d6d9e3e 100644 --- a/backends/hol4/primitivesBaseTacLib.sml +++ b/backends/hol4/primitivesBaseTacLib.sml @@ -2,8 +2,7 @@ structure primitivesBaseTacLib = struct -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory +open HolKernel boolLib bossLib intLib val debug = ref false diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml index cf7368a6..eed50e25 100644 --- a/backends/hol4/primitivesLib.sml +++ b/backends/hol4/primitivesLib.sml @@ -2,10 +2,7 @@ structure primitivesLib = struct -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory - -open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory +open primitivesBaseTacLib primitivesTheory val primitives_theory_name = "primitives" diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index 5ef51f2e..2a13e76d 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -1,10 +1,7 @@ -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory - +open stringTheory open primitivesArithTheory primitivesBaseTacLib ilistTheory -val primitives_theory_name = "primitives" -val _ = new_theory primitives_theory_name +val _ = new_theory "primitives" (*** Result *) Datatype: @@ -203,7 +200,6 @@ val all_to_int_bounds_lemmas = [ Note that for isize and usize, we write the lemmas in such a way that the proofs are easily automatable for constants. *) -(* TODO: remove the condition on u16_max, and make the massage tactic automatically use usize_bounds *) val isize_to_int_int_to_isize = new_axiom ("isize_to_int_int_to_isize", “!n. isize_min <= n /\ n <= isize_max ==> isize_to_int (int_to_isize n) = n”) @@ -252,8 +248,7 @@ val u128_to_int_int_to_u128 = new_axiom ("u128_to_int_int_to_u128", “!n. 0 <= n /\ n <= u128_max ==> u128_to_int (int_to_u128 n) = n”) -(* TODO: rename *) -val all_conversion_id_lemmas = [ +val all_int_to_scalar_to_int_lemmas = [ isize_to_int_int_to_isize, i8_to_int_int_to_i8, i16_to_int_int_to_i16, @@ -268,6 +263,103 @@ val all_conversion_id_lemmas = [ u128_to_int_int_to_u128 ] +val prove_int_to_scalar_to_int_unfold_tac = + assume_tac isize_bounds >> (* Only useful for isize of course *) + assume_tac usize_bounds >> (* Only useful for usize of course *) + rw [] >> MAP_FIRST irule all_int_to_scalar_to_int_lemmas >> int_tac + +(* Custom unfolding lemmas for the purpose of evaluation *) + +(* For isize, we don't use isize_{min,max} (which are opaque) but i16_{min,max} *) +Theorem isize_to_int_int_to_isize_unfold: + ∀n. isize_to_int (int_to_isize n) = if i16_min <= n /\ n <= i16_max then n else isize_to_int (int_to_isize n) +Proof + prove_int_to_scalar_to_int_unfold_tac +QED + +Theorem i8_to_int_int_to_i8_unfold: + ∀n. i8_to_int (int_to_i8 n) = if i8_min <= n /\ n <= i8_max then n else i8_to_int (int_to_i8 n) +Proof + prove_int_to_scalar_to_int_unfold_tac +QED + +Theorem i16_to_int_int_to_i16_unfold: + ∀n. i16_to_int (int_to_i16 n) = if i16_min <= n /\ n <= i16_max then n else i16_to_int (int_to_i16 n) +Proof + prove_int_to_scalar_to_int_unfold_tac +QED + +Theorem i32_to_int_int_to_i32_unfold: + ∀n. i32_to_int (int_to_i32 n) = if i32_min <= n /\ n <= i32_max then n else i32_to_int (int_to_i32 n) +Proof + prove_int_to_scalar_to_int_unfold_tac +QED + +Theorem i64_to_int_int_to_i64_unfold: + ∀n. i64_to_int (int_to_i64 n) = if i64_min <= n /\ n <= i64_max then n else i64_to_int (int_to_i64 n) +Proof + prove_int_to_scalar_to_int_unfold_tac +QED + +Theorem i128_to_int_int_to_i128_unfold: + ∀n. i128_to_int (int_to_i128 n) = if i128_min <= n /\ n <= i128_max then n else i128_to_int (int_to_i128 n) +Proof + prove_int_to_scalar_to_int_unfold_tac +QED + +(* For usize, we don't use isize_{min,max} (which are opaque) but u16_{min,max} *) +Theorem usize_to_int_int_to_usize_unfold: + ∀n. usize_to_int (int_to_usize n) = if 0 ≤ n ∧ n <= u16_max then n else usize_to_int (int_to_usize n) +Proof + prove_int_to_scalar_to_int_unfold_tac +QED + +Theorem u8_to_int_int_to_u8_unfold: + ∀n. u8_to_int (int_to_u8 n) = if 0 <= n /\ n <= u8_max then n else u8_to_int (int_to_u8 n) +Proof + prove_int_to_scalar_to_int_unfold_tac +QED + +Theorem u16_to_int_int_to_u16_unfold: + ∀n. u16_to_int (int_to_u16 n) = if 0 <= n /\ n <= u16_max then n else u16_to_int (int_to_u16 n) +Proof + prove_int_to_scalar_to_int_unfold_tac +QED + +Theorem u32_to_int_int_to_u32_unfold: + ∀n. u32_to_int (int_to_u32 n) = if 0 <= n /\ n <= u32_max then n else u32_to_int (int_to_u32 n) +Proof + prove_int_to_scalar_to_int_unfold_tac +QED + +Theorem u64_to_int_int_to_u64_unfold: + ∀n. u64_to_int (int_to_u64 n) = if 0 <= n /\ n <= u64_max then n else u64_to_int (int_to_u64 n) +Proof + prove_int_to_scalar_to_int_unfold_tac +QED + +Theorem u128_to_int_int_to_u128_unfold: + ∀n. u128_to_int (int_to_u128 n) = if 0 <= n /\ n <= u128_max then n else u128_to_int (int_to_u128 n) +Proof + prove_int_to_scalar_to_int_unfold_tac +QED + +val all_int_to_scalar_to_int_unfold_lemmas = [ + isize_to_int_int_to_isize_unfold, + i8_to_int_int_to_i8_unfold, + i16_to_int_int_to_i16_unfold, + i32_to_int_int_to_i32_unfold, + i64_to_int_int_to_i64_unfold, + i128_to_int_int_to_i128_unfold, + usize_to_int_int_to_usize_unfold, + u8_to_int_int_to_u8_unfold, + u16_to_int_int_to_u16_unfold, + u32_to_int_int_to_u32_unfold, + u64_to_int_int_to_u64_unfold, + u128_to_int_int_to_u128_unfold +] +val _ = evalLib.add_unfold_thms (all_int_to_scalar_to_int_unfold_lemmas) + val int_to_i8_i8_to_int = new_axiom ("int_to_i8_i8_to_int", “∀i. int_to_i8 (i8_to_int i) = i”) val int_to_i16_i16_to_int = new_axiom ("int_to_i16_i16_to_int", “∀i. int_to_i16 (i16_to_int i) = i”) val int_to_i32_i32_to_int = new_axiom ("int_to_i32_i32_to_int", “∀i. int_to_i32 (i32_to_int i) = i”) @@ -282,6 +374,22 @@ val int_to_u64_u64_to_int = new_axiom ("int_to_u64_u64_to_int", “∀i. val int_to_u128_u128_to_int = new_axiom ("int_to_u128_u128_to_int", “∀i. int_to_u128 (u128_to_int i) = i”) val int_to_usize_usize_to_int = new_axiom ("int_to_usize_usize_to_int", “∀i. int_to_usize (usize_to_int i) = i”) +val all_scalar_to_int_to_scalar_lemmas = [ + int_to_i8_i8_to_int, + int_to_i16_i16_to_int, + int_to_i32_i32_to_int, + int_to_i64_i64_to_int, + int_to_i128_i128_to_int, + int_to_isize_isize_to_int, + int_to_u8_u8_to_int, + int_to_u16_u16_to_int, + int_to_u32_u32_to_int, + int_to_u64_u64_to_int, + int_to_u128_u128_to_int, + int_to_usize_usize_to_int +] +val _ = evalLib.add_rewrites all_scalar_to_int_to_scalar_lemmas + (** Utilities to define the arithmetic operations *) val mk_isize_def = Define ‘mk_isize n = @@ -558,7 +666,7 @@ val (asms,g) = top_goal () fun prove_arith_unop_eq (asms, g) = let - val rw_thms = List.concat [all_neg_defs, all_mk_int_defs, all_conversion_id_lemmas] + val rw_thms = List.concat [all_neg_defs, all_mk_int_defs, all_int_to_scalar_to_int_lemmas] in (rpt gen_tac >> rpt disch_tac >> @@ -630,7 +738,7 @@ fun prove_arith_op_eq (asms, g) = | _ => failwith "Unexpected" val x = (snd o dest_comb) x_to_int; val y = (snd o dest_comb) y_to_int; - val rw_thms = int_rem_def :: List.concat [all_rem_defs, all_add_defs, all_sub_defs, all_mul_defs, all_div_defs, all_mk_int_defs, all_to_int_bounds_lemmas, all_conversion_id_lemmas]; + val rw_thms = int_rem_def :: List.concat [all_rem_defs, all_add_defs, all_sub_defs, all_mul_defs, all_div_defs, all_mk_int_defs, all_to_int_bounds_lemmas, all_int_to_scalar_to_int_lemmas]; fun inst_first_lem arg lems = map_first_tac (fn th => (assume_tac (SPEC arg th) handle HOL_ERR _ => fail_tac "")) lems; in @@ -650,11 +758,11 @@ fun prove_arith_op_eq (asms, g) = qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_div_pos_le_init >> cooper_tac, (* For remainder *) - dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs [] >> + dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_int_to_scalar_to_int_lemmas >> fs [] >> qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_mod_pos_is_pos >> qspecl_assume [‘^x_to_int’, ‘^y_to_int’] pos_mod_pos_le_init >> cooper_tac, - dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs [] + dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_int_to_scalar_to_int_lemmas >> fs [] ]) (asms, g) end diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index 3b029c05..3e82565c 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -225,30 +225,35 @@ sig val i128_neg_eq : thm val i128_rem_eq : thm val i128_sub_eq : thm + val i128_to_int_int_to_i128_unfold : thm val i16_add_eq : thm val i16_div_eq : thm val i16_mul_eq : thm val i16_neg_eq : thm val i16_rem_eq : thm val i16_sub_eq : thm + val i16_to_int_int_to_i16_unfold : thm val i32_add_eq : thm val i32_div_eq : thm val i32_mul_eq : thm val i32_neg_eq : thm val i32_rem_eq : thm val i32_sub_eq : thm + val i32_to_int_int_to_i32_unfold : thm val i64_add_eq : thm val i64_div_eq : thm val i64_mul_eq : thm val i64_neg_eq : thm val i64_rem_eq : thm val i64_sub_eq : thm + val i64_to_int_int_to_i64_unfold : thm val i8_add_eq : thm val i8_div_eq : thm val i8_mul_eq : thm val i8_neg_eq : thm val i8_rem_eq : thm val i8_sub_eq : thm + val i8_to_int_int_to_i8_unfold : thm val index_update_diff : thm val index_update_same : thm val isize_add_eq : thm @@ -257,6 +262,7 @@ sig val isize_neg_eq : thm val isize_rem_eq : thm val isize_sub_eq : thm + val isize_to_int_int_to_isize_unfold : thm val num2error_11 : thm val num2error_ONTO : thm val num2error_error2num : thm @@ -273,26 +279,31 @@ sig val u128_mul_eq : thm val u128_rem_eq : thm val u128_sub_eq : thm + val u128_to_int_int_to_u128_unfold : thm val u16_add_eq : thm val u16_div_eq : thm val u16_mul_eq : thm val u16_rem_eq : thm val u16_sub_eq : thm + val u16_to_int_int_to_u16_unfold : thm val u32_add_eq : thm val u32_div_eq : thm val u32_mul_eq : thm val u32_rem_eq : thm val u32_sub_eq : thm + val u32_to_int_int_to_u32_unfold : thm val u64_add_eq : thm val u64_div_eq : thm val u64_mul_eq : thm val u64_rem_eq : thm val u64_sub_eq : thm + val u64_to_int_int_to_u64_unfold : thm val u8_add_eq : thm val u8_div_eq : thm val u8_mul_eq : thm val u8_rem_eq : thm val u8_sub_eq : thm + val u8_to_int_int_to_u8_unfold : thm val update_len : thm val update_spec : thm val usize_add_eq : thm @@ -300,6 +311,7 @@ sig val usize_mul_eq : thm val usize_rem_eq : thm val usize_sub_eq : thm + val usize_to_int_int_to_usize_unfold : thm val vec_insert_back_spec : thm val vec_len_spec : thm val vec_to_list_int_bounds : thm @@ -308,6 +320,8 @@ sig (* [ilist] Parent theory of "primitives" + [string] Parent theory of "primitives" + [isize_bounds] Axiom [oracles: ] [axioms: isize_bounds] [] @@ -1390,6 +1404,14 @@ sig ∃z. i128_sub x y = Return z ∧ i128_to_int z = i128_to_int x − i128_to_int y + [i128_to_int_int_to_i128_unfold] Theorem + + [oracles: DISK_THM] + [axioms: usize_bounds, i128_to_int_int_to_i128, isize_bounds] [] + ⊢ ∀n. i128_to_int (int_to_i128 n) = + if i128_min ≤ n ∧ n ≤ i128_max then n + else i128_to_int (int_to_i128 n) + [i16_add_eq] Theorem [oracles: DISK_THM] @@ -1451,6 +1473,14 @@ sig ∃z. i16_sub x y = Return z ∧ i16_to_int z = i16_to_int x − i16_to_int y + [i16_to_int_int_to_i16_unfold] Theorem + + [oracles: DISK_THM] + [axioms: usize_bounds, i16_to_int_int_to_i16, isize_bounds] [] + ⊢ ∀n. i16_to_int (int_to_i16 n) = + if i16_min ≤ n ∧ n ≤ i16_max then n + else i16_to_int (int_to_i16 n) + [i32_add_eq] Theorem [oracles: DISK_THM] @@ -1512,6 +1542,14 @@ sig ∃z. i32_sub x y = Return z ∧ i32_to_int z = i32_to_int x − i32_to_int y + [i32_to_int_int_to_i32_unfold] Theorem + + [oracles: DISK_THM] + [axioms: usize_bounds, i32_to_int_int_to_i32, isize_bounds] [] + ⊢ ∀n. i32_to_int (int_to_i32 n) = + if i32_min ≤ n ∧ n ≤ i32_max then n + else i32_to_int (int_to_i32 n) + [i64_add_eq] Theorem [oracles: DISK_THM] @@ -1573,6 +1611,14 @@ sig ∃z. i64_sub x y = Return z ∧ i64_to_int z = i64_to_int x − i64_to_int y + [i64_to_int_int_to_i64_unfold] Theorem + + [oracles: DISK_THM] + [axioms: usize_bounds, i64_to_int_int_to_i64, isize_bounds] [] + ⊢ ∀n. i64_to_int (int_to_i64 n) = + if i64_min ≤ n ∧ n ≤ i64_max then n + else i64_to_int (int_to_i64 n) + [i8_add_eq] Theorem [oracles: DISK_THM] @@ -1634,6 +1680,13 @@ sig ∃z. i8_sub x y = Return z ∧ i8_to_int z = i8_to_int x − i8_to_int y + [i8_to_int_int_to_i8_unfold] Theorem + + [oracles: DISK_THM] + [axioms: usize_bounds, i8_to_int_int_to_i8, isize_bounds] [] + ⊢ ∀n. i8_to_int (int_to_i8 n) = + if i8_min ≤ n ∧ n ≤ i8_max then n else i8_to_int (int_to_i8 n) + [index_update_diff] Theorem ⊢ ∀ls i j y. 0 ≤ i ⇒ i < len ls ⇒ index i (update ls i y) = y @@ -1723,6 +1776,14 @@ sig ∃z. isize_sub x y = Return z ∧ isize_to_int z = isize_to_int x − isize_to_int y + [isize_to_int_int_to_isize_unfold] Theorem + + [oracles: DISK_THM] + [axioms: usize_bounds, isize_to_int_int_to_isize, isize_bounds] [] + ⊢ ∀n. isize_to_int (int_to_isize n) = + if i16_min ≤ n ∧ n ≤ i16_max then n + else isize_to_int (int_to_isize n) + [num2error_11] Theorem ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r') @@ -1826,6 +1887,13 @@ sig ∃z. u128_sub x y = Return z ∧ u128_to_int z = u128_to_int x − u128_to_int y + [u128_to_int_int_to_u128_unfold] Theorem + + [oracles: DISK_THM] + [axioms: usize_bounds, u128_to_int_int_to_u128, isize_bounds] [] + ⊢ ∀n. u128_to_int (int_to_u128 n) = + if 0 ≤ n ∧ n ≤ u128_max then n else u128_to_int (int_to_u128 n) + [u16_add_eq] Theorem [oracles: DISK_THM] @@ -1876,6 +1944,13 @@ sig ∃z. u16_sub x y = Return z ∧ u16_to_int z = u16_to_int x − u16_to_int y + [u16_to_int_int_to_u16_unfold] Theorem + + [oracles: DISK_THM] + [axioms: usize_bounds, u16_to_int_int_to_u16, isize_bounds] [] + ⊢ ∀n. u16_to_int (int_to_u16 n) = + if 0 ≤ n ∧ n ≤ u16_max then n else u16_to_int (int_to_u16 n) + [u32_add_eq] Theorem [oracles: DISK_THM] @@ -1926,6 +2001,13 @@ sig ∃z. u32_sub x y = Return z ∧ u32_to_int z = u32_to_int x − u32_to_int y + [u32_to_int_int_to_u32_unfold] Theorem + + [oracles: DISK_THM] + [axioms: usize_bounds, u32_to_int_int_to_u32, isize_bounds] [] + ⊢ ∀n. u32_to_int (int_to_u32 n) = + if 0 ≤ n ∧ n ≤ u32_max then n else u32_to_int (int_to_u32 n) + [u64_add_eq] Theorem [oracles: DISK_THM] @@ -1976,6 +2058,13 @@ sig ∃z. u64_sub x y = Return z ∧ u64_to_int z = u64_to_int x − u64_to_int y + [u64_to_int_int_to_u64_unfold] Theorem + + [oracles: DISK_THM] + [axioms: usize_bounds, u64_to_int_int_to_u64, isize_bounds] [] + ⊢ ∀n. u64_to_int (int_to_u64 n) = + if 0 ≤ n ∧ n ≤ u64_max then n else u64_to_int (int_to_u64 n) + [u8_add_eq] Theorem [oracles: DISK_THM] @@ -2026,6 +2115,13 @@ sig ∃z. u8_sub x y = Return z ∧ u8_to_int z = u8_to_int x − u8_to_int y + [u8_to_int_int_to_u8_unfold] Theorem + + [oracles: DISK_THM] + [axioms: usize_bounds, u8_to_int_int_to_u8, isize_bounds] [] + ⊢ ∀n. u8_to_int (int_to_u8 n) = + if 0 ≤ n ∧ n ≤ u8_max then n else u8_to_int (int_to_u8 n) + [update_len] Theorem ⊢ ∀ls i y. len (update ls i y) = len ls @@ -2090,6 +2186,14 @@ sig ∃z. usize_sub x y = Return z ∧ usize_to_int z = usize_to_int x − usize_to_int y + [usize_to_int_int_to_usize_unfold] Theorem + + [oracles: DISK_THM] + [axioms: usize_bounds, usize_to_int_int_to_usize, isize_bounds] [] + ⊢ ∀n. usize_to_int (int_to_usize n) = + if 0 ≤ n ∧ n ≤ u16_max then n + else usize_to_int (int_to_usize n) + [vec_insert_back_spec] Theorem [oracles: DISK_THM] diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml index 0e16ead3..79026376 100644 --- a/backends/hol4/testHashmapScript.sml +++ b/backends/hol4/testHashmapScript.sml @@ -1,4 +1,3 @@ -open HolKernel boolLib bossLib Parse open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory |