rewrite cmov c,0,-1 to sbb

src/Rewriter/Rules.v

@@ -395,6 +395,13 @@ Definition arith_with_casts_rewrite_rulesT (adc_no_carry_to_add : bool) : list (
                    y ∈ ry -> y = Z.ones (Z.succ (Z.log2 y))
                    -> cstZ rv (cstZ ry ('y) &' cstZ rx x) = cstZ rx x)
              ]%Z%zrange
+         ; mymap
+             do_again
+             [ (forall c M rv r0 rM, 0 ∈ r0 -> M ∈ rM -> M ∈ rv -> 2^Z.log2 (M+1) = M + 1 -> 1 <= M ->
+                  cstZ rv (Z.zselect (cstZ r[0~>1] c) (cstZ r0 ('0)) (cstZ rM ('M)))
+                  = (dlet vc := cstZZ rv r[0~>1] (Z.sub_with_get_borrow_full ('(M+1)) (cstZ r[0~>1] c) 0 0) in
+                     cstZ rv (fst vc)))
+                  ]
          ; mymap
              do_again
              [ (* [do_again], so that we can trigger add/sub rules on the output *)
@@ -1213,7 +1220,8 @@ Section with_bitwidth.
     := Eval cbv [myapp mymap myflatten] in
         mymap
           dont_do_again
-          [(* no-op rule to prevent firing on selects between 0 and mask (since
+          [
+          (* no-op rule to prevent firing on selects between 0 and mask (since
                these can be succinctly expressed as 0-c *)
             (forall rc c,
                 singlewidth (Z.zselect (cstZ rc c)

src/Rewriter/RulesProofs.v

@@ -571,6 +571,11 @@ Proof using Type.
   all: repeat interp_good_t_step_arith.
   all: remove_casts; try fin_with_nia.
   all: try (reflect_hyps; lia).
+
+  { (* cmov c 0 -1 -> sbb 0 0 c *)
+    enough (- c mod (M + 1) = M) as E by (rewrite E; remove_casts; trivial).
+    match goal with H5 : _ |- _ => apply unfold_is_bounded_by_bool in H5; cbn in H5 end.
+    rewrite Z.mod_opp_l_nz; rewrite ?Z.mod_small; nia. }
 Qed.
 
 Lemma strip_literal_casts_rewrite_rules_proofs