Apex_ContractForge

A bounded transition compiler for CPU and FPGA implementations, starting with one frozen Tick-compatible order-admission profile.

ContractForge generates C++ and SystemVerilog from typed guard expressions and a fixed ordered-effect template. A qualification runner compares both baseline and counter-narrowed variants against a pinned independent dictionary oracle and the original Apex_Tick RTL. Seven deliberately unsafe transformations must be detected on both generated backends.

This is an executable first compiler slice. It supports one frozen profile, not arbitrary C++, Python, exchange protocols or user-defined state machines. FPGA deployment, full stateful RTL equivalence, physical latency, LUT savings, energy measurements, measured Pareto improvements and official STAC execution remain unqualified.

51 fewer declared RTL counter bits is a code-generation result. Synthesis can already optimize unused bits; this number does not establish fewer flip-flops, LUTs, lower power or faster execution.

Requirements: Python 3.11+, a tested Clang or GCC with unsigned __int128, Icarus Verilog (iverilog and vvp), and Z3. Missing tools and unresolved required obligations fail rather than silently skip. Tested dependency versions are recorded in requirements-tested.txt; CI uses those pins. Install Icarus through your normal platform tooling.

python3 -m venv .venv
.venv/bin/python -m pip install -r requirements-tested.txt
.venv/bin/python -m pip install --no-build-isolation -e .
.venv/bin/python -m pytest -q
.venv/bin/apex-forge check contracts/tick-compatible.json
.venv/bin/apex-forge prove-counters
.venv/bin/apex-forge compile --variant narrow-counters --output /tmp/apex-forge-generated
.venv/bin/apex-forge qualify --steps 2000 --seeds 17,29,53 --output /tmp/apex-forge-run
.venv/bin/apex-forge validate-evidence /tmp/apex-forge-run
.venv/bin/apex-forge export-atlas /tmp/apex-forge-run

Output directories must be absent or empty; existing evidence is not overwritten. export-atlas writes a new run.json once. To check it with Apex_PerfAtlas, run apex-atlas validate /tmp/apex-forge-run/run.json in an Atlas environment.

Valid measured Atlas exports require an observed source revision and dirty state from the ContractForge checkout. A standalone wheel can generate and qualify the profile; without checkout provenance it retains a null source revision and cannot label an Atlas record valid measured.

The randomized budget is at most one million cycles per qualification invocation, plus the deterministic corpus and scenario resets. Counts describe replay cycles, including idle, stalls and reset—not packets, orders or physical throughput. The testbench's artificial clock is not a device frequency measurement.

%%{init: {"theme":"dark","flowchart":{"htmlLabels":false},"themeVariables":{"edgeLabelBackground":"#0b1220"}}}%%
flowchart TB
    C["Frozen Tick-compatible contract"]
    IR["Typed guards and fixed effect schedule"]
    P["Local counter-range SMT obligations"]
    CPP["Generated C++ baseline and narrow variant"]
    SV["Generated RTL baseline and narrow variant"]
    REF["Pinned independent Tick oracle and RTL"]
    Q["Five-backend functional qualification"]
    N["Seven unsafe mutations on both backends"]
    E["Retained traces and divergent prefixes"]
    A["Implemented simulation-only PerfAtlas exporter"]
    C --> IR
    IR --> P & CPP & SV
    P -->|required for narrowing| Q
    CPP & SV & REF --> Q
    N --> Q
    Q --> E --> A
    classDef default fill:#172554,stroke:#93c5fd,color:#ffffff;
    classDef check fill:#163329,stroke:#6ee7b7,color:#ffffff;
    class P,REF,Q check;

The ten full architecture views are the broader proposed design, with dark SVGs and editable Mermaid sources. Their private-environment, general search, vendor-shell, eFPGA and ASIC connections are future qualification work. Release status separates the executable subset from those proposals.

• Readiness is sampled from pre-transition state.
• Reset overrides the normal transition. Observed pre-state readiness is recorded, but reset accepts no quote.
• An existing output handshake precedes terminal processing in that cycle.
• The rate window advances on every non-reset cycle, including idle and stalls.
• Recovery takes priority over terminal events; terminal events take priority over quotes.
• A terminal event can retire only a matching transmitted identity, once.
• Reservation commits quantity, identity, rate count, pending entry and output together.
• Hold prevents new admissions while preserving the reference policy for already reserved outputs.
• Hard reset erases local knowledge; a real adapter must reconcile external obligations before restoring authority.

The original profile has no terminal-epoch field. Adding it, retiming commits, changing the window to wall time, adding partial fills or changing capacity requires a new contract and new qualification. See semantic rules and verification scope.

This project has no implemented Exegy adapter, exchange session, MAC/PHY, physical board runner or official STAC harness. Hardware gates and economics describe what those extensions require. No partnership, contract value or guaranteed benchmark win is implied.

Retained releases live under evidence/. Run apex-forge validate-evidence EVIDENCE_DIRECTORY to replay the retained observations against the independent oracle and check source identity, count accounting and counterexample bindings. The evidence manifest establishes byte identity and local consistency, not authenticated custody or independent review.

The 2026-10-01 retained qualification passed 1,000,162 cycles per backend, with 5,000,810 matching backend transitions across the five executions. This includes one million randomized cycles over ten seeds, fifteen named scenarios and scenario resets. All 14 negative-control checks detected their intended fault. Ninety normalized observation fields were compared per cycle; the compact Atlas trace retains ten public fields. The source provenance records clean revision b2e9d3eeb5c9b13a1e020c29bfb3d777a1a17722; the tool inventory records native arm64 Darwin replay and Icarus simulation, with no physical board.

The Atlas record passes Apex_PerfAtlas validation at revision 53e142cf8234d389226ce6e6113cade8168400a6. Its measured quantity is the functional cycle count, not elapsed time or trading latency. Its metric uses the per-backend population, not the five-backend aggregate. Thirty-five compiler/evidence tests pass at the recorded source revision. Source and wheel qualification were both exercised; the release packages include templates, reference provenance and the frozen contract.

apex-forge validate-evidence evidence/functional/2026-10-01
apex-atlas validate evidence/functional/2026-10-01/run.json

The four local SMT obligations establish a counter invariant and narrowing value preservation under recorded transition assumptions. They do not prove the entire generated RTL state machine, the compiler, board integration, exchange correctness or physical timing.

Original code, RTL templates and documentation are Apache-2.0. The attributed RTL template is derived from Apex_Tick; its independent oracle and RTL are vendored byte-for-byte from commit 1b665d3a0ec1fc106525edcece8a43b7254244e1. See NOTICE and src/apex_forge/reference/provenance.json. Tools, hardware IP and benchmark materials retain their own terms.