From 7229b6289f6fe90254845dfb9e83c3a1c0aaa435 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 6 Mar 2025 20:26:54 -0800 Subject: [PATCH] Move signed to Z.signed in ZUtil.Definitions --- src/Assembly/Symbolic.v | 35 ++++------------------- src/Assembly/WithBedrock/Semantics.v | 16 +++++------ src/Assembly/WithBedrock/SymbolicProofs.v | 10 +++---- src/Util/ZUtil/Definitions.v | 3 ++ src/Util/ZUtil/Signed.v | 33 +++++++++++++++++++++ 5 files changed, 52 insertions(+), 45 deletions(-) create mode 100644 src/Util/ZUtil/Signed.v diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v index 5849e9547a..dd5faa6fb5 100644 --- a/src/Assembly/Symbolic.v +++ b/src/Assembly/Symbolic.v @@ -24,6 +24,7 @@ Require Import Crypto.Util.ZUtil.Land. Require Import Crypto.Util.ZUtil.Land.Fold. Require Import Crypto.Util.ZUtil.Ones. Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Signed. Require Import Crypto.Util.Equality. Require Import Crypto.Util.Bool.Reflect. Require Import Crypto.Util.Option. @@ -587,7 +588,6 @@ Import ListNotations. Section WithContext. Context (ctx : symbol -> option Z). - Definition signed s n : Z := (Z.land (Z.shiftl 1 (Z.of_N s-1) + n) (Z.ones (Z.of_N s)) - Z.shiftl 1 (Z.of_N s-1))%Z. Definition op_to_Z_binop (o : op) : option _ := match o with | add _ => Some Z.add @@ -618,12 +618,12 @@ Section WithContext. | subborrow s, cons a args' => Some ((- Z.shiftr (a - List.fold_right Z.add 0 args') (Z.of_N s)) mod 2) | addoverflow s, args => Some (Z.b2z (negb (Z.eqb - (signed s (keep s (List.fold_right Z.add 0 args))) - (List.fold_right Z.add 0%Z (List.map (signed s) args))))) + (Z.signed s (keep s (List.fold_right Z.add 0 args))) + (List.fold_right Z.add 0%Z (List.map (Z.signed s) args))))) | neg s, [a] => Some (keep s (- a)) | shl s, [a; b] => Some (keep s (Z.shiftl a b)) | shr s, [a; b] => Some (keep s (Z.shiftr a b)) - | sar s, [a; b] => Some (keep s (Z.shiftr (signed s a) b)) + | sar s, [a; b] => Some (keep s (Z.shiftr (Z.signed s a) b)) | rcr s, [v1; cf; cnt] => Some ( let v1c := Z.lor v1 (Z.shiftl cf (Z.of_N s)) in let l := Z.lor v1c (Z.shiftl v1 (1+Z.of_N s)) in @@ -2595,18 +2595,6 @@ Proof using Type. rewrite Z.ones_equiv in * |- ; rewrite Z.shiftr_div_pow2, Z.div_small; cbn; lia. Qed. -Lemma signed_small s v (Hv : (0 <= v <= Z.ones (Z.of_N s-1))%Z) : signed s v = v. -Proof using Type. - destruct (N.eq_dec s 0); subst; cbv [signed]. - { rewrite Z.land_0_r. cbn in *; Lia.lia. } - rewrite !Z.land_ones, !Z.shiftl_mul_pow2, ?Z.add_0_r, ?Z.mul_1_l by Lia.lia. - rewrite Z.ones_equiv in Hv. - rewrite Z.mod_small; try ring. - enough (2 ^ Z.of_N s = 2 ^ (Z.of_N s - 1) + 2 ^ (Z.of_N s - 1))%Z; try Lia.lia. - replace (Z.of_N s) with (1+(Z.of_N s-1))%Z at 1 by Lia.lia. - rewrite Z.pow_add_r; try Lia.lia. -Qed. - Definition addoverflow_small (d : dag) := fun e => match e with ExprApp (addoverflow s, ([_]|[_;_]|[_;_;_]) as args) => @@ -2623,7 +2611,7 @@ Proof using Type. BreakMatch.break_match_hyps; Option.inversion_option; t; epose proof Z.ones_equiv (Z.of_N s -1); destruct_head'_and; reflect_hyps; destruct_head'_and. - all : rewrite Z.land_ones, !Z.mod_small, !signed_small, !Z.eqb_refl; trivial. + all : rewrite Z.land_ones, !Z.mod_small, !Z.signed_small, !Z.eqb_refl; trivial. all : try split; try Lia.lia. all : replace (Z.of_N s) with (1+(Z.of_N s-1))%Z at 1 by Lia.lia; rewrite Z.pow_add_r; try Lia.lia. @@ -2685,19 +2673,6 @@ Proof. apply fold_right_filter_identity_gen with (G:=id); cbv [id]; intuition (subst; eauto). Qed. -Lemma signed_0 s : signed s 0 = 0%Z. -Proof using Type. - destruct (N.eq_dec s 0); subst; trivial. - cbv [signed]. - rewrite !Z.land_ones, !Z.shiftl_mul_pow2, ?Z.add_0_r, ?Z.mul_1_l by Lia.lia. - rewrite Z.mod_small; try ring. - split; try (eapply Z.pow_lt_mono_r; Lia.lia). - eapply Z.pow_nonneg; Lia.lia. -Qed. -#[global] -Hint Rewrite signed_0 : zsimplify_const zsimplify zsimplify_fast. -Global Hint Resolve signed_0 : zarith. - Lemma interp_op_drop_identity o id : identity o = Some id -> forall G xs, interp_op G o xs = interp_op G o (List.filter (fun v => negb (Z.eqb v id)) xs). Proof using Type. diff --git a/src/Assembly/WithBedrock/Semantics.v b/src/Assembly/WithBedrock/Semantics.v index d8f6ef024e..7c0519aa38 100644 --- a/src/Assembly/WithBedrock/Semantics.v +++ b/src/Assembly/WithBedrock/Semantics.v @@ -12,6 +12,7 @@ Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Notations. +Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Assembly.Syntax. Require Crypto.Util.Tuple. Import ListNotations. @@ -148,9 +149,6 @@ Definition HavocFlagsFromResult s st v : machine_state := Definition PreserveFlag (st : machine_state) (f : FLAG) st' := update_flag_with st (fun fs => set_flag_internal fs f (get_flag st' f)). -Definition signed (s : N) (z : Z) : Z := - Z.land (Z.shiftl 1 (Z.of_N s-1) + z) (Z.ones (Z.of_N s)) - Z.shiftl 1 (Z.of_N s-1). - Definition rcrcnt s cnt : Z := if N.eqb s 8 then Z.land cnt 0x1f mod 9 else if N.eqb s 16 then Z.land cnt 0x1f mod 17 else @@ -207,7 +205,7 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi st <- SetOperand sa s st dst v; let st := HavocFlagsFromResult s st v in let st := SetFlag st CF (Z.odd (Z.shiftr (v1 + v2 + c) (Z.of_N s))) in - Some (SetFlag st OF (negb (signed s v =? signed s v1 + signed s v2 + signed s c)%Z)) + Some (SetFlag st OF (negb (Z.signed s v =? Z.signed s v1 + Z.signed s v2 + Z.signed s c)%Z)) | (adcx | adox) as opc, [dst; src] => let flag := match opc with adcx => CF | _ => OF end in v1 <- DenoteOperand sa s st dst; @@ -226,19 +224,19 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi st <- SetOperand sa s st dst v; let st := HavocFlagsFromResult s st v in let st := SetFlag st CF (Z.odd (Z.shiftr (v1 - (v2 + c)) (Z.of_N s))) in - Some (SetFlag st OF (negb (signed s v =? signed s v1 - (signed s v2 + c))%Z)) + Some (SetFlag st OF (negb (Z.signed s v =? Z.signed s v1 - (Z.signed s v2 + c))%Z)) | dec, [dst] => v1 <- DenoteOperand sa s st dst; let v := Z.land (v1 - 1) (Z.ones (Z.of_N s)) in st <- SetOperand sa s st dst v; let st := PreserveFlag (HavocFlagsFromResult s st v) CF st in - Some (SetFlag st OF (negb (signed s v =? signed s v1 - 1)%Z)) + Some (SetFlag st OF (negb (Z.signed s v =? Z.signed s v1 - 1)%Z)) | inc, [dst] => v1 <- DenoteOperand sa s st dst; let v := Z.land (v1 + 1) (Z.ones (Z.of_N s)) in st <- SetOperand sa s st dst v; let st := PreserveFlag (HavocFlagsFromResult s st v) CF st in - Some (SetFlag st OF (negb (signed s v =? signed s v1 + 1)%Z)) + Some (SetFlag st OF (negb (Z.signed s v =? Z.signed s v1 + 1)%Z)) | mulx, [hi; lo; src2] => (* Flags Affected: None *) let src1 : ARG := rdx in (* Note: assumes s=64 *) v1 <- DenoteOperand sa s st src1; @@ -269,7 +267,7 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi v1 <- DenoteOperand sa s st dst; cnt' <- DenoteOperand sa s st cnt; let cnt := Z.land cnt' (Z.of_N s-1) in - let v := Z.land (Z.shiftr (signed s v1) cnt) (Z.ones (Z.of_N s)) in + let v := Z.land (Z.shiftr (Z.signed s v1) cnt) (Z.ones (Z.of_N s)) in st <- SetOperand sa s st dst v; Some (if cnt =? 0 then st else let st := HavocFlagsFromResult s st v in @@ -324,7 +322,7 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi if cnt =? 0 then Some st else if Z.of_N s destruct_one_match | _ => progress intuition idtac end; rewrite ?Z.add_0_r, ?Z.odd_opp; eauto; try Lia.lia; try congruence. - replace (Semantics.signed n 0) with 0; cycle 1. + replace (Z.signed n 0) with 0; cycle 1. { pose_operation_size_cases. clear -H0; intuition (subst; cbv; trivial). } - rewrite Z.add_0_r; cbv [Semantics.signed Symbolic.signed]; congruence. } + rewrite Z.add_0_r; cbv [Z.signed]; congruence. } Unshelve. all : match goal with H : context[Syntax.adc] |- _ => idtac | _ => shelve end. { destruct s'; @@ -1259,8 +1258,7 @@ Proof using Type. | _ => progress (cbv [R_flags Tuple.fieldwise Tuple.fieldwise'] in *; cbn -[Syntax.operation_size] in * ; subst) | _ => destruct_one_match | _ => progress intuition idtac - end; rewrite ?Z.add_assoc, ?Z.add_0_r, ?Z.odd_opp; eauto; try Lia.lia; try congruence. - change Symbolic.signed with Semantics.signed. congruence. } + end; rewrite ?Z.add_assoc, ?Z.add_0_r, ?Z.odd_opp; eauto; try Lia.lia; try congruence. } Unshelve. all : match goal with H : context[Syntax.adcx] |- _ => idtac | _ => shelve end. { cbn [fold_right] in *; rewrite ?Z.bit0_odd, ?Z.add_0_r, ?Z.add_assoc in *; assumption. } diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v index 19aea9df66..e1ad2b7efa 100644 --- a/src/Util/ZUtil/Definitions.v +++ b/src/Util/ZUtil/Definitions.v @@ -166,6 +166,9 @@ Module Z. Definition twos_complement_mul ma mb a b := (sign_extend ma (ma + mb) a) * (sign_extend mb (ma + mb) b). + + Definition signed (s : N) (n : Z) : Z := + Z.land (Z.shiftl 1 (Z.of_N s-1) + n) (Z.ones (Z.of_N s)) - Z.shiftl 1 (Z.of_N s-1). End Z. Module Export Notations. diff --git a/src/Util/ZUtil/Signed.v b/src/Util/ZUtil/Signed.v new file mode 100644 index 0000000000..7d7fa59714 --- /dev/null +++ b/src/Util/ZUtil/Signed.v @@ -0,0 +1,33 @@ +From Coq Require Import ZArith. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.LetIn. +Local Open Scope Z_scope. + +Module Z. + Lemma signed_small s v (Hv : (0 <= v <= Z.ones (Z.of_N s-1))) : Z.signed s v = v. + Proof. + destruct (N.eq_dec s 0); subst; cbv [Z.signed]. + { rewrite Z.land_0_r. cbn in *; Lia.lia. } + rewrite !Z.land_ones, !Z.shiftl_mul_pow2, ?Z.add_0_r, ?Z.mul_1_l by Lia.lia. + rewrite Z.ones_equiv in Hv. + rewrite Z.mod_small; try ring. + enough (2 ^ Z.of_N s = 2 ^ (Z.of_N s - 1) + 2 ^ (Z.of_N s - 1))%Z; try Lia.lia. + replace (Z.of_N s) with (1+(Z.of_N s-1))%Z at 1 by Lia.lia. + rewrite Z.pow_add_r; try Lia.lia. + Qed. + + Lemma signed_0 s : Z.signed s 0 = 0. + Proof. + destruct (N.eq_dec s 0); subst; trivial. + cbv [Z.signed]. + rewrite !Z.land_ones, !Z.shiftl_mul_pow2, ?Z.add_0_r, ?Z.mul_1_l by Lia.lia. + rewrite Z.mod_small; try ring. + split; try (eapply Z.pow_lt_mono_r; Lia.lia). + eapply Z.pow_nonneg; Lia.lia. + Qed. + #[global] + Hint Rewrite signed_0 : zsimplify_const zsimplify zsimplify_fast. + Global Hint Resolve signed_0 : zarith. +End Z. \ No newline at end of file