Sounio Hardware

Reference hardware contracts and, eventually, implementations for Sounio and EISA semantics.

The repository begins with executable contracts rather than decorative RTL. The first contract specifies exact ordered-pair zero-divisor detection for the 16-dimensional Cayley-Dickson algebra (sed16). Its software oracle, vectors, and receipts define what a later RTL implementation must reproduce.

Run the current gate with:

bash scripts/gate_zd_pair_contract.sh
bash scripts/gate_zd_pair_formal_partition_surface.sh
bash scripts/slurm/run_zd_pair_formal_partition_emit.sh
bash scripts/slurm/run_zd_pair_synth.sh

Claim boundary

The software contract proves that ten required cases are deterministic and that eight specified mutation classes are rejected. The RTL gate simulates nine fixed-width cases, six adversarial boundaries, and all 1,024 signed basis combinations on an iterative 256-MAC core; malformed operand shape remains an interface-layer rejection. That simulation receipt does not claim synthesis or any physical result.

The synthesis gate runs through Slurm and includes the signed-basis-exhaustive RTL gate before proving deterministic replay with Yosys 0.33 on the same tool and host. It produces a fully lowered generic netlist with no remaining behavioral processes. The same common testbench then executes against the generated Verilog netlist, covering all 1,024 signed basis products, fifteen fixed v1 cases, and one reset-aborted transaction. This is bounded post-synthesis simulation parity, not full-domain or formal equivalence. Its cell count is not a physical area claim; technology mapping, timing, power, FPGA, ASIC, and silicon evidence remain separate milestones.

The direct scripts/gate_zd_pair_synth.sh entrypoint is the worker-side gate. Use the Slurm launcher from the interactive workspace; its returned job ID, node, logs, source commit, and artifact hashes are part of the evidence. The bundled Yosys/Icarus toolchain is explicitly limited to Linux x86_64 with glibc. Its files and the node's absolute ELF loader are checksum-verified before execution, so a heterogeneous loader ABI is classified as blocked. The post-synthesis replay is intentionally a long-running promotion gate with a one-hour Slurm allocation; GitHub Actions performs only its static contract checks.

The state-step formal obligation also has an exact consequent-partition surface. It preserves the complete 5,147-bit relation as the antecedent of every sub-obligation and divides only the next-step consequent into four disjoint maps whose union is checked against the original map hash. This is a proof decomposition, not a weaker invariant. Full formal equivalence remains unclaimed until every partition CNF has an independently replayed certificate. The Slurm partition-emission launcher generates all four CNFs through the hash-bound temporal drivers, validates their DIMACS structure, and returns a complete checksummed bundle. Emission is not an UNSAT result. The 27-bit control partition now has a CaDiCaL UNSAT proof, an independent drat-trim replay on a second Slurm node, and a bit-identical reemission through the audited gate. The other three partition certificates remain pending, so full state-step equivalence remains unclaimed.

The PIREUS material-parity contract (eisa_h.pireus_material_parity.v1) decides whether a PIREUS material-parity receipt is admissible evidence of the measurement it reports. It validates receipt admissibility only: it does not re-run the measurement, does not touch hardware, and accepting a receipt asserts nothing about whether the measured result is correct, reproducible, or advantageous. Its refusals include a receipt whose mutation controls produced no mismatch, which measured nothing, and a receipt carrying any gain or promotion field, which is a separate obligation from parity.

Run it with bash scripts/gate_pireus_material_parity_contract.sh.

Ownership

• Sounio-lang/sounio owns language-level semantics and cross-repository compiler integration.
• This repository owns hardware-facing contracts, RTL, testbenches, synthesis, formal verification, and hardware receipts.

Apache-2.0 licensed. See LICENSE.