Merge pull request #677 from pq-code-package/ntt_no_div

NTT: Simplify computation of zeta index

Author: mkannwischer

.github/workflows/base.yml

@@ -272,3 +272,26 @@ jobs:
             ./scripts/autogen ${{ matrix.backend.arg }} ${{ matrix.simplify.arg }}
             make clean
             OPT=1 make quickcheck
+  scan-build:
+    strategy:
+      fail-fast: false
+      matrix:
+        external:
+         - ${{ github.repository_owner != 'pq-code-package' }}
+        target:
+         - runner: pqcp-arm64
+           name: 'aarch64'
+         - runner: ubuntu-latest
+           name: 'x86_64'
+    name: scan-build (${{ matrix.target.name }})
+    runs-on: ${{ matrix.target.runner }}
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - uses: ./.github/actions/setup-apt
+        with:
+          packages: clang-tools clang
+      - name: make quickcheck
+        run: |
+          scan-build --status-bugs make quickcheck OPT=0
+          make clean >/dev/null
+          scan-build --status-bugs make quickcheck OPT=1 

.github/workflows/bench_ec2_reusable.yml

@@ -100,7 +100,7 @@ jobs:
           echo "Using AMI ID: $AMI_ID"
           echo "AMI_ID=$AMI_ID" >> $GITHUB_OUTPUT
       - name: Configure AWS credentials
-        uses: aws-actions/configure-aws-credentials@4fc4975a852c8cd99761e2de1f4ba73402e44dd9 # v4.0.3
+        uses: aws-actions/configure-aws-credentials@ececac1a45f3b08a01d2dd070d28d111c5fe6722 # v4.1.0
         with:
           role-to-assume: ${{ env.AWS_ROLE }}
           aws-region: ${{ inputs.aws_region }}
@@ -209,7 +209,7 @@ jobs:
     if: ${{ always() }} # required to stop the runner even if the error happened in the previous jobs
     steps:
       - name: Configure AWS credentials
-        uses: aws-actions/configure-aws-credentials@4fc4975a852c8cd99761e2de1f4ba73402e44dd9 # v4.0.3
+        uses: aws-actions/configure-aws-credentials@ececac1a45f3b08a01d2dd070d28d111c5fe6722 # v4.1.0
         with:
           role-to-assume: ${{ env.AWS_ROLE }}
           aws-region: ${{ inputs.aws_region }}

.github/workflows/ci_ec2_container.yml

@@ -95,7 +95,7 @@ jobs:
           echo "Using AMI ID: $AMI_ID"
           echo "AMI_ID=$AMI_ID" >> $GITHUB_OUTPUT
       - name: Configure AWS credentials
-        uses: aws-actions/configure-aws-credentials@4fc4975a852c8cd99761e2de1f4ba73402e44dd9 # v4.0.3
+        uses: aws-actions/configure-aws-credentials@ececac1a45f3b08a01d2dd070d28d111c5fe6722 # v4.1.0
         with:
           role-to-assume: ${{ env.AWS_ROLE }}
           aws-region: ${{ env.AWS_REGION }}
@@ -168,7 +168,7 @@ jobs:
     if: ${{ always() }} # required to stop the runner even if the error happened in the previous jobs
     steps:
       - name: Configure AWS credentials
-        uses: aws-actions/configure-aws-credentials@4fc4975a852c8cd99761e2de1f4ba73402e44dd9 # v4.0.3
+        uses: aws-actions/configure-aws-credentials@ececac1a45f3b08a01d2dd070d28d111c5fe6722 # v4.1.0
         with:
           role-to-assume: ${{ env.AWS_ROLE }}
           aws-region: ${{ env.AWS_REGION }}

.github/workflows/ci_ec2_reusable.yml

@@ -92,7 +92,7 @@ jobs:
           echo "Using AMI ID: $AMI_ID"
           echo "AMI_ID=$AMI_ID" >> $GITHUB_OUTPUT
       - name: Configure AWS credentials
-        uses: aws-actions/configure-aws-credentials@4fc4975a852c8cd99761e2de1f4ba73402e44dd9 # v4.0.3
+        uses: aws-actions/configure-aws-credentials@ececac1a45f3b08a01d2dd070d28d111c5fe6722 # v4.1.0
         with:
           role-to-assume: ${{ env.AWS_ROLE }}
           aws-region: ${{ env.AWS_REGION }}
@@ -153,7 +153,7 @@ jobs:
     if: ${{ always() }} # required to stop the runner even if the error happened in the previous jobs
     steps:
       - name: Configure AWS credentials
-        uses: aws-actions/configure-aws-credentials@4fc4975a852c8cd99761e2de1f4ba73402e44dd9 # v4.0.3
+        uses: aws-actions/configure-aws-credentials@ececac1a45f3b08a01d2dd070d28d111c5fe6722 # v4.1.0
         with:
           role-to-assume: ${{ env.AWS_ROLE }}
           aws-region: ${{ env.AWS_REGION }}

.github/workflows/scorecard.yaml

@@ -30,7 +30,7 @@ jobs:
           persist-credentials: false
 
       - name: "Run analysis"
-        uses: ossf/scorecard-action@62b2cac7ed8198b15735ed49ab1e5cf35480ba46 # v2.4.0
+        uses: ossf/scorecard-action@f49aabe0b5af0936a0987cfb85d86b75731b0186 # v2.4.1
         with:
           results_file: results.sarif
           results_format: sarif
@@ -48,7 +48,7 @@ jobs:
       # Upload the results as artifacts (optional). Commenting out will disable uploads of run results in SARIF
       # format to the repository Actions tab.
       - name: "Upload artifact"
-        uses: actions/upload-artifact@65c4c4a1ddee5b72f698fdd19549f0f0fb45cf08 # v4.6.0
+        uses: actions/upload-artifact@4cec3d8aa04e39d1a68397de0c4cd6fb9dce8ec1 # v4.6.1
         with:
           name: SARIF file
           path: results.sarif

mlkem/poly.c

@@ -349,29 +349,22 @@ __contract__(
  * Compute one layer of forward NTT
  * Parameters:
  * - r: Pointer to base of polynomial
- * - len: Stride of butterflies in this layer.
- * - layer: Ghost variable indicating which layer is being applied.
- *          Must match `len` via `len == MLKEM_N >> layer`.
- * Note: `len` could be dropped and computed in the function, but
- *   we are following the structure of the reference NTT from the
- *   official Kyber implementation here, merely adding `layer` as
- *   a ghost variable for the specifications.
+ * - layer: Variable indicating which layer is being applied.
  */
 
 /* Reference: Embedded in `ntt()` in the reference implementation. */
-static void mlk_ntt_layer(int16_t r[MLKEM_N], unsigned len, unsigned layer)
+static void mlk_ntt_layer(int16_t r[MLKEM_N], unsigned layer)
 __contract__(
   requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
-  requires(1 <= layer && layer <= 7 && len == (MLKEM_N >> layer))
+  requires(1 <= layer && layer <= 7)
   requires(array_abs_bound(r, 0, MLKEM_N, layer * MLKEM_Q))
   assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
   ensures(array_abs_bound(r, 0, MLKEM_N, (layer + 1) * MLKEM_Q)))
 {
-  unsigned start, k;
-  /* `layer` is a ghost variable only needed in the CBMC specification */
-  ((void)layer);
-  /* Twiddle factors for layer n start at index 2^(layer-1) */
-  k = MLKEM_N / (2 * len);
+  unsigned start, k, len;
+  /* Twiddle factors for layer n are at indices 2^(n-1)..2^n-1. */
+  k = 1u << (layer - 1);
+  len = MLKEM_N >> layer;
   for (start = 0; start < MLKEM_N; start += 2 * len)
   __loop__(
     invariant(start < MLKEM_N + 2 * len)
@@ -393,21 +386,23 @@ __contract__(
  * the proof may need strengthening.
  */
 
-/* Reference: `ntt()` in the reference implementation. */
+/* Reference: `ntt()` in the reference implementation.
+ * - Iterate over `layer` instead of `len` in the outer loop
+ *   to simplify computation of zeta index. */
 MLK_INTERNAL_API
 void mlk_poly_ntt(mlk_poly *p)
 {
-  unsigned len, layer;
+  unsigned layer;
   int16_t *r;
   mlk_assert_abs_bound(p, MLKEM_N, MLKEM_Q);
   r = p->coeffs;
 
-  for (len = 128, layer = 1; len >= 2; len >>= 1, layer++)
+  for (layer = 1; layer <= 7; layer++)
   __loop__(
-    invariant(1 <= layer && layer <= 8 && len == (MLKEM_N >> layer))
+    invariant(1 <= layer && layer <= 8)
     invariant(array_abs_bound(r, 0, MLKEM_N, layer * MLKEM_Q)))
   {
-    mlk_ntt_layer(r, len, layer);
+    mlk_ntt_layer(r, layer);
   }
 
   /* Check the stronger bound */
@@ -429,19 +424,17 @@ void mlk_poly_ntt(mlk_poly *p)
 /* Compute one layer of inverse NTT */
 
 /* Reference: Embedded into `invntt()` in the reference implementation */
-static void mlk_invntt_layer(int16_t *r, unsigned len, unsigned layer)
+static void mlk_invntt_layer(int16_t *r, unsigned layer)
 __contract__(
   requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
-  requires(2 <= len && len <= 128 && 1 <= layer && layer <= 7)
-  requires(len == (1 << (8 - layer)))
+  requires(1 <= layer && layer <= 7)
   requires(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))
   assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
   ensures(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q)))
 {
-  unsigned start, k;
-  /* `layer` is a ghost variable used only in the specification */
-  ((void)layer);
-  k = MLKEM_N / len - 1;
+  unsigned start, k, len;
+  len = (MLKEM_N >> layer);
+  k = (1u << layer) - 1;
   for (start = 0; start < MLKEM_N; start += 2 * len)
   __loop__(
     invariant(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))
@@ -478,7 +471,7 @@ void mlk_poly_invntt_tomont(mlk_poly *p)
    * and NTT twist. This also brings coefficients down to
    * absolute value < MLKEM_Q.
    */
-  unsigned j, len, layer;
+  unsigned j, layer;
   const int16_t f = 1441; /* check-magic: 1441 == pow(2,32 - 7,MLKEM_Q) */
   int16_t *r = p->coeffs;
 
@@ -491,12 +484,12 @@ void mlk_poly_invntt_tomont(mlk_poly *p)
   }
 
   /* Run the invNTT layers */
-  for (len = 2, layer = 7; len <= 128; len <<= 1, layer--)
+  for (layer = 7; layer > 0; layer--)
   __loop__(
-    invariant(2 <= len && len <= 256 && layer <= 7 && len == (1 << (8 - layer)))
+    invariant(0 <= layer && layer < 8)
     invariant(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q)))
   {
-    mlk_invntt_layer(p->coeffs, len, layer);
+    mlk_invntt_layer(r, layer);
   }
 
   mlk_assert_abs_bound(p, MLKEM_N, MLK_INVNTT_BOUND);

proofs/cbmc/invntt_layer/invntt_layer_harness.c

@@ -6,11 +6,11 @@
 #include "common.h"
 
 
-void mlk_invntt_layer(int16_t *p, unsigned len, unsigned layer);
+void mlk_invntt_layer(int16_t *p, unsigned layer);
 
 void harness(void)
 {
   int16_t *a;
-  unsigned len, layer;
-  mlk_invntt_layer(a, len, layer);
+  unsigned layer;
+  mlk_invntt_layer(a, layer);
 }

proofs/cbmc/ntt_layer/ntt_layer_harness.c

@@ -5,11 +5,11 @@
 #include "poly.h"
 
 
-void mlk_ntt_layer(int16_t *p, unsigned len, unsigned layer);
+void mlk_ntt_layer(int16_t *p, unsigned layer);
 
 void harness(void)
 {
   int16_t *a;
-  unsigned len, layer;
-  mlk_ntt_layer(a, len, layer);
+  unsigned layer;
+  mlk_ntt_layer(a, layer);
 }

test/mk/rules.mk

@@ -20,6 +20,8 @@ $(BUILD_DIR)/%.a: $(CONFIG)
 	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
 	$(Q)rm -f $@
 	$(Q)$(CC_AR) rcs $@ $(filter %.o,$^)
+# skip test when run in scan-build as it does not work
+ifneq ($(findstring ccc-analyzer,$(CC)),ccc-analyzer)
         # $AR doesn't care about duplicated symbols, one can only find it out
         # via actually linking. The easiest one to do this that one can think
         # of is to create a dummy C file with empty main function on the fly,
@@ -42,6 +44,7 @@ else                                           # if not on macOS or cross compil
 	$(Q)rm -f $(@:%.a=%_tmp.a.out)
 endif
 	$(Q)echo "  AR         Checked for duplicated symbols"
+endif
 
 $(BUILD_DIR)/mlkem512/%.c.o: %.c $(CONFIG)
 	$(Q)echo "  CC      $@"