Skip to content

W6.2: codegen-quality audit — tri-backend compile matrix (empty intersection) - #42

Merged
gHashTag merged 4 commits into
mainfrom
feat/w6-codegen-audit
Jul 5, 2026
Merged

gHashTag merged 4 commits into
mainfrom
feat/w6-codegen-audit

Conversation

@gHashTag

@gHashTag gHashTag commented Jul 5, 2026

Copy link
Copy Markdown
Owner

Summary

Establishes downstream compilability of t27c output across the three
declared backends. gen/ tree audited comes from
bf50ad64 on
feat/strategic-audit-2026-07-04.

backend tool OK FAIL dominant defect
Rust rustc 1.93.1, --emit=metadata 19/68 (28%) 49/68 E0425 = 2609
C cc -c -std=c11 -Wall -Wextra 2/68 (2.9%) 66/68 undeclared 1957 + assert(cond,msg) 867
Zig static + git-log verdict 0/68 (0%) 68/68 64 miss types.zig + 4 @CompileError

Cross-backend OK intersection: empty. W6.2-B (runtime differential)
structurally infeasible as originally scoped — this is the finding.

Deliverables

  • scripts/audit/{rust,c,zig}_*.sh — reproducibility package
  • docs/W6_CODEGEN_AUDIT_2026-07-05.md — 397-line report:
    • methodology asymmetry disclosure (Rust library-only vs C
      library+tests; hardline empty-intersection unaffected)
    • precise Zig claims split by mode (64 hard, 4 soft, empirical 0.15.2
      marked cross-environment)
    • §4.5 reconciliation companion phrasing (paper NOT modified in this
      PR; only companion text proposed)
    • anchor-bias record for three iterations (Vec<>, differential
      narrative, 'all modes')
  • docs/W6_WEAK_POINTS_AND_W7_PLAN.md — 8 weak points + literature
    review + W7 decomposed plan

Non-modifications

  • Does not alter t27c source.
  • Does not change paper §4.5 (companion phrasing recommendation only).
  • Does not run generated code (W6.2-B cancelled by empty intersection).

Verification

All three sweeps reproduce on feat/strategic-audit-2026-07-04:

git checkout feat/strategic-audit-2026-07-04
bash scripts/audit/rust_compile_sweep.sh
bash scripts/audit/c_compile_sweep.sh
bash scripts/audit/zig_static_check.sh

phi^2 + phi^-2 = 3

Establishes downstream compilability of t27c-generated code across
Rust, C, Zig backends. 68 modules from feat/strategic-audit-2026-07-04
(bf50ad6) audited under rustc 1.93.1 --emit=metadata, cc -c -std=c11
-Wall -Wextra, and static/version-invariant Zig verdict.

Findings:
- Rust: 19/68 OK (28%), 49 FAIL — undeclared identifier (E0425 = 2609)
  dominates at 93% of errors
- C:    2/68 OK (2.9%), 66 FAIL — undeclared (1957) + assert(cond,msg)
  2-arg misuse (867)
- Zig:  0/68 OK — 64 files import non-existent types.zig (hard,
  version-invariant), 4 files @compileError-bearing (soft, reachability)
- Cross-backend compile intersection: EMPTY. No module compiles across
  all three backends. W6.2-B runtime differential structurally
  infeasible as originally scoped.

Deliverables:
- scripts/audit/{rust,c,zig}_*.sh — reproducibility package
- docs/W6_CODEGEN_AUDIT_2026-07-05.md — full 397-line report with
  methodology asymmetry disclosure, precise Zig claims separated by
  compile mode, section 4.5 reconciliation companion phrasing, and
  self-errata for three anchor-bias iterations (Vec<>, differential
  narrative, 'all modes' overclaim)
- docs/W6_WEAK_POINTS_AND_W7_PLAN.md — 8 self-audit findings +
  literature review (YARPGen, C4, IRFuzzer, Fuzz4All, MT-SLR) + W7
  decomposed plan (8 workstreams)

Does not modify paper §4.5. Recommends companion phrasing only;
paper commit deferred to explicit approval.

phi^2 + phi^-2 = 3
@gHashTag gHashTag added the documentation Docs label Jul 5, 2026
Perplexity Computer added 3 commits July 5, 2026 10:43
- docs/WAVE_REPORT_2026-07-05.md — full week retrospective (66 commits,
  20 PRs) organized into 6 waves. Each wave has metaphor, key commits,
  and a scientific parallel (YARPGen, CompCert, C4, etc). Includes
  anchor-bias episode case studies (Vec<>, differential-narrative,
  'all modes'), bedrock artifacts list, what does not survive, and
  full provenance table for every quoted number.
- docs/W7_COLLAB_OPTIONS.md — three collaboration variants for next
  Wave loop: Option A (cloud drives, local verifies), Option B (by
  concern-layer), Option C (sequential with gates). Recommendation:
  Option B.

phi^2 + phi^-2 = 3
Zone 1 (§4.5 reconciliation companion phrasing):
Removed bare per-backend gradient (28%→0%) from proposed §4.5 text.
Gradient is methodology-contaminated (Rust library-only vs C+Zig
library+tests, see §Methodology asymmetry two paragraphs below).
Keeping it inline in §4.5 without co-located caveat reintroduces
the anchor-risk the audit disarms — reader who stops at §4.5 gets
unqualified gradient.

Kept in §4.5: 0/68 cross-backend intersection only. This finding
is methodology-independent (Zig 0/68 driven by structural missing-
types.zig at module scope, not test content). Explicitly tagged as
such. Gradient and its methodology are deferred to the audit body,
where §Methodology asymmetry already co-locates the caveat.

Result: iron finding surfaces in paper §4.5, methodology-contaminated
number stays in audit where caveat is co-located.

Zone 2 (Zig 4-file disclaimer):
Optional-precision polish per general review. Replaced
'Under zig test these are triggered by test-block analysis' with
'sufficient to prevent compilation under zig test; these files may
additionally exhibit test-block defects not individually characterized
here'. @CompileError is sufficient cause but not exhaustive — 4 files
may also carry undeclared-identifier defects in test blocks like
transport_tx_fsm does, but we did not enumerate.

Zone 3: unchanged (approved as-is by review — 'partly attributable'
hedge and 'finding of interest is not the gradient but the empty
intersection' remain verbatim).

phi^2 + phi^-2 = 3
…ach)

Line 272 read 'Eight modules each carry 24 stub sites' which parses as
8*24=192; the following list (1+6+1+2+1+5+5+3=24) contradicts the 'each'
reading. Reworded to 'The 24 stub sites are distributed across eight
modules:' — matches the list totals, and preserves precision-discipline
that is the whole thesis of this document.

Semantic content unchanged (24 stubs, 8 modules, same distribution).
Only wording precision.

phi^2 + phi^-2 = 3
@gHashTag
gHashTag marked this pull request as ready for review July 5, 2026 11:56
@gHashTag
gHashTag merged commit 1890349 into main Jul 5, 2026
2 checks passed
gHashTag pushed a commit that referenced this pull request Jul 5, 2026
….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 added a commit that referenced this pull request Jul 5, 2026
… downstream compilability companion (#36)

Paper-delta v0 skeleton: δ-paper positioning against mesh + formal-methods landscape, plus §4.5 empirical bench matrix (204 cells clean per byte-determinism predicate) plus §4.5.6 downstream compilability companion (Rust 19/68, C 2/68, Zig 0/68, cross-backend ∅) sourced from W6.2 codegen audit (PR #42 @ 1890349).

The §4.5.6 addition (commit 08f0401) applies the audit's Section 4.5 reconciliation recommendation without altering any true-per-predicate claim in §4.5.1–§4.5.5. §4.5.2 (byte-determinism of generation, 204/204 clean) and §4.5.6 (downstream compilability, 21/204 OK) measure orthogonal properties.

Discipline log — Anchor #5 recorded: 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.

Merged under user autonomy override ("сам мержи") issued 2026-07-05 21:32 +07, after user's own verification of §4.5 predicate against ground truth in audit doc §Section 4.5 reconciliation and PR #36 committed body.

Commits (post-squash provenance):
- 178608a docs(paper-delta): v0 skeleton — spec-first + reproducible-HDL positioning
- 527886c docs(paper-delta): add Section 5 — reference implementation of audit-trail primitive
- 171f675 docs(paper-delta): add §4.5 empirical bench matrix — 27 specs × 3 backends
- be70505 docs(paper): §4.5 catch-up — 27/81 → 68/204, coverage 100.0%
- af9f48c docs(paper-delta): integrate real W5 bench harness numbers into §5.5
- 08f0401 docs(paper-delta): add §4.5.6 downstream compilability companion + §4.5.5 gap bullet

phi^2 + phi^-2 = 3
gHashTag pushed a commit that referenced this pull request Jul 22, 2026
…rsal brick

#42 gave each side its public address (STUN); the missing half is USING two
addresses to connect across networks. HolePunch.swift is the connectivity check:
both peers send probes to each other's candidates at the SAME time, and that
simultaneous open punches a pinhole through each NAT (NAT B admits A's inbound
because B just sent outbound toward A). The pair that completes a probe/ack
round-trip is the one the media call uses.

Pure + standalone (like StunClient). Three verified layers, all in
smoke/harness/holepunch.swift (the 9th verify.sh test, verify: 9 passed, 0 failed):
  1. probe/ack wire codec bit-exact (0xFD 0x1C / 0xFD 0x1D + big-endian txid);
  2. ICE-style pair priority (RFC 8445 6.1.2.3) + nomination on synthetic
     candidates — host outranks srflx, pair priority is identical from the
     controlling and controlled views, nominate returns the best SUCCEEDED pair;
  3. TWO real agents hole-punch each other over loopback UDP (real sockets, two
     threads) and both hear an ack — run 5x, 5/5, so it is deterministic not lucky.

Robustness by design, not luck: each agent retransmits its probe every 50ms for
the whole window and answers every probe it sees, so the ack is guaranteed
regardless of who sends first; acks reply to the OBSERVED source (recvfrom's
from-addr), which is the pinhole a symmetric NAT opens.

Boundary: a single machine proves the check/wire/selection over real UDP, NOT
traversal of a real NAT (needs two separate NATs). Wiring candidate exchange over
a signaling channel + running punch() before the media socket is the third brick;
HolePunch.swift is harness-proven but not in project.yml until used.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
gHashTag pushed a commit that referenced this pull request Jul 23, 2026
…NAT brick)

#42 gave each side its public address (STUN), #43 punched between two KNOWN
ports. The missing glue: serialize the candidate LIST so the two sides can
exchange it over a signaling/rendezvous channel, and orchestrate a real connect
that probes ALL of the peer's candidates and nominates the one that answers (a
NAT may silently drop some pairs). IceSession.swift does both, pure + standalone,
reusing HolePunch's probe/ack codec and priority:
  * Ice.encode/decode: [count:2][kind:1][port:2][ipLen:1][ip] per candidate,
    bounds-checked on parse;
  * Ice.connect(localPort, remote[]): bind one socket, probe every remote for the
    whole window, ack observed sources, nominate the highest-priority remote that
    actually answered; report the bound port as the media socket to hand off.

Verified in smoke/harness/ice_session.swift (10th verify.sh test, verify: 10
passed, 0 failed): serialization round-trips + rejects garbage; and TWO real
in-process sessions exchange serialized blobs and connect over loopback UDP while
correctly discarding a decoy candidate (192.0.2.2, RFC 5737 unroutable) that
never answers. Ran 3x, 3/3 deterministic.

Nominate by "did it ACK", never by priority alone — that is what makes a dead
higher-priority candidate get skipped instead of selected. Do not early-exit on
first success (strands the peer mid-handshake); run the full window, keep acking.

Boundary: loopback proves serialize/exchange/connect/nominate over real UDP, NOT
traversal of a real NAT (two separate NATs). The three bricks (STUN, punch,
session) are harness-proven; wiring connect() into CallManager before the media
socket, fed by the room's exchanged candidates, is the integration step.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
gHashTag pushed a commit that referenced this pull request Jul 23, 2026
…fore building it

The three NAT bricks (STUN #42, punch #43, ICE session #44) all assume the peers
already hold each other's candidate lists. Whatever rendezvous carries that list
must NOT be trusted to read or forge it: an injected candidate redirects the call
to a machine the attacker controls (classic ICE candidate-injection / call hijack;
WebRTC blocks it with signed SDP + a DTLS fingerprint). This is a prerequisite for
a rendezvous, not an afterthought — shipping candidate exchange unsealed is a
call-hijack hole.

CandidateOffer.swift (pure; reuses MeshCrypto.inviteAuthKey + Ice serialization):
seal [version][tiebreaker:8][expiry:8][Ice candidate list] under a room-derived
key, with an expiry so a captured offer cannot be replayed later, and an ICE
controlling/controlled tiebreaker. The offer key is domain-separated from the
invite key by one HKDF step so a candidate offer and an invite can never be
cross-interpreted.

Verified in smoke/harness/candidate_offer.swift (11th verify.sh test, 13 checks,
verify: 11 passed, 0 failed): honest round-trip recovers the list + tiebreaker;
wrong room passphrase -> nil (confidential); flipped auth-tag byte -> nil
(unforgeable); the offer does NOT open under the raw invite key (domain
separation); past-TTL -> nil (stale, un-replayable); role resolves oppositely for
the two peers. Clock is injected so expiry is deterministic; only static room-key
derivation is used, so no MeshCrypto() is built and the Keychain is untouched.

Four harness-proven NAT/exchange modules now exist (StunClient, HolePunch,
IceSession, CandidateOffer); none are in project.yml / wired into CallManager yet —
that integration, fed by a rendezvous carrying these sealed offers, is next.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
gHashTag pushed a commit that referenced this pull request Jul 23, 2026
…r -> sealed offer)

Four waves built harness-proven but UNWIRED NAT modules (StunClient #42, HolePunch
#43, IceSession #44, CandidateOffer #45). Proven-in-a-harness is not
proven-in-the-product, and four modules outside the binary is a growing debt. This
wave puts them in the shipping Mac app and proves they run there, WITHOUT touching
the working same-subnet call.

  * project.yml: register the four modules + a new NatDiagnostics; xcodegen
    regenerated the tracked pbxproj (clean +20 lines, only the 5 files, no churn).
  * NatDiagnostics.run(): off-main at launch (.onAppear), gathers host + STUN
    server-reflexive candidates and seals a CandidateOffer under the current room,
    then logs it. Additive only — nothing in the call/media path changes.

Verified LIVE in the built binary (not a harness): launched with TRINET_LOG and
read back
  TRINET NAT: candidates host=["192.168.1.104"] srflx=182.232.218.171:59434
              -> sealed offer 83B (room=lobby)
so StunClient.hostCandidates + gatherServerReflexive (real public address via
Google STUN) + CandidateOffer.make all execute inside the app; the app did not
crash, so the working call is intact.

Deferred deliberately: the iOS embed (static file list is fragile) and the real
integration — deliver the offer via a rendezvous and run Ice.connect before the
media socket. The app now HOLDS its sealed candidate offer; delivering it and
connecting on it is next.

Co-Authored-By: Claude Opus 4.8 <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