Skip to content

Source annotations: post-module header attachment law; finish M1C-1 jwt/self-application binding - #7977

Merged
briansrls merged 9 commits into
mainfrom
session/quick-tern-444-m1c1
Aug 7, 2026
Merged

briansrls merged 9 commits into
mainfrom
session/quick-tern-444-m1c1

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 7, 2026 •

Copy link
Copy Markdown
Contributor

Follow-on to #7955, closing the module-header attachment defect found by review 49881 (and re-found on this branch by reviews 49976 and 50039): the module-level prose that M1C-1 self-applied was placed where the documented binder law binds it to the first module member, not the module.

What this PR does

Attachment law — post-module header blocks now bind to the module, structurally.

  • A // block on the line immediately after the module declaration, ending before the first module item, attaches to the module. A blank line after the module line opts out: the block then follows the ordinary nearest-following rule (witnessed both ways).
  • Two new facts are observed at capture (the same pattern, and the same reason, as the existing preceded_by_blank_line): preceded_by_annotation_line — the previous line is itself a standalone annotation line — and module_root on the subject roster — the realization declares which subject IS the module rather than the fold guessing it structurally.
  • Block continuation is now structural: a block's subject is decided by its first line; continuation lines merge by observed adjacency (pending_adjacent in the attach fold), and a continuation of a refused line falls back to being judged on its own rather than riding into an older open block.

Why not the smaller fixes reviews proposed. Review 50039 suggested dropping the + 12 byte window alone; executed evidence refutes that: with the bare removal, the adjacent second line of a blank-separated block below the module falls into the gap arm and splits the block (w_adjacent_comment_lines_form_one_block goes red). The + 12 window itself was the smuggled-heuristic class DESIGN §5 forbids — it under-covered long dotted module names and only masked the continuation bug when the module name was short. Identifying the module as "earliest subject by span start" was the same class one level up: the synthetic attachment fixture (gamma between f and g) proves any roster whose earliest subject is an ordinary member would misbind. Both heuristics are replaced by declared/observed facts.

jwt.dag layout fixed. The blank line between module extdeps.auth.jwt and its module annotation is removed, so the migrated verification-boundary prose actually binds to the module under the law above.

Witness coverage (v1_annotation_binding_test, 16 executing witnesses): single-line and multi-line post-module headers, module-name-length independence (the exact shape the + 12 window under-covered), blank-separated opt-out, two-line body block refusing both lines, plus all pre-existing M1A behavior. The subject-map receipt (tools/m1c1_subject_map_receipt.txt) is regenerated by execution over the real files — the previous receipt was hand-authored and its MODULE rows were false on main.

Suites run

  • v1_annotation_binding_test — 16/16 PASS (recipe in-file)
  • v1_annotation_round_trip_test, v1_annotation_capture_test, v1_annotation_erasure_test, v1_annotation_target_emission_test, source_annotation_attachment_witness_test — 15/15, 6/6, 9/9, 1/1, 11/11 PASS
  • regen_stage0 --verify — divergence 0 (seed regenerated from the edited .dag)

gunbc-ci-auto-heal and others added 7 commits August 7, 2026 00:05
Move the deferred jwt registered-claims and verification-boundary prose
into leading // annotations (module-level for the verification boundary),
migrate stable WHY prose in source_annotation, annotation_bind, and the
round-trip witness to authored annotations, update the prose audit state,
and regenerate stage0 to fixed point.

Co-authored-by: Cursor <cursoragent@cursor.com>
Keep `):\n    ` and `\n    if ` on one comment line so the depicted
lexeme strings stay readable after migration from escaped string literals.

Co-authored-by: Cursor <cursoragent@cursor.com>
The module verification-boundary annotation no longer claims a decoder
sits above it; the syntax-only caveat now leads jwt_string_or_uri_of_wire
with wording accurate at that declaration.

Co-authored-by: Cursor <cursoragent@cursor.com>
Re-add the describe-not-verify / hand-authored migration paragraph as
leading // annotation prose above the render helpers.

Co-authored-by: Cursor <cursoragent@cursor.com>
Pre-declaration annotations moved the module keyword off line 1, which
tripped the fail-closed diff-before-first-declaration gate in discovery
corpus selection. Restore `module` as the first line and place migrated
prose immediately after it (or above its original subject).

Co-authored-by: Cursor <cursoragent@cursor.com>
Move each // block to its intended structural subject, retain lifecycle facts in typed data rows, widen prose_row_migration_scope to the three self-applied paths, reconcile audit slice status, enroll the full 11-test binding roster, and regen stage0 to fixed point.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls
briansrls marked this pull request as ready for review August 7, 2026 04:51
Brian Searls and others added 2 commits August 7, 2026 05:07
… jwt.dag layout fixed

Closes the defect from review 49881 (re-found by 49976/50039): module-level
prose migrated by M1C-1 bound to the first module member, not the module.

The law: a // block on the line immediately after the module declaration,
ending before the first module item, attaches to the module; a blank line
after the module line opts out into the ordinary nearest-following rule.
Two heuristics in the draft arm are replaced by declared/observed facts:

- preceded_by_annotation_line is observed at capture (same pattern and
  reason as preceded_by_blank_line); the gap arm fires only on block-initial
  captures, and block continuation is structural: a block's subject is its
  first line's subject (pending_adjacent in the attach fold), with a
  continuation of a refused line judged on its own.
- The +12 byte window is deleted. Executed evidence shows the bare removal
  reviews proposed is insufficient: the adjacent second line of a
  blank-separated block below the module then splits the block
  (w_adjacent_comment_lines_form_one_block red). The window itself
  under-covered long dotted module names and masked the continuation bug
  only when the module name was short.
- The module is no longer guessed as earliest-subject-by-start: the roster
  declares module_root (the synthetic attachment fixture proves the guess
  misbinds when the earliest subject is an ordinary member).

jwt.dag's blank line before its module annotation is removed so the migrated
verification-boundary prose binds to the module; annotation_bind.dag's two
blank-separated header paragraphs merge into one adjacent block for the same
reason (the executed receipt caught the second paragraph binding to an
import).

Witnesses: v1_annotation_binding_test grows to 16 (multi-line module header,
name-length independence, blank-separated opt-out, two-line body block);
round-trip 15/15, capture 6/6, erasure 9/9, target-emission 1/1, synthetic
attachment 11/11, all by execution. tools/m1c1_subject_map_receipt.txt is
regenerated BY EXECUTION over the real files (the prior revision was
hand-authored and its MODULE rows were false). regen_stage0 --verify at
divergence 0.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot changed the title M1C-1: self-apply source annotations and finish the JWT module Source annotations: post-module header attachment law; finish M1C-1 jwt/self-application binding Aug 7, 2026
@gunbai-bot

gunbai-bot Bot commented Aug 7, 2026

Copy link
Copy Markdown
Contributor Author

Addressing the three module-header attachment reviews together, all fixed at head 1c7244748a:

  • review 49881 (M1C-1: self-apply source annotations and finish jwt.dag #7955) and review 49976: confirmed and fixed. The migrated module prose did bind to the first member. The receipt that claimed MODULE bindings was hand-authored; it is now produced by execution (see the header of tools/m1c1_subject_map_receipt.txt), and the executed run also caught one more instance the reviews missed — annotation_bind.dag's second header paragraph binding to an import — fixed by merging the paragraphs into one adjacent block.
  • review 50039: the + 12 window is removed, and the requested two-line post-module witness added (w_multi_line_module_header_stays_one_module_block). One correction to that review's analysis, established by execution rather than argument: dropping the window alone is not sufficient — with the bare removal, the adjacent second line of a blank-separated block below the module falls into the gap arm and splits the block (w_adjacent_comment_lines_form_one_block goes red; preceded_by_blank_line covers only the block's first line). The fix therefore adds an observed preceded_by_annotation_line bit and makes block continuation structural (a block's subject is its first line's subject). The review's own framing — a heuristic where a grounded bound exists — also applied to identifying the module as earliest-subject-by-start, so the roster now declares module_root instead.

Binding suite 16/16, round-trip 15/15, capture 6/6, erasure 9/9, target-emission 1/1, synthetic attachment 11/11, regen_stage0 --verify divergence 0.

— sent from fierce-pike-375

@briansrls
briansrls merged commit 47bc833 into main Aug 7, 2026
5 checks passed
@briansrls
briansrls deleted the session/quick-tern-444-m1c1 branch August 7, 2026 16:03
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