Conversation
…itor scan Overnight autonomous improvement loop (issue #5083). Baseline measured on untouched master: 148 corpus reds; the reframe finding is the parser's silent discard — 114 specs lose top-level tokens (worst ternary_inference 1813), 65 specs' invariant bodies are discarded unchecked, 23 specs refused outright. Competitor scan: everyone we race fails loudly where we continue silently. Safety constitution + iteration protocol in the charter; remote mutex held via tri loop claim. Closes #5083 (loop PR will carry the fixes; this commit is the loop's record) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
This was referenced Sep 28, 2026
…iscarding them The colon-form forall arm of parse_invariant_clause was the dominant silent discard channel: 581 whole-block fallbacks across 35 specs, 84% of all amnestied tokens (19,939/23,831) rode bdd-block-fallback. Preservation keeps the statement verbatim in block.value marked partial (NOT CHECKED emitted, children empty so emitted bytes and committed seals do not move), consumes the tokens instead of dropping them, and leaves lowering to #2774. Measured: discarded top-level tokens corpus-wide 27,562 -> 14,364 (-48%); ternary_inference 1813 -> 87; corpus reds 148 -> 148 (volume, not count); failing-spec set identical to baseline; zero new reds. Ratchet ledger re-blessed CLEAN: discard sum pinned 14,364, max_entries 152 -> 148, and the population resynced to measured reality (52 stale entries dropped, 47 never-tracked failing specs added -- every added path verified already failing at baseline; none caused by this change). Closes #5083 (loop PR #5084) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-09-28 18:02:13 UTC
Summary
Seal Status
|
…me since Jul 31 Deliberate rewrite per the issue's second option: format! x8 (three with string args became corpus-idiom concat; three with int args became constant strings, each with a comment naming what was dropped and where the data still lives), Rust suffix T? x2 became the corpus prefix ?T. Everything else in the file -- let mut, for-in over .lines(), +=, ! prefix, chained string methods, if-expression struct fields, ... spread -- already parsed; the file was one macro and two type suffixes away from parsing for two months. AST verified whole (orphan tail included), trailing newline added. Ratchet: unexpected failures 0, unexpected passes 1 (this spec), corpus PRIMARY 148 -> 147, ledger entry retired (147/147 cap), RATCHET CLEAN. Closes #5079, closes #5083 (loop PR #5084) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-09-28 18:22:50 UTC
Summary
Seal Status
|
… reads first tri loop claim guards the REMOTE collision (two sessions, one task list). This guards the LOCAL one, measured on the first overnight loop: a session resumed in the main checkout while the loop's worktree sat elsewhere, and state.md's branch: line was the only thing that said so -- unread. A state file updated by hand after every iteration is also a file a crashed write can leave half-empty, which is exactly when a firing reads it. Parses the fenced block with its real multi-line values (current-task routinely carries a four-space-aligned continuation; alignment padding is trimmed, not appended), names missing required keys by name (not count), refuses to guess between multiple docs/loop/*/state.md, cross-checks the branch the state names against the checkout, warns on dirty files without failing (mid-iteration is the normal dirty state) and on unpushed or never-pushed work. Exit 0 clean, 1 state-vs-tree divergence, 2 could-not-run. Tests pin the arms: multiline parse, named missing keys, exit-1-not-2 on branch divergence (needle-pinned like the claim tests). Live check: run against the loop's own state.md it caught the ci-gates .gitattributes side-write and the unset upstream on the first invocation. Closes #5083 (loop PR #5084) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-09-28 18:26:49 UTC
Summary
Seal Status
|
The largest remaining whole-block-fallback row was 256 events across 29 specs: BARE `invariant NAME` whose body leads with its binder (forall acc : i32, a : i8 ...). The clause walker hit forall, did not recognize it, and the whole remaining body became one fallback event -- every token after it silently discarded. Same preservation as site 1 (a976e54), reusing the same walker capture_to_next_top_level: forall arriving at the head of a not-yet- lowered block is captured verbatim into value, marked partial (emitter prints NOT CHECKED), tokens consumed (stop counting as dropped), children empty so emitted bytes and committed seals do not move, and #2774 keeps owning lowering semantics. Measured: discarded tokens 14,364 -> 8,559 (-5,805; cumulative -69% from the 27,562 baseline); forall row gone from the census; ternary_mac 0 events; corpus PRIMARY 147 (preservation is volume, not count); gate diff rc=0 no new reds. Ledger re-blessed 147/147, RATCHET CLEAN, added entries not failing at baseline: []. FROZEN_HASH 5bd6c20baf5e4e79 -> d925e634aa4cfbca (tri reseal write; the compiler's own seal, not a corpus reseal). Closes #5083 (loop PR #5084) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…sealed) 681 FAIL lines -> 358 mismatch specs + 313 no-file specs, classed by signature: 249 SPEC+all-backends (source normalization waves; spec_hash is sha256 over raw source bytes, confirmed at main.rs:2938), 31 pure codegen quotes-fix class, 27 zig-only, 23 shared-emitter, 12 comment-only edits, ~16 tails. Smallest honest reseal batch ~81 pure-codegen specs IF each underlying commit is confirmed intended. New defect found while measuring: seal-name collision -- the namer flattens specs/ + '/'->'_', so specs/a/b_c.t27 and specs/a_b/c.t27 both map to a_b_c_spec.json. Exactly one colliding pair exists today. Nothing was resealed to produce this; the standing no-mass-reseal rule is restated inside. Closes #5083 (loop PR #5084) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-09-28 19:00:08 UTC
Summary
Seal Status
|
This was referenced Sep 28, 2026
Merged
Merged
…idate-lean-standalone phase and rewrite the W472 block in real Lean One defect, four layers, each hiding the next: 1. W472 (PR #4765, 2026-08-06 bulk merge) committed Lean that never compiled: 'struct' for 'structure', Rust Array API (arr.length/ arr.update/arr.idx), list literals for Array, nonexistent Array.forall, hallucinated .0/.1/.data.(1) fields. Rewritten against the real core API (Array.set with proof param, primed [i]'(h), dif_pos, Array.all, #[...] literals) + imports Trinity.TernaryMac/TernaryGemm. Builds clean: 0 errors, 0 warnings, 0 sorry. Two statements were FALSE lemmas, not proof failures — corrected with comments, not papered over: raw_ns_preserved_under_jitter (RawNsPredicate base does not imply RawNsPredicate (base+2)) and worst_case_jitter_envelope_bound (use 200_002, falsified at 200_000+jitter). 2. The same bulk merge dropped the validate_lean_standalone phase body from smoke_gate; the flag it never set made every requesting run report passed:false. Restored from a002243: build standalone .lean from theorem-matrix fixtures via measured_to_lean (21-arg signature unchanged), compile in a temp lake package, set the flag, write the entry the snapshot pins. 3. d51db4a (#2305) had restored the dry_run_sweep flag but the merge had ALSO dropped the synthetic-JSON sweep check and the 18th synthetic_operating_point parameter from cclk_sweep itself, leaving every dry-run operating_point.source hardcoded "not_read". Restored: the json sweep verification (variant count + per-variant source check), the W450 entry shape the snapshot pins, the cclk_sweep param, and the --synthetic-operating-point CLI flag (conflicts_with xadc). Dry-run PVT labels now closed-vocabulary correct (pvt_context_file/synthetic/ not_read). d51db4a's reshaped keys (variants/report_file) had no readers. 4. Master lean CI has no push trigger (deliberate, #5082 pending workflows scope) — which is why layers 1-3 stacked invisibly. Verified: lake build Trinity.TernaryFPGABoot clean; 4/4 lean_standalone tests green; full cargo test -p tri: 827 passed / 0 failed (was 824/3, proven pre-existing on master at 2925def). Corpus untouched; no bootstrap/ change, seals and FROZEN_HASH unaffected. Closes #5083 (loop PR #5084, iteration 5 — report: docs/loop/auto-2026-09-29/iterations/05-fpga-lean-restoration.md) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Contributor
PR DashboardGenerated at: 2026-09-28 21:25:22 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
…es (Refs #5083) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Contributor
PR DashboardGenerated at: 2026-09-28 21:27:06 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
… 824/3→827/0 pass (Refs #5083) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This was referenced Oct 5, 2026
…ests replace 4 vacuous ones backward said dL/dp = (p - t) / p; the derivative of -t ln p is -t / p (the old form is the softmax+CE logit gradient p - t, divided by p). New test backward_matches_finite_difference ties backward to forward. Tests read default_input() (defined nowhere) and asserted result != undefined of void fns; now fixtures run one sample and compare numbers computed by hand. u32 <- .len became usize, f32(x) -> x as f32, f32.max/log -> @max/@log. tri lab-exec: compiles, 6/6 tests pass; a mutated expected value is reported FALSE. Refs #5083 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…the loop's tools Refs #5083 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This was referenced Oct 5, 2026
Merged
…n overflow, checked against independent definitions - tanh: the (e^x - e^-x)/(e^x + e^-x) body was NaN for |x| > ~44 (inf/inf); now 1 - 2/(e^2x + 1). math::exp -> @exp; forward_batch writes a caller-owned output instead of `[]f32{input.len}`. New tests: odd symmetry, saturation, central-difference derivative. - silu_swish: beta was ignored, so Swish_beta was false for every beta != 1; forward_batch was a placeholder returning its input (the zero-input test could not see it). Now x*sigmoid(beta*x) and its derivative; finite difference at beta 1 and 2; restoring the old body fails exactly the two beta tests on the lab. `then true` invariants -> one real assert + a NOT CHECKED note. - gelu_approx: math::tanh named nothing (Zig has no tanh builtin); forward_batch indexed into a zero-length slice; the header called the tanh approximation "exact GELU". The old test derivative(-1) > 0 was false (exact GELU'(-1) = -0.0833; lab: -0.08296). New: published value at 1, gelu(x) - gelu(-x) = x, finite-difference derivatives. Lab (58e452e): tanh 7/7, silu_swish 10/10, gelu_approx 12/12; each mutation check reported FALSE. Refs #5083 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The exact branch computed phi(x) = exp(-x^2/2) / sqrt(2), so the x*phi(x) term of GELU' was 1.77x too large at every x != 0. Every backward test sat at x = 0, where that term vanishes. New gelu_backward_exact_matches_ finite_difference: with the old divisor the lab reports |grad - slope| = 0.179 at x = 0.8; with 1/sqrt(2*pi) it passes. @tanh and @erf are not Zig builtins: tanh is the saturating 1 - 2/(e^2z + 1), erf is Abramowitz & Stegun 7.1.26 (|err| <= 1.5e-7). Tests now use fixture fns over [1]f32 arrays (the `[]f32{0.0}` given-forms did not lower) and check GELU(1) = Phi(1) = 0.8413447, the tanh form's 0.8411920, finite differences on both branches, saturation at +-50. `then true` on the cubic coefficient is now a value check. Lab (9f98d1a): 11/11. Refs #5083 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Every test passed one argument fewer than forward(input, output, config) and backward(grad_output, input, grad_input, config) declare (lab-exec: 6 argument-count errors), so none of them ever ran. Fixture fns over [3]f32 arrays now hold the buffers; the claims are unchanged, plus a finite-difference check of backward on both sides of the kink. Moving the gate to `>=` fails backward_input_gate on the lab. Two `!= undefined` tests over an undefined default_input() and two `then true` invariants are gone; the latter are NOT CHECKED notes. Lab (9f98d1a): 5/5. Refs #5083 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…f which exist forward_batch now writes a caller-owned output (lab-exec: UNDECLARED alloc, range). The three batch tests compared arrays with `==` and are per-index checks over fixture arrays; -0.05 and -0.01 compare with a tolerance (0.01 is not exact in f32). New finite-difference check of derivative on both sides of the kink: making the negative branch return 1.0 fails it and derivative_negative_input on the lab. Four `then true` invariants -> one assert on DEFAULT_ALPHA + a NOT CHECKED note. Lab (9f98d1a): 10/10. Refs #5083 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This was referenced Oct 5, 2026
backward computed grad_output[i] * p[i] * (1 - p[i]), which drops the -p[i] * p[j] cross terms and ignores the temperature. The vector-Jacobian product of p = softmax(z / T) is p[i] * (g[i] - sum_j g[j] p[j]) / T. The only backward test asked for `!= 0.0`. New finite-difference tests of L(z) = sum g[i] p[i] at T = 1 and T = 2: with the old formula the lab reports |grad - slope| = 0.022 and 0.039; with the VJP they pass. forward: range()/math::exp did not exist (lab-exec UNDECLARED); now while loops and @exp. Tests: values of softmax([1,2,3]), shift invariance at logits ~1000 (the max subtraction), T = 2 equals halved logits. `then true` invariants -> one assert on MIN_TEMP + a NOT CHECKED note. Lab (ce57702): 5/5. Refs #5083 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This was referenced Oct 5, 2026
…ng, gradient of forward
sigmoid was a rational returning 3.146 at 0; log_approx scored 0 for every
p < 0.5; the probability gradient had the wrong sign on its (1-t) term;
forward added epsilon instead of clipping. Reduction restored as
enum { MEAN, SUM, NONE } from trinity specs/algo/binary_ce.tri.
Tests on values, symmetry, saturation and central differences; a sign
mutation of the logits gradient fails. Three tests run FALSE on the lab
because the Zig backend emits -(a + b) as -a + b: reported as #6549, not
dodged.
Refs #5083
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…again The .tri -> .t27 port kept only the first parameter and returned void, so each forward computed a number and discarded it; KL summed p log p and ignored q; tests asserted result != undefined. Signatures and formulas restored from trinity specs/algo/*.tri. Tests use published values, identities (KL >= 0, asymmetry; Huber continuity at delta), and a central difference for MSE backward. One mutation per spec turns lab-exec FALSE. Lab: mse 3/3, huber 4/4, kl 4/4, contrastive 4/4. Refs #5083 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ir .tri sources Each port kept a placeholder body: rmsprop squared grad[0] and dropped it, adam only checked finiteness, adagrad called range/len/sqrt that do not exist, sgd added weight_decay*params (growing the weights) and ignored nesterov. Bodies now follow trinity specs/algo/*.tri with caller-owned buffers. Tests are checked against hand-computed values: Adam's first step is lr*sign(g) and its second step is worked by hand, Adagrad steps shrink as 1/sqrt(n), the RMSprop cache is a moving average, and SGD Nesterov matches PyTorch's form (the .tri nesterov counts the momentum twice; not followed, noted in the spec). Lab: 15/15 pass; one mutation per spec turns it FALSE. Refs #5083 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…tri sources Refs #5083 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This was referenced Oct 5, 2026
This branch has not been deployed
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.
Closes #5083.
Overnight autonomous loop (charter:
docs/loop/auto-2026-09-29/README.md). This PR carries the loop's landing work and grows commit-by-commit as 15-minute iterations complete; each iteration report lands indocs/loop/auto-2026-09-29/iterations/.Iteration 01 (in this PR now)
loop/auto-2026-09-29off master 2925def, remote mutextri loop claim auto-2026-09-29held, safety constitution (never on master / no force-push / reds may only shrink / no mass reseal).baseline.md): 148 corpus reds; the reframe finding — parser error recovery discards and continues:parse-no-discard114 specs (worstternary_inference1813 tokens),no-vacuous-invariant65 specs (invariants that check nothing),parse23 refused.competitors-2026-09-29.md): Vericert line, Sep-2026 BitNet-on-CGLA ternary hardware, Verilator/Yosys discipline — mapped to our gaps.docs/README.mdmap:docs/loop/registered (DOCS-TREE).Planned in following iterations (see
plan.md)tri unparsedprobes; make the parser fail loudly or accept the construct)verilog_bench_harness.t27(specs/test_framework/verilog_bench_harness.t27 is truncated: parse fails at line 172 (born in #1399) #5079).tricodegen: refuse loudly instead of emitting garbaget27cunknown-flag rejection (the--out/accident)Not in this loop: merging #5078/#5081 (owner's), the lean yml gate (#5082, workflows scope), any mass reseal.
🤖 Generated with Claude Code