Merge branch 'main' into jakemas/rej-uniform-asm

Resolves conflicts in:
- BIBLIOGRAPHY.md: combine HOL-Light asm file references
- mldsa/mldsa_native_asm.S: include both poly_caddq and rej_uniform
- proofs/hol_light/x86_64/Makefile: OBJ list combines both
- proofs/hol_light/x86_64/proofs/dump_bytecode.ml: dump both bytecodes
- test/bench/bench_components_mldsa.c: include both benchmarks

Signed-off-by: Jake Massimo <jakemas@amazon.com>

Author: jakemas

.github/actions/cbmc/action.yml

@@ -21,6 +21,9 @@ inputs:
   mldsa_parameter_set:
     description: "Security level for ML-DSA (2,3,5)"
     default: "2"
+  reduce_ram:
+    description: "Run CBMC proofs with MLD_CONFIG_REDUCE_RAM enabled"
+    default: "false"
   gh_token:
     description: Github access token to use
     required: true
@@ -47,22 +50,30 @@ runs:
               - $(nix --version)
               - $(cbmc --version)
               - litani Version $(litani --version)
-              - Cadical Version $(cadical --version)
               - $(bash --version | grep -m1 "")
             EOF
-      - name: Run CBMC proofs (MLD_CONFIG_PARAMETER_SET=${{ inputs.mldsa_parameter_set }})
+      - name: Run CBMC proofs (MLD_CONFIG_PARAMETER_SET=${{ inputs.mldsa_parameter_set }}, reduce_ram=${{ inputs.reduce_ram }})
         shell: ${{ env.SHELL }}
         env:
           GH_TOKEN: ${{ inputs.gh_token }}
         run: |
           echo "::group::cbmc_${{ inputs.mldsa_parameter_set }}"
-          tests cbmc --mldsa-parameter-set ${{ inputs.mldsa_parameter_set }} --per-proof-timeout 1800 --output-result-json ${{ github.workspace }}/cbmc_result_${{ inputs.mldsa_parameter_set }}.json || cbmc_failed=true
+          reduce_ram_flag=""
+          data_dir="dev/cbmc"
+          variant=""
+          if [ "${{ inputs.reduce_ram }}" = "true" ]; then
+            reduce_ram_flag="--reduce-ram"
+            data_dir="dev/cbmc-reduce-ram"
+            variant="reduce-ram"
+          fi
+          tests cbmc --mldsa-parameter-set ${{ inputs.mldsa_parameter_set }} --per-proof-timeout 1800 --output-result-json ${{ github.workspace }}/cbmc_result_${{ inputs.mldsa_parameter_set }}.json $reduce_ram_flag || cbmc_failed=true
           echo "::endgroup::"
           python3 ${{ github.action_path }}/report.py \
             --results-json "${{ github.workspace }}/cbmc_result_${{ inputs.mldsa_parameter_set }}.json" \
             --mldsa-parameter-set "${{ inputs.mldsa_parameter_set }}" \
             --min-runtime 20 \
             --regression-threshold 1.5 \
             --gh-pages-branch gh-pages \
-            --data-dir dev/cbmc
+            --data-dir "$data_dir" \
+            --variant "$variant"
           if [ "$cbmc_failed" = "true" ]; then exit 1; fi

.github/actions/cbmc/report.py

@@ -23,6 +23,7 @@
 OK = "✅"
 WARN = "⚠️"
 FAIL = "❌"
+SKIP = "⏭️"
 
 ProofResult = namedtuple(
     "ProofResult", ["name", "status", "current", "previous", "change"]
@@ -39,6 +40,12 @@ def get_args():
     parser.add_argument("--regression-threshold", type=float, default=1.5)
     parser.add_argument("--gh-pages-branch", default="gh-pages")
     parser.add_argument("--data-dir", default="dev/cbmc")
+    parser.add_argument(
+        "--variant",
+        default="",
+        help="Optional label distinguishing a build variant (e.g. 'reduce-ram'). "
+        "Used in PR comment tag/title so variants don't overwrite each other.",
+    )
     return parser.parse_args()
 
 
@@ -128,8 +135,26 @@ def build_comment(current, baseline, cfg):
         if is_alert:
             alerts.append(result)
 
+    skipped = sorted(current.get("skipped", []))
+    skipped_rows = []
+    for name in skipped:
+        base = baseline_runtimes.get(name, {})
+        if base.get("status") == "failed":
+            prev = "failed"
+        elif base.get("value") is not None:
+            prev = f"{base['value']}s"
+        else:
+            prev = "-"
+        skipped_rows.append(ProofResult(name, SKIP, "skipped", prev, "-"))
+    alerts.extend(skipped_rows)
+    all_rows.extend(skipped_rows)
+
     def sort_key(r):
-        return -1 if r.current == "-" else -int(r.current.rstrip("s"))
+        if r.current == "skipped":
+            return 1  # skipped proofs sink below any timed row
+        if r.current == "-":
+            return -1
+        return -int(r.current.rstrip("s"))
 
     all_rows.sort(key=sort_key)
 
@@ -155,15 +180,22 @@ def sort_key(r):
         alerts.insert(0, total_row)
 
     lines = [
-        f"<!-- {COMMENT_TAG}(start): mldsa-{cfg.param_set} -->",
-        f"## CBMC Results (ML-DSA-{cfg.param_set})",
+        f"<!-- {COMMENT_TAG}(start): mldsa-{cfg.param_set}{cfg.tag_suffix} -->",
+        f"## CBMC Results (ML-DSA-{cfg.param_set}{cfg.title_suffix})",
         "",
     ]
 
+    if skipped:
+        lines += [
+            f"{SKIP} **{len(skipped)} proof(s) skipped** "
+            f"(see `proofs/cbmc/reduce_ram_skip.txt`)",
+            "",
+        ]
+
     if alerts:
         lines += [f"{WARN} **Attention Required**", ""] + render_table(alerts) + [""]
 
-    total = current.get("summary", {}).get("total", len(all_rows))
+    total = current.get("summary", {}).get("total", len(all_rows)) + len(skipped)
     lines += (
         [
             "<details>",
@@ -175,15 +207,15 @@ def sort_key(r):
             "",
             "</details>",
             "",
-            f"<!-- {COMMENT_TAG}(end): mldsa-{cfg.param_set} -->",
+            f"<!-- {COMMENT_TAG}(end): mldsa-{cfg.param_set}{cfg.tag_suffix} -->",
         ]
     )
     return "\n".join(lines)
 
 
 def post_or_update_comment(pr_number, body, cfg):
     """Post or update PR comment."""
-    tag = f"<!-- {COMMENT_TAG}(start): mldsa-{cfg.param_set} -->"
+    tag = f"<!-- {COMMENT_TAG}(start): mldsa-{cfg.param_set}{cfg.tag_suffix} -->"
     result = subprocess.run(
         [
             "gh",
@@ -279,6 +311,8 @@ def push_to_gh_pages(current, cfg):
 def main():
     args = get_args()
     args.param_set = args.mldsa_parameter_set
+    args.tag_suffix = f"-{args.variant}" if args.variant else ""
+    args.title_suffix = f", {args.variant.upper()}" if args.variant else ""
 
     with open(args.results_json) as f:
         current = json.load(f)