diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 27 | ||||
| -rw-r--r-- | backends/hol4/primitivesLib.sml | 552 | ||||
| -rw-r--r-- | backends/hol4/testHashmapScript.sml | 550 | ||||
| -rw-r--r-- | backends/hol4/testHashmapTheory.sig | 202 |
4 files changed, 568 insertions, 763 deletions
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml index 3f298a04..28f8ab97 100644 --- a/backends/hol4/primitivesBaseTacLib.sml +++ b/backends/hol4/primitivesBaseTacLib.sml @@ -330,7 +330,7 @@ fun apply_dep_rewrites_match_concl_with_terms_tac val thms = map thm_to_conj_implies thms; in (* Apply each theorem *) - MAP_EVERY (sg_premise_then prove_premise then_tac) thms + map_every_tac (try_tac o sg_premise_then prove_premise then_tac) thms end (* Attempt to apply dependent rewrites with a theorem by matching its @@ -497,30 +497,35 @@ val dest_assums_conjs_tac : tactic = (* Defining those here so that they are evaluated once and for all (parsing depends on the context) *) val int_tac_int_ty = “:int” -val int_tac_pat = “(x : 'a) <> (y : 'a)” +val int_tac_num_ty = “:num” +val int_tac_pat1 = “(x : 'a) <> (y : 'a)” +val int_tac_pat2 = “(x : 'a) = (y : 'a)” (* We boost COOPER_TAC a bit *) fun int_tac (asms, g) = let (* Following the bug we discovered in COOPER_TAC, we filter all the - inequalities which terms are not between terms of type “:int”. + inequalities/equalities which terms are not between terms of type “:int” + or “:num”. TODO: issue/PR for HOL4 *) - fun keep (asm : term) : bool = + fun keep_with_pat (asm : term) (pat : term) : bool = let - val (_, s) = match_term int_tac_pat asm + val (_, s) = match_term pat asm in case s of - [{redex = _, residue = ty}] => ty = int_tac_int_ty + [{redex = _, residue = ty}] => (ty = int_tac_int_ty orelse ty = int_tac_num_ty) | [] => (* Can happen if the term has exactly the same types as the pattern - unlikely *) false | _ => failwith "int_tac: match error" end handle HOL_ERR _ => true - in - (dest_assums_conjs_tac >> - filter_assums_tac keep >> - first_tac [cooper_tac, exfalso >> cooper_tac]) (asms, g) - end + fun keep (asm : term) : bool = + forall (keep_with_pat asm) [int_tac_pat1, int_tac_pat2] + in + (dest_assums_conjs_tac >> + filter_assums_tac keep >> + first_tac [cooper_tac, exfalso >> cooper_tac]) (asms, g) + end end diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml index 5803c531..543ded23 100644 --- a/backends/hol4/primitivesLib.sml +++ b/backends/hol4/primitivesLib.sml @@ -1,9 +1,557 @@ (* Advanced tactics for the primitives library *) -structure primitivesBaseTacLib = +structure primitivesLib = struct open HolKernel boolLib bossLib Parse open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory -open primitivesBaseTacLib primitivesTheory + +open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory + +val primitives_theory_name = "primitives" + +(* Small utility: compute the set of assumptions in the context. + + We isolate this code in a utility in order to be able to improve it: + for now we simply put all the assumptions in a set, but in the future + we might want to split the assumptions which are conjunctions in order + to be more precise. + *) +fun compute_asms_set ((asms,g) : goal) : term Redblackset.set = + Redblackset.fromList Term.compare asms + +val integer_bounds_defs_list = [ + i8_min_def, + i8_max_def, + i16_min_def, + i16_max_def, + i32_min_def, + i32_max_def, + i64_min_def, + i64_max_def, + i128_min_def, + i128_max_def, + u8_max_def, + u16_max_def, + u32_max_def, + u64_max_def, + u128_max_def +] + +val integer_bounds_lemmas = + Redblackmap.fromList String.compare + [ + ("isize", isize_to_int_bounds), + ("i8", i8_to_int_bounds), + ("i16", i16_to_int_bounds), + ("i32", i32_to_int_bounds), + ("i64", i64_to_int_bounds), + ("i128", i128_to_int_bounds), + ("usize", usize_to_int_bounds), + ("u8", u8_to_int_bounds), + ("u16", u16_to_int_bounds), + ("u32", u32_to_int_bounds), + ("u64", u64_to_int_bounds), + ("u128", u128_to_int_bounds) + ] + +val integer_types_names = + Redblackset.fromList String.compare + (map fst (Redblackmap.listItems integer_bounds_lemmas)) + +(* See {!assume_bounds_for_all_int_vars}. + + This tactic is in charge of adding assumptions for one variable. + *) +fun assume_bounds_for_int_var + (asms_set: term Redblackset.set) (var : string) (ty : string) : + tactic = + let + (* Lookup the lemma to apply *) + val lemma = Redblackmap.find (integer_bounds_lemmas, ty); + (* Instantiate the lemma *) + val ty_t = mk_type (ty, []); + val var_t = mk_var (var, ty_t); + val lemma = SPEC var_t lemma; + (* Split the theorem into a list of conjuncts. + + The bounds are typically a conjunction: + {[ + ⊢ 0 ≤ u32_to_int x ∧ u32_to_int x ≤ u32_max: thm + ]} + *) + val lemmas = CONJUNCTS lemma; + (* Filter the conjuncts: some of them might already be in the context, + we don't want to introduce them again, as it would pollute it. + *) + val lemmas = filter (fn lem => not (Redblackset.member (asms_set, concl lem))) lemmas; + in + (* Introduce the assumptions in the context *) + assume_tacl lemmas + end + +(* Introduce bound assumptions for all the machine integers in the context. + + Exemple: + ======== + If there is “x : u32” in the input set, then we introduce: + {[ + 0 <= u32_to_int x + u32_to_int x <= u32_max + ]} + *) +fun assume_bounds_for_all_int_vars (asms, g) = + let + (* Compute the set of integer variables in the context *) + val vars = free_varsl (g :: asms); + (* Compute the set of assumptions already present in the context *) + val asms_set = compute_asms_set (asms, g); + val vartys_set = ref (Redblackset.empty String.compare); + (* Filter the variables to keep only the ones with type machine integer, + decompose the types at the same time *) + fun decompose_var (v : term) : (string * string) = + let + val (v, ty) = dest_var v; + val {Args=args, Thy=thy, Tyop=ty} = dest_thy_type ty; + val _ = assert null args; + val _ = assert (fn thy => thy = primitives_theory_name) thy; + val _ = assert (fn ty => Redblackset.member (integer_types_names, ty)) ty; + val _ = vartys_set := Redblackset.add (!vartys_set, ty); + in (v, ty) end; + val vars = mapfilter decompose_var vars; + (* Add assumptions for one variable *) + fun add_var_asm (v, ty) : tactic = + assume_bounds_for_int_var asms_set v ty; + (* Add the bounds for isize, usize *) + val size_bounds = + append + (if Redblackset.member (!vartys_set, "usize") then CONJUNCTS usize_bounds else []) + (if Redblackset.member (!vartys_set, "isize") then CONJUNCTS isize_bounds else []); + val size_bounds = + filter (fn th => not (Redblackset.member (asms_set, concl th))) size_bounds; + in + ((* Add assumptions for all the variables *) + map_every_tac add_var_asm vars >> + (* Add assumptions about the size bounds *) + assume_tacl size_bounds) (asms, g) + end + +val integer_conversion_lemmas_list = [ + isize_to_int_int_to_isize, + i8_to_int_int_to_i8, + i16_to_int_int_to_i16, + i32_to_int_int_to_i32, + i64_to_int_int_to_i64, + i128_to_int_int_to_i128, + usize_to_int_int_to_usize, + u8_to_int_int_to_u8, + u16_to_int_int_to_u16, + u32_to_int_int_to_u32, + u64_to_int_int_to_u64, + u128_to_int_int_to_u128 +] + +(* Look for conversions from integers to machine integers and back. + {[ + u32_to_int (int_to_u32 x) + ]} + + Attempts to prove and apply equalities of the form: + {[ + u32_to_int (int_to_u32 x) = x + ]} + *) +val rewrite_with_dep_int_lemmas : tactic = + (* We're not trying to be smart: we just try to rewrite with each theorem at + a time *) + let + val prove_premise = full_simp_tac simpLib.empty_ss integer_bounds_defs_list >> int_tac; + val then_tac1 = (fn th => full_simp_tac simpLib.empty_ss [th]); + val rewr_tac1 = apply_dep_rewrites_match_concl_with_all_tac prove_premise then_tac1; + val then_tac2 = (fn th => full_simp_tac simpLib.empty_ss [th]); + val rewr_tac2 = apply_dep_rewrites_match_first_premise_with_all_tac (fn _ => true) prove_premise then_tac2; + in + map_every_tac rewr_tac1 integer_conversion_lemmas_list >> + map_every_tac rewr_tac2 [] + end + +(* Massage a bit the goal, for instance by introducing integer bounds in the + assumptions. +*) +val massage : tactic = + assume_bounds_for_all_int_vars >> + rewrite_with_dep_int_lemmas + +(* Lexicographic order over pairs *) +fun pair_compare (comp1 : 'a * 'a -> order) (comp2 : 'b * 'b -> order) + ((p1, p2) : (('a * 'b) * ('a * 'b))) : order = + let + val (x1, y1) = p1; + val (x2, y2) = p2; + in + case comp1 (x1, x2) of + LESS => LESS + | GREATER => GREATER + | EQUAL => comp2 (y1, y2) + end + +(* A constant name (theory, constant name) *) +type const_name = string * string + +val const_name_compare = pair_compare String.compare String.compare + +(* The registered spec theorems, that {!progress} will automatically apply. + + The keys are the function names (it is a pair, because constant names + are made of the theory name and the name of the constant itself). + + Also note that we can store several specs per definition (in practice, when + looking up specs, we will try them all one by one, in a LIFO order). + + We store theorems where all the premises are in the goal, with implications + (i.e.: [⊢ H0 ==> ... ==> Hn ==> H], not [H0, ..., Hn ⊢ H]). + + We do this because, when doing proofs by induction, {!progress} might have to + handle *unregistered* theorems coming the current goal assumptions and of the shape + (the conclusion of the theorem is an assumption, and we want to ignore this assumption): + {[ + [∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒ + case nth ls i of + Return x => ... + | ... => ...] + ⊢ ∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒ + case nth ls i of + Return x => ... + | ... => ... + ]} + *) +val reg_spec_thms: (const_name, thm) Redblackmap.dict ref = + ref (Redblackmap.mkDict const_name_compare) + +(* Retrieve the specified application in a spec theorem. + + A spec theorem for a function [f] typically has the shape: + {[ + !x0 ... xn. + H0 ==> ... Hm ==> + (exists ... + (exists ... . f y0 ... yp = ... /\ ...) \/ + (exists ... . f y0 ... yp = ... /\ ...) \/ + ... + ]} + + Or: + {[ + !x0 ... xn. + H0 ==> ... Hm ==> + case f y0 ... yp of + ... => ... + | ... => ... + ]} + + We return: [f y0 ... yp] +*) +fun get_spec_app (t : term) : term = + let + (* Remove the universally quantified variables, the premises and + the existentially quantified variables *) + val t = (snd o strip_exists o snd o strip_imp o snd o strip_forall) t; + (* Remove the exists, take the first disjunct *) + val t = (hd o strip_disj o snd o strip_exists) t; + (* Split the conjunctions and take the first conjunct *) + val t = (hd o strip_conj) t; + (* Remove the case if there is, otherwise destruct the equality *) + val t = + if TypeBase.is_case t then let val (_, t, _) = TypeBase.dest_case t in t end + else (fst o dest_eq) t; + in t end + +(* Given a function call [f y0 ... yn] return the name of the function *) +fun get_fun_name_from_app (t : term) : const_name = + let + val f = (fst o strip_comb) t; + val {Name=name, Thy=thy, Ty=_} = dest_thy_const f; + val cn = (thy, name); + in cn end + +(* Register a spec theorem in the spec database. + + For the shape of spec theorems, see {!get_spec_thm_app}. + *) +fun register_spec_thm (th: thm) : unit = + let + (* Transform the theroem a bit before storing it *) + val th = SPEC_ALL th; + (* Retrieve the app ([f x0 ... xn]) *) + val f = get_spec_app (concl th); + (* Retrieve the function name *) + val cn = get_fun_name_from_app f; + in + (* Store *) + reg_spec_thms := Redblackmap.insert (!reg_spec_thms, cn, th) + end + +val all_add_eqs = [ + isize_add_eq, + i8_add_eq, + i16_add_eq, + i32_add_eq, + i64_add_eq, + i128_add_eq, + usize_add_eq, + u8_add_eq, + u16_add_eq, + u32_add_eq, + u64_add_eq, + u128_add_eq +] +val _ = app register_spec_thm all_add_eqs + +val all_sub_eqs = [ + isize_sub_eq, + i8_sub_eq, + i16_sub_eq, + i32_sub_eq, + i64_sub_eq, + i128_sub_eq, + usize_sub_eq, + u8_sub_eq, + u16_sub_eq, + u32_sub_eq, + u64_sub_eq, + u128_sub_eq +] +val _ = app register_spec_thm all_sub_eqs + +val all_mul_eqs = [ + isize_mul_eq, + i8_mul_eq, + i16_mul_eq, + i32_mul_eq, + i64_mul_eq, + i128_mul_eq, + usize_mul_eq, + u8_mul_eq, + u16_mul_eq, + u32_mul_eq, + u64_mul_eq, + u128_mul_eq +] +val _ = app register_spec_thm all_mul_eqs + +val all_div_eqs = [ + isize_div_eq, + i8_div_eq, + i16_div_eq, + i32_div_eq, + i64_div_eq, + i128_div_eq, + usize_div_eq, + u8_div_eq, + u16_div_eq, + u32_div_eq, + u64_div_eq, + u128_div_eq +] +val _ = app register_spec_thm all_div_eqs + +val all_rem_eqs = [ + isize_rem_eq, + i8_rem_eq, + i16_rem_eq, + i32_rem_eq, + i64_rem_eq, + i128_rem_eq, + usize_rem_eq, + u8_rem_eq, + u16_rem_eq, + u32_rem_eq, + u64_rem_eq, + u128_rem_eq +] +val _ = app register_spec_thm all_rem_eqs + +val all_vec_lems = [ + vec_len_spec, + vec_insert_back_spec +] +val _ = app register_spec_thm all_vec_lems + +(* Repeatedly destruct cases and return the last scrutinee we get *) +fun strip_all_cases_get_scrutinee (t : term) : term = + if TypeBase.is_case t + then (strip_all_cases_get_scrutinee o fst o TypeBase.strip_case) t + else t + +(* +TypeBase.dest_case “case ls of [] => T | _ => F” +TypeBase.strip_case “case ls of [] => T | _ => F” +TypeBase.strip_case “case (if b then [] else [0, 1]) of [] => T | _ => F” +TypeBase.strip_case “3” +TypeBase.dest_case “3” + +strip_all_cases_get_scrutinee “case ls of [] => T | _ => F” +strip_all_cases_get_scrutinee “case (if b then [] else [0, 1]) of [] => T | _ => F” +strip_all_cases_get_scrutinee “3” +*) + + +(* Provided the goal contains a call to a monadic function, return this function call. + + The goal should be of the shape: + 1. + {[ + case (* potentially expanded function body *) of + ... => ... + | ... => ... + ]} + + 2. Or: + {[ + exists ... . + ... (* potentially expanded function body *) = Return ... /\ + ... (* Various properties *) + ]} + + 3. Or a disjunction of cases like the one above, below existential binders + (actually: note sure this last case exists in practice): + {[ + exists ... . + (exists ... . (* body *) = Return ... /\ ...) \/ + ... + ]} + + The function body should be of the shape: + {[ + x <- f y0 ... yn; + ... + ]} + + Or (typically if we expanded the monadic binds): + {[ + case f y0 ... yn of + ... + ]} + + Or simply (typically if we reached the end of the function we're analyzing): + {[ + f y0 ... yn + ]} + + For all the above cases we would return [f y0 ... yn]. + *) +fun get_monadic_app_call (t : term) : term = + (* We do something slightly imprecise but hopefully general and robut *) + let + (* Case 3.: strip the existential binders, and take the first disjuntion *) + val t = (hd o strip_disj o snd o strip_exists) t; + (* Case 2.: strip the existential binders, and take the first conjunction *) + val t = (hd o strip_conj o snd o strip_exists) t; + (* If it is an equality, take the lhs *) + val t = if is_eq t then lhs t else t; + (* Expand the binders to transform them to cases *) + val t = + (rhs o concl) (REWRITE_CONV [bind_def] t) + handle UNCHANGED => t; + (* Strip all the cases *) + val t = strip_all_cases_get_scrutinee t; + in t end + +(* Use the given theorem to progress by one step (we use this when + analyzing a function body: this goes forward by one call to a monadic function). + + We transform the goal by: + - pushing the theorem premises to a subgoal + - adding the theorem conclusion in the assumptions in another goal, and + getting rid of the monadic call + + Then [then_tac] receives as paramter the monadic call on which we applied + the lemma. This can be useful, for instance, to make a case disjunction. + + This function is the most primitive of the [progress...] functions. + *) +fun pure_progress_with (premise_tac : tactic) + (then_tac : term -> thm_tactic) (th : thm) : tactic = + fn (asms,g) => + let + (* Remove all the universally quantified variables from the theorem *) + val th = SPEC_ALL th; + (* Retrieve the monadic call from the goal *) + val fgoal = get_monadic_app_call g; + (* Retrieve the app call from the theroem *) + val gth = get_spec_app (concl th); + (* Match and instantiate *) + val (var_s, ty_s) = match_term gth fgoal; + (* Instantiate the theorem *) + val th = INST var_s (INST_TYPE ty_s th); + (* Retrieve the premises of the theorem *) + val th = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] th; + in + (* Apply the theorem *) + sg_premise_then premise_tac (then_tac fgoal) th (asms, g) + end + +(* +val (asms, g) = top_goal () +val t = g + +val th = U32_SUB_EQ + +val premise_tac = massage >> TRY COOPER_TAC +fun then_tac fgoal = + fn thm => ASSUME_TAC thm >> Cases_on ‘^fgoal’ >> + rw [] >> fs [st_ex_bind_def] >> massage >> fs [] + +pure_progress_with premise_tac then_tac th +*) + +fun progress_with (th : thm) : tactic = + let + val premise_tac = massage >> fs [] >> rw [] >> TRY COOPER_TAC; + fun then_tac fgoal thm = + mp_tac thm >> strip_tac >> Cases_on ‘^fgoal’ >> + fs [bind_def] >> massage >> fs []; + in + pure_progress_with premise_tac then_tac th + end + +(* +progress_with U32_SUB_EQ +*) + +(* This function lookups the theorem to use to make progress *) +val progress : tactic = + fn (asms, g) => + let + (* Retrieve the monadic call from the goal *) + val fgoal = get_monadic_app_call g; + val fname = get_fun_name_from_app fgoal; + (* Lookup the theorem: first look in the assumptions (we might want to + use the inductive hypothesis for instance) *) + fun asm_to_spec asm = + let + (* Fail if there are no universal quantifiers *) + val _ = + if is_forall asm then asm + else assert is_forall ((snd o strip_imp) asm); + val asm_fname = (get_fun_name_from_app o get_spec_app) asm; + (* Fail if the name is not the one we're looking for *) + val _ = assert (fn n => fname = n) asm_fname; + in + ASSUME asm + end + val asms_thl = mapfilter asm_to_spec asms; + (* Lookup a spec in the database *) + val thl = + case Redblackmap.peek (!reg_spec_thms, fname) of + NONE => asms_thl + | SOME spec => spec :: asms_thl; + val _ = + if null thl then + raise (failwith "progress: could not find a suitable theorem to apply") + else (); + in + (* Attempt to use the theorems one by one *) + map_first_tac progress_with thl (asms, g) + end end diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml index 71b0109d..249bc0bf 100644 --- a/backends/hol4/testHashmapScript.sml +++ b/backends/hol4/testHashmapScript.sml @@ -2,556 +2,10 @@ open HolKernel boolLib bossLib Parse open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory +open primitivesLib val _ = new_theory "testHashmap" -val primitives_theory_name = "primitives" - -(* Small utility: compute the set of assumptions in the context. - - We isolate this code in a utility in order to be able to improve it: - for now we simply put all the assumptions in a set, but in the future - we might want to split the assumptions which are conjunctions in order - to be more precise. - *) -fun compute_asms_set ((asms,g) : goal) : term Redblackset.set = - Redblackset.fromList Term.compare asms - -val integer_bounds_defs_list = [ - i8_min_def, - i8_max_def, - i16_min_def, - i16_max_def, - i32_min_def, - i32_max_def, - i64_min_def, - i64_max_def, - i128_min_def, - i128_max_def, - u8_max_def, - u16_max_def, - u32_max_def, - u64_max_def, - u128_max_def -] - -val integer_bounds_lemmas = - Redblackmap.fromList String.compare - [ - ("isize", isize_to_int_bounds), - ("i8", i8_to_int_bounds), - ("i16", i16_to_int_bounds), - ("i32", i32_to_int_bounds), - ("i64", i64_to_int_bounds), - ("i128", i128_to_int_bounds), - ("usize", usize_to_int_bounds), - ("u8", u8_to_int_bounds), - ("u16", u16_to_int_bounds), - ("u32", u32_to_int_bounds), - ("u64", u64_to_int_bounds), - ("u128", u128_to_int_bounds) - ] - -val integer_types_names = - Redblackset.fromList String.compare - (map fst (Redblackmap.listItems integer_bounds_lemmas)) - -(* See {!assume_bounds_for_all_int_vars}. - - This tactic is in charge of adding assumptions for one variable. - *) -fun assume_bounds_for_int_var - (asms_set: term Redblackset.set) (var : string) (ty : string) : - tactic = - let - (* Lookup the lemma to apply *) - val lemma = Redblackmap.find (integer_bounds_lemmas, ty); - (* Instantiate the lemma *) - val ty_t = mk_type (ty, []); - val var_t = mk_var (var, ty_t); - val lemma = SPEC var_t lemma; - (* Split the theorem into a list of conjuncts. - - The bounds are typically a conjunction: - {[ - ⊢ 0 ≤ u32_to_int x ∧ u32_to_int x ≤ u32_max: thm - ]} - *) - val lemmas = CONJUNCTS lemma; - (* Filter the conjuncts: some of them might already be in the context, - we don't want to introduce them again, as it would pollute it. - *) - val lemmas = filter (fn lem => not (Redblackset.member (asms_set, concl lem))) lemmas; - in - (* Introduce the assumptions in the context *) - assume_tacl lemmas - end - -(* Introduce bound assumptions for all the machine integers in the context. - - Exemple: - ======== - If there is “x : u32” in the input set, then we introduce: - {[ - 0 <= u32_to_int x - u32_to_int x <= u32_max - ]} - *) -fun assume_bounds_for_all_int_vars (asms, g) = - let - (* Compute the set of integer variables in the context *) - val vars = free_varsl (g :: asms); - (* Compute the set of assumptions already present in the context *) - val asms_set = compute_asms_set (asms, g); - val vartys_set = ref (Redblackset.empty String.compare); - (* Filter the variables to keep only the ones with type machine integer, - decompose the types at the same time *) - fun decompose_var (v : term) : (string * string) = - let - val (v, ty) = dest_var v; - val {Args=args, Thy=thy, Tyop=ty} = dest_thy_type ty; - val _ = assert null args; - val _ = assert (fn thy => thy = primitives_theory_name) thy; - val _ = assert (fn ty => Redblackset.member (integer_types_names, ty)) ty; - val _ = vartys_set := Redblackset.add (!vartys_set, ty); - in (v, ty) end; - val vars = mapfilter decompose_var vars; - (* Add assumptions for one variable *) - fun add_var_asm (v, ty) : tactic = - assume_bounds_for_int_var asms_set v ty; - (* Add the bounds for isize, usize *) - val size_bounds = - append - (if Redblackset.member (!vartys_set, "usize") then CONJUNCTS usize_bounds else []) - (if Redblackset.member (!vartys_set, "isize") then CONJUNCTS isize_bounds else []); - val size_bounds = - filter (fn th => not (Redblackset.member (asms_set, concl th))) size_bounds; - in - ((* Add assumptions for all the variables *) - map_every_tac add_var_asm vars >> - (* Add assumptions about the size bounds *) - assume_tacl size_bounds) (asms, g) - end - -val integer_conversion_lemmas_list = [ - isize_to_int_int_to_isize, - i8_to_int_int_to_i8, - i16_to_int_int_to_i16, - i32_to_int_int_to_i32, - i64_to_int_int_to_i64, - i128_to_int_int_to_i128, - usize_to_int_int_to_usize, - u8_to_int_int_to_u8, - u16_to_int_int_to_u16, - u32_to_int_int_to_u32, - u64_to_int_int_to_u64, - u128_to_int_int_to_u128 -] - -(* Look for conversions from integers to machine integers and back. - {[ - u32_to_int (int_to_u32 x) - ]} - - Attempts to prove and apply equalities of the form: - {[ - u32_to_int (int_to_u32 x) = x - ]} - *) -val rewrite_with_dep_int_lemmas : tactic = - (* We're not trying to be smart: we just try to rewrite with each theorem at - a time *) - let - val prove_premise = full_simp_tac simpLib.empty_ss integer_bounds_defs_list >> cooper_tac; - val then_tac1 = (fn th => full_simp_tac simpLib.empty_ss [th]); - val rewr_tac1 = apply_dep_rewrites_match_concl_with_all_tac prove_premise then_tac1; - val then_tac2 = (fn th => full_simp_tac simpLib.empty_ss [th]); - val rewr_tac2 = apply_dep_rewrites_match_first_premise_with_all_tac (fn _ => true) prove_premise then_tac2; - in - map_every_tac rewr_tac1 integer_conversion_lemmas_list >> - map_every_tac rewr_tac2 [] - end - -(* Massage a bit the goal, for instance by introducing integer bounds in the - assumptions. -*) -val massage : tactic = - assume_bounds_for_all_int_vars >> - rewrite_with_dep_int_lemmas - -(* Lexicographic order over pairs *) -fun pair_compare (comp1 : 'a * 'a -> order) (comp2 : 'b * 'b -> order) - ((p1, p2) : (('a * 'b) * ('a * 'b))) : order = - let - val (x1, y1) = p1; - val (x2, y2) = p2; - in - case comp1 (x1, x2) of - LESS => LESS - | GREATER => GREATER - | EQUAL => comp2 (y1, y2) - end - -(* A constant name (theory, constant name) *) -type const_name = string * string - -val const_name_compare = pair_compare String.compare String.compare - -(* The registered spec theorems, that {!progress} will automatically apply. - - The keys are the function names (it is a pair, because constant names - are made of the theory name and the name of the constant itself). - - Also note that we can store several specs per definition (in practice, when - looking up specs, we will try them all one by one, in a LIFO order). - - We store theorems where all the premises are in the goal, with implications - (i.e.: [⊢ H0 ==> ... ==> Hn ==> H], not [H0, ..., Hn ⊢ H]). - - We do this because, when doing proofs by induction, {!progress} might have to - handle *unregistered* theorems coming the current goal assumptions and of the shape - (the conclusion of the theorem is an assumption, and we want to ignore this assumption): - {[ - [∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒ - case nth ls i of - Return x => ... - | ... => ...] - ⊢ ∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒ - case nth ls i of - Return x => ... - | ... => ... - ]} - *) -val reg_spec_thms: (const_name, thm) Redblackmap.dict ref = - ref (Redblackmap.mkDict const_name_compare) - -(* Retrieve the specified application in a spec theorem. - - A spec theorem for a function [f] typically has the shape: - {[ - !x0 ... xn. - H0 ==> ... Hm ==> - (exists ... - (exists ... . f y0 ... yp = ... /\ ...) \/ - (exists ... . f y0 ... yp = ... /\ ...) \/ - ... - ]} - - Or: - {[ - !x0 ... xn. - H0 ==> ... Hm ==> - case f y0 ... yp of - ... => ... - | ... => ... - ]} - - We return: [f y0 ... yp] -*) -fun get_spec_app (t : term) : term = - let - (* Remove the universally quantified variables, the premises and - the existentially quantified variables *) - val t = (snd o strip_exists o snd o strip_imp o snd o strip_forall) t; - (* Remove the exists, take the first disjunct *) - val t = (hd o strip_disj o snd o strip_exists) t; - (* Split the conjunctions and take the first conjunct *) - val t = (hd o strip_conj) t; - (* Remove the case if there is, otherwise destruct the equality *) - val t = - if TypeBase.is_case t then let val (_, t, _) = TypeBase.dest_case t in t end - else (fst o dest_eq) t; - in t end - -(* Given a function call [f y0 ... yn] return the name of the function *) -fun get_fun_name_from_app (t : term) : const_name = - let - val f = (fst o strip_comb) t; - val {Name=name, Thy=thy, Ty=_} = dest_thy_const f; - val cn = (thy, name); - in cn end - -(* Register a spec theorem in the spec database. - - For the shape of spec theorems, see {!get_spec_thm_app}. - *) -fun register_spec_thm (th: thm) : unit = - let - (* Transform the theroem a bit before storing it *) - val th = SPEC_ALL th; - (* Retrieve the app ([f x0 ... xn]) *) - val f = get_spec_app (concl th); - (* Retrieve the function name *) - val cn = get_fun_name_from_app f; - in - (* Store *) - reg_spec_thms := Redblackmap.insert (!reg_spec_thms, cn, th) - end - -val all_add_eqs = [ - isize_add_eq, - i8_add_eq, - i16_add_eq, - i32_add_eq, - i64_add_eq, - i128_add_eq, - usize_add_eq, - u8_add_eq, - u16_add_eq, - u32_add_eq, - u64_add_eq, - u128_add_eq -] -val _ = app register_spec_thm all_add_eqs - -val all_sub_eqs = [ - isize_sub_eq, - i8_sub_eq, - i16_sub_eq, - i32_sub_eq, - i64_sub_eq, - i128_sub_eq, - usize_sub_eq, - u8_sub_eq, - u16_sub_eq, - u32_sub_eq, - u64_sub_eq, - u128_sub_eq -] -val _ = app register_spec_thm all_sub_eqs - -val all_mul_eqs = [ - isize_mul_eq, - i8_mul_eq, - i16_mul_eq, - i32_mul_eq, - i64_mul_eq, - i128_mul_eq, - usize_mul_eq, - u8_mul_eq, - u16_mul_eq, - u32_mul_eq, - u64_mul_eq, - u128_mul_eq -] -val _ = app register_spec_thm all_mul_eqs - -val all_div_eqs = [ - isize_div_eq, - i8_div_eq, - i16_div_eq, - i32_div_eq, - i64_div_eq, - i128_div_eq, - usize_div_eq, - u8_div_eq, - u16_div_eq, - u32_div_eq, - u64_div_eq, - u128_div_eq -] -val _ = app register_spec_thm all_div_eqs - -val all_rem_eqs = [ - isize_rem_eq, - i8_rem_eq, - i16_rem_eq, - i32_rem_eq, - i64_rem_eq, - i128_rem_eq, - usize_rem_eq, - u8_rem_eq, - u16_rem_eq, - u32_rem_eq, - u64_rem_eq, - u128_rem_eq -] -val _ = app register_spec_thm all_rem_eqs - -val all_vec_lems = [ - vec_len_spec, - vec_insert_back_spec -] -val _ = app register_spec_thm all_vec_lems - -(* Repeatedly destruct cases and return the last scrutinee we get *) -fun strip_all_cases_get_scrutinee (t : term) : term = - if TypeBase.is_case t - then (strip_all_cases_get_scrutinee o fst o TypeBase.strip_case) t - else t - -(* -TypeBase.dest_case “case ls of [] => T | _ => F” -TypeBase.strip_case “case ls of [] => T | _ => F” -TypeBase.strip_case “case (if b then [] else [0, 1]) of [] => T | _ => F” -TypeBase.strip_case “3” -TypeBase.dest_case “3” - -strip_all_cases_get_scrutinee “case ls of [] => T | _ => F” -strip_all_cases_get_scrutinee “case (if b then [] else [0, 1]) of [] => T | _ => F” -strip_all_cases_get_scrutinee “3” -*) - - -(* Provided the goal contains a call to a monadic function, return this function call. - - The goal should be of the shape: - 1. - {[ - case (* potentially expanded function body *) of - ... => ... - | ... => ... - ]} - - 2. Or: - {[ - exists ... . - ... (* potentially expanded function body *) = Return ... /\ - ... (* Various properties *) - ]} - - 3. Or a disjunction of cases like the one above, below existential binders - (actually: note sure this last case exists in practice): - {[ - exists ... . - (exists ... . (* body *) = Return ... /\ ...) \/ - ... - ]} - - The function body should be of the shape: - {[ - x <- f y0 ... yn; - ... - ]} - - Or (typically if we expanded the monadic binds): - {[ - case f y0 ... yn of - ... - ]} - - Or simply (typically if we reached the end of the function we're analyzing): - {[ - f y0 ... yn - ]} - - For all the above cases we would return [f y0 ... yn]. - *) -fun get_monadic_app_call (t : term) : term = - (* We do something slightly imprecise but hopefully general and robut *) - let - (* Case 3.: strip the existential binders, and take the first disjuntion *) - val t = (hd o strip_disj o snd o strip_exists) t; - (* Case 2.: strip the existential binders, and take the first conjunction *) - val t = (hd o strip_conj o snd o strip_exists) t; - (* If it is an equality, take the lhs *) - val t = if is_eq t then lhs t else t; - (* Expand the binders to transform them to cases *) - val t = - (rhs o concl) (REWRITE_CONV [bind_def] t) - handle UNCHANGED => t; - (* Strip all the cases *) - val t = strip_all_cases_get_scrutinee t; - in t end - -(* Use the given theorem to progress by one step (we use this when - analyzing a function body: this goes forward by one call to a monadic function). - - We transform the goal by: - - pushing the theorem premises to a subgoal - - adding the theorem conclusion in the assumptions in another goal, and - getting rid of the monadic call - - Then [then_tac] receives as paramter the monadic call on which we applied - the lemma. This can be useful, for instance, to make a case disjunction. - - This function is the most primitive of the [progress...] functions. - *) -fun pure_progress_with (premise_tac : tactic) - (then_tac : term -> thm_tactic) (th : thm) : tactic = - fn (asms,g) => - let - (* Remove all the universally quantified variables from the theorem *) - val th = SPEC_ALL th; - (* Retrieve the monadic call from the goal *) - val fgoal = get_monadic_app_call g; - (* Retrieve the app call from the theroem *) - val gth = get_spec_app (concl th); - (* Match and instantiate *) - val (var_s, ty_s) = match_term gth fgoal; - (* Instantiate the theorem *) - val th = INST var_s (INST_TYPE ty_s th); - (* Retrieve the premises of the theorem *) - val th = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] th; - in - (* Apply the theorem *) - sg_premise_then premise_tac (then_tac fgoal) th (asms, g) - end - -(* -val (asms, g) = top_goal () -val t = g - -val th = U32_SUB_EQ - -val premise_tac = massage >> TRY COOPER_TAC -fun then_tac fgoal = - fn thm => ASSUME_TAC thm >> Cases_on ‘^fgoal’ >> - rw [] >> fs [st_ex_bind_def] >> massage >> fs [] - -pure_progress_with premise_tac then_tac th -*) - -fun progress_with (th : thm) : tactic = - let - val premise_tac = massage >> fs [] >> rw [] >> TRY COOPER_TAC; - fun then_tac fgoal thm = - ASSUME_TAC thm >> Cases_on ‘^fgoal’ >> - rw [] >> fs [bind_def] >> massage >> fs []; - in - pure_progress_with premise_tac then_tac th - end - -(* -progress_with U32_SUB_EQ -*) - -(* This function lookups the theorem to use to make progress *) -val progress : tactic = - fn (asms, g) => - let - (* Retrieve the monadic call from the goal *) - val fgoal = get_monadic_app_call g; - val fname = get_fun_name_from_app fgoal; - (* Lookup the theorem: first look in the assumptions (we might want to - use the inductive hypothesis for instance) *) - fun asm_to_spec asm = - let - (* Fail if there are no universal quantifiers *) - val _ = - if is_forall asm then asm - else assert is_forall ((snd o strip_imp) asm); - val asm_fname = (get_fun_name_from_app o get_spec_app) asm; - (* Fail if the name is not the one we're looking for *) - val _ = assert (fn n => fname = n) asm_fname; - in - ASSUME asm - end - val asms_thl = mapfilter asm_to_spec asms; - (* Lookup a spec in the database *) - val thl = - case Redblackmap.peek (!reg_spec_thms, fname) of - NONE => asms_thl - | SOME spec => spec :: asms_thl; - val _ = - if null thl then - raise (failwith "progress: could not find a suitable theorem to apply") - else (); - in - (* Attempt to use the theorems one by one *) - map_first_tac progress_with thl (asms, g) - end - (* * Examples of proofs *) @@ -594,7 +48,7 @@ Proof exfalso >> cooper_tac QED -Theorem nth_mut_fwd_lem: +Theorem nth_mut_fwd_spec: !(ls : 't list_t) (i : u32). u32_to_int i < len (list_t_v ls) ==> case nth_mut_fwd ls i of diff --git a/backends/hol4/testHashmapTheory.sig b/backends/hol4/testHashmapTheory.sig deleted file mode 100644 index a08511cd..00000000 --- a/backends/hol4/testHashmapTheory.sig +++ /dev/null @@ -1,202 +0,0 @@ -signature testHashmapTheory = -sig - type thm = Thm.thm - - (* Axioms *) - val insert_def : thm - - (* Definitions *) - val distinct_keys_def : thm - val list_t_TY_DEF : thm - val list_t_case_def : thm - val list_t_size_def : thm - val list_t_v_def : thm - val lookup_def : thm - - (* Theorems *) - val datatype_list_t : thm - val index_eq : thm - val insert_lem : thm - val list_t_11 : thm - val list_t_Axiom : thm - val list_t_case_cong : thm - val list_t_case_eq : thm - val list_t_distinct : thm - val list_t_induction : thm - val list_t_nchotomy : thm - val lookup_raw_def : thm - val lookup_raw_ind : thm - val nth_mut_fwd_def : thm - val nth_mut_fwd_ind : thm - val nth_mut_fwd_lem : thm - - val testHashmap_grammars : type_grammar.grammar * term_grammar.grammar -(* - [primitives] Parent theory of "testHashmap" - - [insert_def] Axiom - - [oracles: ] [axioms: insert_def] [] - ⊢ insert key value ls = - case ls of - ListCons (ckey,cvalue) tl => - if ckey = key then Return (ListCons (ckey,value) tl) - else - do - tl0 <- insert key value tl; - Return (ListCons (ckey,cvalue) tl0) - od - | ListNil => Return (ListCons (key,value) ListNil) - - [distinct_keys_def] Definition - - ⊢ ∀ls. - distinct_keys ls ⇔ - ∀i j. - 0 < i ⇒ - i < len ls ⇒ - 0 < j ⇒ - j < len ls ⇒ - FST (index i ls) = FST (index j ls) ⇒ - i = j - - [list_t_TY_DEF] Definition - - ⊢ ∃rep. - TYPE_DEFINITION - (λa0'. - ∀ $var$('list_t'). - (∀a0'. - (∃a0 a1. - a0' = - (λa0 a1. - ind_type$CONSTR 0 a0 - (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) - a0 a1 ∧ $var$('list_t') a1) ∨ - a0' = - ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒ - $var$('list_t') a0') ⇒ - $var$('list_t') a0') rep - - [list_t_case_def] Definition - - ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧ - ∀f v. list_t_CASE ListNil f v = v - - [list_t_size_def] Definition - - ⊢ (∀f a0 a1. - list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧ - ∀f. list_t_size f ListNil = 0 - - [list_t_v_def] Definition - - ⊢ list_t_v ListNil = [] ∧ - ∀x tl. list_t_v (ListCons x tl) = x::list_t_v tl - - [lookup_def] Definition - - ⊢ ∀key ls. lookup key ls = lookup_raw key (list_t_v ls) - - [datatype_list_t] Theorem - - ⊢ DATATYPE (list_t ListCons ListNil) - - [index_eq] Theorem - - ⊢ (∀x ls. index 0 (x::ls) = x) ∧ - ∀i x ls. - index i (x::ls) = - if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then index (i − 1) ls - else if i = 0 then x - else ARB - - [insert_lem] Theorem - - [oracles: DISK_THM] [axioms: insert_def] [] - ⊢ ∀ls key value. - distinct_keys (list_t_v ls) ⇒ - case insert key value ls of - Return ls1 => - lookup key ls1 = SOME value ∧ - ∀k. k ≠ key ⇒ lookup k ls = lookup k ls1 - | Fail v1 => F - | Loop => F - - [list_t_11] Theorem - - ⊢ ∀a0 a1 a0' a1'. - ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1' - - [list_t_Axiom] Theorem - - ⊢ ∀f0 f1. ∃fn. - (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧ - fn ListNil = f1 - - [list_t_case_cong] Theorem - - ⊢ ∀M M' f v. - M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧ - (M' = ListNil ⇒ v = v') ⇒ - list_t_CASE M f v = list_t_CASE M' f' v' - - [list_t_case_eq] Theorem - - ⊢ list_t_CASE x f v = v' ⇔ - (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v' - - [list_t_distinct] Theorem - - ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil - - [list_t_induction] Theorem - - ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l - - [list_t_nchotomy] Theorem - - ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil - - [lookup_raw_def] Theorem - - ⊢ (∀key. lookup_raw key [] = NONE) ∧ - ∀v ls key k. - lookup_raw key ((k,v)::ls) = - if k = key then SOME v else lookup_raw key ls - - [lookup_raw_ind] Theorem - - ⊢ ∀P. (∀key. P key []) ∧ - (∀key k v ls. (k ≠ key ⇒ P key ls) ⇒ P key ((k,v)::ls)) ⇒ - ∀v v1. P v v1 - - [nth_mut_fwd_def] Theorem - - ⊢ ∀ls i. - nth_mut_fwd ls i = - case ls of - ListCons x tl => - if u32_to_int i = 0 then Return x - else do i0 <- u32_sub i (int_to_u32 1); nth_mut_fwd tl i0 od - | ListNil => Fail Failure - - [nth_mut_fwd_ind] Theorem - - ⊢ ∀P. (∀ls i. - (∀x tl i0. ls = ListCons x tl ∧ u32_to_int i ≠ 0 ⇒ P tl i0) ⇒ - P ls i) ⇒ - ∀v v1. P v v1 - - [nth_mut_fwd_lem] Theorem - - ⊢ ∀ls i. - u32_to_int i < len (list_t_v ls) ⇒ - case nth_mut_fwd ls i of - Return x => x = index (u32_to_int i) (list_t_v ls) - | Fail v1 => F - | Loop => F - - -*) -end |