Skip to content

No-smuggled-programs HALF B (follow-on to #6589, same worker retains context): generalize medium_structure_containment per the signed design doc — grammar-as-classifier over string literals in substrate layers (composition of a modeled language = typed located COUNTED violation; atom = clean), count - #6637

Merged
briansrls merged 26 commits into
mainfrom
session/stern-eagle-53
Jul 15, 2026

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session stern-eagle-53.
Pushing to session/stern-eagle-53 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

Brian Searls and others added 7 commits July 14, 2026 21:01
…tion_justification (CI gate)

Two fixes:
1. Correctness (parent §5 catch): a parts-projection Hole is a .dag compose-time
   value spliced into the source string BEFORE bash parses it — NOT a bash-runtime
   $var (that is a literal ConstPart bash does not re-parse). An UNQUOTED Hole could
   itself be/complete a separator, so it is undecidable -> AmbiguousParse (T3), never
   assume-Clean. scan_part now sets hole_straddle when a Hole appears in unquoted
   context (quote_is_out); classify routes it AFTER P2 static-token composition
   (a Violation decided by real tokens stays Violation). Earnable escape: a QUOTED
   Hole is bounded (operators cannot apply inside quotes) -> Clean.
   Tests: rec_hole_arg_is_clean -> rec_hole_arg_unquoted_is_ambiguous; add
   rec_hole_quoted_is_clean and rec_literal_dollar_var_const_is_clean controls.
2. CI gate: v2.lens.bash_composition_recognizer had no construction_justification;
   added WallAfterGrounding{dissolves_to: RealizationDispatch} (marker heuristic ->
   grammar-derived classifier), mirroring the containing lens.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jul 14, 2026

Copy link
Copy Markdown
Contributor

Status guard (not abandoned — actively in progress): this is HALF B of the no-smuggled-programs wall. Landed so far: the grammar-as-classifier recognizer (bash_composition_recognizer.dag), the ingest-lex view addition, and 20 discriminator controls. Deliberately still DRAFT because (1) the CI floor is validating the discriminators by execution right now, and (2) the remaining HALF-B pieces — seed parts-projection (census.rs), lens wiring in medium_structure_containment.dag, fixtures, and Path A (path-exemption tighten + EAGAIN roster) — land into this same PR next. Will flip ready once the floor is green and the lens wiring is in. Please leave in draft.

Brian Searls and others added 8 commits July 14, 2026 22:15
# Conflicts:
#	src/v2/lens/medium_structure_containment.dag
…ExprRecordLit, add DecodeFidelity residue witness

- lens/recognizer notes: replace {ident} spans that .dag string-interpolation
  read as undefined variables (RawLine{text}/Heredoc{body}/{NoLanguageDecision}/
  {HoleStraddlesToken}) with plain prose (parent CI red run 29373614299).
- census producer: skip empty-parts facts (RawLine{text:""} fold sentinels have
  no program to classify); match-arm patterns (RawLine{text:t}=>) are
  MatchPattern::VariantPattern held in match_pattern, never walked, so excluded
  by construction (parent review check 1).
- new scanner/decode_fidelity_residue_test: assert ambiguous_count_live == 2
  (the 2 nbd_proxy_serve unquoted-Hole RawLines) && violation_count_live == 0,
  with the dissolution trigger (quote or type the holes -> Clean/Violation).
  Counted+reported residue, not a silent gap (DESIGN.md §5).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jul 14, 2026

Copy link
Copy Markdown
Contributor

Intentionally DRAFT — not abandoned. Parent (sharp-crane-105) set an explicit gate: mark ready only after a NON-VACUOUS floor receipt on this commit (8b31251), i.e. in the SAME run: clean_tree violation_count_live==0 GREEN, planted_leak RED (5 compositions), perturb_red green->red flip, lens_unit synthetic RED-on-5.2/GREEN-on-5.3, heredoc-ambiguous control, and the new DecodeFidelity residue witness (ambiguous_count_live==2). Floor run 29375341318 is in progress (~20min); will flip ready on green.

Brian Searls and others added 6 commits July 14, 2026 23:22
…rge)

The auto-committed merge (7e60dce) captured a bad lens resolution (kept BOTH
baseline=0 and the old baseline=60 roster). Correct it to the parent-approved
prune: exception_roster=[] baseline=0.

Main's #6629 migrated nbd_proxy_serve RawLine->modeled Command/ShellWord/Lit, so
the merged tree has ZERO RawLine.text/Heredoc.body literal sinks in scope — the
2 AmbiguousParse holes dissolved (the exact dissolution trigger the residue note
predicted). Updated:
- decode_fidelity_residue witness: assert ambiguous_count_live==0 (was ==2), with
  the dissolution recorded; stays a live ledger (new residue reds it).
- roster_prune_note: record nbd_proxy migration; roster==violating==EMPTY still
  honest, classifier still proven non-vacuous via fixtures + lens_unit controls.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review July 15, 2026 01:13
Brian Searls and others added 5 commits July 15, 2026 01:24
…ent lens

Review nit (claude/claude-opus-4-7 on #6637): the lens uses only
disposition_is_violation and disposition_is_ambiguous; disposition_is_clean was
imported but never referenced. Pruned. Verified the other 10 recognizer imports
are all used. No logic change.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Review finding (claude/claude-opus-4-7 on #6637, valid): the note claimed
'maximal-munch takes done over do', but do is spelled with a REQUIRED leading
space (" do") while done is "done", so at the d of done, do's spelling can never
be a prefix candidate — they do not collide at the same start position and no
maximal-munch arbitration between them occurs. Corrected the note to state the
actual mechanism (the leading-space boundary). Doc-only; no logic/emit change.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ledger notes

All 3 findings were advisory/non-blocking; addressed comprehensively:
- §2: quote_terminated and quote_is_out were byte-identical QuoteMode folds. Folded
  to the single quote_terminated predicate (read two ways: munch-termination at
  end-of-scan, unquoted-position at a Hole); deleted quote_is_out, rewired scan_part
  and hole_straddle_note. No behavior change (both were match q { QuoteOut=>true; _=>false }).
- §3: named the dissolution trigger for RawLiteralPartsFact.{constructor,field} — the
  in-band String discriminator becomes a typed sink COPRODUCT discriminant when the
  projection moves in-substrate (census.rs scaffold note).
- §5: added operand_framing_residue_note — backticks / dollar-paren / brace-groups fall
  through as OperandFraming (accidental-splicing threat model, acceptable per the reviewer);
  named so the residue is counted, not silent, with a widen-scope dissolution trigger.

Doc + a no-op §2 dedup; no logic/emit change.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Floor parse aborted at bash_composition_recognizer.dag:313 (expected item
declaration): the §2 dedup comment I added used // lines, but .dag supports
NO comment syntax (neither // nor #) — marks live in data _note String fields.
The dedup rationale is already carried by hole_straddle_note ('the same single
QuoteOut predicate the munch-termination check reads'). No logic change.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@briansrls
briansrls merged commit 7b149a5 into main Jul 15, 2026
2 checks passed
@briansrls
briansrls deleted the session/stern-eagle-53 branch July 15, 2026 02:50
briansrls added a commit that referenced this pull request Jul 15, 2026
…ry).

Proven by execution the type-level compile wall does NOT fire: neither v1 seed nor v2 04_infer typechecks fn-application arg types (04_infer carrier-checks only Branch/Match/Loop), so a raw String where TargetText is declared compiles clean (injected-smuggle gate = 0 diagnostics). Reframe from 'by construction, not lens-validated' to §5 wall-AFTER-grounding: typed seam; LIVE enforcement = HALF B composition-recognizer lens (#6637) + runtime .source guard; declared FRONTIER ROW, dissolution trigger = 04_infer application-argument typechecking (absent today; its absence leaves every type-based construction guarantee unenforced at the call boundary).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jul 15, 2026
…iteral may be an ATOM, never a COMPOSITION. Two halves, design doc FIRST then implement: HALF A construction — emit-seam output becomes a typed carrier (not String); only eliminators = whole-value render to artifact sink + grammar- (#6656)

* WIP: No-smuggled-programs wall (operator directive 2026-07-14): a string lite

* WIP A1: TargetText carrier (std) + bound_tokens carrier-native + concrete-token path + generic_apply/args type-expr (checkpoint, not yet compiling)

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* WIP: No-smuggled-programs wall (operator directive 2026-07-14): a string lite

* WIP: No-smuggled-programs wall (operator directive 2026-07-14): a string lite

* WIP: No-smuggled-programs wall (operator directive 2026-07-14): a string lite

* A1: correct scaffold-note enforcement claim (parent-directed, mandatory).

Proven by execution the type-level compile wall does NOT fire: neither v1 seed nor v2 04_infer typechecks fn-application arg types (04_infer carrier-checks only Branch/Match/Loop), so a raw String where TargetText is declared compiles clean (injected-smuggle gate = 0 diagnostics). Reframe from 'by construction, not lens-validated' to §5 wall-AFTER-grounding: typed seam; LIVE enforcement = HALF B composition-recognizer lens (#6637) + runtime .source guard; declared FRONTIER ROW, dissolution trigger = 04_infer application-argument typechecking (absent today; its absence leaves every type-based construction guarantee unenforced at the call boundary).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* WIP: No-smuggled-programs wall (operator directive 2026-07-14): a string lite

* WIP: No-smuggled-programs wall (operator directive 2026-07-14): a string lite

---------

Co-authored-by: Brian Searls <briansrls@gunb.ai>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls pushed a commit that referenced this pull request Jul 15, 2026
…6637)

The affected-set-falsifier has been red on every cold sweep since 2026-07-15
04:32 UTC (last green 07-14 23:10, run 29374839251). It was doing its job:
three discovery witnesses returned Bool(false) against the whole corpus that
per-PR selection had predict-skipped. This clears the two non_fold_residue
ones; the inert_carrier one is a separate lens-precision question, left red
deliberately rather than papered over.

Stale rows deleted (roster 120 unique -> live 118; each verified as genuinely
migrated, NOT merely gone lens-invisible -- the converge_cli_applied_knob_count
trap):
  - nbd_proxy_serve.dag::shell_command_leading_lit_text
  - nbd_proxy_serve.dag::shell_rawline_starts_with_tool
    both fns DELETED by #6629 (P6 Part 2: RawLine body -> typed session-lease
    effect), firing the dissolve-on their rows carried.
  - emit_host.dag::run_test_claim_emit_vs_eval_verdict
    fn still exists (emit_host.dag:335) but #6650 enumerated its wildcard into
    three explicit constructor arms -- residue genuinely folded, no bare `_ =>`
    remains. Ratchet tightens.

Unrostered row backfilled: bash_composition_recognizer.dag::apply_role, landed
by #6637. Two-special-variant dispatch over TokenRole's 5 variants; the other
three all reduce to the closed run, so enumerating would clone the general arm
3x. Same class as the orch_emit_let_step row above it (receipt #10).

Green-by-execution (claim_batch, local):
  PASS non_fold_residue_no_unrostered_or_stale (src/v2/lens)
  PASS non_fold_residue_clean_holds            (dag/test/claim)
  FAIL inert_carrier_no_unrostered_or_stale    <- unchanged, see PR body
Discriminating RED control: both nfr witnesses were red on this same tree
before the roster edit and green after; no witness or assertion was weakened.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jul 16, 2026
…; re-enroll cargo fmt in CI (de-fused from nextest) (#6691)

* WIP: falsifier is failing

* non_fold_residue roster: burn down 3 stale rows, backfill apply_role (#6637)

The affected-set-falsifier has been red on every cold sweep since 2026-07-15
04:32 UTC (last green 07-14 23:10, run 29374839251). It was doing its job:
three discovery witnesses returned Bool(false) against the whole corpus that
per-PR selection had predict-skipped. This clears the two non_fold_residue
ones; the inert_carrier one is a separate lens-precision question, left red
deliberately rather than papered over.

Stale rows deleted (roster 120 unique -> live 118; each verified as genuinely
migrated, NOT merely gone lens-invisible -- the converge_cli_applied_knob_count
trap):
  - nbd_proxy_serve.dag::shell_command_leading_lit_text
  - nbd_proxy_serve.dag::shell_rawline_starts_with_tool
    both fns DELETED by #6629 (P6 Part 2: RawLine body -> typed session-lease
    effect), firing the dissolve-on their rows carried.
  - emit_host.dag::run_test_claim_emit_vs_eval_verdict
    fn still exists (emit_host.dag:335) but #6650 enumerated its wildcard into
    three explicit constructor arms -- residue genuinely folded, no bare `_ =>`
    remains. Ratchet tightens.

Unrostered row backfilled: bash_composition_recognizer.dag::apply_role, landed
by #6637. Two-special-variant dispatch over TokenRole's 5 variants; the other
three all reduce to the closed run, so enumerating would clone the general arm
3x. Same class as the orch_emit_let_step row above it (receipt #10).

Green-by-execution (claim_batch, local):
  PASS non_fold_residue_no_unrostered_or_stale (src/v2/lens)
  PASS non_fold_residue_clean_holds            (dag/test/claim)
  FAIL inert_carrier_no_unrostered_or_stale    <- unchanged, see PR body
Discriminating RED control: both nfr witnesses were red on this same tree
before the roster edit and green after; no witness or assertion was weakened.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* WIP: falsifier is failing

* WIP: falsifier is failing

* Re-enroll cargo fmt in CI as a standalone step, de-fused from the nextest bundle

Operator ruling 2026-07-15. Restores fmt enforcement without re-enrolling
RustMonolithGate (still rejected).

WHY IT WAS GONE: tools.rust_gates_ci.run_gates welds two separable facts into
one ProcessExit -- fmt (4.3s measured, parse-only, no build, green) and nextest
(~37 GiB, compile+run, red on main). The 2026-07-11 ruling removed the bundle
for reasons that are ALL facts about nextest; fmt was collateral damage of that
fusion (DESIGN 3).

WHY THE HOOK ISN'T COVERAGE: the ruling's declared replacement was the pre-push
hook. That is an escape hatch (DESIGN 5) -- opt-in per clone via a manual
core.hooksPath, bypassable with --no-verify, absent in container worktrees --
and PROVEN ineffective, not just theoretically weak: in this very worktree
core.hooksPath points at a directory with no pre-push hook at all, and #6658
landed an unformatted .rs on main 2026-07-15 with nothing catching it. The hook
stays as fast local feedback, never as the wall.

SHAPE: standalone RunStep, FIRST in the build job -- a 4-second violation now
fails in 4 seconds instead of after the ~33min release build. build is not
protection-required itself, but ci needs:[build], so a red fmt blocks the
required job by construction. Toolchain already installs the rustfmt component
in ci_prelude_steps, so marginal cost is ~4s and no build.

Step-budget discipline (gunbc_ci_job_timeout_policy_disposition: "the backstop
is the exact step-sum + prelude"): the new step carries the aux cap and
gunbc_ci_build_job_backstop_timeout_minutes() gains exactly one aux term
(65 -> 70), so no step is uncapped and the sum stays exact.

Authority updated, not left lying: commit_gate_rust_suite_removed_disposition
declared "cargo fmt stays enforced by the pre-push hook". That claim is now
retracted in-row and the fmt half marked reversed; the nextest half and the
RustMonolithGate rejection are preserved verbatim.

ci.yml regenerated through the emit authority (expected_ci_yml), never hand-
edited; trailing-newline gotcha handled.

GREEN-BY-EXECUTION:
  PASS generated_artifact_drift_witnesses   <- the real drift gate, ci.yml byte-exact
  0 FAILs across ci_yaml_serializer, ci_compile_jobs, placement_grain,
    rust_gates_ci, ci_budget_tree witnesses
DISCRIMINATING RED: planted a fmt violation, ran the EXACT emitted step command
  -> exit 1 (caught); restored tree -> exit 0. The gate discriminates.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* Resolve merge conflict: drop duplicate nfr roster work, main landed it first

main (#6680 lane) independently made the identical nfr roster fix while this PR
was in review: same two nbd_proxy_serve stale rows deleted, same
emit_host::run_test_claim_emit_vs_eval_verdict stale row deleted, and the same
apply_role backfill added (its own wording, different position in the roster).

Resolution takes MAIN's side wholesale. Keeping mine would have produced two
apply_role rows -- harmless at use (the roster collapses to a BTreeSet) but a
pointless redundancy, and re-litigating identical work for authorship is not a
reason to diverge. cli_run.rs is now byte-identical to origin/main.

This PR therefore reduces to the work main does NOT have, verified against
origin/main:
  - the cargo fmt CI gate (de-fused from the nextest bundle) + its authority
    note amendment + regenerated ci.yml
  - the latent main fmt red fix (main still carries the unformatted import)

Independent convergence on the roster is a receipt for the falsifier itself:
two lanes hit the same cold-sweep reds and reached the same verdicts on which
rows were genuinely migrated vs still live.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* WIP: falsifier is failing

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant