diff --git a/.github/workflows/pr-dashboard.yml b/.github/workflows/pr-dashboard.yml index 176554d6..ed9fcd5e 100644 --- a/.github/workflows/pr-dashboard.yml +++ b/.github/workflows/pr-dashboard.yml @@ -40,6 +40,14 @@ jobs: echo "" >> /tmp/pr_dashboard.md + # Compute summary counts BEFORE rendering the table. + # Prior version referenced $TOTAL / $FAILING before they were assigned, + # which crashed under `set -u` with "unbound variable" on every PR. + TOTAL=$(echo "$PR_DATA" | jq -r 'length') + FAILING=$(echo "$PR_DATA" | jq -r '[.[] | select((.statusCheckRollup // []) | any(.conclusion == "FAILURE" or .conclusion == "CANCELLED" or .conclusion == "TIMED_OUT"))] | length') + READY=$(echo "$PR_DATA" | jq -r '[.[] | select((.statusCheckRollup // []) | all(.conclusion == "SUCCESS" or .conclusion == "SKIPPED" or .conclusion == null))] | length') + PENDING=$(echo "$PR_DATA" | jq -r '[.[] | select((.statusCheckRollup // []) | any(.conclusion == null))] | length') + # Summary table echo "## Summary" >> /tmp/pr_dashboard.md echo "" >> /tmp/pr_dashboard.md @@ -49,12 +57,8 @@ jobs: echo "| PRs with Failing Checks | $FAILING |" >> /tmp/pr_dashboard.md echo "| PRs with All Checks Green | $((TOTAL - FAILING)) |" >> /tmp/pr_dashboard.md - READY=$(echo "$PR_DATA" | jq -r '[.[] | select((.statusCheckRollup // []) | all(.conclusion == "SUCCESS" or .conclusion == "SKIPPED" or .conclusion == null))] | length') - FAILED=$(echo "$PR_DATA" | jq -r '[.[] | select((.statusCheckRollup // []) | any(.conclusion == "FAILURE" or .conclusion == "CANCELLED" or .conclusion == "TIMED_OUT"))] | length') - PENDING=$(echo "$PR_DATA" | jq -r '[.[] | select((.statusCheckRollup // []) | any(.conclusion == null))] | length') - echo "| READY | $READY |" >> /tmp/pr_dashboard.md - echo "| FAILING | $FAILED |" >> /tmp/pr_dashboard.md + echo "| FAILING | $FAILING |" >> /tmp/pr_dashboard.md echo "| PENDING | $PENDING |" >> /tmp/pr_dashboard.md - name: Post PR Comment diff --git a/BENCHMARKS.md b/BENCHMARKS.md new file mode 100644 index 00000000..4f39989e --- /dev/null +++ b/BENCHMARKS.md @@ -0,0 +1,104 @@ +# BENCHMARKS.md -- Restrained Benchmark Posture + +> **Policy:** publish only numbers we can reproduce from this repo, +> from a sealed spec or generated file. No "expected" or "projected" +> figures appear here. **When in doubt, omit the row.** + +This document is a register of what is benchmarked (and what is **not**) in +this repository, kept conservative on purpose. It complements +[`COMPETITORS.md`](COMPETITORS.md), which states what we do not claim. + +--- + +## 1. What exists in-repo today + +### 1.1 Conformance vectors (correctness, not throughput) + +| Vector file (under `conformance/`) | Purpose | +|--------------------------------------------|--------------------------------------------------| +| `FORMAT-SPEC-001.json` | GoldenFloat family registry (SSOT for the line). | +| `gf*_vectors.json` | Arithmetic conformance vectors for GF widths. | +| `ar_*.json` | CLARA-style assurance reasoning vectors. | +| `nn_*.json` | Neural architecture conformance vectors. | +| `sacred_physics*.json` | phi / Trinity identity conformance. | +| `gf_competitive_bench.json` | Skeleton benchmark file. **Most rows are placeholders.** | + +Validation entry point: `./scripts/tri validate-conformance`. These vectors +test **correctness against the spec**, not silicon throughput. + +### 1.2 Benchmark specs (under `specs/benchmarks/`) + +- `bench_main.t27` +- `bench_nn.t27` +- `ternary_vs_binary.t27` + +These specs define **measurement procedures**. The numbers they would +produce belong with the chip repos or with a future +`bench/results_*.json` set. **No silicon-level numbers from these specs +appear in this document.** + +### 1.3 FPGA / Vivado scripts + +- `fpga/vivado/build.tcl`, `fpga/vivado/build_gf16.tcl` +- testbenches: `gf16_add_tb.v`, `gf16_mul_tb.v`, `gf16_dot4_tb.v`, + `gf16_matmul4x4_tb.v` + +These produce simulation and synthesis-level evidence (latch-free, +timing-reported), but **not** end-to-end accelerator throughput numbers. + +### 1.4 Misc + +- `bench/results_v02_real.json` -- legacy results file, not maintained as a + benchmark target for this line. Treat as historical. +- `benchmarks/phi_attractor_convergence.py` -- a research convergence + script, not a product benchmark. + +--- + +## 2. What we deliberately do not publish here + +Items in this list are **not** to be quoted from this document: + +1. TOPS or TOPS/W for any TRI-NET chip until that chip reaches **SILICON** + per [`STATUS.md`](STATUS.md). +2. Latency / throughput vs. Hailo-8, Coral Edge TPU, Axelera Metis, + Qualcomm Cloud AI 100 Ultra, MediaTek Dimensity 9400+ -- see + [`COMPETITORS.md`](COMPETITORS.md) for why. +3. Accuracy parity with FP16 / BF16 on ImageNet, LLM perplexity, or any + other model-level benchmark, until a reproducible vector lands under + `conformance/`. +4. Any "expected" / "projected" / "target" figure. If a number is not + measured, it is not in this document. + +--- + +## 3. How to add a benchmark (the only allowed way) + +1. **Land the spec.** Add a `.t27` under `specs/benchmarks/` describing + the measurement. +2. **Land conformance vectors.** Add a `*_vectors.json` under + `conformance/`. +3. **Land a results file.** Add `bench/_results.json` produced by + `./scripts/tri test` or an equivalent reproducible run, including the + commit hash of the run. +4. **Add a row to this document** pointing to the spec + vectors + results. + +Rows that point at "expected" results MUST NOT be added. + +--- + +## 4. External references (for context only) + +For research context cited elsewhere in this docs package: + +- BitNet b1.58, 1.58-bit ternary LLM weights: + https://arxiv.org/abs/2402.17764 +- Tiny Tapeout chip catalogue: + https://tinytapeout.com/chips/ + +These links are **not** sources of benchmark numbers for TRI-NET; they are +sources of **direction** for the research line. + +--- + +**phi^2 + 1/phi^2 = 3 | TRINITY** diff --git a/CLARA_TRACEABILITY.md b/CLARA_TRACEABILITY.md new file mode 100644 index 00000000..eb18ba2c --- /dev/null +++ b/CLARA_TRACEABILITY.md @@ -0,0 +1,93 @@ +# CLARA_TRACEABILITY.md -- Mapping to DARPA CLARA Public Goals + +> **Scope:** this document maps **public-facing** goals of DARPA's CLARA +> program to **specific artefacts in this repository**, so that an +> external reviewer can trace claim -> file. +> +> It is **not** a claim of CLARA participation, award, or endorsement. +> Where the word "CLARA" appears below, it refers to the **publicly +> described program** at: +> +> - DARPA CLARA: https://www.darpa.mil/research/programs/clara + +--- + +## 1. Why this document exists + +The TRI-NET line is positioned in the **high-assurance** corner of AI +silicon (see [`COMPETITORS.md`](COMPETITORS.md)). DARPA CLARA is the most +visible public program articulating goals in this corner. Rather than make +loose "CLARA-aligned" statements, this document gives a single page that +points each public CLARA goal at a file or directory in this repo, with +honest gaps marked. + +Sources of CLARA goals: the public program page above. All wording of +"CLARA goal" rows is paraphrased from public material; treat the linked +page as authoritative. + +--- + +## 2. Mapping table + +The "goal" column paraphrases public language; the "artefact" column points +into this repo; the "level" column uses [`STATUS.md`](STATUS.md) readiness +levels where it makes sense, or `n/a` where the artefact is a document not +a build target. + +| Public CLARA goal (paraphrased) | Artefact in this repo | Level | +|-----------------------------------------------------------------|-------------------------------------------------------------|-----------| +| Compositional AI assurance -- combining ML and AR components | `clara-bridge/` (4 hybrid patterns documented in README) | demo | +| Bounded reasoning / explainability over inference steps | `clara-bridge/` proof-trace work; `specs/ar/` AR specs | demo/SPEC | +| Polynomial-time complexity guarantees on the assurance path | Stated in `clara-bridge/README.md`; specs under `specs/ar/` | demo | +| Formal verification of components prior to composition | `coq/Kernel/`, `coq/Theorems/`, `coq/IGLA/`, `proofs/` | partial | +| Reproducible build pipeline auditable end-to-end | `.t27` -> `t27c` -> `gen/*` -> `.trinity/seals/` | GREEN | +| Open and inspectable artefacts | This repo + linked chip repos (see [`LINEUP.md`](LINEUP.md))| n/a | + +Honest gaps: + +- **No claim of submission acceptance** to CLARA. `clara-bridge/submission/` + and `clara-bridge/proposal/` are documents in this repo; their state in + any external program is **not** asserted here. +- **No claim of CLARA TA-level mapping** (Technical Area X.Y wording). + When the public program page details such structure, a follow-up PR can + refine this table. +- **Coq surface is "partial"**: see [`STATUS.md`](STATUS.md) section 2.4. + +--- + +## 3. Reproducing the trace + +Anyone with this repo can verify the mapping: + +```bash +# Spec-to-gen reproducibility +./scripts/tri parse specs/numeric/gf16.t27 +./scripts/tri gen-verilog specs/numeric/gf16.t27 +./scripts/tri seal specs/numeric/gf16.t27 --verify + +# Assurance bridge examples +ls clara-bridge/ +cat clara-bridge/README.md + +# Conformance gating +./scripts/tri validate-conformance +./scripts/tri validate-gen-headers +``` + +The intent is: a reviewer who has never used t27 should be able to land +on this file, click into each row's artefact, and reach a reproducible +build or proof from there. + +--- + +## 4. What this document is not + +- Not a CLARA program proposal (those live, if at all, under + `clara-bridge/submission/` and `clara-bridge/proposal/`). +- Not a CLARA endorsement or affiliation statement. +- Not a substitute for [`STATUS.md`](STATUS.md), which still governs + what level each component is at. + +--- + +**phi^2 + 1/phi^2 = 3 | TRINITY** diff --git a/COMPETITORS.md b/COMPETITORS.md new file mode 100644 index 00000000..34cb6b6c --- /dev/null +++ b/COMPETITORS.md @@ -0,0 +1,133 @@ +# COMPETITORS.md -- Honest Positioning + +> **One-line positioning:** Commercial NPUs own the production TOPS / SDK / +> compliance corner. TRI-NET / t27 own the **inspectable open silicon and +> formal / assurance workflow** corner. These are different products; this +> document is written to keep us out of races we are not running. + +This page describes **adjacent products** in the AI-accelerator space and +states, as restrained as possible, what TRI-NET / t27 is and is not, relative +to each. **No throughput parity is claimed against any product on this page.** + +External links are kept as primary sources. All claims attributed to a +vendor are sourced from the linked page; any other claim is attributed to +this repo. + +--- + +## 1. Adjacent products (alphabetical) + +### 1.1 Axelera Metis (AIPU) + +- **Vendor page:** https://axelera.ai/ai-accelerators/aipu/metis +- **What they sell:** edge AI inference cards / modules with their own + AIPU silicon, Voyager SDK, model zoo. +- **What TRI-NET is not:** we do not provide an SDK at this scale or a model + zoo. Our compute volume target (`tt-trinity-gamma`, 32 PEs) is research-tier. +- **What TRI-NET differs in:** every Verilog block in our line comes from a + `.t27` spec under `specs/` with conformance vectors under `conformance/`. + The silicon submission target is the Tiny Tapeout shuttle, not a private + fab run. + +### 1.2 Coral Edge TPU + +- **Benchmarks page:** https://www.coral.ai/docs/edgetpu/benchmarks/ +- **What they sell:** USB / M.2 / PCIe Edge TPU accelerators, post-training + INT8 quantised models, the Edge TPU Compiler. +- **What TRI-NET is not:** we do not ship a binary toolchain that takes a + TFLite file and produces a ready-to-run device image. Coral does. +- **What TRI-NET differs in:** the numeric format itself is open and + inspectable (see [`FORMAT_REGISTRY.md`](FORMAT_REGISTRY.md)); the path + from spec to RTL is reproducible and sealed. + +### 1.3 Hailo-8 + +- **Vendor page:** https://hailo.ai/products/ai-accelerators/hailo-8-ai-accelerator/ +- **What they sell:** edge AI processor IC with a dataflow architecture, + Hailo Dataflow Compiler, production deployments in automotive / industrial. +- **What TRI-NET is not:** we are not a production embedded inference + processor. We do not claim TOPS, mW/TOPS, or automotive compliance. +- **What TRI-NET differs in:** all of our numeric kernel and ISA are + spec-driven; we publish proofs (`coq/`) and seals (`.trinity/seals/`). + This is an **orthogonal** value proposition, not a substitute. + +### 1.4 MediaTek Dimensity 9400+ + +- **Vendor page:** https://www.mediatek.com/products/smartphones/mediatek-dimensity-9400-plus +- **What they sell:** smartphone application SoC with an integrated NPU, in + shipping mobile devices. +- **What TRI-NET is not:** we are not an SoC and not a phone-class platform. +- **What TRI-NET differs in:** TRI-NET targets the **open-shuttle** + (Tiny Tapeout) economic regime, not high-volume mobile silicon. + +### 1.5 Qualcomm Cloud AI 100 Ultra + +- **Vendor PDF:** https://www.qualcomm.com/content/dam/qcomm-martech/dm-assets/documents/Prod-Brief-QCOM-Cloud-AI-100-Ultra.pdf +- **What they sell:** datacentre-class inference accelerator with a closed + SDK, drivers, and ecosystem. +- **What TRI-NET is not:** we are not a datacentre accelerator and never + will be on this codebase. +- **What TRI-NET differs in:** TRI-NET's compute volume is research-tier; + our differentiator is that the **whole spec chain** -- numeric format, + ISA, RTL -- is openly auditable. + +### 1.6 BitNet b1.58 (research, not a product) + +- **Paper:** https://arxiv.org/abs/2402.17764 +- **What it is:** a research result showing that LLM weights can be + represented in ternary form (`{-1, 0, +1}`) with competitive accuracy at + ~1.58 bits/weight. +- **Why we cite it:** it validates the **direction** TRI-NET pursues in the + large -- ternary inference is plausible at scale. It does **not** validate + any claim about t27 or the chip line; we cite it only as motivation for + the ternary numeric path documented in [`FORMAT_REGISTRY.md`](FORMAT_REGISTRY.md). + +### 1.7 Tiny Tapeout (open shuttle, not a competitor) + +- **Catalogue:** https://tinytapeout.com/chips/ +- **What it is:** an educational / open silicon shuttle program that lets + designers submit small digital designs as tiles on a shared die. +- **Relation:** Tiny Tapeout is the **submission channel** for the three + TRI-NET chip repos (`tt-trinity-phi`, `tt-trinity-euler`, + `tt-trinity-gamma`). It is part of our pipeline, not a competitor. + +--- + +## 2. What we do not claim + +To keep this document honest, the following claims are **explicitly out of +scope** for t27 and the TRI-NET line as of this writing: + +1. No claim of **TOPS parity** or **TOPS/W parity** with any product listed above. +2. No claim of **SDK feature parity** with Hailo, Coral, Qualcomm, MediaTek, + or Axelera. We do not ship a vendor compiler for popular framework + formats (TFLite / ONNX / PyTorch Mobile). +3. No claim of **compliance certifications** (automotive, aerospace, medical). +4. No claim that GoldenFloat formats outperform FP8 / BF16 at any specific + model or task. +5. No claim about silicon performance until a chip repo demonstrates + `SILICON` level (see [`STATUS.md`](STATUS.md) definitions). + +--- + +## 3. What we do claim (narrow, defensible) + +1. **Spec-to-RTL reproducibility.** A `.t27` spec compiles to Verilog under + `gen/verilog/` (and to Zig / C software backends), with conformance + vectors under `conformance/`. See [`STATUS.md`](STATUS.md) for the levels. +2. **A single numeric SSOT** -- `conformance/FORMAT-SPEC-001.json` -- used + uniformly across the line. See [`FORMAT_REGISTRY.md`](FORMAT_REGISTRY.md). +3. **Open-shuttle silicon target.** The chip repos submit to Tiny Tapeout, + not a closed fab. +4. **Formal / assurance workflow** -- Coq proofs (`coq/`), seal-based + integrity (`.trinity/seals/`), and the `clara-bridge/` worked example + for DARPA CLARA-style compositional assurance + (see [`CLARA_TRACEABILITY.md`](CLARA_TRACEABILITY.md) for the public-goal + mapping). + +These four claims, together, define the "open high-assurance ternary AI +silicon substrate" positioning. + +--- + +**phi^2 + 1/phi^2 = 3 | TRINITY** diff --git a/FORMAT_REGISTRY.md b/FORMAT_REGISTRY.md new file mode 100644 index 00000000..fa61599c --- /dev/null +++ b/FORMAT_REGISTRY.md @@ -0,0 +1,169 @@ +# FORMAT_REGISTRY.md -- Numeric Format Surface (t27) + +> **Role:** t27 is the **numeric format registry** for the TRI-NET line. +> All chips in the line draw their numeric kernel from the JSON +> SSOT `conformance/FORMAT-SPEC-001.json`. This document is the +> human-readable mirror of that file plus interop notes. + +> **L6 CEILING:** `conformance/FORMAT-SPEC-001.json` and +> `specs/numeric/gf16.t27` are the **numeric SSOT**. If this Markdown +> disagrees with either, **the JSON / spec wins** -- file an issue, do not +> hand-edit the consumers. + +--- + +## 1. Primary path -- GoldenFloat GF16 + +GF16 is the **primary numeric format** of the line. It is the default for the +gamma mesh and the only GoldenFloat width with hand-built Verilog top-levels +in this repo (`fpga/vivado/gf16_top.v`, `fpga/vivado/gf16_matmul4x4_top.v`). + +### 1.1 Bit layout + +``` +GF16 = [ S(1) | E(6) | M(9) ] bits 15..0 + 15 14..9 8..0 +``` + +| Field | Bits | Mask | Notes | +|---------|-------|---------|------------------------------------------| +| Sign | 1 | 0x8000 | bit 15 | +| Exponent| 6 | 0x7E00 | bits 14..9, bias = 31 | +| Mantissa| 9 | 0x01FF | bits 8..0 | + +**Decoded value:** `(-1)^S * 2^(E - 31) * (1 + M / 2^9)` +(special cases: signed zero on E=0,M=0; subnormals on E=0,M!=0; +/-inf on +E=63,M=0; NaN on E=63,M!=0). + +**Source:** `specs/numeric/gf16.t27`, `specs/numeric/formats.t27`, +`conformance/FORMAT-SPEC-001.json` (field `formats.GF16`). + +### 1.2 phi anchor (L5 IDENTITY) + +`FORMAT-SPEC-001.json` records the following IEEE f64 evidence for the +phi identity: + +| Quantity | f64 hex | Decimal | +|---------------------|--------------------------|---------------------| +| `phi` | `0x1.9E3779B97F4A8p+0` | 1.6180339887498948...| +| `phi^2` | `0x1.4F1BBCDCBFA54p+1` | 2.6180339887498948...| +| `phi + 1` | `0x1.4F1BBCDCBFA54p+1` | 2.6180339887498948...| +| `phi^2 - (phi + 1)` | `0.0` (exact in f64) | 0 | + +Tolerance for any other tolerance-using check: `1e-15`. + +Identity: **`phi^2 + 1/phi^2 = 3`**, exact in the ternary world, witnessed in +f64 to within the tolerance above. + +--- + +## 2. GoldenFloat family (all widths) + +All widths are sign-magnitude with a single-stage normalised representation. +Bias is `2^(exp-1) - 1`. Source: `FORMAT-SPEC-001.json` field `formats.*`. + +| Format | Bits | S | E | M | Bias | phi distance | Status (this repo) | +|--------|------|---|----|----|-------|--------------|---------------------------| +| GF4 | 4 | 1 | 1 | 2 | 0 | 0.118 | SPEC | +| GF8 | 8 | 1 | 3 | 4 | 3 | 0.132 | SPEC | +| GF12 | 12 | 1 | 4 | 7 | 7 | 0.047 | SPEC | +| **GF16** | 16 | 1 | 6 | 9 | 31 | 0.0486 | **PRIMARY, SIM-level** | +| GF20 | 20 | 1 | 7 | 12 | 63 | 0.035 | SPEC | +| GF24 | 24 | 1 | 9 | 14 | 255 | 0.025 | SPEC | +| GF32 | 32 | 1 | 12 | 19 | 2047 | 0.014 | SPEC | + +"phi distance" is the L5-IDENTITY-related metric documented in +`FORMAT-SPEC-001.json` (`phi_dist`) -- smaller is closer to the +phi-optimal exp/mant split. + +Status column follows [`STATUS.md`](STATUS.md) levels (SPEC / RTL / SIM / +SYNTH / GDS-TAPEOUT / SILICON). + +--- + +## 3. Ternary path -- TF3 + +`specs/numeric/tf3.t27` -- balanced ternary representation +`{-1, 0, +1}`, also expressed in the 27 Coptic register ISA +(`specs/isa/` and `specs/fpga/ternary_isa.t27`). Generated to +`gen/verilog/numeric/tf3.v`. + +Used for the 32-PE mesh on `tt-trinity-gamma`. Not a floating-point format. + +--- + +## 4. Compatibility path -- FP8 + +**Purpose:** interop with mainstream low-bit AI accelerators +(e.g. NVIDIA Hopper / Blackwell FP8, AMD MI300 OCP-FP8). t27 does **not** +ship its own FP8 implementation today; the listed widths above are the +GoldenFloat family. + +**Intent (not implemented in this repo):** + +- Provide a `fp8 <-> GF8` and `fp8 <-> GF16` bridge in `specs/numeric/`. +- Reuse the same `FORMAT-SPEC-001.json` framing: a future entry + `formats.FP8_E4M3` and `formats.FP8_E5M2` would sit alongside the + GoldenFloat rows. + +When implemented, the bridge SHOULD live in `specs/numeric/fp8_bridge.t27` +with conformance vectors under `conformance/fp8_*_vectors.json`. Until then, +the FP8 entry is marked **PLANNED**, not SPEC. + +--- + +## 5. Quantisation bridge -- NF4 / INT4 / INT8 + +**Purpose:** consume quantised checkpoints from the open weights ecosystem +(NF4 weights from `bitsandbytes`-style flows, INT4/INT8 from GPTQ / AWQ / +GGML / TFLite) and feed them into the gamma mesh's ternary MAC. + +**Current state in this repo:** + +- `specs/numeric/formats.t27` -- has the conversion utility skeleton but + is FP-centric (GF16 <-> f32), not yet INT-centric. +- `specs/benchmarks/ternary_vs_binary.t27` -- comparison harness for + ternary against low-bit binary, useful as a target for the bridge. +- No `int4_bridge.t27` / `nf4_bridge.t27` / `int8_bridge.t27` exists yet. + +**Intent:** a single `specs/numeric/quant_bridge.t27` that performs +`{NF4, INT4, INT8} -> {TF3, GF16}` with conformance vectors. Treated as +**PLANNED**. + +The reference for the related research line (1-bit / 1.58-bit ternary LLM +weights) is BitNet b1.58: https://arxiv.org/abs/2402.17764 . + +--- + +## 6. GF formats as research differentiator + +The GoldenFloat family is presented as a **research-grade numeric** rather +than a production replacement for FP16/BF16/FP8. The honest claim is +narrow: + +- GF widths use a **phi-driven exp/mant split**, recorded as `phi_dist` in + `FORMAT-SPEC-001.json`. +- The split is **derived from a single identity** (`phi^2 = phi + 1`) rather + than picked per width by industry preference. +- The same identity is used as a CI gate (L5 IDENTITY). + +This is interesting because it is reproducible and inspectable. It is **not** +a claim of superior throughput, lower error, or better convergence at any +specified workload. Such claims, if they appear, must cite a benchmark file +in this repo (see [`BENCHMARKS.md`](BENCHMARKS.md)). + +--- + +## 7. Cross-references + +- JSON SSOT: `conformance/FORMAT-SPEC-001.json` +- Schema: `schemas/numeric-format-v1.json` +- Primary spec: `specs/numeric/gf16.t27` +- Generated Verilog: `gen/verilog/numeric/gf16.v` +- Hand-built top: `fpga/vivado/gf16_top.v`, `fpga/vivado/gf16_matmul4x4_top.v` +- Family overview: `specs/numeric/goldenfloat_family.t27` +- Identity proofs: `coq/Kernel/` and `proofs/sacred/` + +--- + +**phi^2 + 1/phi^2 = 3 | TRINITY** diff --git a/LINEUP.md b/LINEUP.md new file mode 100644 index 00000000..d5641ad5 --- /dev/null +++ b/LINEUP.md @@ -0,0 +1,119 @@ +# LINEUP.md -- TRI-NET Product Line + +> **Positioning, one line:** TRI-NET is an **open high-assurance ternary AI +> silicon substrate** -- not a TOPS race. The line trades raw throughput for +> inspectable specs, reproducible builds, and a formal-friendly toolchain. + +This document is the **single page** for "what are the four pieces and how do +they relate?". It links out; it does not duplicate per-repo READMEs. + +--- + +## 1. The four products + +| # | Repo (external, separate) | Role in the line | Silicon target | +|-----|---------------------------|-------------------------------------------|----------------------------| +| 1 | **`t27`** (this repo) | Spec-first toolchain + numeric format registry | N/A -- toolchain | +| 2 | `tt-trinity-phi` | phi-anchor proof / identity chip | Tiny Tapeout, 1x1 tile | +| 3 | `tt-trinity-euler` | e-engine -- safety / control engine | Tiny Tapeout, 8x2 tiles | +| 4 | `tt-trinity-gamma` | gamma-surface 32-PE ternary mesh | Tiny Tapeout, 8x4 tiles | + +Tiny Tapeout shuttle program: https://tinytapeout.com/chips/ + +### 1.1 t27 -- the foundation + +Spec-first language (`.t27`), bootstrap Rust compiler (`bootstrap/`), generator +backends (`gen/zig/`, `gen/c/`, `gen/verilog/`), conformance vectors +(`conformance/`), seals (`.trinity/seals/`), formal proofs (`coq/`, `proofs/`). + +**Primary product of t27:** `.t27 -> Verilog RTL -> Tiny Tapeout` -- a +reproducibility path that lets sibling chip repos generate their RTL from +sealed specifications rather than hand-written HDL. + +See [`STATUS.md`](STATUS.md) for what is actually shipped today, +[`FORMAT_REGISTRY.md`](FORMAT_REGISTRY.md) for the numeric SSOT, and +[`COMPETITORS.md`](COMPETITORS.md) for honest positioning. + +### 1.2 tt-trinity-phi -- 1x1 phi-anchor + +Smallest of the three chips. Carries the `phi` identity +(`phi^2 = phi + 1`, `phi^2 + 1/phi^2 = 3`) as an in-silicon witness; serves +as proof-of-life and CI gate for the line's numeric kernel. Status, pinout, +GDS, and Tiny Tapeout submission live in the chip repo. + +### 1.3 tt-trinity-euler -- 8x2 e-engine + +Mid-tile. Acts as the **safety / control** engine: bounded reasoning, restraint +behaviour, and the gateway through which the gamma mesh's outputs are exposed. +Pairs with the `clara-bridge/` assurance workflow in t27. + +### 1.4 tt-trinity-gamma -- 8x4 gamma-surface + +Largest tile. A **32-PE ternary mesh** for inference workloads (low-bit MAC, +ternary attention kernels). The compute volume of the line; deliberately not +benchmarked against commercial NPUs (see `BENCHMARKS.md`). + +--- + +## 2. How the four fit together + +``` + +-----------------------------+ + | t27 (this repo) | + | .t27 specs | + | bootstrap compiler | + | FORMAT-SPEC-001 registry | + | conformance vectors | + | coq / clara-bridge | + +--------------+--------------+ + | + v (.t27 -> Verilog RTL) + +----------------------+----------------------+ + | | | + v v v ++-----------------+ +------------------+ +---------------------+ +| tt-trinity-phi | | tt-trinity-euler | | tt-trinity-gamma | +| 1x1 phi anchor | | 8x2 safety/ctrl | | 8x4 32-PE ternary | ++--------+--------+ +---------+--------+ +----------+----------+ + | | | + +---------------------+----------------------+ + | + v + +-----------------------------+ + | Tiny Tapeout shuttle | + | (open submission) | + +-----------------------------+ +``` + +**Edges in this diagram are not asserted as "currently green for all three";** +they describe the **intended** flow. For each chip's actual status, see its +repo. For t27's status, see [`STATUS.md`](STATUS.md). + +--- + +## 3. Why a line and not one big chip + +- **Risk isolation.** A 1x1 phi-anchor that fails to bring up does not block + the 32-PE mesh; an 8x4 that fails physical verification does not invalidate + the safety engine. +- **Layered evidence.** phi-anchor proves the numeric kernel. euler proves + control + safety wiring. gamma proves compute volume. Each chip is a + separate, reviewable artifact. +- **Open-shuttle economics.** Tiny Tapeout's 1x1 / 2x2 / 4x4 / 8x4 tile sizes + match the line's risk tiers naturally. +- **Format symmetry.** All three chips draw from the same + `FORMAT-SPEC-001.json` numeric registry maintained in t27 -- one numeric + surface, three silicon expressions. + +--- + +## 4. Out of scope for this document + +- Per-chip status, pinout, schematic, GDS, or tape-out date -- see chip repos. +- Marketing comparisons against commercial NPUs -- see + [`COMPETITORS.md`](COMPETITORS.md) for the restrained version. +- Benchmark numbers -- see [`BENCHMARKS.md`](BENCHMARKS.md). + +--- + +**phi^2 + 1/phi^2 = 3 | TRINITY** diff --git a/README.md b/README.md index c0878f43..bfed86a2 100644 --- a/README.md +++ b/README.md @@ -16,6 +16,32 @@ The canonical source of truth for Trinity S3AI. --- +## What this repo is + +**t27** is the **spec-first toolchain and numeric format registry** for the +**TRI-NET line** of open high-assurance ternary AI silicon. The primary +product of t27 is the path `.t27 → Verilog RTL → Tiny Tapeout` with sealed, +inspectable artefacts at every step. + +- **How to verify:** `cd bootstrap && cargo build --release && cd .. && ./scripts/tri test` + (full Quick Start below). Validators: `./scripts/tri validate-conformance` and `validate-gen-headers`. +- **Primary numeric path:** GoldenFloat **GF16** (default), with the family + GF4–GF32 registered in [`conformance/FORMAT-SPEC-001.json`](conformance/FORMAT-SPEC-001.json). + FP8 compat and NF4 / INT4 / INT8 quant bridges are **planned**, not shipped. + Full details: [`FORMAT_REGISTRY.md`](FORMAT_REGISTRY.md). +- **Readiness:** [`STATUS.md`](STATUS.md) records what is at SPEC / RTL / SIM / + SYNTH / GDS / SILICON, conservatively, from this repo's own evidence only. +- **Sibling chip repos (separate):** `tt-trinity-phi` (1×1 φ-anchor), + `tt-trinity-euler` (8×2 e-engine, safety/control), `tt-trinity-gamma` + (8×4 γ-surface 32-PE ternary mesh). Tape-out target: + [Tiny Tapeout](https://tinytapeout.com/chips/). See [`LINEUP.md`](LINEUP.md). +- **Positioning:** [`COMPETITORS.md`](COMPETITORS.md) — we do not race + commercial NPUs on TOPS or SDK breadth; we own the inspectable open silicon + and formal / assurance corner. Benchmark policy: [`BENCHMARKS.md`](BENCHMARKS.md). +- **CLARA traceability:** [`CLARA_TRACEABILITY.md`](CLARA_TRACEABILITY.md). + +--- + ## System Status | Domain | Component | Status | Details | diff --git a/STATUS.md b/STATUS.md new file mode 100644 index 00000000..db90f523 --- /dev/null +++ b/STATUS.md @@ -0,0 +1,155 @@ +# STATUS.md -- t27 Readiness Levels + +> **Position in TRI-NET line:** t27 is the **spec-to-RTL toolchain and numeric format registry**. +> Sibling chip repositories (separate repos): +> - `tt-trinity-phi` -- 1x1 phi-anchor proof / identity chip +> - `tt-trinity-euler` -- 8x2 e-engine safety / control engine +> - `tt-trinity-gamma` -- 8x4 gamma-surface 32-PE ternary mesh +> +> See [`LINEUP.md`](LINEUP.md) for the four-product map, and +> [`FORMAT_REGISTRY.md`](FORMAT_REGISTRY.md) for the numeric SSOT +> shared across the line. + +This document records what t27 has actually shipped, at what readiness +level, with conservative wording. Sources are limited to **this repository's +own evidence** (specs, generated files, seals, conformance vectors, CI logs). +Claims about external chip repositories are deliberately omitted here; cross +to those repos for their own STATUS. + +--- + +## 1. Readiness levels (definitions) + +t27 uses a six-level scale for any artifact that targets silicon. Each level +is a strict superset of the levels below it. + +| Level | Meaning | +|---------------|-------------------------------------------------------------------------------------------------------------| +| **SPEC** | A `.t27` specification exists, parses, has `test` / `invariant` / `bench` per L4 TESTABILITY. | +| **RTL** | Verilog generated under `gen/verilog/` (or `fpga/vivado/` hand-built blocks), produced from a `.t27` spec. | +| **SIM** | Logic simulation passes (Verilator / Icarus / Yosys check), with conformance vectors when applicable. | +| **SYNTH** | Synthesis to a real cell library passes (Yosys `synth_xilinx` or equivalent), no latches, timing reported. | +| **GDS/TAPEOUT** | Layout closed, DRC/LVS clean, tape-out submission made (e.g. Tiny Tapeout shuttle). Repo-local proof only. | +| **SILICON** | Physical die received and bring-up reported in writing. **Asserted only on direct device evidence.** | + +A component at level **N** is not claimed at level **N+1** without textual +evidence in this repo. When in doubt, the level is *lowered*, not raised. + +--- + +## 2. Component status (this repo) + +### 2.1 Compiler and toolchain + +| Component | Level | Evidence | +|----------------------------|---------|------------------------------------------------------------------------------------------------------| +| `bootstrap/` (Stage-0 Rust)| SPEC+ | `bootstrap/stage0/FROZEN_HASH` seal, `cargo build --release` documented in `README.md`. | +| `t27c parse` | GREEN | 170+ specs parse (see README "System Status" table). | +| `t27c gen-verilog` | SIM | 5/5 FPGA modules synthesize per README; Verilog under `gen/verilog/` and `fpga/vivado/`. | +| `t27c gen-zig` | RTL-eq | Backend present under `gen/zig/` for 28 modules; treated as software backend, not silicon. | +| `t27c gen-c` | RTL-eq | Backend present under `gen/c/` for 28 modules; treated as software backend, not silicon. | +| `t27c seal` | GREEN | `.trinity/seals/` contains many sealed artifacts (729 files at audit time). | +| `./scripts/tri` | GREEN | Canonical CLI wrapper, documented in `README.md` Quick Start. | + +### 2.2 Numeric stack (GoldenFloat family) + +| Format | Level | Evidence | +|--------|----------|-------------------------------------------------------------------------------------------------------| +| GF4 | SPEC | `specs/numeric/gf4.t27`, entry in `conformance/FORMAT-SPEC-001.json`. | +| GF8 | SPEC | `specs/numeric/gf8.t27`, entry in `FORMAT-SPEC-001.json`. | +| GF12 | SPEC | `specs/numeric/gf12.t27`, entry in `FORMAT-SPEC-001.json`. | +| **GF16** | **SIM** | **Primary format.** `specs/numeric/gf16.t27`, `gen/verilog/numeric/gf16.v`, `fpga/vivado/gf16_*.v`, | +| | | hand-built top-levels (`gf16_top.v`, `gf16_matmul4x4_top.v`), `conformance/gf*_vectors.json`. | +| GF20 | SPEC | `specs/numeric/gf20.t27`, entry in `FORMAT-SPEC-001.json`. | +| GF24 | SPEC | `specs/numeric/gf24.t27`, entry in `FORMAT-SPEC-001.json`. | +| GF32 | SPEC | `specs/numeric/gf32.t27`, entry in `FORMAT-SPEC-001.json`. | +| TF3 (ternary) | SPEC | `specs/numeric/tf3.t27`, generated to `gen/verilog/numeric/tf3.v`. | + +GF16 is also documented at FPGA top-level under `fpga/vivado/` (Vivado-buildable +top + UART + matmul testbench), which is the most advanced numeric artifact +in this repository. See [`FORMAT_REGISTRY.md`](FORMAT_REGISTRY.md) for the +full bit layout and interop notes. + +### 2.3 FPGA / RTL surface + +| Block | Level | Evidence | +|--------------------------------|-----------|----------------------------------------------------------------| +| MAC unit (`specs/fpga/mac.t27`)| SYNTH | README: "5/5 FPGA modules synthesize" with `synth_xilinx`. | +| `gf16_top.v` / `gf16_matmul` | SYNTH | `fpga/vivado/build.tcl`, `build_gf16.tcl`, testbenches present.| +| QMTECH XC7A100T profile | SYNTH | Listed in README "System Status"; pins IR + XDC emitter green. | +| Arty A7 profile | SYNTH | Listed in README "System Status". | +| Bitstream artifact in CI | SYNTH | README: ".bit uploaded per PR (7-day retention)". | + +> Tiny Tapeout tape-outs (1x1, 8x2, 8x4) live in **sibling repositories** and +> are out of scope for this document. See `LINEUP.md`. + +### 2.4 Formal / proof surface + +| Surface | Level | Evidence | +|-------------------|----------|---------------------------------------------------------------------------| +| Coq kernel | partial | `coq/Kernel/`, `coq/Theorems/`, `coq/IGLA/`; multiple Wave* commits cite Qed counts (`git log`). | +| Phi identity (L5) | GREEN | `conformance/FORMAT-SPEC-001.json` records IEEE f64 hex + zero residual. | +| Sacred physics | SPEC+ | `proofs/sacred/`, `proofs/trinity/`, `proofs/gravity/`. | + +### 2.5 CLARA / assurance bridge + +| Artifact | Level | Evidence | +|-------------------------|----------|---------------------------------------------------------| +| `clara-bridge/` | demo | README in `clara-bridge/README.md`, Python examples, | +| | | scenarios, audit-trail, explainability harness. | +| Submission package | draft | `clara-bridge/submission/` and `clara-bridge/proposal/`.| + +See [`CLARA_TRACEABILITY.md`](CLARA_TRACEABILITY.md) for how t27 maps to the +public DARPA CLARA program goals. + +--- + +## 3. Conservative status decisions + +The following decisions were made when authoring this document, in line with +the rule "when in doubt, lower": + +1. **No SILICON claim anywhere in t27.** Silicon belongs to the chip repos, not here. +2. **No GDS/TAPEOUT claim in t27.** Tape-out artifacts live in `tt-trinity-*` repos. +3. **GF16 marked SIM, not SYNTH-on-vendor-cells**, because the Verilog evidence in this repo + is Yosys-friendly + Vivado scripts; we do not assert a closed vendor flow from t27 alone. +4. **CLARA bridge is "demo / draft"**, not "submitted" -- the repo contains examples and a + `submission/` directory, but no public award or acceptance evidence is asserted. +5. **Coq surface is "partial"**, even though recent commits add Qed counts; an external + reviewer should still audit each `*.v` rather than trust the aggregate. + +--- + +## 4. How to verify + +Reproducible checks **from this repo only**: + +```bash +# Build bootstrap (Rust) +cd bootstrap && cargo build --release && cd .. + +# Parse specs +./scripts/tri parse specs/numeric/gf16.t27 + +# Run the Rust test suite (parse / gen / seal / fixed-point) +./scripts/tri test + +# Validate conformance vectors and gen headers +./scripts/tri validate-conformance +./scripts/tri validate-gen-headers + +# Inspect format registry +cat conformance/FORMAT-SPEC-001.json +``` + +For RTL flow, see `fpga/vivado/build.tcl` and `fpga/vivado/build_gf16.tcl`. + +--- + +## 5. Update policy + +`STATUS.md` is updated only when **textual evidence in this repo** moves a +component up or down a level. PRs that change levels must cite the file(s), +seal(s), or CI run(s) that justify the change. + +**phi^2 + 1/phi^2 = 3 | TRINITY** diff --git a/docs/NOW.md b/docs/NOW.md index a94bc1a8..e322f345 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,6 +1,18 @@ # NOW — Trinity t27 sync -Last updated: 2026-05-16 +Last updated: 2026-05-17 + +## docs(TRI-NET) — positioning package (this PR, #693, Closes #627) + +- **NEW** (root-level, docs-only): `STATUS.md`, `LINEUP.md`, `FORMAT_REGISTRY.md`, `COMPETITORS.md`, `BENCHMARKS.md`, `CLARA_TRACEABILITY.md` +- **README.md first screen**: additive "What this repo is" block linking to the six new docs; rest of README unchanged +- **Positioning**: t27 framed as the fourth product of the TRI-NET line — spec-first toolchain + numeric format registry; chip siblings `tt-trinity-phi` (1×1 phi-anchor), `tt-trinity-euler` (8×2 e-engine), `tt-trinity-gamma` (8×4 32-PE ternary mesh) +- **Readiness ladder**: SPEC / RTL / SIM / SYNTH / GDS-TAPEOUT / SILICON; conservative — no SILICON or GDS claim in t27, GF16 at SIM only, CLARA bridge demo/draft, Coq partial +- **Numeric SSOT** kept: `conformance/FORMAT-SPEC-001.json` (primary = GF16), FP8 + NF4/INT4/INT8 bridges marked PLANNED (no spec yet) +- **No code touched**: zero changes under `gen/`, `specs/`, `bootstrap/`, `coq/`. R-SI-1 and L2 GENERATION held +- **Validation**: `scripts/check_first_party_doc_language.py` PASS; `FORMAT-SPEC-001.json` sanity PASS; full `./scripts/tri test` not run locally (no cargo in env) — CI is authoritative +- **External sources cited in docs**: DARPA CLARA (darpa.mil/research/programs/clara), Qualcomm Cloud AI 100 Ultra brief, Hailo-8, Axelera Metis, Coral Edge TPU benchmarks, MediaTek Dimensity 9400+, BitNet b1.58 (arxiv 2402.17764), Tiny Tapeout chip catalogue +- Closes #627 ## Wave-45 Lane PP — Avs96Safe.v AVS-96 Dopamine Safety Coq (NEW, this PR)