Unobjectionable rewrite rules for saturated arithmetic

[JasonGross]

For #1609

We don't yet include the ones that are higher-order-than 3, those need more debugging.

[JasonGross]

@jadephilipoom perhaps we should standardize on Z.add_get_carry_full and get rid of other variants?

Originally posted by @andres-erbsen in #1609 (comment)

[JasonGross]

@andres-erbsen turn mul_split with negated intput into negated mul_split first

Originally posted by @andres-erbsen in #1609 (comment)

[JasonGross]

@andres-erbsen Is this something that should be done before merging?

[JasonGross]

@andres-erbsen These rewrite rules break current synthesis:

Which with some casts elided is:
(λ x1,
  let x2 := Z.sub_with_get_borrow((2^51), (0, ((uint64_t)(x1[0]), 0x7ffffffffffed))) (* : uint64_t, uint1_t *) in
  let x3 := Z.sub_with_get_borrow((2^51), ((uint1_t)x2₂, ((uint64_t)(x1[1]), (2^51-1)))) (* : uint64_t, uint1_t *) in
  let x4 := Z.sub_with_get_borrow((2^51), ((uint1_t)x3₂, ((uint64_t)(x1[2]), (2^51-1)))) (* : uint64_t, uint1_t *) in
  let x5 := Z.sub_with_get_borrow((2^51), ((uint1_t)x4₂, ((uint64_t)(x1[3]), (2^51-1)))) (* : uint64_t, uint1_t *) in
  let x6 := Z.sub_with_get_borrow((2^51), ((uint1_t)x5₂, ((uint64_t)(x1[4]), (2^51-1)))) (* : uint64_t, uint1_t *) in
  let x7 := -x6₂ mod 2^64 (* : uint64_t *) in
  let x8 := Z.add_get_carry((2^51), ((uint64_t)x2₁, (uint64_t)(x7 & 0x7ffffffffffed))) (* : uint64_t, uint1_t *) in
  let x9 := Z.add_with_get_carry((2^51), ((uint1_t)x8₂, ((uint64_t)x3₁, (uint64_t)(x7 & (2^51-1))))) (* : uint64_t, uint1_t *) in
  let x10 := Z.add_with_get_carry((2^51), ((uint1_t)x9₂, ((uint64_t)x4₁, (uint64_t)(x7 & (2^51-1))))) (* : uint64_t, uint1_t *) in
  let x11 := Z.add_with_get_carry((2^51), ((uint1_t)x10₂, ((uint64_t)x5₁, (uint64_t)(x7 & (2^51-1))))) (* : uint64_t, uint1_t *) in
  let x12 := Z.add_with_get_carry((2^51), ((uint1_t)x11₂, ((uint64_t)x6₁, (uint64_t)(x7 & (2^51-1))))) (* : uint64_t, uint1_t *) in
  let x13 := x12₁ << 4 (* : uint64_t *) in
  let x14 := x11₁ * 2 (* : uint64_t *) in
  let x15 := x10₁ << 6 (* : uint64_t *) in
  let x16 := x9₁ << 3 (* : uint64_t *) in
  let x17 := x8₁ & 255 (* : uint8_t *) in
  let x18 := x8₁ >> 8 (* : uint64_t *) in
  let x19 := x18 & 255 (* : uint8_t *) in
  let x20 := x18 >> 8 (* : uint64_t *) in
  let x21 := x20 & 255 (* : uint8_t *) in
  let x22 := x20 >> 8 (* : uint64_t *) in
  let x23 := x22 & 255 (* : uint8_t *) in
  let x24 := x22 >> 8 (* : uint64_t *) in
  let x25 := x24 & 255 (* : uint8_t *) in
  let x26 := x24 >> 8 (* : uint64_t *) in
  let x27 := x26 & 255 (* : uint8_t *) in
  let x28 := x26 >> 8 (* : uint8_t *) in
  let x29 := x16 + x28 (* : uint64_t *) in
  let x30 := x29 & 255 (* : uint8_t *) in
  let x31 := x29 >> 8 (* : uint64_t *) in
  let x32 := x31 & 255 (* : uint8_t *) in
  let x33 := x31 >> 8 (* : uint64_t *) in
  let x34 := x33 & 255 (* : uint8_t *) in
  let x35 := x33 >> 8 (* : uint64_t *) in
  let x36 := x35 & 255 (* : uint8_t *) in
  let x37 := x35 >> 8 (* : uint64_t *) in
  let x38 := x37 & 255 (* : uint8_t *) in
  let x39 := x37 >> 8 (* : uint64_t *) in
  let x40 := x39 & 255 (* : uint8_t *) in
  let x41 := x39 >> 8 (* : uint8_t *) in
  let x42 := x15 + x41 (* : uint64_t *) in
  let x43 := x42 & 255 (* : uint8_t *) in
  let x44 := x42 >> 8 (* : uint64_t *) in
  let x45 := x44 & 255 (* : uint8_t *) in
  let x46 := x44 >> 8 (* : uint64_t *) in
  let x47 := x46 & 255 (* : uint8_t *) in
  let x48 := x46 >> 8 (* : uint64_t *) in
  let x49 := x48 & 255 (* : uint8_t *) in
  let x50 := x48 >> 8 (* : uint64_t *) in
  let x51 := x50 & 255 (* : uint8_t *) in
  let x52 := x50 >> 8 (* : uint64_t *) in
  let x53 := x52 & 255 (* : uint8_t *) in
  let x54 := x52 >> 8 (* : uint64_t *) in
  let x55 := x54 & 255 (* : uint8_t *) in
  let x56 := x54 >> 8 (* : uint1_t *) in
  let x57 := x14 + x56 (* : uint64_t *) in
  let x58 := x57 & 255 (* : uint8_t *) in
  let x59 := x57 >> 8 (* : uint64_t *) in
  let x60 := x59 & 255 (* : uint8_t *) in
  let x61 := x59 >> 8 (* : uint64_t *) in
  let x62 := x61 & 255 (* : uint8_t *) in
  let x63 := x61 >> 8 (* : uint64_t *) in
  let x64 := x63 & 255 (* : uint8_t *) in
  let x65 := x63 >> 8 (* : uint64_t *) in
  let x66 := x65 & 255 (* : uint8_t *) in
  let x67 := x65 >> 8 (* : uint64_t *) in
  let x68 := x67 & 255 (* : uint8_t *) in
  let x69 := x67 >> 8 (* : uint8_t *) in
  let x70 := x13 + x69 (* : uint64_t *) in
  let x71 := x70 & 255 (* : uint8_t *) in
  let x72 := x70 >> 8 (* : uint64_t *) in
  let x73 := x72 & 255 (* : uint8_t *) in
  let x74 := x72 >> 8 (* : uint64_t *) in
  let x75 := x74 & 255 (* : uint8_t *) in
  let x76 := x74 >> 8 (* : uint64_t *) in
  let x77 := x76 & 255 (* : uint8_t *) in
  let x78 := x76 >> 8 (* : uint64_t *) in
  let x79 := x78 & 255 (* : uint8_t *) in
  let x80 := x78 >> 8 (* : uint64_t *) in
  let x81 := x80 & 255 (* : uint8_t *) in
  let x82 := x80 >> 8 (* : uint8_t *) in
  x17 :: x19 :: x21 :: x23 :: x25 :: x27 :: x30 :: x32 :: x34 :: x36 :: x38 :: x40 :: x43 :: x45 :: x47 :: x49 :: x51 :: x53 :: x55 :: x58 :: x60 :: x62 :: x64 :: x66 :: x68 :: x71 :: x73 :: x75 :: x77 :: x79 :: x81 :: x82 :: []
)
Error in converting ToBytes to Go:
Invalid identifier in arithmetic expression (mod)

Can you take over debugging here?