Skip to content

feat(reproduce): consume the t27 contracts byte for byte at a pinned revision (Refs #989) - #1213

Merged
dmitrii-f-t27 merged 1 commit into
mainfrom
spec/trinity-s12-contracts
Oct 1, 2026
Merged

dmitrii-f-t27 merged 1 commit into
mainfrom
spec/trinity-s12-contracts

Conversation

@dmitrii-f-t27

@dmitrii-f-t27 dmitrii-f-t27 commented Oct 1, 2026 •

Copy link
Copy Markdown
Contributor

S12 of #988, third part (Refs #989): consume the canonical t27 manifest/specs byte-identically with pinned revision and compiler hashes.

Why

Until now trinity met t27 only through the website mirror, apps/website/public/t27/files/. That is a catalog snapshot, not a lock:

  • its manifest.json says it was read from a tarball of t27 master with nine files of a second branch laid over it (generatedFrom.overlayRefs);
  • it records no hash per file;
  • its compiler is "the copy already vendored here" (generatedFrom.wasmSource).

So nothing could say whether a contract trinity reads is the one t27 holds.

What this adds

  • external/t27/: 75 files of gHashTag/t27 at de2a1aca (2026-10-01 15:21 UTC), byte for byte and at their t27 paths. That is all of specs/trinity/ (the S01 project manifest, build graph, compiler matrix and 51 capability cards), the 16 canonical specs and 2 implementation files the cards name, and tools/trinity_manifest.py, the checker the cards answer to. The set is computed from the cards, not chosen: it takes the fields the S01 checker treats as paths (CANONICAL_SPEC, IMPLEMENTATION, GENERATED).
  • specs/reproduce/contracts.t27: the lock. It records the revision; the git ids of what the t27c build reads (root Cargo.toml and Cargo.lock, bootstrap/Cargo.toml, build.rs, src); the Zig that t27 runs its spec tests with (0.16.0, from its oracle-nightly.yml at the revision); the sha256 of every file; and the ledgers below.
  • tools/contracts.py:
    • vendor is the only writer of the copy and of the lock's data;
    • check holds the copy to the lock;
    • --upstream / --t27 DIR hold the lock to t27 at the revision (files, compiler ids, test Zig);
    • --t27c BIN runs the pinned compiler;
    • --self-check plants every rule.
  • .github/workflows/contracts.yml: builds t27c at the pin (cargo build --release --locked -p t27c from the workspace root), sets up Zig 0.16.0 and runs the whole check. It triggers on PRs that touch the copy, the lock, the tool or the workflow, on main, weekly, and by hand.
  • .gitignore re-includes external/t27/**. Its *.md and mcp/ rules left four of the vendored files out of the commit while the check, run in the working tree, passed. The check now asks git as well (IGNORED).

What the pinned compiler says about these contracts

t27c parse-complete and t27c test-report both exit 0 whatever they find, so the verdict is read from what they print.

result
parse-complete 70 specs; 69 are read whole. specs/queen/lotus.t27 loses 48 tokens: the bodies of tests lotus_set_parameter_updates_policy (and then where the grammar wants then) and lotus_episode_id_increments (a CycleResult{...} placeholder). Neither test exists for the compiler.
test-report, Zig 0.16.0 57 specs measured, 77 tests, 77 pass. 2 specs declare no test (specs/tools/mcp/needle.t27, specs/tools/mcp/trinity.t27). 11 of the 16 canonical specs never build a test binary.

The eleven, each with the first error test-report gets from Zig:

canonical spec first error
specs/api/c_abi.t27 value of type 'bool' ignored
specs/api/tri_api_loop.t27 value of type 'bool' ignored
specs/fpga/formal.t27 missing struct field: _dummy
specs/isa/ternary_encoding.t27 value of type 'bool' ignored
specs/numeric/gf16.t27 @intcast must have a known result type
specs/numeric/goldenfloat_family.t27 use of undeclared identifier 'sacred_physics'
specs/queen/lotus.t27 use of undeclared identifier 'then'
specs/tools/catalog.t27 value of type 'bool' ignored
specs/ui/viewport.t27 overflow of integer type 'u8' with value '648'
specs/vsa/trinity_compat.t27 remainder division with 'i32' and 'i32'
specs/vsa/vsa_core.t27 use of undeclared identifier 'Trit'

These are ledgers in the lock, as BLOCKED_ROOTS is in specs/reproduce/headless.t27. The check fails on any of:

  • a new entry, or a vanished one (the ledger may not outlive the defect);
  • a failing contract test;
  • fewer than 77 tests.

t27c typecheck is not used. At the pin it reports ok for pub const A : u32 = "x";, for an undefined name, and for pub const A : u32 = ;, so it cannot fail.

Negative controls

  • Self-check: 21 rules, each planted on a toy t27 and a fake compiler that prints the real output format. It also fails if any rule never fired.
  • Real compiler: one assertion broken in the vendored project.t27 gives DRIFT plus CONTRACT_TEST_FAILED naming the_initial_profile_is_headless.
  • Real .gitignore: with the previous one, IGNORED names all four dropped files.
  • Upstream: check --upstream against a fresh blobless fetch of t27 matches 75/75 files, 5/5 compiler ids and the test Zig, in 42 s.

Not yet (rest of #989)

  • The capability index (capability → spec → artifact → build/test → evidence). It reads these cards and holds the code to them; the S01 checker run against the current tree reports only the expected pin and count drift.
  • The end-to-end task, and the catalog refresh and publication.
  • The eleven blocked contract test suites and lotus' dropped tests are t27-side. This PR records them; it does not fix them.
{
  "version": 1,
  "head_sha": "39247d66ec947866b6b07c8e827c242fbffff92e",
  "summary": "Trinity consumes the S01 t27 contracts byte for byte at a pinned revision, with the compiler's source ids recorded and the pinned compiler run over them, instead of reading an unhashed catalog snapshot.",
  "changes": [
    "Vendored 75 files of gHashTag/t27 at de2a1aca into external/t27: specs/trinity/, the 16 canonical specs and 2 implementation files the capability cards name, and the S01 checker; the set is computed from the cards.",
    "Added specs/reproduce/contracts.t27, the lock: revision, git ids of what the t27c build reads, the Zig t27 tests its specs with, every file's sha256, and ledgers of what the pinned compiler cannot read or build.",
    "Added tools/contracts.py (vendor, check, upstream comparison, the pinned compiler run, a self-check that plants every rule) and .github/workflows/contracts.yml, which builds t27c at the pin and runs the whole check.",
    "Re-included external/t27 in .gitignore, whose *.md and mcp/ rules dropped four vendored files, and taught the check to ask git (IGNORED)."
  ],
  "tests": [
    {
      "command": "python3 tools/contracts.py --self-check",
      "status": "passed",
      "result": "21 rules each planted on a toy t27 and a fake compiler that prints the real output format, and each fired; the meta-check fails if a rule never fires.",
      "evidence": "Run locally on macOS Python 3 before the commit"
    },
    {
      "command": "python3 tools/contracts.py check --upstream",
      "status": "passed",
      "result": "75 of 75 files, 5 of 5 compiler ids and the test Zig match gHashTag/t27 at de2a1aca, fetched shallow and blobless.",
      "evidence": "Run locally against github.com in 42 s"
    },
    {
      "command": "python3 tools/contracts.py check --t27c <t27c built at de2a1aca> with Zig 0.16.0",
      "status": "passed",
      "result": "parse-complete: 69 of 70 specs read whole, lotus.t27 loses 48 tokens as ledgered; test-report: 57 specs, 77 tests, 77 pass; 11 canonical specs blocked and 2 without tests, as ledgered.",
      "evidence": "Run locally on macOS in 1 min 36 s; a broken vendored assertion was reported as DRIFT and CONTRACT_TEST_FAILED"
    }
  ],
  "limitations": [
    "The tests of 11 of the 16 canonical specs do not build with the pinned compiler's test-report, and two tests of lotus.t27 are dropped by its parser; this records them in the lock, it does not fix them in t27.",
    "t27c typecheck is not used as evidence, because at the pin it accepts a syntax error.",
    "The capability index, the end-to-end task and the catalog publication of #989 come next."
  ],
  "tags": [
    "Engineering",
    "Verification",
    "CI"
  ],
  "blog": {
    "title": "Trinity now reads its t27 contracts byte for byte",
    "summary": "A lock, a vendored copy and the pinned compiler replace a catalog snapshot, and show that 11 of 16 canonical contract specs cannot build their own tests.",
    "outline": [
      "Why a website mirror with overlays and no hashes cannot tell you which contract you are reading.",
      "The lock: revision, compiler sources, test toolchain and 75 hashes, and a set the cards choose.",
      "What the pinned compiler says: 77 contract tests pass, 48 tokens dropped, 11 suites that never build."
    ]
  }
}

Dmitrii Fedorov (@dmitrii-f-t27)

…revision (Refs #989)

S12 of #988, third part: consume the canonical t27 manifest and specifications
byte-identically, with a pinned revision and compiler hashes. Until now trinity met
t27 only through the website mirror, a catalog snapshot: a tarball of t27 master with
nine files of a second branch laid over it, no hash per file, and a compiler wasm of
unrecorded origin.

external/t27/ holds 75 files of gHashTag/t27 at de2a1aca (2026-10-01), byte for byte
and at their t27 paths: all of specs/trinity/ (the S01 project manifest and its 51
capability cards), the 16 canonical specs and 2 implementation files the cards name,
and tools/trinity_manifest.py, the checker the cards answer to. The set is computed
from the cards, not chosen. specs/reproduce/contracts.t27 locks the revision, the git
ids of what the t27c build reads (the root Cargo.toml and Cargo.lock,
bootstrap/Cargo.toml, build.rs and src), the Zig t27 runs its spec tests with
(0.16.0), and the sha256 of every file.

tools/contracts.py: `vendor` is the only writer of the copy and of the lock's data;
`check` holds the copy to the lock, `--t27` or `--upstream` hold the lock to t27 at
the revision, and `--t27c` runs the pinned compiler, parse-complete and test-report.
Both exit 0 whatever they find, so the verdict is read from what they print, against
ledgers in the lock: the parser drops 48 tokens of specs/queen/lotus.t27 (the bodies
of two BDD tests); the tests of 11 of the 16 canonical specs do not build with
test-report, each recorded with its first error; 2 specs declare no test; the other
57 specs run 77 tests and all pass. A new or vanished ledger entry, a failing contract
test or fewer tests fail the check. `t27c typecheck` is not used: at the pin it
accepts `pub const A : u32 = ;`. The self-check plants every rule on a toy t27 and a
toy compiler and fails if a rule never fired. .github/workflows/contracts.yml builds
t27c at the pin and runs the whole check.

.gitignore re-includes external/t27/**: its `*.md` and `mcp/` rules left four of the
vendored files out of the commit while the check, run in the working tree, passed.
The check now asks git as well (IGNORED), and against the old .gitignore it names
all four.

Потребляем контракты t27 байт в байт на закреплённой ревизии.

S12 эпика #988, третья часть: потреблять канонический манифест и спецификации t27
побайтно, с закреплённой ревизией и хэшами компилятора. До сих пор trinity видел t27
только через зеркало сайта -- снимок каталога: tarball master t27 с девятью файлами
другой ветки поверх, без хэша на файл и с wasm-компилятором неизвестного
происхождения.

external/t27/ содержит 75 файлов gHashTag/t27 на de2a1aca (2026-10-01), байт в байт
и по их путям в t27: весь specs/trinity/ (манифест проекта S01 и его 51 карточка),
16 канонических спек и 2 файла реализации, которые называют карточки, и
tools/trinity_manifest.py -- проверяющий, перед которым карточки отвечают. Набор
вычисляется по карточкам, а не выбирается. specs/reproduce/contracts.t27 фиксирует
ревизию, git id того, что читает сборка t27c (корневые Cargo.toml и Cargo.lock,
bootstrap/Cargo.toml, build.rs и src), Zig, которым t27 гоняет тесты спек (0.16.0), и
sha256 каждого файла.

tools/contracts.py: `vendor` -- единственный, кто пишет копию и данные lock'а;
`check` сверяет копию с lock'ом, `--t27` или `--upstream` -- lock с t27 на ревизии, а
`--t27c` запускает закреплённый компилятор: parse-complete и test-report. Оба выходят
с 0 при любом результате, поэтому вердикт читается из их вывода и сверяется с
журналами в lock'е: парсер отбрасывает 48 токенов specs/queen/lotus.t27 (тела двух
BDD-тестов); тесты 11 из 16 канонических спек не собираются test-report, у каждой
записана первая ошибка; 2 спеки не объявляют тестов; остальные 57 спек запускают 77
тестов, и все проходят. Новая или исчезнувшая запись журнала, упавший тест контракта
или меньше тестов роняют проверку. `t27c typecheck` не используется: на пине он
принимает `pub const A : u32 = ;`. Self-check подкладывает каждое правило на
игрушечном t27 и игрушечном компиляторе и падает, если правило ни разу не сработало.
.github/workflows/contracts.yml собирает t27c на пине и прогоняет всю проверку.

.gitignore снова включает external/t27/**: его правила `*.md` и `mcp/` оставляли
четыре скопированных файла вне коммита, а проверка в рабочем дереве проходила.
Теперь проверка спрашивает и git (IGNORED), и со старым .gitignore называет все
четыре.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant