From f38453602b71d71079e8f39e8a9e8b16048bd11f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 10 Mar 2025 21:06:22 -0700 Subject: [PATCH 1/2] Actually test more asm functions --- fiat-amd64/gentest.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/fiat-amd64/gentest.py b/fiat-amd64/gentest.py index ee50d4ce1b..a4f0a83430 100755 --- a/fiat-amd64/gentest.py +++ b/fiat-amd64/gentest.py @@ -46,7 +46,7 @@ def removeprefix(s, prefix): asm_op_names = OrderedDict() -regex = re.compile(r'fiat_(?P[^_]+(_(solinas|montgomery|dettman))?)_(?P(carry_)?(square|mul))') +regex = re.compile(r'fiat_(?P[^_]+(_(solinas|montgomery|dettman))?)_(?P(carry_)?(square|mul|from_bytes|to_bytes|add|sub|opp))') for dirname in directories: m = regex.match(os.path.basename(dirname)) if m: From a73ce709db9f03c8d35117b957e95283fc829887 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 7 Mar 2025 11:33:04 -0800 Subject: [PATCH 2/2] Set array sizes from bounds Fix #2040 (I hope) Still TODO: add a test-case for this based on from_bytes assembly --- src/Assembly/Equivalence.v | 81 +++++--- src/Assembly/EquivalenceProofs.v | 239 ++++++++++++++-------- src/Assembly/WithBedrock/Proofs.v | 123 +++++------ src/Assembly/WithBedrock/SymbolicProofs.v | 6 +- src/Util/ZUtil/Land.v | 4 +- 5 files changed, 266 insertions(+), 187 deletions(-) diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v index 2006770e83..de40f9ad38 100644 --- a/src/Assembly/Equivalence.v +++ b/src/Assembly/Equivalence.v @@ -222,7 +222,7 @@ Inductive EquivalenceCheckingError := | Internal_error_output_load_failed (_ : option Symbolic.error) (_ : list ((REG + idx) + idx)) (_ : symbolic_state) | Internal_error_extra_input_arguments (t : API.type) (unused_arguments : list (idx + list idx)) | Internal_error_lingering_memory (_ : symbolic_state) -| Internal_error_LoadOutputs_length_mismatch (outputaddrs : list ((REG + idx) + idx)) (output_types : list (option nat)) +| Internal_error_LoadOutputs_length_mismatch (outputaddrs : list ((REG + idx) + idx)) (output_types : list (N * (option nat))) | Not_enough_registers (num_given num_extra_needed : nat) | Registers_too_narrow (bad_reg : list REG) | Callee_saved_registers_too_narrow (bad_reg : list REG) @@ -233,6 +233,9 @@ Inductive EquivalenceCheckingError := | Expected_const_in_reference_code (_ : idx) | Expected_power_of_two (w : N) (_ : idx) | Unknown_array_length (t : base.type) +| Unknown_array_bounds {t : base.type} (bs : list (ZRange.type.base.option.interp t)) +| Unknown_scalar_size (t : base.type) +| Invalid_zero_size_array (t : base.type) | Registers_not_saved (regs : list (REG * (idx (* before *) * idx (* after *)))) (_ : symbolic_state) | Invalid_arrow_type (t : API.type) | Invalid_argument_type (t : API.type) @@ -266,6 +269,9 @@ Definition symbolic_state_of_EquivalenceCheckingError (e : EquivalenceCheckingEr | Expected_const_in_reference_code _ | Expected_power_of_two _ _ | Unknown_array_length _ + | Unknown_scalar_size _ + | Unknown_array_bounds _ _ + | Invalid_zero_size_array _ | Invalid_arrow_type _ | Invalid_argument_type _ | Invalid_return_type _ @@ -708,6 +714,9 @@ Global Instance show_lines_EquivalenceCheckingError : ShowLines EquivalenceCheck | Invalid_return_type t => ["Invalid type for return: " ++ show t]%string | Unknown_array_length t => ["Unknown array length of type " ++ show t ++ "."]%string + | Unknown_array_bounds t bs => ["Unknown array bounds of type " ++ show t ++ ": " ++ show bs]%string + | Unknown_scalar_size t => ["Unknown scalar size of type " ++ show t ++ "."]%string + | Invalid_zero_size_array t => ["Array of type " ++ show t ++ " has zero size."]%string | Invalid_arrow_type t => ["Invalid higher order function involving the type " ++ show t ++ "."]%string | Invalid_higher_order_application var s d f x => let __ := @Compilers.ToString.PHOAS.expr.partially_show_expr in @@ -780,7 +789,7 @@ Definition RevealWidth (i : idx) : symexM N := then symex_return w else symex_error (Expected_power_of_two s i). -Definition type_spec := list (option nat). (* list of array lengths; None means not an array *) +Definition type_spec := list (N * option nat). (* list of element size in bytes * length; None means not an array *) (** Convert PHOAS info about types and argument bounds into a simplified specification *) Fixpoint simplify_base_type @@ -789,18 +798,24 @@ Fixpoint simplify_base_type := match t return ZRange.type.base.option.interp t -> _ with | base.type.unit => fun 'tt => Success [] - | base.type.type_base base.type.Z - => fun _ => Success [None] + | (base.type.type_base base.type.Z) as t + => fun r + => match ZRange.type.base.option.lift_Some r with + | Some r => Success [(Z.to_N (ZRange.type.base.bitwidth r), None)] + | None => Error (Unknown_scalar_size t) + end | base.type.prod A B => fun '(bA, bB) => (vA <- simplify_base_type A bA; vB <- simplify_base_type B bB; Success (vA ++ vB)) - | base.type.list (base.type.type_base base.type.Z) + | (base.type.list (base.type.type_base base.type.Z as tZ)) as t => fun b - => match b with - | None => Error (Unknown_array_length t) - | Some bs => Success [Some (List.length bs)] + => match b, option_map ZRange.type.base.bitwidth (ZRange.type.base.option.lift_Some b) with + | None, _ => Error (Unknown_array_length t) + | Some b, None => Error (@Unknown_array_bounds tZ b) + | Some nil, _ | _, Some nil => Error (Invalid_zero_size_array t) + | Some _, Some bs => Success [(Z.to_N (List.fold_right Z.max 0%Z bs), Some (List.length bs))] end | base.type.type_base _ | base.type.option _ @@ -829,39 +844,39 @@ Fixpoint simplify_input_type Definition build_inputarray {descr:description} (len : nat) : dag.M (list idx) := List.foldmap (fun _ => merge_fresh_symbol) (List.seq 0 len). -Fixpoint build_inputs {descr:description} (types : type_spec) : dag.M (list (idx + list idx)) +Fixpoint build_inputs {descr:description} (types : type_spec) : dag.M (list (N * (idx + list idx))) := match types with | [] => dag.ret [] - | None :: tys + | (sz, None) :: tys => (idx <- merge_fresh_symbol; rest <- build_inputs tys; - dag.ret (inl idx :: rest)) - | Some len :: tys + dag.ret ((sz, inl idx) :: rest)) + | (sz, Some len) :: tys => (idxs <- build_inputarray len; rest <- build_inputs tys; - dag.ret (inr idxs :: rest)) + dag.ret ((sz, inr idxs) :: rest)) end%dagM. (* we factor this out so that conversion is not slow when proving things about this *) -Definition compute_array_address {opts : symbolic_options_computed_opt} {descr:description} (base : idx) (i : nat) - := (offset <- Symbolic.App (zconst 64%N (8 * Z.of_nat i), nil); +Definition compute_array_address {opts : symbolic_options_computed_opt} {descr:description} {bytes_per_element : N} (base : idx) (i : nat) + := (offset <- Symbolic.App (zconst 64%N (Z.of_N bytes_per_element * Z.of_nat i), nil); Symbolic.App (add 64%N, [base; offset]))%x86symex. -Definition build_merge_array_addresses {opts : symbolic_options_computed_opt} {descr:description} (base : idx) (items : list idx) : M (list idx) +Definition build_merge_array_addresses {opts : symbolic_options_computed_opt} {descr:description} {bytes_per_element : N} (base : idx) (items : list idx) : M (list idx) := mapM (fun '(i, idx) => - (addr <- compute_array_address base i; + (addr <- compute_array_address (bytes_per_element:=bytes_per_element) base i; (fun s => Success (addr, update_mem_with s (cons (addr,idx))))) )%x86symex (List.enumerate items). -Fixpoint build_merge_base_addresses {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} (items : list (idx + list idx)) (reg_available : list REG) : M (list ((REG + idx) + idx)) +Fixpoint build_merge_base_addresses {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} (items : list (N * (idx + list idx))) (reg_available : list REG) : M (list ((REG + idx) + idx)) := match items, reg_available with | [], _ | _, [] => Symbolic.ret [] - | inr idxs :: xs, r :: reg_available + | (sz, inr idxs) :: xs, r :: reg_available => (base <- SetRegFresh r; (* note: overwrites initial value *) - addrs <- build_merge_array_addresses base idxs; (* note: overwrites initial value *) + addrs <- build_merge_array_addresses (bytes_per_element:=sz) base idxs; (* note: overwrites initial value *) rest <- build_merge_base_addresses (dereference_scalar:=dereference_scalar) xs reg_available; Symbolic.ret (inr base :: rest)) - | inl idx :: xs, r :: reg_available => + | (_sz, inl idx) :: xs, r :: reg_available => (addr <- (if dereference_scalar then (addr <- SetRegFresh r; @@ -1273,10 +1288,10 @@ Definition symex_PHOAS_PHOAS {opts : symbolic_options_computed_opt} {t} (expr : Definition symex_PHOAS {opts : symbolic_options_computed_opt} {t} (expr : API.Expr t) - (inputs : list (idx + list idx)) + (inputs : list (N * (idx + list idx))) (d : dag) : ErrorT EquivalenceCheckingError (list (idx + list idx) * dag) - := (input_var_data <- build_input_var t inputs; + := (input_var_data <- build_input_var t (List.map snd inputs); let '(input_var_data, unused_inputs) := input_var_data in _ <- (if (List.length unused_inputs =? 0)%nat then Success tt @@ -1307,18 +1322,18 @@ Definition build_merge_stack_placeholders {opts : symbolic_options_computed_opt} : M idx := (stack_placeholders <- lift_dag (build_inputarray stack_size); stack_base <- compute_stack_base stack_size; - _ <- build_merge_array_addresses stack_base stack_placeholders; + _ <- build_merge_array_addresses (bytes_per_element:=8) stack_base stack_placeholders; ret stack_base)%x86symex. -Definition LoadArray {opts : symbolic_options_computed_opt} {descr:description} (base : idx) (len : nat) : M (list idx) +Definition LoadArray {opts : symbolic_options_computed_opt} {descr:description} {bytes_per_element : N} (base : idx) (len : nat) : M (list idx) := mapM (fun i => - (addr <- compute_array_address base i; + (addr <- compute_array_address (bytes_per_element:=bytes_per_element) base i; Remove64 addr)%x86symex) (seq 0 len). Definition LoadOutputs_internal {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} (outputaddrs : list ((REG + idx) + idx)) (output_types : type_spec) : M (list (idx + list idx)) - := (mapM (fun '(ocells, spec) => + := (mapM (fun '(ocells, (sz, spec)) => match ocells, spec with | inl _, Some _ | inr _, None => err (error.unsupported_memory_access_size 0) | inl addr, None @@ -1331,7 +1346,7 @@ Definition LoadOutputs_internal {opts : symbolic_options_computed_opt} {descr:de end; ret (inl v)) | inr base, Some len - => (v <- LoadArray base len; + => (v <- LoadArray (bytes_per_element:=sz) base len; ret (inr v)) end) (List.combine outputaddrs output_types))%N%x86symex. @@ -1358,7 +1373,7 @@ Definition symex_asm_func_M {dereference_output_scalars:bool} (callee_saved_registers : list REG) (output_types : type_spec) (stack_size : nat) - (inputs : list (idx + list idx)) (reg_available : list REG) (asm : Lines) + (inputs : list (N * (idx + list idx))) (reg_available : list REG) (asm : Lines) : M (ErrorT EquivalenceCheckingError (list (idx + list idx))) := (output_placeholders <- lift_dag (build_inputs (descr:=Build_description "output_placeholders" true) output_types); let n_outputs := List.length output_placeholders in @@ -1369,12 +1384,12 @@ Definition symex_asm_func_M initial_register_values <- mapM (GetReg (descr:=Build_description "initial_register_values" true)) callee_saved_registers; _ <- SymexLines asm; final_register_values <- mapM (GetReg (descr:=Build_description "final_register_values" true)) callee_saved_registers; - _ <- LoadArray (descr:=Build_description "load final stack" true) stack_base stack_size; + _ <- LoadArray (descr:=Build_description "load final stack" true) (bytes_per_element:=8) stack_base stack_size; let unsaved_registers : list (REG * (idx * idx)) := List.filter (fun '(r, (init, final)) => negb (init =? final)%N) (List.combine callee_saved_registers (List.combine initial_register_values final_register_values)) in asm_output <- LoadOutputs (descr:=Build_description "asm_output" true) (dereference_scalar:=dereference_output_scalars) outputaddrs output_types; (* also load inputs, for the sake of the proof *) (* reconstruct input types *) - let input_types := List.map (fun v => match v with inl _ => None | inr ls => Some (List.length ls) end) inputs in + let input_types := List.map (fun '(sz, v) => (sz, match v with inl _ => None | inr ls => Some (List.length ls) end)) inputs in asm_input <- LoadOutputs (descr:=Build_description "asm_input <- LoadOutputs" true) (dereference_scalar:=dereference_input_scalars) inputaddrs input_types; (fun s => Success (match asm_output, asm_input, unsaved_registers, s.(symbolic_mem_state) with @@ -1394,7 +1409,7 @@ Definition symex_asm_func {opts : symbolic_options_computed_opt} {dereference_output_scalars:bool} (d : dag) (callee_saved_registers : list REG) (output_types : type_spec) (stack_size : nat) - (inputs : list (idx + list idx)) (reg_available : list REG) (asm : Lines) + (inputs : list (N * (idx + list idx))) (reg_available : list REG) (asm : Lines) : ErrorT EquivalenceCheckingError (list (idx + list idx) * symbolic_state) := let num_reg_given := List.length reg_available in let num_reg_needed := List.length inputs + List.length output_types in @@ -1452,7 +1467,7 @@ Section check_equivalence. Local Notation map_err_None v := (ErrorT.map_error (fun e => (None, e)) v). Local Notation map_err_Some label v := (ErrorT.map_error (fun e => (Some label, e)) v). - Definition map_symex_asm (inputs : list (idx + list idx)) (output_types : type_spec) (d : dag) + Definition map_symex_asm (inputs : list (N * (idx + list idx))) (output_types : type_spec) (d : dag) : ErrorT (option (string (* fname *) * Lines (* asm lines *)) * EquivalenceCheckingError) (list ((string (* fname *) * Lines (* asm lines *)) * (list (idx + list idx) * symbolic_state))) := diff --git a/src/Assembly/EquivalenceProofs.v b/src/Assembly/EquivalenceProofs.v index f086330c74..8374780f80 100644 --- a/src/Assembly/EquivalenceProofs.v +++ b/src/Assembly/EquivalenceProofs.v @@ -737,8 +737,8 @@ Theorem symex_PHOAS_correct {opts : symbolic_options_computed_opt} {t} (expr : API.Expr t) (d : dag) - (inputs : list (idx + list idx)) (runtime_inputs : list (Z + list Z)) - (Hinputs : List.Forall2 (eval_idx_or_list_idx G d) inputs runtime_inputs) + (inputs : list (N * (idx + list idx))) (runtime_inputs : list (Z + list Z)) + (Hinputs : List.Forall2 (eval_idx_or_list_idx G d) (List.map snd inputs) runtime_inputs) (rets : list (idx + list idx)) (d' : dag) (Hwf : API.Wf expr) @@ -800,32 +800,36 @@ Qed. End WithFixedCtx. -Definition val_or_list_val_matches_spec (arg : Z + list Z) (spec : option nat) +Definition val_or_list_val_matches_spec_nosize (arg : Z + list Z) (spec : option nat) := match arg, spec with | inl _, None => True | inr ls, Some len => List.length ls = len | inl _, Some _ | inr _, None => False end. - - +Definition val_or_list_val_matches_spec (arg : N * (Z + list Z)) (spec : N * option nat) + := fst arg = fst spec /\ val_or_list_val_matches_spec_nosize (snd arg) (snd spec). Local Ltac build_runtime_ok_t_step := first [ progress subst | progress destruct_head'_unit | progress inversion_option | progress inversion_prod + | progress inversion_list | progress destruct_head'_prod | progress destruct_head'_and | progress destruct_head'_ex - | progress cbv [Crypto.Util.Option.bind Rewriter.Util.Option.bind ErrorT.bind] in * - | progress cbn [val_or_list_val_matches_spec] in * + | progress cbv [Crypto.Util.Option.bind Rewriter.Util.Option.bind ErrorT.bind val_or_list_val_matches_spec] in * + | progress cbn [val_or_list_val_matches_spec_nosize] in * | progress cbn [fst snd ZRange.type.base.option.is_bounded_by type.andb_bool_for_each_lhs_of_arrow] in * | progress split_andb | progress break_innermost_match_hyps | rewrite <- !List.app_assoc in * + | rewrite !List.map_app in * + | rewrite !length_map in * | discriminate | progress specialize_by_assumption | match goal with + | [ H : S _ = S _ |- _ ] => inversion H; clear H | [ H : ?x = Some _ |- context[?x] ] => rewrite H | [ H : forall extra, ?f (?x ++ extra) = Some _ |- context[?f (?x ++ _)] ] => rewrite !H | [ H : Success _ = Success _ |- _ ] => inversion H; clear H @@ -846,11 +850,27 @@ Local Ltac build_runtime_ok_t_step := | [ |- Forall2 _ (_ ++ _) (_ ++ _) ] => apply Forall2_app | [ H : FoldBool.fold_andb_map _ _ _ = true |- List.length _ = List.length _ ] => apply FoldBool.fold_andb_map_length in H + | [ H : FoldBool.fold_andb_map _ _ _ = true |- List.length _ = S (List.length _) ] + => apply FoldBool.fold_andb_map_length in H + | [ H : Option.List.lift _ = Some _ |- List.length _ = List.length _ ] + => apply Option.List.lift_Some_nth_error_all_iff in H + | [ H : Option.List.lift _ = Some _ |- List.length _ = S (List.length _) ] + => apply Option.List.lift_Some_nth_error_all_iff in H + | [ H : context[@List.length ?A ?x] |- context[@List.length ?B ?x] ] + => progress change A with B in * + | [ H : context[@List.length ?A ?x], H' : context[@List.length ?B ?x] |- _ ] + => progress change A with B in * + | [ H : List.map _ ?x = _ :: _ |- _ ] + => is_var x; destruct x; cbn [List.map] in H end | progress intros | apply conj | reflexivity - | (idtac + symmetry); assumption ]. + | (idtac + symmetry); assumption + | progress cbn [ZRange.type.base.option.lift_Some List.length List.map ZRange.type.base.bitwidth] in * + | progress cbv [option_map] in * + | progress break_match_hyps + | congruence ]. Lemma build_base_runtime_ok t arg_bounds args types PHOAS_args extra (H : simplify_base_type t arg_bounds = Success types) @@ -859,7 +879,7 @@ Lemma build_base_runtime_ok t arg_bounds args types PHOAS_args extra : exists args', args = args' ++ extra /\ (forall extra', build_base_runtime t (args' ++ extra') = Some (PHOAS_args, extra')) - /\ Forall2 val_or_list_val_matches_spec args' types. + /\ Forall2 val_or_list_val_matches_spec_nosize args' (List.map snd types). Proof using Type. revert args extra types H Hargs HPHOAS_args; induction t; intros; cbn [simplify_base_type build_base_runtime type.for_each_lhs_of_arrow Language.Compilers.base.interp] in *; @@ -868,6 +888,7 @@ Proof using Type. | constructor ]. Qed. + Lemma build_runtime_ok t arg_bounds args types PHOAS_args extra (H : simplify_type t arg_bounds = Success types) (Hargs : build_runtime t args = Some (PHOAS_args, extra)) @@ -875,7 +896,7 @@ Lemma build_runtime_ok t arg_bounds args types PHOAS_args extra : exists args', args = args' ++ extra /\ (forall extra', build_runtime t (args' ++ extra') = Some (PHOAS_args, extra')) - /\ Forall2 val_or_list_val_matches_spec args' types. + /\ Forall2 val_or_list_val_matches_spec_nosize args' (List.map snd types). Proof using Type. revert args extra types H Hargs HPHOAS_args; induction t; intros; cbn [simplify_type build_runtime type.for_each_lhs_of_arrow] in *; @@ -889,7 +910,7 @@ Lemma build_input_runtime_ok t arg_bounds args input_types PHOAS_args extra : exists args', args = args' ++ extra /\ (forall extra', build_input_runtime t (args' ++ extra') = Some (PHOAS_args, extra')) - /\ Forall2 val_or_list_val_matches_spec args' input_types. + /\ Forall2 val_or_list_val_matches_spec_nosize args' (List.map snd input_types). Proof using Type. revert args extra input_types H Hargs HPHOAS_args; induction t as [|t1 ? t2]; intros; [ eexists [] | pose proof (build_runtime_ok t1) ]; @@ -902,7 +923,7 @@ Lemma build_input_runtime_ok_nil t arg_bounds args input_types PHOAS_args (H : simplify_input_type t arg_bounds = Success input_types) (Hargs : build_input_runtime t args = Some (PHOAS_args, [])) (HPHOAS_args : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) arg_bounds PHOAS_args = true) - : Forall2 val_or_list_val_matches_spec args input_types. + : Forall2 val_or_list_val_matches_spec_nosize args (List.map snd input_types). Proof using Type. pose proof (build_input_runtime_ok t arg_bounds args input_types PHOAS_args [] H Hargs HPHOAS_args). destruct_head'_ex; destruct_head'_and; subst; rewrite app_nil_r; assumption. @@ -976,18 +997,18 @@ Fixpoint build_merge_base_addresses_G {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} - (items : list (idx + list idx)) (reg_available : list REG) (runtime_reg : list Z) {struct items} + (items : list (N * (idx + list idx))) (reg_available : list REG) (runtime_reg : list Z) {struct items} : G.M (list ((REG + idx) + idx)) := match items, reg_available, runtime_reg with | [], _, _ | _, [], _ => G.ret [] | _, _, [] => fun _ => None - | inr idxs :: xs, r :: reg_available, rv :: runtime_reg + | (sz, inr idxs) :: xs, r :: reg_available, rv :: runtime_reg => (base <- SetRegFresh_G r rv; (* note: overwrites initial value *) - addrs <- G.lift (build_merge_array_addresses base idxs); + addrs <- G.lift (build_merge_array_addresses (bytes_per_element:=sz) base idxs); rest <- build_merge_base_addresses_G (dereference_scalar:=dereference_scalar) xs reg_available runtime_reg; G.ret (inr base :: rest)) - | inl idx :: xs, r :: reg_available, rv :: runtime_reg => + | (_sz, inl idx) :: xs, r :: reg_available, rv :: runtime_reg => (addr <- (if dereference_scalar then (addr <- SetRegFresh_G r rv; @@ -1010,7 +1031,7 @@ Definition build_merge_stack_placeholders_G {opts : symbolic_options_computed_op := (let stack_size := List.length stack_vals in stack_placeholders <- lift_dag_G (build_inputarray_G stack_vals); stack_base <- compute_stack_base_G rsp_val stack_size; - _ <- G.lift (build_merge_array_addresses stack_base stack_placeholders); + _ <- G.lift (build_merge_array_addresses (bytes_per_element:=8) stack_base stack_placeholders); G.ret stack_base)%GM. (* TODO: Move to SymbolicProofs? *) @@ -1313,8 +1334,11 @@ Qed. Definition type_spec_of_runtime {A} (ls : list (A + list A)) : list (option nat) := List.map (fun v => match v with inl _ => None | inr ls => Some (List.length ls) end) ls. -Lemma type_spec_of_runtime_val_or_list_val_matches_spec vals types - : types = type_spec_of_runtime vals <-> Forall2 val_or_list_val_matches_spec vals types. +Lemma length_type_spec_of_runtime A ls : List.length (@type_spec_of_runtime A ls) = List.length ls. +Proof. cbv [type_spec_of_runtime]; rewrite length_map; reflexivity. Qed. + +Lemma type_spec_of_runtime_val_or_list_val_matches_spec_nosize vals types + : types = type_spec_of_runtime vals <-> Forall2 val_or_list_val_matches_spec_nosize vals types. Proof. split. { intro; subst; induction vals; cbn; constructor; break_innermost_match; cbn; eauto. } @@ -1322,21 +1346,52 @@ Proof. repeat (subst || cbn in * || destruct_head' option || break_innermost_match || intuition). } Qed. -Lemma build_inputs_eq_G {descr:description} G d vals (types := type_spec_of_runtime vals) - : build_inputs types d = (fst (build_inputs_G vals (G, d)), snd (snd (build_inputs_G vals (G, d)))). -Proof. - revert G d; subst types; induction vals as [|v vals IHvals]; [ reflexivity | ]. - cbn [build_inputs type_spec_of_runtime List.map build_inputs_G]; fold (type_spec_of_runtime vals); intros. - cbv [dag.bind dag.ret]; break_innermost_match; destruct_head'_prod; cbn [fst snd]. - all: repeat first [ progress cbn [fst snd] in * +Lemma build_inputs_eq_G_and_length {descr:description} G d vals types (Htypes : List.map snd types = type_spec_of_runtime vals) + : build_inputs types d = (List.combine (List.map fst types) (fst (build_inputs_G vals (G, d))), snd (snd (build_inputs_G vals (G, d)))) + /\ List.length types = List.length (fst (build_inputs_G vals (G, d))). +Proof. + remember (G, d) as Gd eqn:HGd. + revert types Htypes G d Gd HGd; induction vals as [|v vals IHvals], types as [|ty types]. + all: cbn [build_inputs type_spec_of_runtime List.map build_inputs_G List.map List.combine List.length fst snd]. + all: try solve [ intros; subst; inversion_list; repeat constructor ]. + all: [ > ]. + fold (type_spec_of_runtime vals); intros. + inversion_list. + specialize (IHvals _ ltac:(eassumption)). + split_and. + cbv [dag.bind dag.ret]; break_innermost_match; destruct_head'_prod; cbn [fst snd] in *; inversion_list; inversion_option; subst; split. + all: repeat first [ progress cbn [fst snd List.length] in * | progress subst | reflexivity + | progress inversion_pair + | apply (f_equal S) + | rewrite <- surjective_pairing | match goal with - | [ H : pair _ _ = pair _ _ |- _ ] => inversion H; clear H | [ H : merge_fresh_symbol _ = _, H' : merge_fresh_symbol_G _ _ = _ |- _ ] => erewrite merge_fresh_symbol_eq_G, H' in H | [ H : build_inputarray _ _ = _, H' : build_inputarray_G _ _ = _ |- _ ] => erewrite build_inputarray_eq_G, H' in H - | [ H : build_inputs _ _ = _, H' : build_inputs_G _ _ = _ |- _ ] => erewrite IHvals, H' in H - end ]. + | [ H : build_inputs _ _ = _, H' : build_inputs_G _ _ = _, IHvals : forall G d Gd, _ -> _ = _ |- _ ] => erewrite IHvals, H' in H + | [ H : forall G d Gd, _ = _ -> List.length ?t = List.length _ |- List.length ?t = List.length _ ] => eapply H + end + | progress inversion_prod ]. +Qed. + +Lemma build_inputs_eq_G {descr:description} G d vals types (Htypes : List.map snd types = type_spec_of_runtime vals) + : build_inputs types d = (List.combine (List.map fst types) (fst (build_inputs_G vals (G, d))), snd (snd (build_inputs_G vals (G, d)))). +Proof. eapply build_inputs_eq_G_and_length; assumption. Qed. + +Lemma length_types_eq_length_fst_build_inputs_G {descr:description} G d vals types (Htypes : List.map (@snd N _) types = type_spec_of_runtime vals) + : List.length types = List.length (fst (build_inputs_G vals (G, d))). +Proof. eapply build_inputs_eq_G_and_length; assumption. Qed. + +Lemma length_fst_build_inputs_G {descr:description} Gd vals + : List.length (fst (build_inputs_G vals Gd)) = List.length vals. +Proof. + destruct Gd; erewrite <- length_types_eq_length_fst_build_inputs_G with (types := List.combine (List.map _ _) _); revgoals. + { rewrite map_snd_combine, firstn_all; try reflexivity. + rewrite length_map; reflexivity. } + { rewrite length_combine, length_map, length_type_spec_of_runtime, Nat.min_id; reflexivity. } + Unshelve. + now constructor. Qed. Lemma build_inputs_G_ok {descr:description} G d vals G' d' inputs @@ -1378,16 +1433,19 @@ Lemma build_inputs_ok {descr:description} G d types inputs args d' | inl v => (0 <= v < 2^64)%Z | inr vs => Forall (fun v => (0 <= v < 2^64)%Z) vs end) args) - (Hargs : Forall2 val_or_list_val_matches_spec args types) + (Hargs : Forall2 val_or_list_val_matches_spec_nosize args (List.map snd types)) : exists G', - Forall2 (eval_idx_or_list_idx G' d') inputs args + Forall2 (eval_idx_or_list_idx G' d') (List.map snd inputs) args /\ gensym_dag_ok G' d' /\ (forall e n, eval G d e n -> eval G' d' e n). Proof. - apply type_spec_of_runtime_val_or_list_val_matches_spec in Hargs; subst types. + apply type_spec_of_runtime_val_or_list_val_matches_spec_nosize in Hargs. erewrite build_inputs_eq_G in H; inversion_prod. eexists; eapply build_inputs_G_ok; try eassumption. - repeat first [ eassumption | apply path_prod | reflexivity ]. + all: repeat first [ eassumption | apply path_prod; cbn [fst snd] | reflexivity ]. + all: subst inputs. + all: rewrite map_snd_combine, length_map, firstn_all; try reflexivity. + all: apply length_types_eq_length_fst_build_inputs_G; assumption. Qed. Lemma lift_dag_eq_G {A} G v_G v s s' res @@ -1869,8 +1927,8 @@ Proof. rewrite get_reg_set_reg_full; break_innermost_match; reflect_hyps; cbv beta in *; try reflexivity; lia. Qed. -Lemma compute_array_address_ok {opts : symbolic_options_computed_opt} {descr:description} G s s' base i idx base_val - (H : compute_array_address base i s = Success (idx, s')) +Lemma compute_array_address_ok {opts : symbolic_options_computed_opt} {descr:description} bytes_per_element G s s' base i idx base_val + (H : compute_array_address (bytes_per_element:=bytes_per_element) base i s = Success (idx, s')) (d := s.(dag_state)) (d' := s'.(dag_state)) (r := s.(symbolic_reg_state)) @@ -1881,7 +1939,7 @@ Lemma compute_array_address_ok {opts : symbolic_options_computed_opt} {descr:des (m' := s'.(symbolic_mem_state)) (Hd : gensym_dag_ok G d) (Hidx : eval_idx_Z G d base base_val) - : (eval_idx_Z G d' idx (Z.land (base_val + 8 * Z.of_nat i) (Z.ones 64)) + : (eval_idx_Z G d' idx (Z.land (base_val + Z.of_N bytes_per_element * Z.of_nat i) (Z.ones 64)) /\ r = r' /\ f = f' /\ m = m') @@ -1930,14 +1988,13 @@ Proof. [ solve [ intros ->; eauto 10 ] | ] end - | progress change (Z.of_N 64) with 64%Z | rewrite !Z.land_ones by lia | progress autorewrite with zsimplify_const | progress (push_Zmod; pull_Zmod) ]. Qed. -Lemma compute_array_address_ok_bounded {opts : symbolic_options_computed_opt} {descr:description} G s s' base i idx base_val - (H : compute_array_address base i s = Success (idx, s')) +Lemma compute_array_address_ok_bounded {opts : symbolic_options_computed_opt} {descr:description} bytes_per_element G s s' base i idx base_val + (H : compute_array_address (bytes_per_element:=bytes_per_element) base i s = Success (idx, s')) (d := s.(dag_state)) (d' := s'.(dag_state)) (r := s.(symbolic_reg_state)) @@ -1948,22 +2005,22 @@ Lemma compute_array_address_ok_bounded {opts : symbolic_options_computed_opt} {d (m' := s'.(symbolic_mem_state)) (Hd : gensym_dag_ok G d) (Hidx : eval_idx_Z G d base base_val) - (Hv : (0 <= base_val + 8 * Z.of_nat i < 2^64)%Z) - : (eval_idx_Z G d' idx (base_val + 8 * Z.of_nat i) + (Hv : (0 <= base_val + Z.of_N bytes_per_element * Z.of_nat i < 2^64)%Z) + : (eval_idx_Z G d' idx (base_val + Z.of_N bytes_per_element * Z.of_nat i) /\ r = r' /\ f = f' /\ m = m') /\ gensym_dag_ok G d' /\ (forall e n, eval G d e n -> eval G d' e n). Proof. - set (v := (base_val + 8 * Z.of_nat i)%Z) in *. + set (v := (base_val + Z.of_N bytes_per_element * Z.of_nat i)%Z) in *. replace v with (Z.land v (Z.ones (Z.of_N 64))); [ eapply compute_array_address_ok; eassumption | rewrite land_ones_eq_of_bounded by assumption ]. reflexivity. Qed. -Lemma build_merge_array_addresses_ok {opts : symbolic_options_computed_opt} {descr:description} G s s' +Lemma build_merge_array_addresses_ok {opts : symbolic_options_computed_opt} {descr:description} bytes_per_element G s s' base base_val items addrs - (H : build_merge_array_addresses base items s = Success (addrs, s')) + (H : build_merge_array_addresses (bytes_per_element:=bytes_per_element) base items s = Success (addrs, s')) (d := s.(dag_state)) (d' := s'.(dag_state)) (r := s.(symbolic_reg_state)) @@ -1973,7 +2030,7 @@ Lemma build_merge_array_addresses_ok {opts : symbolic_options_computed_opt} {des (m := s.(symbolic_mem_state)) (m' := s'.(symbolic_mem_state)) (Hd : gensym_dag_ok G d) - (addrs_vals := List.map (fun i => Z.land (base_val + 8 * Z.of_nat i) (Z.ones 64)) (seq 0 (List.length items))) + (addrs_vals := List.map (fun i => Z.land (base_val + Z.of_N bytes_per_element * Z.of_nat i) (Z.ones 64)) (seq 0 (List.length items))) (Hbase : eval_idx_Z G d base base_val) : (r = r' /\ f = f' @@ -1988,7 +2045,7 @@ Proof. (R_inv := fun st => eval_idx_Z G st base base_val) (R_static := fun _ => True) (R := fun st i_array_val_idx array_addr_idx - => eval_idx_Z G st.(dag_state) array_addr_idx (Z.land (base_val + 8 * Z.of_nat (fst (i_array_val_idx))) (Z.ones 64))) + => eval_idx_Z G st.(dag_state) array_addr_idx (Z.land (base_val + Z.of_N bytes_per_element * Z.of_nat (fst (i_array_val_idx))) (Z.ones 64))) (upd_flag := fun st _ => st) (upd_reg := fun st _ => st) in H; @@ -2201,7 +2258,7 @@ Ltac handle_eval_eval := Lemma build_merge_base_addresses_G_ok {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} - : forall (idxs : list (idx + list idx)) + : forall idxs (reg_available : list REG) (runtime_reg : list Z) G s G' s' @@ -2215,7 +2272,8 @@ Lemma build_merge_base_addresses_G_ok else eval_idx_Z G d idx rv | inr _ => True end) - idxs (List.firstn (List.length idxs) runtime_reg)) + (List.map snd idxs) + (List.firstn (List.length idxs) runtime_reg)) (Hreg : Nat.min (List.length idxs) (List.length reg_available) <= List.length runtime_reg) (Henough_reg : List.length idxs <= List.length reg_available) (d' := s'.(dag_state)) @@ -2228,9 +2286,9 @@ Lemma build_merge_base_addresses_G_ok (Hd : gensym_dag_ok G d) (Hruntime_reg_bounded : Forall (fun v => (0 <= v < 2^64)%Z) runtime_reg) (Hreg_available_wide : Forall (fun reg => let '(rn, lo, sz) := index_and_shift_and_bitcount_of_reg reg in sz = 64%N) reg_available), - ((exists (outputaddrs' : list (idx * option idx + idx * list idx)), - let addrs_vals_of := fun base_reg_val addrs' => List.map (fun i => Z.land (base_reg_val + 8 * Z.of_nat i) (Z.ones 64)) (seq 0 (List.length addrs')) in - fold_left (fun rst '(r, idx') + ((exists (outputaddrs' : list (N * (idx * option idx + idx * list idx))), + let addrs_vals_of := fun sz base_reg_val addrs' => List.map (fun i => Z.land (base_reg_val + Z.of_N sz * Z.of_nat i) (Z.ones 64)) (seq 0 (List.length addrs')) in + fold_left (fun rst '(r, (_sz, idx')) => set_reg rst (reg_index r) match idx' with | inl (idx', _) => idx' @@ -2241,7 +2299,7 @@ Lemma build_merge_base_addresses_G_ok = r' /\ ((* TODO: Is this too specific a spec? *) List.rev (List.flat_map - (fun '(idx', idx) + (fun '((_sz, idx'), idx) => match idx', idx with | inl (reg_val, Some addr), inl val => if dereference_scalar then [(addr, val)] else [] @@ -2249,12 +2307,12 @@ Lemma build_merge_base_addresses_G_ok | inr (base', addrs'), inr items => List.combine addrs' items end) - (List.combine outputaddrs' idxs)) + (List.combine outputaddrs' (List.map snd idxs))) ++ m) = m' /\ (* outputaddrs' base / array *) Forall2 - (fun idx' v => + (fun '(sz, idx') v => match idx' with | inl (idx', addr') (* scalars *) => eval_idx_Z G' d' idx' (Z.land v (Z.ones 64)) @@ -2265,7 +2323,7 @@ Lemma build_merge_base_addresses_G_ok /\ *) eval_idx_Z G' d' base' (Z.land base_reg_val (Z.ones 64))) *) => eval_idx_Z G' d' base' (Z.land v (Z.ones 64)) /\ (* arrays : Forall2 (eval_idx_Z G' d') addrs addrs_vals *) - Forall2 (eval_idx_Z G' d') addrs' (addrs_vals_of v addrs') + Forall2 (eval_idx_Z G' d') addrs' (addrs_vals_of sz v addrs') end) outputaddrs' (List.firstn (List.length outputaddrs') runtime_reg) @@ -2289,7 +2347,7 @@ Lemma build_merge_base_addresses_G_ok end) outputaddrs (List.firstn (List.length outputaddrs) reg_available) - /\ Forall2 (fun addr idx => + /\ Forall2 (fun '(sz, addr) idx => match addr, idx with | inl (idx, _), inl val_idx => if dereference_scalar @@ -2298,8 +2356,8 @@ Lemma build_merge_base_addresses_G_ok | inr (_, ls), inr ls' => List.length ls = List.length ls' | inl _, inr _ | inr _, inl _ => False end) - outputaddrs' idxs - /\ Forall2 (fun addr idx => + outputaddrs' (List.map snd idxs) + /\ Forall2 (fun addr '(sz, idx) => match addr, idx with | inl (inl _), inl (_, None) => dereference_scalar = false | inl (inr addr), inl (_, Some addr') => dereference_scalar = true /\ addr = addr' @@ -2336,7 +2394,7 @@ Proof. | assumption | progress specialize_by_assumption | progress specialize_by (eapply Forall2_weaken; [ | eassumption ]; intros; break_innermost_match; eauto using lift_eval_idx_Z_impl) - | progress cbn [length firstn List.combine fold_left flat_map rev Symbolic.dag_state Symbolic.symbolic_reg_state Symbolic.symbolic_mem_state Symbolic.symbolic_flag_state update_mem_with fst snd] in * + | progress cbn [length firstn List.combine fold_left flat_map rev Symbolic.dag_state Symbolic.symbolic_reg_state Symbolic.symbolic_mem_state Symbolic.symbolic_flag_state update_mem_with fst snd List.map] in * | progress destruct_head' symbolic_state | match goal with | [ H : (_, _) = (_, _) |- _ ] => inversion H; clear H @@ -2369,11 +2427,11 @@ Proof. | progress cbv [index_and_shift_and_bitcount_of_reg] in * ]. (* above is all reversible, evar-free; below is irreversible *) all: exactly_once ((lazymatch goal with |- context[inr _ :: _] => idtac end; - eexists (inr (_, _) :: _)) + eexists ((_, inr (_, _)) :: _)) + (lazymatch goal with |- context[inl (inl _) :: _] => idtac end; - eexists (inl (_, None) :: _)) + eexists ((8%N, inl (_, None)) :: _)) + (lazymatch goal with |- context[inl (inr _) :: _] => idtac end; - eexists (inl (_, Some _) :: _))). + eexists ((8%N, inl (_, Some _)) :: _))). all: repeat repeat first [ progress cbn [length firstn List.combine fold_left flat_map rev] in * @@ -2483,7 +2541,7 @@ Qed. Lemma build_merge_base_addresses_ok {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} - (idxs : list (idx + list idx)) + (idxs : list (N * (idx + list idx))) (reg_available : list REG) (runtime_reg : list Z) G s @@ -2495,7 +2553,7 @@ Lemma build_merge_base_addresses_ok else eval_idx_Z G d idx rv | inr _ => True end) - idxs (List.firstn (List.length idxs) runtime_reg)) + (List.map snd idxs) (List.firstn (List.length idxs) runtime_reg)) (Hreg : Nat.min (List.length idxs) (List.length reg_available) <= List.length runtime_reg) (Henough_reg : List.length idxs <= List.length reg_available) s' @@ -2512,9 +2570,9 @@ Lemma build_merge_base_addresses_ok (Hruntime_reg_bounded : Forall (fun v => (0 <= v < 2^64)%Z) runtime_reg) (Hreg_available_wide : Forall (fun reg => let '(rn, lo, sz) := index_and_shift_and_bitcount_of_reg reg in sz = 64%N) reg_available) : exists G', - ((exists (outputaddrs' : list (idx * option idx + idx * list idx)), - let addrs_vals_of := fun base_reg_val addrs' => List.map (fun i => Z.land (base_reg_val + 8 * Z.of_nat i) (Z.ones 64)) (seq 0 (List.length addrs')) in - fold_left (fun rst '(r, idx') + ((exists (outputaddrs' : list (N * (idx * option idx + idx * list idx))), + let addrs_vals_of := fun sz base_reg_val addrs' => List.map (fun i => Z.land (base_reg_val + Z.of_N sz * Z.of_nat i) (Z.ones 64)) (seq 0 (List.length addrs')) in + fold_left (fun rst '(r, (sz, idx')) => set_reg rst (reg_index r) match idx' with | inl (idx', _) => idx' @@ -2525,7 +2583,7 @@ Lemma build_merge_base_addresses_ok = r' /\ ((* TODO: Is this too specific a spec? *) List.rev (List.flat_map - (fun '(idx', idx) + (fun '((sz, idx'), idx) => match idx', idx with | inl (reg_val, Some addr), inl val => if dereference_scalar then [(addr, val)] else [] @@ -2533,12 +2591,12 @@ Lemma build_merge_base_addresses_ok | inr (base', addrs'), inr items => List.combine addrs' items end) - (List.combine outputaddrs' idxs)) + (List.combine outputaddrs' (List.map snd idxs))) ++ m) = m' /\ (* outputaddrs' base / array *) Forall2 - (fun idx' v => + (fun '(sz, idx') v => match idx' with | inl (idx', addr') (* scalars *) => eval_idx_Z G' d' idx' (Z.land v (Z.ones 64)) @@ -2549,7 +2607,7 @@ Lemma build_merge_base_addresses_ok /\ *) eval_idx_Z G' d' base' (Z.land base_reg_val (Z.ones 64))) *) => eval_idx_Z G' d' base' (Z.land v (Z.ones 64)) /\ (* arrays : Forall2 (eval_idx_Z G' d') addrs addrs_vals *) - Forall2 (eval_idx_Z G' d') addrs' (addrs_vals_of v addrs') + Forall2 (eval_idx_Z G' d') addrs' (addrs_vals_of sz v addrs') end) outputaddrs' (List.firstn (List.length outputaddrs') runtime_reg) @@ -2573,7 +2631,7 @@ Lemma build_merge_base_addresses_ok end) outputaddrs (List.firstn (List.length outputaddrs) reg_available) - /\ Forall2 (fun addr idx => + /\ Forall2 (fun '(sz, addr) idx => match addr, idx with | inl (idx, _), inl val_idx => if dereference_scalar @@ -2582,8 +2640,8 @@ Lemma build_merge_base_addresses_ok | inr (_, ls), inr ls' => List.length ls = List.length ls' | inl _, inr _ | inr _, inl _ => False end) - outputaddrs' idxs - /\ Forall2 (fun addr idx => + outputaddrs' (List.map snd idxs) + /\ Forall2 (fun addr '(sz, idx) => match addr, idx with | inl (inl _), inl (_, None) => dereference_scalar = false | inl (inr addr), inl (_, Some addr') => dereference_scalar = true /\ addr = addr' @@ -3347,8 +3405,8 @@ Proof. Qed. Local Existing Instance Permutation_cons | 0. -Lemma LoadArray_ok {opts : symbolic_options_computed_opt} {descr:description} G s s' base base_val len idxs - (H : LoadArray base len s = Success (idxs, s')) +Lemma LoadArray_ok {opts : symbolic_options_computed_opt} {descr:description} bytes_per_element G s s' base base_val len idxs + (H : LoadArray (bytes_per_element:=bytes_per_element) base len s = Success (idxs, s')) (d := s.(dag_state)) (d' := s'.(dag_state)) (r := s.(symbolic_reg_state)) @@ -3362,7 +3420,7 @@ Lemma LoadArray_ok {opts : symbolic_options_computed_opt} {descr:description} G : ((exists addrs : list idx, Permutation m (List.combine addrs idxs ++ m') /\ List.length idxs = len - /\ Forall2 (eval_idx_Z G d') addrs (List.map (fun i => Z.land (base_val + 8 * Z.of_nat i) (Z.ones 64)) (seq 0 len)) + /\ Forall2 (eval_idx_Z G d') addrs (List.map (fun i => Z.land (base_val + Z.of_N bytes_per_element * Z.of_nat i) (Z.ones 64)) (seq 0 len)) /\ Forall (fun addr => Forall (fun x => (fst x =? addr)%N = false) m') addrs) /\ r = r' /\ f = f') @@ -3482,11 +3540,11 @@ Lemma LoadOutputs_ok {opts : symbolic_options_computed_opt} {descr:description} | inl (inr _) => dereference_scalar = true | _ => True end) outputaddrs) - : ((exists outputaddrs' : list (idx + list idx), - Forall2 (fun idxs '((base, len), base_val) + : ((exists outputaddrs' : list (N * (idx + list idx)), + Forall2 (fun '(sz, idxs) '((base, len), base_val) => match idxs, base, len with | inr idxs, inr base, Some len - => Forall2 (eval_idx_Z G d') idxs (List.map (fun i => Z.land (base_val + 8 * Z.of_nat i) (Z.ones 64)) (seq 0 len)) + => Forall2 (eval_idx_Z G d') idxs (List.map (fun i => Z.land (base_val + Z.of_N sz * Z.of_nat i) (Z.ones 64)) (seq 0 len)) | inl idx, inl (inl r), None => (exists idx', get_reg s' (reg_index r) = Some idx' @@ -3499,9 +3557,9 @@ Lemma LoadOutputs_ok {opts : symbolic_options_computed_opt} {descr:description} | _, _, _ => False end) outputaddrs' - (List.combine (List.combine outputaddrs output_types) output_vals) + (List.combine (List.combine outputaddrs (List.map snd output_types)) output_vals) /\ Permutation m (List.flat_map - (fun '(addrs, idxs) + (fun '((sz, addrs), idxs) => match addrs, idxs with | inr addrs, inr idxs => List.combine addrs idxs @@ -3514,7 +3572,7 @@ Lemma LoadOutputs_ok {opts : symbolic_options_computed_opt} {descr:description} (List.combine outputaddrs' idxs) ++ m') /\ Forall2 - (fun addrs idxs + (fun '(sz, addrs) idxs => match addrs, idxs with | inl idx, inl val_idx => if dereference_scalar @@ -3526,11 +3584,12 @@ Lemma LoadOutputs_ok {opts : symbolic_options_computed_opt} {descr:description} end) outputaddrs' idxs - /\ Forall (fun addrs => match addrs with - | inl idx => True - | inr addrs - => Forall (fun addr => Forall (fun x => (fst x =? addr)%N = false) m') addrs - end) + /\ Forall (fun '(sz, addrs) + => match addrs with + | inl idx => True + | inr addrs + => Forall (fun addr => Forall (fun x => (fst x =? addr)%N = false) m') addrs + end) outputaddrs' /\ List.length output_types = List.length outputaddrs) /\ r = r' @@ -3611,9 +3670,9 @@ Proof. | progress destruct_head' symbolic_state ]. all: lazymatch goal with | [ |- context[Forall2 _ _ ((inr _, _, _) :: _)] ] - => eexists (inr _ :: _) + => eexists ((_, inr _) :: _) | [ |- context[Forall2 _ _ ((inl _, _, _) :: _)] ] - => eexists (inl _ :: _) + => eexists ((8%N, inl _) :: _) end. all: repeat first [ rewrite Forall2_cons_cons_iff | match goal with diff --git a/src/Assembly/WithBedrock/Proofs.v b/src/Assembly/WithBedrock/Proofs.v index ff7e9fc1f1..915b7757cc 100644 --- a/src/Assembly/WithBedrock/Proofs.v +++ b/src/Assembly/WithBedrock/Proofs.v @@ -81,31 +81,32 @@ Require Import bedrock2.ZnWords. Require Import Rupicola.Lib.Tactics. (* for sepsimpl *) Import LittleEndianList. Import coqutil.Word.Interface. -Definition cell64 wa (v : Z) : Semantics.mem_state -> Prop := +Definition cell (nbytes : N) wa (v : Z) : Semantics.mem_state -> Prop := Lift1Prop.ex1 (fun bs => sep (emp ( - length bs = 8%nat /\ v = le_combine bs)) + length bs = N.to_nat nbytes /\ v = le_combine bs)) (eq (OfListWord.map.of_list_word_at wa bs))). +Notation cell64 := (cell 8). -Definition R_scalar_or_array {dereference_scalar:bool} +Definition R_scalar_or_array {dereference_scalar:bool} {bytes_per_element : N} (val : Z + list Z) (asm_val : Naive.word 64) := match val with - | inr array_vals => array cell64 (word.of_Z 8) asm_val array_vals + | inr array_vals => array (cell bytes_per_element) (word.of_Z (Z.of_N bytes_per_element)) asm_val array_vals | inl scalar_val => if dereference_scalar - then cell64 asm_val scalar_val + then cell bytes_per_element asm_val scalar_val else emp (word.unsigned asm_val = scalar_val) end. Definition R_list_scalar_or_array_nolen {dereference_scalar:bool} - (Z_vals : list (Z + list Z)) (asm_vals : list (Naive.word 64)) + (sizes : list N) (Z_vals : list (Z + list Z)) (asm_vals : list (Naive.word 64)) := List.fold_right sep (emp True) (List.map - (fun '(val, asm_val) => R_scalar_or_array (dereference_scalar:=dereference_scalar) val asm_val) - (List.combine Z_vals asm_vals)). + (fun '((sz, val), asm_val) => R_scalar_or_array (dereference_scalar:=dereference_scalar) (bytes_per_element:=sz) val asm_val) + (List.combine (List.combine sizes Z_vals) asm_vals)). Definition R_list_scalar_or_array {dereference_scalar:bool} - (Z_vals : list (Z + list Z)) (asm_vals : list (Naive.word 64)) - := sep (emp (List.length Z_vals = List.length asm_vals)) - (R_list_scalar_or_array_nolen (dereference_scalar:=dereference_scalar) Z_vals asm_vals). + (sizes : list N) (Z_vals : list (Z + list Z)) (asm_vals : list (Naive.word 64)) + := sep (emp (List.length Z_vals = List.length asm_vals /\ List.length sizes = List.length Z_vals)) + (R_list_scalar_or_array_nolen (dereference_scalar:=dereference_scalar) sizes Z_vals asm_vals). Definition get_asm_reg (m : Semantics.reg_state) (reg_available : list REG) : list Z := List.map (Semantics.get_reg m) reg_available. @@ -113,7 +114,7 @@ Definition get_asm_reg (m : Semantics.reg_state) (reg_available : list REG) : li Definition R_runtime_input_mem {output_scalars_are_pointers:bool} (frame : Semantics.mem_state -> Prop) - (output_types : type_spec) (runtime_inputs : list (Z + list Z)) + (output_types : type_spec) (input_sizes : list N) (runtime_inputs : list (Z + list Z)) (stack_size : nat) (stack_base : Naive.word 64) (asm_arguments_out asm_arguments_in : list (Naive.word 64)) (runtime_reg : list Z) @@ -122,7 +123,7 @@ Definition R_runtime_input_mem := exists (stack_placeholder_values : list Z) (output_placeholder_values : list (Z + list Z)), Forall (fun v : Z => (0 <= v < 2 ^ 64)%Z) stack_placeholder_values /\ stack_size = List.length stack_placeholder_values - /\ Forall2 val_or_list_val_matches_spec output_placeholder_values output_types + /\ Forall2 val_or_list_val_matches_spec_nosize output_placeholder_values (List.map snd output_types) /\ Forall (fun v => match v with | inl v => (0 <= v < 2^64)%Z | inr vs => Forall (fun v => (0 <= v < 2^64)%Z) vs @@ -138,15 +139,15 @@ Definition R_runtime_input_mem output_placeholder_values (firstn (length output_types) runtime_reg) /\ ((frame * - R_list_scalar_or_array (dereference_scalar:=output_scalars_are_pointers) output_placeholder_values asm_arguments_out * - R_list_scalar_or_array (dereference_scalar:=false) runtime_inputs asm_arguments_in * + R_list_scalar_or_array (dereference_scalar:=output_scalars_are_pointers) (List.map fst output_types) output_placeholder_values asm_arguments_out * + R_list_scalar_or_array (dereference_scalar:=false) input_sizes runtime_inputs asm_arguments_in * array cell64 (word.of_Z 8) stack_base stack_placeholder_values)%sep) m. Definition R_runtime_input {output_scalars_are_pointers:bool} (frame : Semantics.mem_state -> Prop) - (output_types : type_spec) (runtime_inputs : list (Z + list Z)) + (output_types : type_spec) (input_sizes : list N) (runtime_inputs : list (Z + list Z)) (stack_size : nat) (stack_base : Naive.word 64) (asm_pointer_arguments_out asm_pointer_arguments_in : list (Naive.word 64)) (reg_available : list REG) (runtime_reg : list Z) @@ -161,7 +162,7 @@ Definition R_runtime_input /\ List.length asm_arguments_out = List.length output_types /\ List.map word.unsigned asm_arguments_out = List.firstn (List.length output_types) runtime_reg /\ List.map word.unsigned asm_arguments_in = List.firstn (List.length runtime_inputs) (List.skipn (List.length output_types) runtime_reg) - /\ List.map fst (List.filter (fun '(_, v) => output_scalars_are_pointers || Option.is_Some v)%bool (List.combine asm_arguments_out output_types)) = asm_pointer_arguments_out + /\ List.map fst (List.filter (fun '(_, v) => output_scalars_are_pointers || Option.is_Some v)%bool (List.combine asm_arguments_out (List.map snd output_types))) = asm_pointer_arguments_out /\ List.map fst (List.filter (fun '(_, v) => match v with inl _ => false | inr _ => true end)%bool (List.combine asm_arguments_in runtime_inputs)) = asm_pointer_arguments_in /\ (Semantics.get_reg m rsp - 8 * Z.of_nat stack_size)%Z = word.unsigned stack_base /\ (* it must be the case that all the scalars in the real input values match what's in registers / the calling convention *) @@ -172,12 +173,13 @@ Definition R_runtime_input end) runtime_inputs (firstn (length runtime_inputs) (skipn (length output_types) runtime_reg)) - /\ R_runtime_input_mem (output_scalars_are_pointers:=output_scalars_are_pointers) frame output_types runtime_inputs stack_size stack_base asm_arguments_out asm_arguments_in runtime_reg m. + /\ R_runtime_input_mem (output_scalars_are_pointers:=output_scalars_are_pointers) frame output_types input_sizes runtime_inputs stack_size stack_base asm_arguments_out asm_arguments_in runtime_reg m. (* TODO : should we preserve inputs? *) Definition R_runtime_output_mem {output_scalars_are_pointers:bool} (frame : Semantics.mem_state -> Prop) + (output_sizes : list N) (runtime_outputs : list (Z + list Z)) (input_types : type_spec) (stack_size : nat) (stack_base : Naive.word 64) (asm_arguments_out asm_arguments_in : list (Naive.word 64)) @@ -186,20 +188,21 @@ Definition R_runtime_output_mem := exists (stack_placeholder_values : list Z) (input_placeholder_values : list (Z + list Z)), Forall (fun v : Z => (0 <= v < 2 ^ 64)%Z) stack_placeholder_values /\ stack_size = List.length stack_placeholder_values - /\ Forall2 val_or_list_val_matches_spec input_placeholder_values input_types + /\ Forall2 val_or_list_val_matches_spec_nosize input_placeholder_values (List.map snd input_types) /\ Forall (fun v => match v with | inl v => (0 <= v < 2^64)%Z | inr vs => Forall (fun v => (0 <= v < 2^64)%Z) vs end) input_placeholder_values /\ ((frame * - R_list_scalar_or_array (dereference_scalar:=output_scalars_are_pointers) runtime_outputs asm_arguments_out * - R_list_scalar_or_array (dereference_scalar:=false) input_placeholder_values asm_arguments_in * + R_list_scalar_or_array (dereference_scalar:=output_scalars_are_pointers) output_sizes runtime_outputs asm_arguments_out * + R_list_scalar_or_array (dereference_scalar:=false) (List.map fst input_types) input_placeholder_values asm_arguments_in * array cell64 (word.of_Z 8) stack_base stack_placeholder_values)%sep) m. Definition R_runtime_output {output_scalars_are_pointers:bool} (frame : Semantics.mem_state -> Prop) + (output_sizes : list N) (runtime_outputs : list (Z + list Z)) (input_types : type_spec) (stack_size : nat) (stack_base : Naive.word 64) (asm_pointer_arguments_out asm_pointer_arguments_in : list (Naive.word 64)) @@ -210,8 +213,8 @@ Definition R_runtime_output Forall (fun v => (0 <= v < 2^64)%Z) (Tuple.to_list _ m.(machine_reg_state)) /\ get_asm_reg m callee_saved_registers = runtime_callee_saved_registers /\ List.map fst (List.filter (fun '(_, v) => output_scalars_are_pointers || match v with inl _ => false | inr _ => true end)%bool (List.combine asm_arguments_out runtime_outputs)) = asm_pointer_arguments_out - /\ List.map fst (List.filter (fun '(_, v) => Option.is_Some v)%bool (List.combine asm_arguments_in input_types)) = asm_pointer_arguments_in - /\ R_runtime_output_mem (output_scalars_are_pointers:=output_scalars_are_pointers) frame runtime_outputs input_types stack_size stack_base asm_arguments_out asm_arguments_in m. + /\ List.map fst (List.filter (fun '(_, (_, v)) => Option.is_Some v)%bool (List.combine asm_arguments_in input_types)) = asm_pointer_arguments_in + /\ R_runtime_output_mem (output_scalars_are_pointers:=output_scalars_are_pointers) frame output_sizes runtime_outputs input_types stack_size stack_base asm_arguments_out asm_arguments_in m. Definition word_args_to_Z_args : list (Naive.word 64 + list (Naive.word 64)) -> list (Z + list Z) @@ -220,7 +223,7 @@ Definition word_args_to_Z_args | inr vs => inr (List.map word.unsigned vs) end). -Lemma word_args_to_Z_args_bounded args +Lemma word_args_to_Z_args_bounded args (sizes : list N) : Forall (fun v => match v with | inl v => (0 <= v < 2^64)%Z | inr vs => Forall (fun v => (0 <= v < 2^64)%Z) vs @@ -627,33 +630,35 @@ Proof. all: eauto. Qed. -Lemma R_list_scalar_or_array_cons_iff dereference_scalar i1 i2 w1 w2 +Lemma R_list_scalar_or_array_cons_iff dereference_scalar s1 s2 i1 i2 w1 w2 : Lift1Prop.iff1 - (@R_list_scalar_or_array dereference_scalar (i1 :: i2) (w1 :: w2)) - (@R_scalar_or_array dereference_scalar i1 w1 * @R_list_scalar_or_array dereference_scalar i2 w2)%sep. + (@R_list_scalar_or_array dereference_scalar (s1 :: s2) (i1 :: i2) (w1 :: w2)) + (@R_scalar_or_array dereference_scalar s1 i1 w1 * @R_list_scalar_or_array dereference_scalar s2 i2 w2)%sep. Proof. cbv [R_list_scalar_or_array R_list_scalar_or_array_nolen]; cbn [List.length List.combine List.map fold_right]. SeparationLogic.cancel; cbn [seps]; split; cbv [emp]; intros; sepsimpl; inversion_nat_eq; subst; congruence. Qed. -Lemma R_list_scalar_or_array_nolen_app_iff dereference_scalar i1 i2 w1 w2 +Lemma R_list_scalar_or_array_nolen_app_iff dereference_scalar s1 s2 i1 i2 w1 w2 (H : List.length i1 = List.length w1) + (Hs : List.length s1 = List.length i1) : Lift1Prop.iff1 - (@R_list_scalar_or_array_nolen dereference_scalar (i1 ++ i2) (w1 ++ w2)) - (@R_list_scalar_or_array_nolen dereference_scalar i1 w1 * @R_list_scalar_or_array_nolen dereference_scalar i2 w2)%sep. + (@R_list_scalar_or_array_nolen dereference_scalar (s1 ++ s2) (i1 ++ i2) (w1 ++ w2)) + (@R_list_scalar_or_array_nolen dereference_scalar s1 i1 w1 * @R_list_scalar_or_array_nolen dereference_scalar s2 i2 w2)%sep. Proof. cbv [R_list_scalar_or_array_nolen]. - rewrite !combine_app_samelength, map_app, fold_right_app by assumption. - generalize (List.combine i1 w1). + rewrite !combine_app_samelength, map_app, fold_right_app by now rewrite ?length_combine, ?Hs, ?H, ?Nat.min_idempotent. + generalize (List.combine (List.combine s1 i1) w1). intro l; induction l as [|?? IH]; cbn [List.map fold_right]; [ | rewrite IH ]; SeparationLogic.cancel; cbn [seps]. Qed. -Lemma R_list_scalar_or_array_app_iff dereference_scalar i1 i2 w1 w2 +Lemma R_list_scalar_or_array_app_iff dereference_scalar s1 s2 i1 i2 w1 w2 (H : List.length i1 = List.length w1) + (Hs : List.length s1 = List.length i1) : Lift1Prop.iff1 - (@R_list_scalar_or_array dereference_scalar (i1 ++ i2) (w1 ++ w2)) - (@R_list_scalar_or_array dereference_scalar i1 w1 * @R_list_scalar_or_array dereference_scalar i2 w2)%sep. + (@R_list_scalar_or_array dereference_scalar (s1 ++ s2) (i1 ++ i2) (w1 ++ w2)) + (@R_list_scalar_or_array dereference_scalar s1 i1 w1 * @R_list_scalar_or_array dereference_scalar s2 i2 w2)%sep. Proof. cbv [R_list_scalar_or_array]. rewrite R_list_scalar_or_array_nolen_app_iff by assumption. @@ -705,8 +710,8 @@ Proof. rewrite ?SeparationLogic.sep_emp_l; cbv [emp]; tauto. } Qed. -Lemma R_cell64_ex_cell64_iff G d ia iv - : Lift1Prop.iff1 (R_cell64 G d ia iv) +Lemma R_cell_ex_cell_iff G d nbytes ia iv + : Lift1Prop.iff1 (R_cell nbytes G d ia iv) (Lift1Prop.ex1 (fun a => Lift1Prop.ex1 @@ -729,24 +734,24 @@ Proof. all: sepsimpl; subst; [ > apply le_combine_bound | eapply Z.lt_le_trans; [ apply le_combine_bound | ] ]. rewrite (ltac:(eassumption) : List.length _ = _); reflexivity. Qed. - -Lemma bounded_of_cell64 wa v m - (H : cell64 wa v m) - : (0 <= v < 2^64)%Z. +Print cell. +Lemma bounded_of_cell nbytes wa v m + (H : cell nbytes wa v m) + : (0 <= v < 2^(8 * Z.of_N nbytes))%Z. Proof. - cbv [cell64] in H. + cbv [cell] in H. sepsimpl; subst; [ apply le_combine_bound | eapply Z.lt_le_trans; [ apply le_combine_bound | ] ]. - rewrite H; reflexivity. + rewrite H; zify; reflexivity. Qed. -Lemma bounded_of_array_cell64 v +Lemma bounded_of_array_cell nbytes v : forall wa base m - (H : array cell64 base wa v m), - Forall (fun v => 0 <= v < 2^64)%Z v. + (H : array (cell nbytes) base wa v m), + Forall (fun v => 0 <= v < 2^(8 * Z.of_N nbytes))%Z v. Proof. induction v as [|v vs IH]; cbn [array]; constructor; cbv [sep] in *; sepsimpl. - all: try now eapply bounded_of_cell64; eassumption. - eauto. + all: try now eapply bounded_of_cell; eassumption. + all: eauto. Qed. (* TODO: move? *) @@ -763,14 +768,14 @@ Proof. split; intro; sepsimpl; eauto. Qed. -Lemma R_mem_combine_ex_array_iff frame G d n addrs val_idxs base_value base_word_value init - (Haddrs : Forall2 (eval_idx_Z G d) addrs (List.map (fun i => Z.land (base_value + 8 * Z.of_nat i) (Z.ones 64)) (seq init n))) +Lemma R_mem_combine_ex_array_iff frame G d n bytes_per_cell addrs val_idxs base_value base_word_value init + (Haddrs : Forall2 (eval_idx_Z G d) addrs (List.map (fun i => Z.land (base_value + Z.of_N bytes_per_cell * Z.of_nat i) (Z.ones 64)) (seq init n))) (*(Hn : List.length val_idxs = n)*) (Hbase : base_value = word.unsigned base_word_value) : Lift1Prop.iff1 (R_mem frame G d (List.combine addrs val_idxs)) (Lift1Prop.ex1 (fun vals - => emp (Forall2 (eval_idx_Z G d) (firstn n val_idxs) vals /\ Forall (fun v => 0 <= v < 2^64)%Z vals) * frame * array cell64 (word.of_Z 8) (word.add base_word_value (word.of_Z (8 * Z.of_nat init))) vals))%sep. + => emp (Forall2 (eval_idx_Z G d) (firstn n val_idxs) vals /\ Forall (fun v => 0 <= v < 2^(8 * Z.of_N bytes_per_cell))%Z vals) * frame * array (cell bytes_per_cell) (word.of_Z (Z.of_N bytes_per_cell)) (word.add base_word_value (word.of_Z (Z.of_N bytes_per_cell * Z.of_nat init))) vals))%sep. Proof. subst. revert val_idxs n init Haddrs. @@ -864,7 +869,7 @@ Lemma R_mem_combine_array_iff_helper frame G d addrs val_idxs base_value base_wo : Lift1Prop.iff1 (R_mem frame G d (List.combine addrs val_idxs)) (frame * (emp (Forall (fun v => 0 <= v < 2^64)%Z vals) * array cell64 (word.of_Z 8) (word.add base_word_value (word.of_Z (8 * Z.of_nat init))) vals))%sep. Proof. - rewrite (@sep_emp_holds_l _ _ (@bounded_of_array_cell64 _ _ _)). + rewrite (@sep_emp_holds_l _ _ (@bounded_of_array_cell _ _ _ _)). rewrite R_mem_combine_ex_array_iff by eassumption. subst. cbv [Lift1Prop.iff1 Lift1Prop.ex1]; split; intros; [ | exists vals ]; sepsimpl; eauto. @@ -911,9 +916,9 @@ Local Ltac cleanup_min := | rewrite (Nat.min_r x y) in * by assumption ] end. -Lemma bounded_of_R_scalar_or_array {dereference_scalar:bool} v +Lemma bounded_of_R_scalar_or_array {dereference_scalar:bool} {bytes_per_element:N} v : forall ws m - (H : R_scalar_or_array (dereference_scalar:=dereference_scalar) v ws m), + (H : R_scalar_or_array (dereference_scalar:=dereference_scalar) (bytes_per_element:=bytes_per_element) v ws m), match v with | inl v => 0 <= v < 2^64 | inr vs => Forall (fun v => 0 <= v < 2^64) vs @@ -1437,7 +1442,7 @@ Lemma build_inputs_ok_R {descr:description} G ss types inputs args d' frame ms (d := ss.(dag_state)) (H : build_inputs types d = (inputs, d')) (HR : R frame G ss ms) - (Hargs : Forall2 val_or_list_val_matches_spec args types) + (Hargs : Forall2 val_or_list_val_matches_spec_nosize args types) (Hbounds : Forall (fun v => match v with | inl v => (0 <= v < 2^64)%Z | inr vs => Forall (fun v => (0 <= v < 2^64)%Z) vs @@ -3013,7 +3018,7 @@ Proof. | [ |- Forall _ ?ls ] => rewrite Forall_forall_iff_nth_error in Hreg_wide_enough; cbv [get_asm_reg] in *; - cbv [val_or_list_val_matches_spec] in *; + cbv [val_or_list_val_matches_spec_nosize] in *; subst; Foralls_to_nth_error; cbv [index_and_shift_and_bitcount_of_reg] in *; inversion_pair; subst; @@ -3092,8 +3097,8 @@ Proof. | _ => idtac end). all: lazymatch goal with - | [ |- Forall2 val_or_list_val_matches_spec _ _ ] - => cbv [eval_idx_or_list_idx val_or_list_val_matches_spec type_spec_of_runtime] in *; + | [ |- Forall2 val_or_list_val_matches_spec_nosize _ _ ] + => cbv [eval_idx_or_list_idx val_or_list_val_matches_spec_nosize type_spec_of_runtime] in *; rewrite ?@Forall2_map_l_iff, ?@Forall2_map_r_iff in *; saturate_lengths; Foralls_to_nth_error; @@ -3114,7 +3119,7 @@ Proof. all: apply List.Forall2_filter_same. all: pose proof Hreg_wide_enough as Hreg_wide_enough'. all: rewrite Forall_forall_iff_nth_error in Hreg_wide_enough; - cbv [get_asm_reg val_or_list_val_matches_spec] in *; + cbv [get_asm_reg val_or_list_val_matches_spec_nosize] in *; rewrite <- !@Forall2_eq, ?@Forall2_map_l_iff, ?@Forall2_map_r_iff in *; saturate_lengths; Foralls_to_nth_error. diff --git a/src/Assembly/WithBedrock/SymbolicProofs.v b/src/Assembly/WithBedrock/SymbolicProofs.v index a367e5b74c..59902ae228 100644 --- a/src/Assembly/WithBedrock/SymbolicProofs.v +++ b/src/Assembly/WithBedrock/SymbolicProofs.v @@ -105,14 +105,14 @@ Definition R_flag (x : option idx) (ob : option bool) : Prop := Definition R_flags : Symbolic.flag_state -> Semantics.flag_state -> Prop := Tuple.fieldwise R_flag. -Definition R_cell64 (ia iv : idx) : mem_state -> Prop := +Definition R_cell (nbytes : N) (ia iv : idx) : mem_state -> Prop := Lift1Prop.ex1 (fun a => Lift1Prop.ex1 (fun bs => sep (emp ( eval ia (word.unsigned a) /\ - length bs = 8%nat /\ eval iv (le_combine bs))) + length bs = N.to_nat nbytes /\ eval iv (le_combine bs))) (eq (OfListWord.map.of_list_word_at a bs)))). -Fixpoint R_mem (sm : Symbolic.mem_state) : mem_state -> Prop := +Fixpoint R_mem (nbytes : N) (sm : Symbolic.mem_state) : mem_state -> Prop := match sm with | nil => frame | cons (ia, iv) sm' => sep (R_cell64 ia iv) (R_mem sm') diff --git a/src/Util/ZUtil/Land.v b/src/Util/ZUtil/Land.v index ecf4bfd414..cd3b64b63b 100644 --- a/src/Util/ZUtil/Land.v +++ b/src/Util/ZUtil/Land.v @@ -67,7 +67,7 @@ Module Z. intros. rewrite Z.sub_1_r, <- Z.ones_equiv. apply Z.land_ones; auto with zarith. Qed. - + Lemma land_pow2_testbit a b : a &' 2^b = if Z.testbit a b then 2^b else 0. Proof. @@ -96,6 +96,6 @@ Module Z. Proof. destruct (Z.ltb_spec b 0). - now rewrite Pow.Z.base_pow_neg, Z.land_0_r. - - rewrite land_pow2_testbit, Z.div2_bits, Testbit.Z.bits_above_pow2; + - rewrite land_pow2_testbit, Z.div2_bits, Testbit.Z.bits_above_pow2; try (replace (Z.succ b) with (b + 1); nia). Qed. End Z.