Skip to content

Integrate source-pinned binding, routing, and proof fixes - #4

Open
MauScheff wants to merge 47 commits into
mainfrom
codex/fix-effect-owner-synthesis
Open

MauScheff wants to merge 47 commits into
mainfrom
codex/fix-effect-owner-synthesis

Conversation

@MauScheff

Copy link
Copy Markdown
Owner

Problem and outcome

Integrate the 45 tested RMS maintainer fixes and one formatting-only integration commit. These fixes remove false native binding refusals without granting unchecked authority, and keep incomplete evidence inconclusive.

Review scope

Rust and Swift exact source/call resolution; closed envelope projection flows; source-pinned retained structural compatibility; owner-local routing and authority preflight; proof budgets; temporal unknown propagation; fault-schema discovery; inert typed-rejection resource custody.

Compatibility and state space

Existing bindings retain their prior default. New envelope-flow and retained-structural declarations are explicit opt-ins. Older binaries reject new declaration fields. No consumer product files or provider settings change. New analyzer modules own bounded source decisions; ambiguity and unsupported syntax remain refusal paths. Reference and schema fixtures cover the new binding choices.

Validation

Previous candidate: 936 native unit tests and 11 CLI tests passed; seven optional tests ignored. Integration formatting check passes. A clean native rebuild and all repository CI jobs are required before merge. CI includes cross-platform behavioral contracts, Python bindings, cvc5 conformance, and the exhaustive strict-audit test.

Migration

No mandatory migration for existing bindings. New opt-in declarations require the updated RMS CLI. Formatting is isolated in the final commit.

Recognize callback-free String UTF8 comparisons through concrete parameters and stored-string forwarding fields. Follow statically declared allSatisfy predicates instead of treating them as open dispatch. Keep custom receivers, getters, overloads, shadowing, and effectful callbacks fail-closed. Native proof: 883 unit tests and 11 CLI tests pass; 3 opt-in tests ignored. Read-only SecureMediaSession effect analysis passes. No product or guidance changes.
Recognize conventional package target directories without exempting tracked files or ordinary source directories named target. Fail closed when Git cannot identify tracked inputs. Native proof: six focused production guard tests, 884 unit tests, and 11 CLI tests pass; three opt-in tests ignored. No product audit rerun or product edits.
Treat trait-object receivers as dynamic, refuse ownerless dotted-call body guesses, and retain proven optional/text/iterator-position payload types. Preserve exact named-variant purity rejection and add closed-import and shadowing regressions. Native proof: 900 unit tests and 11 CLI tests pass; 3 unit tests remain ignored. Consumer signature and remaining authority gates stay strict.
Preserve default exact-envelope bindings. Add opt-in source-owned context split/observe/dispatcher proof with canonical identity fields and effect-to-executor mapping, exact status operations, closed constructor and callable references, and fail-closed unsupported syntax. Retain independent IO, scheduling, atomicity and native gates.

Native proof: 906 unit tests and 11 CLI tests pass; 3 existing unit tests remain ignored. Includes schema/mutator round-trip, forgery/alias/shadowing/duplicate-call negatives, synchronous and persistent fixtures, and a compiled native identity/allocation replay. The unmodified consumer still has 12 exact-envelope signature blockers and no authority blockers.
Extend the existing explicit owner-local machine-binding recovery path for only the exact old EffectEnvelope request signature failure. Preserve all other closed-flow, authority, schema, revision and unrelated-error blockers. Recognize explicit binding adoption, document fresh receipt discipline, and retain machine-only mutation authority and final conformance gates.

Native proof: red eligibility regression; 907 unit tests passed, 3 existing ignored; 11 CLI tests passed. No consumer or model-default changes. No new route state or bypass flag.
Use the existing semantic owner-scope predicate for machine-binding recovery eligibility. Keep root, intent and selected-owner errors blocking, retain unrelated module debt as visible evidence, and add scoped negative regressions. No new route state, exemption flag, canonical authority family, or proof relaxation.

Native proof: scope red/green regression; final 907 unit tests passed, 3 existing ignored; 11 CLI tests passed. Consumer source, canonical artifacts and model defaults unchanged.
Accept only built-in unqualified doc attributes on explicit unaliased imports and re-exports. Keep conditional/custom attributes, aliases, globs, ambiguity and all flow provenance checks closed. Preserve exact import spelling, file-level scope and cause through closure, derive and macro refusals. Document the supported form.

Native proof: two red regressions; 8 focused envelope-flow tests; native compiled identity/allocation replay retains doc(hidden); final 909 unit tests passed, 3 existing ignored; 11 CLI tests passed. No consumer source, canonical artifact, model/default or visibility edits.
Permit alignment only for structurally valid persistent-async drivers whose dynamic origins are registered poll or conformant executors. Preserve callback, resolution, purity, snapshot and declaration guards. Document two fresh receipts for row repair and subsequent semantic declarations. Native proof: 921 unit tests and 11 CLI tests passed; 3 existing tests ignored.
Retain local type annotations and source-created concrete future provenance across standard pins and boxes. Preserve body effects, nested opaque awaits, lifetime-only methods, ambiguous symbols and callback rejection. Accept inert built-in lint/layout attributes in closed glob export proof. Document the remaining foreign-facade declaration workflow gap. Native proof: 923 unit and 11 CLI tests pass; 3 existing tests ignored. Consumer read-only source audit preserves both real authority-row failures.

@MauScheff MauScheff left a comment

Copy link
Copy Markdown
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maintainer review complete for d795e29. No blocking finding in the reviewed source-ownership, lexical resolution, authority preflight, binding compatibility, routing, proof-budget, temporal-evidence, and resource-rejection changes. Exact provenance and conservative refusal boundaries remain. Formatting is isolated in the final commit and cargo fmt --all --check passes. Native rebuild and repository CI are still pending; this review does not authorize a merge until every required job passes. Use a merge commit to retain the existing source-pinned commit history.

@MauScheff

Copy link
Copy Markdown
Owner Author

Integration is blocked. Formatting-only commit d795e29 passes cargo fmt --all --check. Clean local native proof passed 936 unit tests and 11 CLI tests; all four native CI shards, both Python jobs, and cvc5 conformance passed. Linux structural validation failed after 21 minutes: proc-macro2 1.0.106 fallback.rs:469 panicked with attempt to add with overflow (exit 101). That line advances the thread-local source-map u32 span offset. Local profiling independently shows repeated syn::parse_file work through RustTypeIndex::external_path. The exact cause still needs a bounded reproducer, but repeated immutable-source parsing is the leading root cause. Duplicate local validation was stopped (exit 130), not claimed as passing, to preserve the coordinated heavy lane. No merge or installation occurred. Do not waive the failed gate.

@MauScheff

Copy link
Copy Markdown
Owner Author

Analyzer root-cause repair e0ae45a: each immutable RustTypeIndex snapshot owns its parsed files (including failed parses) and shares raw source and syntax across scope clones. Type queries and recursive exact symbol lookup borrow the same syntax rather than reparsing source. Existing ambiguity, malformed-source, metadata, and authority decisions remain. Deterministic red regression: 32 query rounds allocated 1,609,265 source-map positions before the fix; after the fix the less-than-128 bound passes, including recursive symbol lookups and scope clones. Focused five-test snapshot/summary group passes. Full native proof passes: 938 unit tests and 11 CLI tests; seven optional tests ignored. Formatting and local composition pass. Duplicate local structural validation advanced past source parsing to call analysis; it was stopped with exit 130 to avoid duplicating CI and is not claimed as passing. Fresh CI must pass all structural, solver, cross-platform, and exhaustive-audit jobs before merge. No main merge or installation yet.

@MauScheff

Copy link
Copy Markdown
Owner Author

Analyzer crash fix is pushed as e0ae45a. Local proof: 938 unit tests and 11 CLI tests passed; focused source-map regression and formatting passed. All four native CI shards and both Python jobs passed in run 38318763339. Linux structural validation completed without the previous proc-macro2 source-map overflow, but returned 119 errors and one warning. Error groups: 62 transitive-purity, 41 failure-discipline, 8 unresolved imports, 4 public-field checks, 2 undeclared Cargo dependencies, 1 undeclared import, and 1 missing semantic function. Concrete binding debt includes proc-macro2/tree-sitter-bash dependencies and run_verify now being cfg(test). Other findings require individual analyzer or implementation investigation; no blanket exemptions or authority-row changes have been applied. Merge and installation remain blocked. Installed revision remains 9a6c2f3. Remaining CI jobs may still be running. The next repair is broader than the bounded source-map crash fix.

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