You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Source recovery was the only partial-decoder contract. A retained pair can answer a query while losing source distinctions, so this change adds query-relative recovery and states the additional success-to-image obligation separately. Query agreement with any compatible source follows from adequacy; unrestricted image-decision extraction would decide every small type.
The observer laws characterize release invariance on generated pairs under an explicit result observer and source relation. Examples separate redacted and transparent results, and distinguish arbitrary-request status differences from private-source leakage. Residue sufficiency uses total simulation relative to already visible information: retaining the query is least sufficient in that semantic preorder. This makes no bit-cost, runtime, cryptographic or new-type-primitive claim.
Validation:
Agda 2.6.4.3: all 31 source modules, 24 intended semantic rejections, five new valid-prefix controls and four mutation controls passed locally.
The exact 23-span warning allowance and canonical Echo pins are unchanged. Checked native source/script hashes match the published worktree.
Hosted Proof Safety run 42394791959 passed both core/rejection and canonical Echo correspondence jobs on signed head 0a2005007f45b347b9aa102a3f99243265527c1e before this PR was opened.
An independent source review removed a redundant success premise and narrowed the arbitrary-request example's interpretation. It is separate from kernel validation.
Full scope and proof ledger: docs/query-recovery.adoc and PROOF-STATUS.adoc. Ordinal work is excluded.
No actionable comments were generated in the recent review.
Summary
Summary by CodeRabbit
New Features
Added formal support for query-relative recovery, observer safety and the sufficiency of retained information, with examples covering their guarantees and limitations.
Documentation
Added an overview of the new concepts and updated verification totals to 31 modules and 24 expected rejections.
Tests
Expanded checks to cover five additional invalid constructions and confirm that valid prefixes compile.
The change adds Agda definitions and examples for query recovery, observer safety and residue sufficiency. It adds expected-rejection fixtures and updates module inventories, validation checks, documentation and proof-status records.
Defines query recovery using retained observation and residue, then relates it to query constancy, image decisions, partial recovery and migration. Examples cover recoverable queries, constant queries and the limits of successful-answer soundness.
Defines relative residue reduction, its reflexive and transitive constructions, and its relationships to migration. Examples compare Boolean representations and show that silent visibility cannot supply a Boolean bit.
Corpus integration and receipts src/EpistemicTypes/All.agda, tests/check-policy.sh, tests/check-rejections.sh, README.adoc, PROOF-STATUS.adoc, docs/query-recovery.adoc
Adds the six modules and five fixtures to the inventories. The rejection check validates each new fixture’s prefix before its expected-rejection marker. The README and proof-status records report the expanded counts and local verification details.
hyperpolymath/epistemic-types#44: Records the prior non-interference boundary that this change addresses with scoped observer-safety definitions and proofs.
Merge Risk: Minimal · up to 0a200
No concrete issue remains that would prevent merging after normal checks.
Pre-merge checks: 5
Check name
Status
Explanation
Title check
The title identifies the three main additions: query recovery, observer safety, and relative residue sufficiency.
Description check
The description accurately covers the main additions, examples, tests, and stated scope.
Docstring Coverage
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentat…
Linked Issues check
Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check
Check skipped because no linked issues were found for this pull request.
Full details: Docstring Coverage
Explanation
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentation-only edits and deletions within surviving functions are included; unchanged diff context and fully deleted functions are excluded. Analyzed 0 functions across 2 files. (15 skipped: 15 unsupported.)
Finishing Touches
Generate docstrings
Commit to this branch
Create a new PR
Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.
Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review.
Recent review details
Context from checks skipped due to timeout: 1
GitHub Check: CodeRabbit
Additional comments: 13
src/EpistemicTypes/QueryRecovery.agda: 1
1-128: LGTM!
src/EpistemicTypes/QueryRecoveryExamples.agda: 1
1-87: LGTM!
tests/reject/QueryIgnoresCollision.agda: 1
1-23: LGTM!
tests/reject/QuerySuccessInventsSource.agda: 1
1-23: LGTM!
docs/query-recovery.adoc: 1
1-124: LGTM!
README.adoc: 1
12-14: LGTM!
Also applies to: 235-235
src/EpistemicTypes/ObserverSafety.agda: 1
1-71: LGTM!
src/EpistemicTypes/ObserverSafetyExamples.agda: 1
1-73: LGTM!
tests/reject/ObserverRevealsSecret.agda: 1
1-19: LGTM!
tests/reject/OffImageStatusHidden.agda: 1
1-22: LGTM!
src/EpistemicTypes/ResidueSufficiency.agda: 1
21-25: LGTM!
Also applies to: 27-29, 31-37, 41-45, 47-50, 54-57, 59-62, 65-72
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
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.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Source recovery was the only partial-decoder contract. A retained pair can answer a query while losing source distinctions, so this change adds query-relative recovery and states the additional success-to-image obligation separately. Query agreement with any compatible source follows from adequacy; unrestricted image-decision extraction would decide every small type.
The observer laws characterize release invariance on generated pairs under an explicit result observer and source relation. Examples separate redacted and transparent results, and distinguish arbitrary-request status differences from private-source leakage. Residue sufficiency uses total simulation relative to already visible information: retaining the query is least sufficient in that semantic preorder. This makes no bit-cost, runtime, cryptographic or new-type-primitive claim.
Validation:
0a2005007f45b347b9aa102a3f99243265527c1ebefore this PR was opened.Full scope and proof ledger:
docs/query-recovery.adocandPROOF-STATUS.adoc. Ordinal work is excluded.