From 496271f86e9dc6df1b23a189d6b8fd2a82db33aa Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 30 Jan 2019 19:13:27 -0500
Subject: Add autogenerated docstrings to synthesized code

We now stringify the correctness conditions to generate docstrings for
the synthesized code.

Closes #512

Time commitment: about 6 hours
---
 p384_64.c | 57 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)

(limited to 'p384_64.c')

diff --git a/p384_64.c b/p384_64.c
index e5cc08628..ad116b2c7 100644
--- a/p384_64.c
+++ b/p384_64.c
@@ -19,6 +19,9 @@ typedef unsigned __int128 fiat_p384_uint128;
 
 
 /*
+ * The function fiat_p384_addcarryx_u64 is an add with carry.
+ * out1 = (arg1 + arg2 + arg3) mod 2^64
+ * ∧ out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
  * Input Bounds:
  *   arg1: [0x0 ~> 0x1]
  *   arg2: [0x0 ~> 0xffffffffffffffff]
@@ -36,6 +39,9 @@ static void fiat_p384_addcarryx_u64(uint64_t* out1, fiat_p384_uint1* out2, fiat_
 }
 
 /*
+ * The function fiat_p384_subborrowx_u64 is a sub with borrow.
+ * out1 = (-arg1 + arg2 + -arg3) mod 2^64
+ * ∧ out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋
  * Input Bounds:
  *   arg1: [0x0 ~> 0x1]
  *   arg2: [0x0 ~> 0xffffffffffffffff]
@@ -53,6 +59,9 @@ static void fiat_p384_subborrowx_u64(uint64_t* out1, fiat_p384_uint1* out2, fiat
 }
 
 /*
+ * The function fiat_p384_mulx_u64 is an extended multiplication.
+ * out1 = (arg1 * arg2) mod 2^64
+ * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋
  * Input Bounds:
  *   arg1: [0x0 ~> 0xffffffffffffffff]
  *   arg2: [0x0 ~> 0xffffffffffffffff]
@@ -69,6 +78,8 @@ static void fiat_p384_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg1, ui
 }
 
 /*
+ * The function fiat_p384_cmovznz_u64 is a single-word conditional move.
+ * out1 = (if arg1 = 0 then arg2 else arg3)
  * Input Bounds:
  *   arg1: [0x0 ~> 0x1]
  *   arg2: [0x0 ~> 0xffffffffffffffff]
@@ -84,6 +95,12 @@ static void fiat_p384_cmovznz_u64(uint64_t* out1, fiat_p384_uint1 arg1, uint64_t
 }
 
 /*
+ * The function fiat_p384_mul does stuff.
+ * 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 out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  *   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -838,6 +855,11 @@ static void fiat_p384_mul(uint64_t out1[6], const uint64_t arg1[6], const uint64
 }
 
 /*
+ * The function fiat_p384_square does stuff.
+ * 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 out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  * Output Bounds:
@@ -1591,6 +1613,12 @@ static void fiat_p384_square(uint64_t out1[6], const uint64_t arg1[6]) {
 }
 
 /*
+ * The function fiat_p384_add does stuff.
+ * 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 out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  *   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -1658,6 +1686,12 @@ static void fiat_p384_add(uint64_t out1[6], const uint64_t arg1[6], const uint64
 }
 
 /*
+ * The function fiat_p384_sub does stuff.
+ * 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 out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  *   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -1712,6 +1746,11 @@ static void fiat_p384_sub(uint64_t out1[6], const uint64_t arg1[6], const uint64
 }
 
 /*
+ * The function fiat_p384_opp does stuff.
+ * 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 out1 < m
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  * Output Bounds:
@@ -1765,6 +1804,11 @@ static void fiat_p384_opp(uint64_t out1[6], const uint64_t arg1[6]) {
 }
 
 /*
+ * The function fiat_p384_from_montgomery does stuff.
+ * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 0 ≤ eval arg1 < m →
+ * eval out1 mod m = (eval arg1 * 9173994466096273082364193663603369469355812071275829017307008127494733112176079729898163604637719575134209^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]]
  * Output Bounds:
@@ -2297,6 +2341,9 @@ static void fiat_p384_from_montgomery(uint64_t out1[6], const uint64_t arg1[6])
 }
 
 /*
+ * The function fiat_p384_nonzero does stuff.
+ * 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
  * Input Bounds:
  *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  * Output Bounds:
@@ -2308,6 +2355,8 @@ static void fiat_p384_nonzero(uint64_t* out1, const uint64_t arg1[6]) {
 }
 
 /*
+ * The function fiat_p384_selectznz is a multi-limb conditional select.
+ * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3)
  * Input Bounds:
  *   arg1: [0x0 ~> 0x1]
  *   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
@@ -2337,6 +2386,9 @@ static void fiat_p384_selectznz(uint64_t out1[6], fiat_p384_uint1 arg1, const ui
 }
 
 /*
+ * The function fiat_p384_to_bytes does stuff.
+ * arg1 = map (λ x, ⌊eval arg1 mod 2^(64 * (x + 1)) / 2^(64 * x)⌋) [0..5] ∧ 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]]
  * Output Bounds:
@@ -2489,6 +2541,11 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) {
 }
 
 /*
+ * The function fiat_p384_from_bytes does stuff.
+ * arg1 = map (λ x, ⌊bytes_eval arg1 mod 2^(8 * (x + 1)) / 2^(8 * x)⌋) [0..47] ∧ 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]]
  * Output Bounds:
-- 
cgit v1.2.3