docs(readme): use the richer visualize-pipeline 3D model #64
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: verify | |
| on: | |
| push: | |
| pull_request: | |
| jobs: | |
| verify: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: true | |
| - uses: astral-sh/setup-uv@v5 | |
| - name: formal verification (must print VERIFIED) | |
| run: uv run verification/verify_radix2.py | |
| - name: INTT halving finding (reproduce + validate fix) | |
| run: uv run verification/bug_intt_halving.py | |
| - name: non-vacuity mutation tests | |
| run: uv run verification/mutation_test.py | |
| - name: deep full-basis N=1024 round-trip | |
| run: DEEP_VERIFY=1 uv run verification/verify_radix2.py | |
| - name: proposed CFNTT-KRED — bit-exact math + e2e polymult | |
| run: uv run kred-butterfly/kred_math.py | |
| - name: proposed CFNTT-KRED — z3 full-domain reduction proof | |
| run: uv run kred-butterfly/verify_kred.py | |
| - name: proposed psi-fold ROM — math + e2e | |
| run: uv run psi-fold-rom/rom_fold_math.py | |
| - name: proposed psi-fold ROM — z3 fold proof | |
| run: uv run psi-fold-rom/verify_rom_fold.py | |
| - name: proposed psi-fold ROM — generated RTL in sync | |
| run: uv run psi-fold-rom/gen_rom_fold.py && git diff --exit-code psi-fold-rom/tf_rom_fold.v | |
| - name: install iverilog for full-core sim | |
| run: sudo apt-get update && sudo apt-get install -y iverilog | |
| - name: proposed full-transform RTL simulation (iverilog) | |
| run: uv run verification/fullcore/run_stream.py | |
| - name: newcore — own-FSM whole-core round-trip + NTT cross-validation | |
| run: python3 ntt-core/run_check.py | |
| - name: generalization — Proth-prime generator (Falcon + Kyber) | |
| run: uv run generator/kred_gen.py | |
| - name: generalization — generated Kyber RTL under iverilog | |
| run: uv run generator/gen_check.py | |
| - name: paper builds (pandoc -> LaTeX skeleton) | |
| run: | | |
| sudo apt-get update && sudo apt-get install -y pandoc | |
| make -C docs/paper paper.tex | |
| yosys-formal: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: true | |
| # Install the OSS CAD Suite with retries: the upstream setup action | |
| # intermittently fails fetching its release tarball, flaking docs-only | |
| # pushes. Fetch directly with curl --retry and cache the extract. | |
| - name: install oss-cad-suite (retrying) | |
| run: | | |
| set -euo pipefail | |
| # Resolve the latest release and fetch its tarball with retries; the | |
| # upstream setup action intermittently fails, flaking CI. | |
| ver=$(curl -fsSL --retry 5 --retry-all-errors \ | |
| https://api.github.com/repos/YosysHQ/oss-cad-suite-build/releases/latest \ | |
| | sed -n 's/.*"tag_name": *"\([0-9-]*\)".*/\1/p' | head -1) | |
| date=${ver//-/} | |
| url="https://github.com/YosysHQ/oss-cad-suite-build/releases/download/${ver}/oss-cad-suite-linux-x64-${date}.tgz" | |
| echo "fetching $url" | |
| for i in 1 2 3 4 5; do | |
| curl -fL --retry 5 --retry-all-errors -o oss.tgz "$url" && break || { echo "retry $i"; sleep 15; } | |
| done | |
| tar xf oss.tgz | |
| echo "$PWD/oss-cad-suite/bin" >> "$GITHUB_PATH" | |
| - name: SymbiYosys + LEC + audits (BMC tasks; see verification/reference-fv/README.md) | |
| run: MODE=bmc ./verification/reference-fv/run_all.sh | |
| - name: FPGA-primitive cost (per-module + whole-core, synth_xilinx) | |
| run: fpga/fpga_cost.sh && fpga/fpga_cost_core.sh | |
| - uses: astral-sh/setup-uv@v5 | |
| - name: proposed suite — RTL proofs, audits, mutation sweep | |
| run: ./run_all.sh |