docs(paper-delta): v0 skeleton — spec-first + reproducible-HDL positioning#36
Merged
Conversation
added 2 commits
July 4, 2026 14:23
…oning Skeleton for the δ-paper positioning Tri-Net against the current mesh / formal-methods landscape: - Thesis: 'a proof is only as good as its spec' (Carrone 2026), instantiated at the codegen level via specs/wire.t27 SSOT + t27c gen-rust + drift-guard. - Related work: Mesh Inference (arXiv 2606.19537v2), MAREF/TLA+ posture, SLD-Spec, Reticulum/Meshtastic landscape, RISC-V HDL Tournament, Qualcomm AI-mesh patent — all with fetched URLs. - Contribution: CI-enforced spec/impl byte-identity as a primitive; language- level SSOT; in-repo audit trail extended to competitor-watch protocol. - Delta section states positioning vs each competing school explicitly. - Honest limits: pre-silicon, Rust-only SSOT until t27#1333, byte-identity not yet functional-correctness proof. - Appendix: reproducibility recipe (5 shell commands) matching drift-guard. Draft only — not for external circulation. Anchor: phi^2 + phi^-2 = 3.
…dit-trail primitive Bounded expansion (not full v1). The skeleton previously proposed the auditability primitive abstractly (Sections 1-4); this commit adds Section 5 reporting that the primitive is now empirically realized end-to-end at tri-net main dc1bebb + t27 master 3c912d9. Section 5 subsections: - 5.1 What is materialized -- one spec (specs/wire.t27), three generated backends (gen/{rust,zig,c}/wire.*), one workflow (spec-drift-guard.yml), consumer path under the same umbrella (src/wire.rs -> u32_be). - 5.2 Audit-trail tuple (concrete instance) -- (tri-net@dc1bebb, t27@3c912d9, spec-drift-guard run) is the minimal fetch set for a third party to independently verify byte-identity. - 5.3 Merge chain table -- 5 tri-net PRs (#33/#34/#35/#37/#38) + 2 t27 PRs (#1320/#1337) with merge SHAs. - 5.4 Empirical checks at HEAD -- three diff -u results (all empty), zero 'unsupported: ExprCast' in Zig/C output, 101 lib tests green including header_roundtrips as empirical byte-order-equivalence proof. - 5.5 What this reference impl does NOT show -- byte-identity is not functional correctness; only one spec is covered so far; no silicon; trust in t27c itself is not eliminated (moved, per Carrone 2026). Sync updates across the doc: - Header cross-link: 91a5b63 -> dc1bebb (post-#38). - Section 3.1: describes all three gen targets, not just Rust. - Section 3.2: drift-guard covers Rust + Zig + C; links to #35 + #38. - Section 3.3: ExprCast marked resolved on all four backends (Rust #1320, Zig+C #1337, Verilog pre-#1320). - Section 6 (Limits): removed obsolete 'Rust-only SSOT until #1333' bullet; added trust-surface-of-t27c and no-HDL-target-yet bullets. - Section 7 (Future work): struck through completed Zig+C drift-guard item; added protocol-stack expansion, t27c deterministic-build items. - Appendix A: three-target reproducibility recipe (8 steps), pins tri-net@dc1bebb + t27@3c912d9. Draft only -- not for external circulation. Anchor: phi^2 + phi^-2 = 3.
gHashTag
force-pushed
the
docs/paper-delta-v0
branch
from
July 4, 2026 14:25
980768b to
527886c
Compare
added 4 commits
July 4, 2026 15:59
…kends New Section 4.5 (Empirical bench matrix) inserted between §4 Contribution and §5 Reference implementation: - 4.5.1 Methodology — cell/clean-predicate/drift-event definitions, explicitly scoped to byte-identity (not semantic equivalence). - 4.5.2 Matrix — 27×3 = 81 cells, all clean, per-spec line counts, row totals (rust 2804, zig 3579, c 5150, grand 11533). - 4.5.3 Layer coverage — 11 protocol layers spanned. - 4.5.4 Language-level constraint — pure-functional-only empirical finding; 4 deferred specs recorded honestly with root causes (3× let-mut, 1× spec syntax error). - 4.5.5 What the matrix does NOT show — explicit non-claims list. §5 preamble updated to position §5 as zoom-in on wire.t27 as one row of the §4.5 matrix, rather than sole reference implementation. Source of truth: docs/BENCH_MATRIX_MANIFEST_2026-07-04.md on branch feat/strategic-audit-2026-07-04. All line counts machine-derived and independently verified (sum-check confirmed). No fabricated numbers. No semantic-equivalence claim. No behavioural claim. No performance claim. Only byte-identity of gen output against committed artifact at the pinned tuple. phi^2 + phi^-2 = 3
Bench matrix section had gone stale twice as the SSOT flip ran ahead of the paper (27 → 31 → 62 → 68 during the 2026-07-04 loop). This commit brings §4.5 in sync with the actual matrix committed on tri-net/feat/strategic-audit-2026-07-04 at 9377d2b, drift-verified against t27/master @ 879c1c7. Changes: - §4.5 title: 27 → 68 specs × 3 backends - §4.5.1 cell count: 81 → 204, added coverage line (68/68 = 100.0%) - §4.5.2 pinned tuple bumped to 9377d2b / 879c1c7; new 68-row matrix regenerated from wc -l gen/{rust,zig,c}/<spec>.<ext> - §4.5.2 row totals: rust 9,993 / zig 11,063 / c 15,830 / grand 36,886 (was: 2,804 / 3,579 / 5,150 / 11,533 across 27 specs) - §4.5.3 layer coverage expanded from 11 → 18 categories. The 7 new categories (monitoring, simulation, tooling, coordination, security-ops, analytics, testing) are marked honestly as 'supporting' rather than protocol layers, and the paragraph updated accordingly. - §4.5.4 rewritten: the four previously-deferred specs (adaptive_retry, link_quality_monitor, multipath_router, auto_config) are now IN the matrix. Recorded the real root cause (missing semicolons on const declarations, not 'let mut' as originally suspected) and that auto_config was actually clean and had been deferred on an unrelated build error. Corpus is 68/68 = 100.0%, zero deferred. - §4.5.5: dropped the 'four specs are not in the matrix' bullet since none exist anymore. - Section 5 intro: '27 specs × 3 backends' → '68 specs × 3 backends'; 'remaining 26' → 'remaining 67'. Arithmetic verified three independent ways: wc -l gen/<be>/<sp>.<ext> == Python sum(1 for _ in open(f)) == markdown table column sums All three agree at rust=9993, zig=11063, c=15830, grand=36886. Anchor: phi^2 + phi^-2 = 3
- §5.5 rewritten: real measurements at tri-net bf50ad6 / t27 879c1c7 * 1020 measurements + 204 warmups (68 specs × 3 backends × 5 runs) * Rust 1.824ms, Zig 1.805ms, C 1.789ms medians; grand mean 1.819ms * cross-backend median spread 3.9%, worst wire 11.7% * numpy.linalg.lstsq R²: Rust 0.645, Zig 0.862, C 0.831 * throughput 539-555 specs/s, sum-of-medians 368.5ms full corpus * links to raw CSV (1020 rows), summary CSV (204 rows), JSON aggregates - old §5.5 ("does NOT show") renumbered to §5.6, updated to reference §5.5 bench numbers as sandbox-VM (not silicon) - §5.1/§5.2 cross-links bumped from dc1bebb → bf50ad6 - §5.3 merge chain rows added for t27#1348 and tri-net#39 - §5.4 pass count 101 → 141 tests, corpus scope generalized to 68 specs - §6 coverage bullet: 68/68 SSOT contract explicit - Appendix A: bf50ad6 + 879c1c7 pinning, 141 test pass count All numbers reproducible from committed scripts/bench/*.py and bench/raw/*.csv. No fabrication: every value in §5.5 comes from the actual analyze.py output committed at bf50ad6. phi^2 + phi^-2 = 3
….5.5 gap bullet Applies the §4.5 reconciliation companion phrasing recommended by the W6.2 codegen audit (docs/W6_CODEGEN_AUDIT_2026-07-05.md, merged via PR #42 at 1890349) to the paper-delta §4.5 empirical bench matrix. Motivation. §4.5.1 defines "clean" as a byte-determinism predicate: (1) no return()/unsupported markers, (2) byte-match against committed artifact, (3) tri-net cargo test --all passes. Under this predicate, "204 cells all clean" and "68/68 = 100% flipped" are TRUE, and §4.5's existing disclaimer (line 109) explicitly scopes the claim to "reproducibility of the pinned generator output" and disclaims semantic cross-backend equivalence. However, the disclaimer covers semantic equivalence but is silent on downstream compilability. A reader who sees "204 clean" plus "not a semantic equivalence proof" can still reasonably infer "the generated code compiles under standard toolchains" — an inference the W6.2 audit shows is not supported (Rust 19/68, C 2/68, Zig 0/68, cross-backend intersection ∅). This is the misleading-by-omission gap the audit's §Section 4.5 reconciliation flags. This commit closes it without altering any true-per-predicate claim in §4.5.1–§4.5.5. Changes. - §4.5.5 gets a fourth bullet: "Not a claim of downstream compilability" — explicit scope note that the clean-predicate is byte-determinism only. - New §4.5.6 "Downstream compilability (companion to §4.5.2)": - Per-backend compile matrix (Rust 19/68, C 2/68, Zig 0/68) with dominant defects, sourced verbatim from the audit. - Cross-backend intersection ∅ statement. - Explicit orthogonality note: §4.5.2 and §4.5.6 measure different properties (generation determinism vs downstream acceptance); the 204/204 clean result is not contradicted by 21/204 compile-OK because they answer different questions. - Scope statement mirroring the audit's Section 4.5 reconciliation recommendation. - Methodology asymmetry disclosure (Rust library-only vs C library+tests) with note that empty-intersection finding is unaffected. - Both §4.5.5 and §4.5.6 link to the audit document at its main-@ merged SHA (1890349) and to PR #42 for provenance. Non-modifications. - §4.5.1 Methodology (clean-predicate lines 101-107): unchanged. - §4.5.2 Matrix table (204/204 clean): unchanged. - §4.5.3 Layer coverage: unchanged. - §4.5.4 Language-level constraint (68/68 flipped statement): unchanged. - Line 109 disclaimer (semantic-equivalence scope): unchanged. The paper-delta document remains a v0 skeleton. This is a companion addition to §4.5, not a rewrite. Discipline anchor recorded in session log (Anchor #5): distinguishing "claim is false" from "claim is true-per-predicate + omission" requires reading the claim's own predicate first, not applying an external predicate. Corollary to Anchor #4 (corpus-scoped verification): claim-scoped verification for accusations. Diff: 26 insertions, 0 deletions. phi^2 + phi^-2 = 3
gHashTag
marked this pull request as ready for review
July 5, 2026 14:44
gHashTag
pushed a commit
that referenced
this pull request
Jul 22, 2026
…r consistency
Single-process loopback could never test the identity crypto: it self-pairs (safety
number over ONE identity, degenerate) and can't stage a MITM. The two-endpoint rig now
can, given DISTINCT identities per instance — added TRINET_KC_ACCOUNT (keychain account
suffix) and TRINET_PINS_KEY (pin-store suffix) so two local instances hold separate
identities + separate TOFU pins (dev-only, inert in a shipping run; mirrored on both
platforms to stay byte-identical).
smoke/two_endpoint_security.sh, verified live:
TEST 1 two honest peers (A,B) with distinct identities derive the SAME safety number
(24514929508 == 24514929508) with ZERO false MITM — the real Signal-style check
that single-process loopback could not do.
TEST 2 A pins B, then an impostor M with a DIFFERENT identity answers at B's address;
A flags "identity CHANGED — session refused" and decodes ZERO video from M — a
real over-the-wire MITM detection of the pinning feature (#36), not a harness.
Also: the MITM rejection now logs ONCE (on the false->true transition) instead of on every
impostor handshake retry (the rig saw 65196 lines; now 2). The latch + session refusal
are unchanged. Both platforms build.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Adds
docs/PAPER_DELTA_v0.md: a DRAFT skeleton for the δ-paper positioning Tri-Net against the current landscape, plus §4.5 empirical bench matrix, plus §4.5.6 downstream compilability companion (added08f0401after W6.2 audit merge).Sections
1890349).Why (§4.5.6 addition,
08f0401)Under §4.5.1's clean-predicate (byte-determinism of generation), "204 cells clean" is true and existing line-109 disclaimer scopes the claim to "reproducibility of pinned generator output," not semantic equivalence. However, the disclaimer covers semantic equivalence but is silent on downstream compilability. A reader who sees "204 clean" plus "not a semantic equivalence proof" could still infer "the generated code compiles under standard toolchains" — an inference W6.2 shows is not supported.
§4.5.6 closes this misleading-by-omission gap without altering any true-per-predicate claim in §4.5.1–§4.5.5. The two rows measure orthogonal properties:
The audit's Section 4.5 reconciliation recommendation is now applied in the paper-delta, at its recommended location, without rewriting the pre-existing 204-clean statement.
Non-modifications
08f0401: 26 insertions, 0 deletions.Scope
DRAFT SKELETON. Merges to
docs/only.Discipline log
Anchor #5 recorded during this PR review: distinguishing "claim is false" from "claim is true-per-predicate + omission" requires reading the claim's own predicate first, not applying an external predicate. Corollary to Anchor #4 (corpus-scoped verification): claim-scoped verification for accusations. Documented in commit
08f0401body.Merge authorization
Merged under user autonomy override ("сам мержи") issued 2026-07-05 21:32 +07 after user's explicit verification of §4.5 predicate against ground truth (audit doc §Section 4.5 reconciliation, PR #36 committed body, clean-predicate lines 101-107). Override recorded, verification path documented.
phi^2 + phi^-2 = 3