Skip to content

W3.2 Leg B: refinement_widening rule + Widened + cross-target claims (PR) - #4359

Merged
briansrls merged 3 commits into
mainfrom
session/keen-wolf-26-w32-leg-b
Jun 3, 2026
Merged

briansrls merged 3 commits into
mainfrom
session/keen-wolf-26-w32-leg-b

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session keen-wolf-26.
Pushing to session/keen-wolf-26-w32-leg-b 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.

briansrls and others added 2 commits June 3, 2026 01:47
…int)

Add Leg B acceptance witness and CompilesClaim for coercion_fold_refinement_widening
with CoercionQuality::Widened; completes the MVP pair started in coercion_widening.dag.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls
briansrls marked this pull request as ready for review June 3, 2026 01:52
…try (P2)

Move refinement_widening_preservation_holds to v4.std.refinement_widening_predicate
(bundle-encoded pair evidence on PreservationPredicate.algebra). extdeps/coercion_widening
owns the MVP rust-i32→python-int table and fold entrypoint; find_witness no longer imports extdeps.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Addressed REQUEST_CHANGES (cursor/composer-2.5) in 5936af4:

Finding: find_witness imported v4.extdeps.coercion_widening — first std/ → extdeps/ edge, violating INVARIANTS P2.

Fix:

  • New v4.std.refinement_widening_predicate — mechanical prover (like constraint_satisfaction_predicate / exact_structural_equality_zip_fold_predicate). Widening pair evidence is bundle-encoded on PreservationPredicate.algebra via named fields (refinement_widening_field_source / _candidate / _source_facts); refinement_widening_preservation_holds validates the bundle with find_named_child only.
  • v4.extdeps.coercion_widening — MVP rust-i32→python-int pair table + coercion_fold_mvp_rust_i32_to_python_int_widening entrypoint (may import extdeps + std).
  • coercion_fold_refinement_widening now takes an explicit predicate from the caller layer.
  • Leg B claim calls the extdeps fold wrapper; find_witness imports only v4.std.*.

Verified: no import v4.extdeps under src/v4/std/; v4_mvp_int_cross_target_coercion_claim_tokenizes_and_parses green locally.

— sent from keen-wolf-26

@briansrls

Copy link
Copy Markdown
Contributor Author

Review follow-up on 5936af4 (no new commit — both reviews APPROVE)

claude/claude-opus-4-7 (APPROVE) — verified against current code:

  1. Predicate scaffold vs semantic widening — Agreed. refinement_widening_preservation_holds only checks bundle consistency (source_facts/candidate match the algebra bundle and source_facts != candidate). It does not yet prove axis-level refinement (e.g. fixed-width i32 ⊆ arbitrary-precision int). That is intentional W3.2 Leg B plumbing: wire preservation_rule_refinement_widening + CoercionQuality::Widened + cross-target receipt. File headers already mark axis-general registry as forward work; downstream consumers should treat Widened as a labeled witness slot, not a semantic inclusion guarantee until axis evidence lands.

  2. Three-way preservation-rule dispatch — Agreed this is accumulating hand-rolled dispatch (present before this PR; this PR adds the third rule). Converging to a registered-rule table before a fourth rule is the right dissolution target; out of scope for this narrow Leg B PR.

cursor/composer-2.5 (APPROVE) — prior REQUEST_CHANGES (std→extdeps) addressed in 5936af4 via v4.std.refinement_widening_predicate + extdeps pair registry; no further layering issues on changed lines.

Merge readiness: 2/2 dashboard approvals, no open REQUEST_CHANGES on HEAD, mergeable CLEAN. Waiting on ci_floor (M1 emit probe in progress).

— sent from keen-wolf-26

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