Repository navigation
Scope admitted equality context and preserve direct Integer roots - #490
Merged
Merged
Conversation
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
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.
The planned equality ABI currently requires an admitted nominal context even when classification or primitive reconstruction uses no nominal key. That blocks existing precise standalone admitted-IR refusals without adding identity safety. This amendment scopes the capability to actual use, while keeping explicit wrong-context rejection global.
Both standalone generation and generated preparation now take Option<&qsl_replay::AdmittedContext>. None permits context-free traversal and key-free refusals; every reached nominal reconstruction requires genuine context and otherwise returns typed MissingAdmittedContext. Some(wrong package) still fails before classification, even for primitives. Complete enum cases, private prepared binding/index, charged traversal/error/cycle order, sibling isolation and no-charge oracle faults remain required. A valid empty index means a successfully resolved zero-enum closure, never a failure fallback.
The same amendment clarifies only directly selected Integer operand/conversion-target roots: canonical base Integer remains unbounded despite another parameter’s range, while explicit integer_range uses its own interval. AC-16 member/base behavior and its exact regression stay unchanged; genuine record/tuple member-bound association and the QSL-937 owner-key gap remain unresolved. No new public descriptor field or guessed lexical ownership is introduced. Genuine asymmetric source evidence does not claim that an erased conversion produced a retained conversion node.
Native OriginalCompositeEqContext authentication is unchanged and mandatory: authentic source, original lock, package identities, strict IR read and full original-package equality before retained context exposure. Ordinary scalar proof manifests/bodies acquire no replay leg. The merged AC-14 intake-stage correction is unchanged. This remains planned behavior pending implementation and qualification, not completion of IR-17 or IR-705.
Validation: installed Quire validation passes all six changed documents; diff whitespace checks pass. Bounded advisor reports all six new method cells Test as catalogued, with no mismatch or inconclusive result. Programmatic checks confirm the native source-retaining interface and AC-8/14/16/26 rows are byte-identical. No Cargo, build, native execution or proof jobs ran.
Owning grounding: QSL FR-394 scopes the genuine declaration/case capability; QSL ADR-011 T12 prohibits backend key construction. IR FR-038 parameter typing retains the actual binder type; QSpec FR-149 equality conversions distinguishes bounded Int from unbounded Integer. The optional capability changes none of those authorities and does not itself authenticate source.
Final review custody: the eight independent review artifacts (SR-14720 through SR-14727) record PASS with no findings and are retained verbatim under the unique ir-17-context-scope names. The trailing custody commit changes review artifacts only; all six specification documents remain unchanged from the reviewed source. Explicit eight-path Quire validation and whitespace checks pass.
This PR remains documentation only. New AC-38 through AC-43 are planned implementation obligations, not implemented or executed acceptance evidence. No aggregate gate, Cargo job, native test or backend proof ran for this Markdown-only amendment. IR-17 and IR-705 remain in progress; the original full-library/native/proof qualification and the remaining owning capability work are not closed by this spec.