From ce583d76bdb8f15148fc4222d8bdec096547682a Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 1 Feb 2019 18:50:00 -0500
Subject: Use Preconditions: Postconditions:, rather than /\ and ->

---
 p224_32.c | 109 +++++++++++++++++++++++++++++++++++++++++---------------------
 1 file changed, 73 insertions(+), 36 deletions(-)

(limited to 'p224_32.c')

diff --git a/p224_32.c b/p224_32.c
index aacad91e5..1341276cb 100644
--- a/p224_32.c
+++ b/p224_32.c
@@ -18,8 +18,10 @@ typedef signed char fiat_p224_int1;
 
 /*
  * The function fiat_p224_addcarryx_u32 is an addition with carry.
- * out1 = (arg1 + arg2 + arg3) mod 2^32
- * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋
+ * Postconditions:
+ *   out1 = (arg1 + arg2 + arg3) mod 2^32
+ *   out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋
+ *
  * Input Bounds:
  *   arg1: [0x0 ~> 0x1]
  *   arg2: [0x0 ~> 0xffffffff]
@@ -38,8 +40,10 @@ static void fiat_p224_addcarryx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat_
 
 /*
  * The function fiat_p224_subborrowx_u32 is a subtraction with borrow.
- * out1 = (-arg1 + arg2 + -arg3) mod 2^32
- * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋
+ * Postconditions:
+ *   out1 = (-arg1 + arg2 + -arg3) mod 2^32
+ *   out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋
+ *
  * Input Bounds:
  *   arg1: [0x0 ~> 0x1]
  *   arg2: [0x0 ~> 0xffffffff]
@@ -58,8 +62,10 @@ static void fiat_p224_subborrowx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat
 
 /*
  * The function fiat_p224_mulx_u32 is a multiplication, returning the full double-width result.
- * out1 = (arg1 * arg2) mod 2^32
- * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋
+ * Postconditions:
+ *   out1 = (arg1 * arg2) mod 2^32
+ *   out2 = ⌊arg1 * arg2 / 2^32⌋
+ *
  * Input Bounds:
  *   arg1: [0x0 ~> 0xffffffff]
  *   arg2: [0x0 ~> 0xffffffff]
@@ -77,7 +83,9 @@ static void fiat_p224_mulx_u32(uint32_t* out1, uint32_t* out2, uint32_t arg1, ui
 
 /*
  * The function fiat_p224_cmovznz_u32 is a single-word conditional move.
- * out1 = (if arg1 = 0 then arg2 else arg3)
+ * Postconditions:
+ *   out1 = (if arg1 = 0 then arg2 else arg3)
+ *
  * Input Bounds:
  *   arg1: [0x0 ~> 0x1]
  *   arg2: [0x0 ~> 0xffffffff]
@@ -94,10 +102,13 @@ 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.
- * 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
+ * Preconditions:
+ *   0 ≤ eval arg1 < m
+ *   0 ≤ eval arg2 < m
+ * Postconditions:
+ *   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]]
  *   arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -977,9 +988,12 @@ 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.
- * 0 ≤ eval arg1 < m →
- * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
- * ∧ 0 ≤ eval out1 < m
+ * Preconditions:
+ *   0 ≤ eval arg1 < m
+ * Postconditions:
+ *   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]]
  * Output Bounds:
@@ -1858,10 +1872,13 @@ 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.
- * 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
+ * Preconditions:
+ *   0 ≤ eval arg1 < m
+ *   0 ≤ eval arg2 < m
+ * Postconditions:
+ *   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]]
  *   arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -1939,10 +1956,13 @@ 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.
- * 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
+ * Preconditions:
+ *   0 ≤ eval arg1 < m
+ *   0 ≤ eval arg2 < m
+ * Postconditions:
+ *   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]]
  *   arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2005,9 +2025,12 @@ 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.
- * 0 ≤ eval arg1 < m →
- * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
- * ∧ 0 ≤ eval out1 < m
+ * Preconditions:
+ *   0 ≤ eval arg1 < m
+ * Postconditions:
+ *   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]]
  * Output Bounds:
@@ -2069,9 +2092,12 @@ 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.
- * 0 ≤ eval arg1 < m →
- * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^7) mod m
- * ∧ 0 ≤ eval out1 < m
+ * Preconditions:
+ *   0 ≤ eval arg1 < m
+ * Postconditions:
+ *   eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^7) mod m
+ *   0 ≤ eval out1 < m
+ *
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
  * Output Bounds:
@@ -2608,8 +2634,11 @@ 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.
- * 0 ≤ eval arg1 < m →
- * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
+ * Preconditions:
+ *   0 ≤ eval arg1 < m
+ * Postconditions:
+ *   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:
@@ -2622,7 +2651,9 @@ static void fiat_p224_nonzero(uint32_t* out1, const uint32_t arg1[7]) {
 
 /*
  * The function fiat_p224_selectznz is a multi-limb conditional select.
- * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3)
+ * Postconditions:
+ *   eval out1 = (if arg1 = 0 then eval arg2 else eval arg3)
+ *
  * Input Bounds:
  *   arg1: [0x0 ~> 0x1]
  *   arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
@@ -2656,8 +2687,11 @@ 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.
- * 0 ≤ eval arg1 < m →
- * out1 = map (λ x, ⌊(eval arg1 mod m) mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..27]
+ * Preconditions:
+ *   0 ≤ eval arg1 < m
+ * Postconditions:
+ *   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]]
  * Output Bounds:
@@ -2751,9 +2785,12 @@ 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.
- * 0 ≤ bytes_eval arg1 < m →
- * eval out1 mod m = bytes_eval arg1 mod m
- * ∧ 0 ≤ eval out1 < m
+ * Preconditions:
+ *   0 ≤ bytes_eval arg1 < m
+ * Postconditions:
+ *   eval out1 mod m = bytes_eval arg1 mod m
+ *   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]]
  * Output Bounds:
-- 
cgit v1.2.3