Move signed to Z.signed in ZUtil.Definitions (mit-plv#2039)

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.
@@ -596,7 +597,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
@@ -627,12 +627,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
@@ -2604,18 +2604,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) =>
@@ -2632,7 +2620,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.
@@ -2694,19 +2682,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.

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 <? cnt then Some (HavocFlags st) else
       let st := HavocFlagsFromResult s st l in
-      let signchange := xorb (signed s lv <? 0)%Z (signed s v <? 0)%Z in
+      let signchange := xorb (Z.signed s lv <? 0)%Z (Z.signed s v <? 0)%Z in
       (* Note: IA-32 SDM does not make it clear what sign change is in question *)
       let st := if cnt =? 1 then SetFlag st OF signchange else st in
       let st := SetFlag st CF (Z.testbit l (cnt-1)) in

src/Assembly/WithBedrock/SymbolicProofs.v

@@ -8,6 +8,7 @@ Require Import Crypto.Util.ErrorT.
 Import Coq.Lists.List. (* [map] is [List.map] not [ErrorT.map] *)
 Require Import Crypto.Util.ListUtil.IndexOf.
 Require Import Crypto.Util.Tactics.WarnIfGoalsRemain.
+Require Import Crypto.Util.ZUtil.Definitions.
 Require Crypto.Util.Option.
 Require Import Crypto.Assembly.Syntax.
 Require Import Crypto.Assembly.Symbolic.
@@ -1198,7 +1199,6 @@ Proof using Type.
              end; eauto; try Lia.lia; try congruence.
              eexists. split. eauto.
              f_equal. f_equal.
-             change Symbolic.signed with Semantics.signed.
              rewrite ?Z.add_0_r.
              f_equal.
              1:congruence.
@@ -1225,7 +1225,6 @@ Proof using Type.
              end; eauto; try Lia.lia; try congruence.
              eexists. split. eauto.
              f_equal. f_equal.
-             change Symbolic.signed with Semantics.signed.
              rewrite ?Z.add_0_r.
              f_equal.
              1:congruence.
@@ -1244,9 +1243,9 @@ Proof using Type.
              | _ => 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. }

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.

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.