From ad2af1d46963f9496d56a6185100fb34199854e7 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 30 Jan 2019 23:32:26 -0500
Subject: Drop `map λ` bits in docstrings
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

They are redundant with the bounds pre- and post-conditions in WBW
montgomery.

Also drop the fiat_p... prefix from the `from_montgomery` bits in most
of the docstrings, under the assumption that shorter strings with less
repetition are more readable.
---
 p224_32.c                                      | 43 +++++++++++---------------
 p224_64.c                                      | 43 +++++++++++---------------
 p256_32.c                                      | 43 +++++++++++---------------
 p256_64.c                                      | 43 +++++++++++---------------
 p384_32.c                                      | 43 +++++++++++---------------
 p384_64.c                                      | 43 +++++++++++---------------
 p484_64.c                                      | 43 +++++++++++---------------
 secp256k1_32.c                                 | 43 +++++++++++---------------
 secp256k1_64.c                                 | 43 +++++++++++---------------
 src/PushButtonSynthesis/Primitives.v           |  9 ++++--
 src/PushButtonSynthesis/WordByWordMontgomery.v |  5 +--
 11 files changed, 172 insertions(+), 229 deletions(-)

diff --git a/p224_32.c b/p224_32.c
index 2cae5b631..bf1df313d 100644
--- a/p224_32.c
+++ b/p224_32.c
@@ -94,10 +94,9 @@ static void fiat_p224_cmovznz_u32(uint32_t* out1, fiat_p224_uint1 arg1, uint32_t
 
 /*
  * The function fiat_p224_mul multiplies two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -978,9 +977,8 @@ static void fiat_p224_mul(uint32_t out1[7], const uint32_t arg1[7], const uint32
 
 /*
  * The function fiat_p224_square squares a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg1)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -1860,10 +1858,9 @@ static void fiat_p224_square(uint32_t out1[7], const uint32_t arg1[7]) {
 
 /*
  * The function fiat_p224_add adds two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) + eval (fiat_p224_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -1942,10 +1939,9 @@ static void fiat_p224_add(uint32_t out1[7], const uint32_t arg1[7], const uint32
 
 /*
  * The function fiat_p224_sub subtracts two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) - eval (fiat_p224_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2009,9 +2005,8 @@ static void fiat_p224_sub(uint32_t out1[7], const uint32_t arg1[7], const uint32
 
 /*
  * The function fiat_p224_opp negates a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p224_from_montgomery out1) mod m = -eval (fiat_p224_from_montgomery arg1) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2074,9 +2069,8 @@ static void fiat_p224_opp(uint32_t out1[7], const uint32_t arg1[7]) {
 
 /*
  * The function fiat_p224_from_montgomery translates a field element out of the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^7) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2614,8 +2608,8 @@ static void fiat_p224_from_montgomery(uint32_t out1[7], const uint32_t arg1[7])
 
 /*
  * The function fiat_p224_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * out1 = 0 ↔ eval (fiat_p224_from_montgomery arg1) mod m = 0
+ * 0 ≤ eval arg1 < m →
+ * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
  * Output Bounds:
@@ -2662,7 +2656,7 @@ static void fiat_p224_selectznz(uint32_t out1[7], fiat_p224_uint1 arg1, const ui
 
 /*
  * The function fiat_p224_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..27]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2757,9 +2751,8 @@ static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) {
 
 /*
  * The function fiat_p224_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
- * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..27] ∧ 0 ≤ bytes_eval arg1 < m →
+ * 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..6]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
diff --git a/p224_64.c b/p224_64.c
index c2cba2768..d44f0a694 100644
--- a/p224_64.c
+++ b/p224_64.c
@@ -96,10 +96,9 @@ static void fiat_p224_cmovznz_u64(uint64_t* out1, fiat_p224_uint1 arg1, uint64_t
 
 /*
  * The function fiat_p224_mul multiplies two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -440,9 +439,8 @@ static void fiat_p224_mul(uint64_t out1[4], const uint64_t arg1[4], const uint64
 
 /*
  * The function fiat_p224_square squares a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) * eval (fiat_p224_from_montgomery arg1)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -782,10 +780,9 @@ static void fiat_p224_square(uint64_t out1[4], const uint64_t arg1[4]) {
 
 /*
  * The function fiat_p224_add adds two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) + eval (fiat_p224_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -837,10 +834,9 @@ static void fiat_p224_add(uint64_t out1[4], const uint64_t arg1[4], const uint64
 
 /*
  * The function fiat_p224_sub subtracts two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p224_from_montgomery out1) mod m = (eval (fiat_p224_from_montgomery arg1) - eval (fiat_p224_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -883,9 +879,8 @@ static void fiat_p224_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64
 
 /*
  * The function fiat_p224_opp negates a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p224_from_montgomery out1) mod m = -eval (fiat_p224_from_montgomery arg1) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -927,9 +922,8 @@ static void fiat_p224_opp(uint64_t out1[4], const uint64_t arg1[4]) {
 
 /*
  * The function fiat_p224_from_montgomery translates a field element out of the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -1149,8 +1143,8 @@ static void fiat_p224_from_montgomery(uint64_t out1[4], const uint64_t arg1[4])
 
 /*
  * The function fiat_p224_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * out1 = 0 ↔ eval (fiat_p224_from_montgomery arg1) mod m = 0
+ * 0 ≤ eval arg1 < m →
+ * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  * Output Bounds:
@@ -1188,7 +1182,7 @@ static void fiat_p224_selectznz(uint64_t out1[4], fiat_p224_uint1 arg1, const ui
 
 /*
  * The function fiat_p224_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffff]]
@@ -1288,9 +1282,8 @@ static void fiat_p224_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
 
 /*
  * The function fiat_p224_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
- * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m →
+ * 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x0], [0x0 ~> 0x0], [0x0 ~> 0x0], [0x0 ~> 0x0]]
diff --git a/p256_32.c b/p256_32.c
index 27c1983df..1bfabfaa7 100644
--- a/p256_32.c
+++ b/p256_32.c
@@ -94,10 +94,9 @@ static void fiat_p256_cmovznz_u32(uint32_t* out1, fiat_p256_uint1 arg1, uint32_t
 
 /*
  * The function fiat_p256_mul multiplies two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -1150,9 +1149,8 @@ static void fiat_p256_mul(uint32_t out1[8], const uint32_t arg1[8], const uint32
 
 /*
  * The function fiat_p256_square squares a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg1)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2204,10 +2202,9 @@ static void fiat_p256_square(uint32_t out1[8], const uint32_t arg1[8]) {
 
 /*
  * The function fiat_p256_add adds two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) + eval (fiat_p256_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2295,10 +2292,9 @@ static void fiat_p256_add(uint32_t out1[8], const uint32_t arg1[8], const uint32
 
 /*
  * The function fiat_p256_sub subtracts two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) - eval (fiat_p256_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2369,9 +2365,8 @@ static void fiat_p256_sub(uint32_t out1[8], const uint32_t arg1[8], const uint32
 
 /*
  * The function fiat_p256_opp negates a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p256_from_montgomery out1) mod m = -eval (fiat_p256_from_montgomery arg1) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2441,9 +2436,8 @@ static void fiat_p256_opp(uint32_t out1[8], const uint32_t arg1[8]) {
 
 /*
  * The function fiat_p256_from_montgomery translates a field element out of the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^8) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -3050,8 +3044,8 @@ static void fiat_p256_from_montgomery(uint32_t out1[8], const uint32_t arg1[8])
 
 /*
  * The function fiat_p256_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * out1 = 0 ↔ eval (fiat_p256_from_montgomery arg1) mod m = 0
+ * 0 ≤ eval arg1 < m →
+ * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
  * Output Bounds:
@@ -3101,7 +3095,7 @@ static void fiat_p256_selectznz(uint32_t out1[8], fiat_p256_uint1 arg1, const ui
 
 /*
  * The function fiat_p256_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -3208,9 +3202,8 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
 
 /*
  * The function fiat_p256_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
- * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m →
+ * 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
diff --git a/p256_64.c b/p256_64.c
index 6961f5433..b9c091129 100644
--- a/p256_64.c
+++ b/p256_64.c
@@ -96,10 +96,9 @@ static void fiat_p256_cmovznz_u64(uint64_t* out1, fiat_p256_uint1 arg1, uint64_t
 
 /*
  * The function fiat_p256_mul multiplies two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -416,9 +415,8 @@ static void fiat_p256_mul(uint64_t out1[4], const uint64_t arg1[4], const uint64
 
 /*
  * The function fiat_p256_square squares a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) * eval (fiat_p256_from_montgomery arg1)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -734,10 +732,9 @@ static void fiat_p256_square(uint64_t out1[4], const uint64_t arg1[4]) {
 
 /*
  * The function fiat_p256_add adds two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) + eval (fiat_p256_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -789,10 +786,9 @@ static void fiat_p256_add(uint64_t out1[4], const uint64_t arg1[4], const uint64
 
 /*
  * The function fiat_p256_sub subtracts two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p256_from_montgomery out1) mod m = (eval (fiat_p256_from_montgomery arg1) - eval (fiat_p256_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -835,9 +831,8 @@ static void fiat_p256_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64
 
 /*
  * The function fiat_p256_opp negates a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p256_from_montgomery out1) mod m = -eval (fiat_p256_from_montgomery arg1) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -879,9 +874,8 @@ static void fiat_p256_opp(uint64_t out1[4], const uint64_t arg1[4]) {
 
 /*
  * The function fiat_p256_from_montgomery translates a field element out of the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -1065,8 +1059,8 @@ static void fiat_p256_from_montgomery(uint64_t out1[4], const uint64_t arg1[4])
 
 /*
  * The function fiat_p256_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * out1 = 0 ↔ eval (fiat_p256_from_montgomery arg1) mod m = 0
+ * 0 ≤ eval arg1 < m →
+ * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  * Output Bounds:
@@ -1104,7 +1098,7 @@ static void fiat_p256_selectznz(uint64_t out1[4], fiat_p256_uint1 arg1, const ui
 
 /*
  * The function fiat_p256_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -1211,9 +1205,8 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
 
 /*
  * The function fiat_p256_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
- * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m →
+ * 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
diff --git a/p384_32.c b/p384_32.c
index 90ad22621..f01dc08b2 100644
--- a/p384_32.c
+++ b/p384_32.c
@@ -94,10 +94,9 @@ static void fiat_p384_cmovznz_u32(uint32_t* out1, fiat_p384_uint1 arg1, uint32_t
 
 /*
  * The function fiat_p384_mul multiplies two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2678,9 +2677,8 @@ static void fiat_p384_mul(uint32_t out1[12], const uint32_t arg1[12], const uint
 
 /*
  * The function fiat_p384_square squares a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg1)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -5260,10 +5258,9 @@ static void fiat_p384_square(uint32_t out1[12], const uint32_t arg1[12]) {
 
 /*
  * The function fiat_p384_add adds two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) + eval (fiat_p384_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -5387,10 +5384,9 @@ static void fiat_p384_add(uint32_t out1[12], const uint32_t arg1[12], const uint
 
 /*
  * The function fiat_p384_sub subtracts two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) - eval (fiat_p384_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -5489,9 +5485,8 @@ static void fiat_p384_sub(uint32_t out1[12], const uint32_t arg1[12], const uint
 
 /*
  * The function fiat_p384_opp negates a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p384_from_montgomery out1) mod m = -eval (fiat_p384_from_montgomery arg1) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -5589,9 +5584,8 @@ static void fiat_p384_opp(uint32_t out1[12], const uint32_t arg1[12]) {
 
 /*
  * The function fiat_p384_from_montgomery translates a field element out of the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^12) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -7227,8 +7221,8 @@ static void fiat_p384_from_montgomery(uint32_t out1[12], const uint32_t arg1[12]
 
 /*
  * The function fiat_p384_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
- * out1 = 0 ↔ eval (fiat_p384_from_montgomery arg1) mod m = 0
+ * 0 ≤ eval arg1 < m →
+ * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
  * Output Bounds:
@@ -7290,7 +7284,7 @@ static void fiat_p384_selectznz(uint32_t out1[12], fiat_p384_uint1 arg1, const u
 
 /*
  * The function fiat_p384_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -7445,9 +7439,8 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) {
 
 /*
  * The function fiat_p384_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
- * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] ∧ 0 ≤ bytes_eval arg1 < m →
+ * 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..11]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
diff --git a/p384_64.c b/p384_64.c
index d3585876a..831e8b2ad 100644
--- a/p384_64.c
+++ b/p384_64.c
@@ -96,10 +96,9 @@ static void fiat_p384_cmovznz_u64(uint64_t* out1, fiat_p384_uint1 arg1, uint64_t
 
 /*
  * The function fiat_p384_mul multiplies two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -856,9 +855,8 @@ static void fiat_p384_mul(uint64_t out1[6], const uint64_t arg1[6], const uint64
 
 /*
  * The function fiat_p384_square squares a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) * eval (fiat_p384_from_montgomery arg1)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -1614,10 +1612,9 @@ static void fiat_p384_square(uint64_t out1[6], const uint64_t arg1[6]) {
 
 /*
  * The function fiat_p384_add adds two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) + eval (fiat_p384_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -1687,10 +1684,9 @@ static void fiat_p384_add(uint64_t out1[6], const uint64_t arg1[6], const uint64
 
 /*
  * The function fiat_p384_sub subtracts two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p384_from_montgomery out1) mod m = (eval (fiat_p384_from_montgomery arg1) - eval (fiat_p384_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -1747,9 +1743,8 @@ static void fiat_p384_sub(uint64_t out1[6], const uint64_t arg1[6], const uint64
 
 /*
  * The function fiat_p384_opp negates a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p384_from_montgomery out1) mod m = -eval (fiat_p384_from_montgomery arg1) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -1805,9 +1800,8 @@ static void fiat_p384_opp(uint64_t out1[6], const uint64_t arg1[6]) {
 
 /*
  * The function fiat_p384_from_montgomery translates a field element out of the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^6) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -2342,8 +2336,8 @@ static void fiat_p384_from_montgomery(uint64_t out1[6], const uint64_t arg1[6])
 
 /*
  * The function fiat_p384_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
- * out1 = 0 ↔ eval (fiat_p384_from_montgomery arg1) mod m = 0
+ * 0 ≤ eval arg1 < m →
+ * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  * Output Bounds:
@@ -2387,7 +2381,7 @@ static void fiat_p384_selectznz(uint64_t out1[6], fiat_p384_uint1 arg1, const ui
 
 /*
  * The function fiat_p384_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -2542,9 +2536,8 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) {
 
 /*
  * The function fiat_p384_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
- * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] ∧ 0 ≤ bytes_eval arg1 < m →
+ * 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
diff --git a/p484_64.c b/p484_64.c
index 41c1a0c90..33c12b7e8 100644
--- a/p484_64.c
+++ b/p484_64.c
@@ -96,10 +96,9 @@ static void fiat_p484_cmovznz_u64(uint64_t* out1, fiat_p484_uint1 arg1, uint64_t
 
 /*
  * The function fiat_p484_mul multiplies two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) * eval (fiat_p484_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -1085,9 +1084,8 @@ static void fiat_p484_mul(uint64_t out1[7], const uint64_t arg1[7], const uint64
 
 /*
  * The function fiat_p484_square squares a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) * eval (fiat_p484_from_montgomery arg1)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -2072,10 +2070,9 @@ static void fiat_p484_square(uint64_t out1[7], const uint64_t arg1[7]) {
 
 /*
  * The function fiat_p484_add adds two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) + eval (fiat_p484_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -2154,10 +2151,9 @@ static void fiat_p484_add(uint64_t out1[7], const uint64_t arg1[7], const uint64
 
 /*
  * The function fiat_p484_sub subtracts two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_p484_from_montgomery out1) mod m = (eval (fiat_p484_from_montgomery arg1) - eval (fiat_p484_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -2221,9 +2217,8 @@ static void fiat_p484_sub(uint64_t out1[7], const uint64_t arg1[7], const uint64
 
 /*
  * The function fiat_p484_opp negates a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_p484_from_montgomery out1) mod m = -eval (fiat_p484_from_montgomery arg1) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -2286,9 +2281,8 @@ static void fiat_p484_opp(uint64_t out1[7], const uint64_t arg1[7]) {
 
 /*
  * The function fiat_p484_from_montgomery translates a field element out of the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^7) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -2934,8 +2928,8 @@ static void fiat_p484_from_montgomery(uint64_t out1[7], const uint64_t arg1[7])
 
 /*
  * The function fiat_p484_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
- * out1 = 0 ↔ eval (fiat_p484_from_montgomery arg1) mod m = 0
+ * 0 ≤ eval arg1 < m →
+ * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  * Output Bounds:
@@ -2982,7 +2976,7 @@ static void fiat_p484_selectznz(uint64_t out1[7], fiat_p484_uint1 arg1, const ui
 
 /*
  * The function fiat_p484_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..55]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x3ffffffffffff]]
@@ -3160,9 +3154,8 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) {
 
 /*
  * The function fiat_p484_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
- * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..55] ∧ 0 ≤ bytes_eval arg1 < m →
+ * 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..6]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x3], [0x0 ~> 0x0]]
diff --git a/secp256k1_32.c b/secp256k1_32.c
index 4ded0f935..bf7e4fb7d 100644
--- a/secp256k1_32.c
+++ b/secp256k1_32.c
@@ -94,10 +94,9 @@ static void fiat_secp256k1_cmovznz_u32(uint32_t* out1, fiat_secp256k1_uint1 arg1
 
 /*
  * The function fiat_secp256k1_mul multiplies two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -1390,9 +1389,8 @@ static void fiat_secp256k1_mul(uint32_t out1[8], const uint32_t arg1[8], const u
 
 /*
  * The function fiat_secp256k1_square squares a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg1)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2684,10 +2682,9 @@ static void fiat_secp256k1_square(uint32_t out1[8], const uint32_t arg1[8]) {
 
 /*
  * The function fiat_secp256k1_add adds two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) + eval (fiat_secp256k1_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2775,10 +2772,9 @@ static void fiat_secp256k1_add(uint32_t out1[8], const uint32_t arg1[8], const u
 
 /*
  * The function fiat_secp256k1_sub subtracts two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) - eval (fiat_secp256k1_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2849,9 +2845,8 @@ static void fiat_secp256k1_sub(uint32_t out1[8], const uint32_t arg1[8], const u
 
 /*
  * The function fiat_secp256k1_opp negates a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_secp256k1_from_montgomery out1) mod m = -eval (fiat_secp256k1_from_montgomery arg1) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2921,9 +2916,8 @@ static void fiat_secp256k1_opp(uint32_t out1[8], const uint32_t arg1[8]) {
 
 /*
  * The function fiat_secp256k1_from_montgomery translates a field element out of the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^8) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -3824,8 +3818,8 @@ static void fiat_secp256k1_from_montgomery(uint32_t out1[8], const uint32_t arg1
 
 /*
  * The function fiat_secp256k1_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
- * out1 = 0 ↔ eval (fiat_secp256k1_from_montgomery arg1) mod m = 0
+ * 0 ≤ eval arg1 < m →
+ * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
  * Output Bounds:
@@ -3875,7 +3869,7 @@ static void fiat_secp256k1_selectznz(uint32_t out1[8], fiat_secp256k1_uint1 arg1
 
 /*
  * The function fiat_secp256k1_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -3982,9 +3976,8 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
 
 /*
  * The function fiat_secp256k1_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
- * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m →
+ * 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(32 * (x + 1)) / 2^(32 * x)⌋) [0..7]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
diff --git a/secp256k1_64.c b/secp256k1_64.c
index b1437e2dc..133702645 100644
--- a/secp256k1_64.c
+++ b/secp256k1_64.c
@@ -96,10 +96,9 @@ static void fiat_secp256k1_cmovznz_u64(uint64_t* out1, fiat_secp256k1_uint1 arg1
 
 /*
  * The function fiat_secp256k1_mul multiplies two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -464,9 +463,8 @@ static void fiat_secp256k1_mul(uint64_t out1[4], const uint64_t arg1[4], const u
 
 /*
  * The function fiat_secp256k1_square squares a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) * eval (fiat_secp256k1_from_montgomery arg1)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -830,10 +828,9 @@ static void fiat_secp256k1_square(uint64_t out1[4], const uint64_t arg1[4]) {
 
 /*
  * The function fiat_secp256k1_add adds two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) + eval (fiat_secp256k1_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -885,10 +882,9 @@ static void fiat_secp256k1_add(uint64_t out1[4], const uint64_t arg1[4], const u
 
 /*
  * The function fiat_secp256k1_sub subtracts two field elements in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * arg2 = map (λ x, ⌊eval arg2 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg2 < m →
- * eval (fiat_secp256k1_from_montgomery out1) mod m = (eval (fiat_secp256k1_from_montgomery arg1) - eval (fiat_secp256k1_from_montgomery arg2)) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg2 < m →
+ * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -931,9 +927,8 @@ static void fiat_secp256k1_sub(uint64_t out1[4], const uint64_t arg1[4], const u
 
 /*
  * The function fiat_secp256k1_opp negates a field element in the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * eval (fiat_secp256k1_from_montgomery out1) mod m = -eval (fiat_secp256k1_from_montgomery arg1) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
+ * 0 ≤ eval arg1 < m →
+ * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -975,9 +970,8 @@ static void fiat_secp256k1_opp(uint64_t out1[4], const uint64_t arg1[4]) {
 
 /*
  * The function fiat_secp256k1_from_montgomery translates a field element out of the Montgomery domain.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -1242,8 +1236,8 @@ static void fiat_secp256k1_from_montgomery(uint64_t out1[4], const uint64_t arg1
 
 /*
  * The function fiat_secp256k1_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
- * out1 = 0 ↔ eval (fiat_secp256k1_from_montgomery arg1) mod m = 0
+ * 0 ≤ eval arg1 < m →
+ * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  * Output Bounds:
@@ -1281,7 +1275,7 @@ static void fiat_secp256k1_selectznz(uint64_t out1[4], fiat_secp256k1_uint1 arg1
 
 /*
  * The function fiat_secp256k1_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
- * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3] ∧ 0 ≤ eval arg1 < m →
+ * 0 ≤ eval arg1 < m →
  * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31]
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -1388,9 +1382,8 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
 
 /*
  * The function fiat_secp256k1_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
- * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..31] ∧ 0 ≤ bytes_eval arg1 < m →
+ * 0 ≤ bytes_eval arg1 < m →
  * eval out1 mod m = bytes_eval arg1 mod m
- * ∧ out1 = map (λ x, ⌊eval out1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..3]
  * ∧ 0 ≤ eval out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v
index ee2793c40..4d3e9c047 100644
--- a/src/PushButtonSynthesis/Primitives.v
+++ b/src/PushButtonSynthesis/Primitives.v
@@ -183,6 +183,9 @@ Module CorrectnessStringification.
       => strip_bounds_info T
     | list_Z_bounded_by _ _ -> ?T
       => strip_bounds_info T
+    | (_ = List.map (fun z => (_ mod _) / _) (List.seq _ _)) /\ (?a <= ?b < ?c) -> ?T
+      => let T := strip_bounds_info T in
+         constr:(a <= b < c -> T)
     | ?T /\ list_Z_bounded_by _ _
       => T
     | ?T /\ (match _ with pair _ _ => _ end = true)
@@ -191,8 +194,10 @@ Module CorrectnessStringification.
       => T
     | iff _ _
       => correctness
-    | _ = _ /\ (_ = _ /\ (_ <= _ < _))
-      => correctness
+    | ?x = ?y /\ (_ = List.map (fun z => (_ mod _) / _) (List.seq _ _)) /\ (?a <= ?b < ?c)
+      => constr:(x = y /\ a <= b < c)
+    | (_ = List.map (fun z => (_ mod _) / _) (List.seq _ _)) /\ (?a <= ?b < ?c)
+      => constr:(a <= b < c)
     | _ = _ :> list Z
       => correctness
     | forall x : ?T, ?f
diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v
index 46ffa083f..d95f35bf4 100644
--- a/src/PushButtonSynthesis/WordByWordMontgomery.v
+++ b/src/PushButtonSynthesis/WordByWordMontgomery.v
@@ -235,10 +235,11 @@ Section __.
           (CorrectnessStringification.dyn_context.cons
              r' ("((2^" ++ decimal_string_of_Z machine_wordsize ++ ")⁻¹ mod m)")%string
              (CorrectnessStringification.dyn_context.cons
-                from_montgomery_res (prefix ++ "from_montgomery")%string
+                from_montgomery_res "from_montgomery"%string
                 (CorrectnessStringification.dyn_context.cons
                    (@eval 8 n_bytes) "bytes_eval"%string
-                   CorrectnessStringification.dyn_context.nil)))).
+                   CorrectnessStringification.dyn_context.nil))))
+         (only parsing).
   Local Notation stringify_correctness prefix pre_extra correctness
     := (stringify_correctness_with_ctx
           (initial_ctx prefix)
-- 
cgit v1.2.3