host: Mac-side LSC-1 runtime and lean_compiler integration scaffold #140
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: CI | |
| on: | |
| push: | |
| pull_request: | |
| permissions: | |
| contents: read | |
| jobs: | |
| executable-models: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 | |
| - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 | |
| with: | |
| python-version: "3.13" | |
| - name: Install pinned Python dependencies | |
| run: python -m pip install -r requirements.txt | |
| - name: Python, analytical counts, and structural checks | |
| run: make check | |
| - name: Record FPGA detection ladder (no board attached; reporting only) | |
| run: make fpga-detect | |
| systemverilog: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 | |
| - name: Install Icarus Verilog | |
| run: sudo apt-get update && sudo apt-get install -y iverilog | |
| - name: Checkout clean detached frozen upstream oracle | |
| run: >- | |
| git clone https://github.com/leanEthereum/leanVM-b.git /tmp/leanVM-b && | |
| git -C /tmp/leanVM-b checkout --detach c308034ab78619b39a59d26f3dc60e7df5b52649 && | |
| test -z "$(git -C /tmp/leanVM-b status --porcelain --untracked-files=all)" && | |
| test -z "$(git -C /tmp/leanVM-b symbolic-ref -q HEAD)" | |
| - name: Install pinned Rust for locked frozen-oracle probe | |
| run: rustup toolchain install 1.88.0 --profile minimal | |
| - name: Compile and simulate RTL | |
| run: LEANVM_B_UPSTREAM=/tmp/leanVM-b make sim m2-differential | |
| lean: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 | |
| - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| lake-package-directory: lean | |
| build: true | |
| - name: Explicit Lean library target | |
| run: cd lean && lake build LeanVMBMinCore | |
| formal-and-lint: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 | |
| - uses: YosysHQ/setup-oss-cad-suite@aefa8397bbf8fc6670a0a62af9805a89738f3cde | |
| - name: Bounded GF(2^8) proof | |
| run: cd formal && sby -f gf8_mul.sby | |
| - name: WIDTH=128 byte-serialization order proof | |
| run: cd formal && sby -f gf128_serialize.sby | |
| - name: Bound checker is elaborated inside the shipped stream ALU | |
| # The built-in Yosys frontend silently drops `bind`, which would make | |
| # the next step a vacuous pass. Fail loudly if no checker cell exists. | |
| # Pre-flight report only: the authoritative gate is the same | |
| # `select -assert-min` assertion inside stream_alu_mul_pulse.sby, which | |
| # ties the check to the run that actually produces the proof. | |
| run: >- | |
| cd formal && yosys -p 'plugin -i slang; | |
| read_slang --top stream_alu_mul_pulse_formal --keep-hierarchy | |
| ../asic_core/rtl/gf2n_mul_bitstream.sv ../asic_core/rtl/gf128_mul_bitstream.sv | |
| ../asic_core/rtl/leanvm_b_stream_alu.sv stream_alu_mul_pulse_formal.sv; | |
| prep -top stream_alu_mul_pulse_formal; | |
| select -assert-min 4 leanvm_b_mul_pulse_check*/t:$check' | |
| - name: Multiplier pulse mutual-exclusion proof on shipped RTL | |
| run: cd formal && sby -f stream_alu_mul_pulse.sby | |
| - name: Yosys lint and synthesis | |
| run: >- | |
| yosys -p 'read_verilog -sv asic_core/rtl/gf2n_mul_bitstream.sv asic_core/rtl/gf128_mul_bitstream.sv asic_core/rtl/leanvm_b_stream_alu.sv asic_core/rtl/lean_silicon_lsc1.sv; | |
| hierarchy -check -top lean_silicon_lsc1; proc; check; synth -top lean_silicon_lsc1; stat' | |
| - name: M2 controller lint and synthesis | |
| run: >- | |
| yosys -p 'read_verilog -sv src/leanvm_b_m2_scalar_controller.sv; | |
| hierarchy -check -top leanvm_b_m2_scalar_controller; proc; check; synth -top leanvm_b_m2_scalar_controller; stat' |