Skip to content

WORKLOAD_VALIDATION.md

Latest commit

 

History

History
110 lines (95 loc) · 6.57 KB

WORKLOAD_VALIDATION.md

File metadata and controls

110 lines (95 loc) · 6.57 KB
Raw

Realistic leanVM-b / zkDSL workload validation

This is the dedicated issue #51 lane. It is non-release work and is explicitly outside the SKY26c submission critical path: it is not called by check, does not modify src/, release/, FPGA bitstreams, GDS, tags, or release gates.

Reproduce

Live compiler execution requires x86_64 Linux, mount namespaces, and non-interactive passwordless sudo for the fixed privileged broker commands. The filesystem root of the selected Rust toolchain must be provisioned as its own read-only mount, making the private copy immutable before this invocation begins. The validator checks these prerequisites while compiling and fails closed when one is absent.

Check out the exact candidate head and the pinned upstream leanVM-b commit, then use private mutable caches outside either checkout:

private=$(mktemp -d /tmp/lean-silicon-workload.XXXXXX)
mkdir -p "$private/receipt" "$private/tmp"
chmod 700 "$private" "$private/receipt" "$private/tmp"
git clone https://github.com/leanEthereum/leanVM-b.git "$private/leanVM-b"
git -C "$private/leanVM-b" checkout --detach c308034ab78619b39a59d26f3dc60e7df5b52649
export CARGO_HOME="$private/cargo" RUSTUP_HOME="$private/rustup" TMPDIR="$private/tmp"
export PATH="$CARGO_HOME/bin:$PATH"
rustup toolchain install 1.88.0-x86_64-unknown-linux-gnu --profile minimal
installed_toolchain=$(dirname "$(dirname "$(rustup which --toolchain 1.88.0-x86_64-unknown-linux-gnu cargo)")")
toolchain_mb=$(du -sm "$installed_toolchain" | awk '{print $1}')
truncate -s "$((toolchain_mb + 256))M" "$private/rust-toolchain.ext4"
/usr/sbin/mkfs.ext4 -q "$private/rust-toolchain.ext4"
mkdir "$private/rust-toolchain-ro"
sudo mount -o loop "$private/rust-toolchain.ext4" "$private/rust-toolchain-ro"
sudo cp -a "$installed_toolchain/." "$private/rust-toolchain-ro/"
sudo umount "$private/rust-toolchain-ro"
rustup toolchain uninstall 1.88.0-x86_64-unknown-linux-gnu
sudo mount -o loop,ro "$private/rust-toolchain.ext4" "$private/rust-toolchain-ro"
rustup toolchain link leanvm-validation-1.88.0 "$private/rust-toolchain-ro"
WORKLOAD_CACHE="$private/receipt" LEANVM_B_UPSTREAM="$private/leanVM-b" make workload-validation
python3 -m json.tool "$private/receipt/receipt.json"
rustup toolchain uninstall leanvm-validation-1.88.0
sudo umount "$private/rust-toolchain-ro"

The command rejects a dirty candidate or upstream checkout, an upstream SHA or Cargo.lock mismatch, a non-private/in-tree receipt directory, changed source, origin, or artifact hashes, changed elaboration counts, and outcomes that do not reproduce the plan. For every workload it recompiles and executes the pinned source through the public upstream lean_compiler/Program::execute interfaces, requires the checked-in bytecode and final execution oracle to match, then runs the leanSilicon host/model comparison. workloads/plan.json pins all inputs, derivations, runtime values, expected successes and expected failures. The per-workload JSON files and aggregate receipt.json are the machine-readable receipts; they are mutable run evidence and are not committed release artifacts.

Selection and coverage

The three small programs are scaled, auditable instances of use cases present at the pinned upstream source, not claims about a broad benchmark suite:

Workload Source ground Included surface Observed result
field_division lean_compiler/tests/field_div.rs compiler back-solving, SET/MUL/XOR/JUMP, final memory and cycles full functional/model match: 16 slots, 9 executed cycles/steps
heap_recurrence rec_aggregation/src/fibonacci.rs HeapBuf, mul_range, pointer/DEREF-shaped recurrence expected failure at pc 1 (bad_pointer): 64 slots, 1/58 steps reached
blake3_stack lean_compiler/tests/stack_buf.rs StackBuf and a realistic BLAKE3 service request full CPU/model match through the host service: 16 slots, 10 executed cycles/steps

The receipt is successful only when all three outcomes reproduce. A lane pass therefore means two matches plus one correctly detected limitation; it does not turn the HeapBuf failure into conformance. CPU/model opcode coverage across the matched workloads is SET_CONSTANT, MUL_NATIVE, XOR, JUMP, and BLAKE3_REQUEST through SERVICE_REQUIRED. The heap source still demonstrates missing HeapBuf pointer preparation before its DEREF path can be credited as covered.

Large XMSS aggregation and recursive-proof workloads from the upstream README are excluded: executing their prover/verification benchmarks would conflate VM workload validation with proof-system and machine benchmarking and take substantial resources. The upstream Fibonacci default is scaled down from 200,000 iterations because this lane asks whether interfaces accept the workload shape, not for a throughput claim. Witness-dependent, negative, and proof-generation tests are also excluded because the public export adapter cannot set or inspect upstream private witness and trace fields. These exclusions bound generality explicitly.

Evidence classification and observations

  • Functional/model: a live pinned Rust compiler/executor is the oracle for bytecode, cycles and final memory. The leanSilicon Python host/model matches the field-division and BLAKE3-stack instances. Per-step upstream comparison is impossible because Execution::trace is private at the pinned revision.
  • RTL/FPGA: no RTL simulation, synthesis, place-and-route, FPGA image, board exchange, timing, or resource-utilization evidence is produced by this lane. The repository's separate bounded RTL/FPGA evidence must not be attributed to these workloads.
  • ASIC: none. Any future fabricated-silicon workload receipt must identify a die/board, bitstream or firmware, instruments, environment and raw exchanges; simulation/model output cannot predict silicon behavior.

The only performance/resource observations are deterministic counts: upstream cycles, bytecode slots, memory prefix length, and model steps in the JSON receipt. Wall-clock compiler/runtime timings and host memory consumption are not recorded as benchmarks; no controlled machine, repetition/warm-up policy, or resource instrumentation exists. No throughput, FPGA utilization, timing closure, power, area, or silicon performance claim is made.

Residual limitations include the finite three-program sample, a fixed public input [1, 0], no public upstream per-step trace, no Lean-to-model/RTL proof, the early HeapBuf pointer failure, BLAKE3 limited to CPU/model service evidence, and no RTL, FPGA, physical-design, or ASIC execution. Promotion into any release or SKY26c gate requires separate evidence and review.