Prove query recovery, observer safety and relative residue sufficiency

PROOF-STATUS.adoc

@@ -6,17 +6,24 @@
 
 [abstract]
 This is the current, source-anchored verification record for the Agda
-formalisation. The authoritative positive tree contains *25 source modules* and
-the negative-control manifest contains *19 expected-rejection fixtures*. The
-partial-recovery extension adds two modules and two fixtures to the preceding
-23-module/17-fixture corpus, retaining four isolated mutation controls. The
+formalisation. The authoritative positive tree contains *31 source modules* and
+the negative-control manifest contains *24 expected-rejection fixtures*. The
+query/observer/sufficiency extension adds six modules and five fixtures to the
+preceding 25-module/19-fixture corpus, retaining four isolated mutation controls. The
 source is constructive, builtins-only, map-only at its base interface, and has
 no postulates or proof escape hatches. Exact theorem scope and trust boundaries
 are recorded below; historical snapshots remain in `AFFIRMATION.adoc` and are
 not current inventory.
 
 == Status vocabulary
 
+The query/observer/sufficiency extension is locally *AGDA-VERIFIED*: 31 source
+modules, 24 semantic rejections, five new valid-prefix controls, four mutation
+controls and the unchanged exact 23-span warning allowance passed under Agda
+2.6.4.3. Its exact assumptions and verification scope are in
+link:docs/query-recovery.adoc[]. The following partial-recovery receipt applies
+to the preceding corpus and is not a receipt for the new six modules.
+
 The partial-recovery extension is locally *AGDA-VERIFIED* by the complete
 Agda 2.6.4.3 core gate: 25 source modules, 19 intended rejections and four
 mutation controls, with the existing exact 23-span warning manifest unchanged.
@@ -92,7 +99,7 @@ its 23 existing warning spans are checked separately against the exact manifest
 in `tests/check-proofs.sh`. A new, moved, or stale location fails the gate. The
 safe proofs check, but no Cubical transport-computation claim is made for those
 indexed eliminations, including `Kripke.Belief.believed`. The policy gate also
-compares all 25 source modules, 19 rejection fixtures, and four integration
+compares all 31 source modules, 24 rejection fixtures, and four integration
 witnesses with exact path manifests; rejects additional `OPTIONS` pragmas, proof
 escape hatches, and non-core imports; and verifies a generated negative
 control: `--safe` must reject a planted postulate with Agda's expected
@@ -254,10 +261,10 @@ external runtime or an unlisted mathematical correspondence.
 | Documentary comparison only; no imported owning definition
 
 | C-1
-| Every one of the 19 intended-invalid constructions is rejected for its
+| All 24 intended-invalid constructions are rejected for their
   enumerated semantic type mismatch. This is negative-control evidence, not a
   positive theorem.
-| TESTED
+| TESTED — local receipt 2026-11-07; five new valid prefixes also accepted
 | `tests/check-rejections.sh`, `tests/reject/*.agda`
 
 | C-2
@@ -294,6 +301,29 @@ external runtime or an unlisted mathematical correspondence.
 | PROVEN — local receipt 2026-11-07
 | `PartialRecovery.agda`; link:docs/partial-recovery.adoc[exact assumptions]
 
+| QR-1
+| Query recovery implies fibre constancy; an explicit image decision and
+  constancy construct a decoder. Success-to-image evidence supplies the
+  converse image decision; compatible-source query agreement follows from
+  adequacy. Universal extraction without that evidence would decide every Set.
+| PROVEN — local receipt 2026-11-07
+| `QueryRecovery.agda`, `QueryRecoveryExamples.agda`
+
+| OS-1
+| For generated pairs and a supplied result observer/source relation,
+  noninterference is equivalent by implications to release invariance.
+  Transparent full recovery forces related sources equal. Arbitrary visible
+  requests can have different success statuses; this is not private leakage.
+| PROVEN — local receipt 2026-11-07
+| `ObserverSafety.agda`, `ObserverSafetyExamples.agda`
+
+| RS-1
+| Total residue simulation relative to visible data is a preorder. The query
+  residue is adequate and least among residues admitting total Migration for
+  that query. Stronger residue preserves adequacy. No bit/cost bound follows.
+| PROVEN — local receipt 2026-11-07
+| `ResidueSufficiency.agda`, `ResidueSufficiencyExamples.agda`
+
 | C-4
 | The local retained-pair image is definitionally canonical `Echo` of the
   retained-pair function. Conversions preserve the source and equality path;

README.adoc

@@ -9,6 +9,10 @@ image:https://img.shields.io/badge/OpenSSF-BestPractices-green[link="https://www
 
 Constructive Agda prototype for standpoint-indexed epistemic modalities, separating knowledge, belief, and warrant, with proof transport sound relative to an explicit claim meaning.
 
+The link:docs/query-recovery.adoc[query-recovery extension] distinguishes answering
+a query from recovering its source, states observer safety for generated inputs,
+and characterises sufficient residue relative to already visible information.
+
 == Overview
 
 When an agent observes a fact, the type of their access matters. Knowledge is factive; belief is not. A warrant records evidence without assuming soundness. Proof transported across a boundary becomes a receipt; a receiving proof requires a successful sound check of the receiver's claim meaning.
@@ -228,7 +232,7 @@ This is a prototype, not a complete epistemic logic. The following are **intenti
 
 [source,bash]
 ----
-just check  # policy guard + 25 positive modules + 19 expected rejections + 4 mutation controls
+just check  # policy guard + 31 positive modules + 24 expected rejections + 4 mutation controls
 ----
 
 `just check` calls `scripts/check.sh`: it uses a local `agda` when one is on

docs/query-recovery.adoc

@@ -0,0 +1,124 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Query recovery, observer safety and sufficient residue
+:revdate: 2026-11-07
+
+This extension distinguishes answering a query from recovering its entire
+source. It reuses `Retention`, `Migration`, and the existing partial-recovery
+image. All carriers are `Set`; image witnesses remain proof-relevant and
+untruncated. No choice, automatic image decision, quotient, proof irrelevance,
+function extensionality or runtime secrecy property is assumed.
+
+== Query-relative recovery
+
+`QueryRecovery C q` has a pair-only `answer : B -> R -> Maybe T` and an
+adequacy law: every generated pair answers `just (q x)`. The decoder does not
+receive a source, `Case`, or consistency witness as input. Off-image behaviour
+is unconstrained by this law.
+
+[cols="1,3",options="header"]
+|===
+|Declaration in `QueryRecovery.agda` |Exact obligation/result
+|`queryConstant`, `queryComplete`
+|An adequate query agrees on every retained-pair fibre and answers any supplied
+image witness's query correctly. This does not implement a search for that witness.
+|`sourceToQuery`, `identityQueryToSource`
+|Full-source partial recovery answers every supplied query. An identity-query
+decoder recovers the source. General query recovery is weaker.
+|`migrationToQuery`, `queryToMigration`
+|Total Migration gives query recovery; an explicit target fallback totalizes a
+query decoder. The fallback is target data, not a source or an assumed inhabitant.
+|`successfulQueryAgrees`
+|Success agrees with the query of any compatible source, by adequacy alone.
+|`QuerySuccessSound`
+|The additional obligation supplies an actual image witness for each success.
+An extra query-equality field would be redundant by the preceding theorem.
+|`soundQueryDecidesImage`
+|This additional success obligation yields an explicit image decision. Failure
+refutes every image witness using adequacy.
+|`fromQueryImageDecision`, `queryImageDecisionSound`
+|Constancy on fibres plus an explicit image decision constructs a query decoder
+with the additional success obligation. These are constructive implications,
+not equalities of functions, records or proof fields.
+|===
+
+`QueryRecoveryExamples.agda` recovers a nonconstant first-bit query while the
+second bit is lost, and proves that full-source recovery is impossible for
+the same retention. A constant query needs no image decision and can succeed
+off-image, so success alone supplies no compatible source. The stronger
+`unrestrictedExtractionDecidesEveryType` is a constructive reduction: an
+extractor from arbitrary query recovery to image decision would decide every
+small type. It does not postulate that extractor or claim a formal independence
+theorem. The finite off-image example alone would not prove undecidability.
+
+== Observer safety
+
+`ObserverSafety.agda` defines `ObservationNI` for an explicit deterministic
+observer of the entire `Maybe T` result, on generated retained pairs and a
+supplied source relation. No equivalence laws for that relation are assumed.
+`releaseInvariantToNI` and `niToReleaseInvariant` relate this property to
+invariance of the observed released query. A transparent result observer forces
+equal query values; a transparent full-source result forces related sources to
+be equal. `hiddenPairForcesQueryAgreement` separately requires equality of the
+actual visible/residue pair; equal visible projections alone do not suffice.
+
+The positive example retains a second bit privately and publishes only the
+first bit of the recovered source. That public observation respects the
+first-bit source relation. Publishing both bits violates it. This is a theorem
+about the explicit result observer, not a claim that the raw input pair, logs,
+timing, memory, certificates or private residue are inaccessible at runtime.
+
+The arbitrary-request example distinguishes a generated request's success from
+an unreachable request's failure even for a constant query. The two requests
+are caller-selected and visible. This demonstrates the limit of the
+generated-input theorem; it is not itself a private-source confidentiality
+breach. A security theorem for arbitrary requests needs its own relation and
+observation contract. Neither this result nor the separate Secret Types
+fuelled-outcome counterexample establishes probabilistic or cryptographic secrecy.
+
+== Residue sufficiency
+
+`RelativeReduction f r s` means that an explicit total simulator reconstructs
+`r x` from `(f x, s x)`. Its law holds on generated inputs. Reflexivity and
+transitivity give a semantic preorder relative to the already visible `f`.
+
+`queryResidueAdequate` shows that retaining the query itself is sufficient.
+`queryResidueLeast` turns any adequate total Migration into a reduction from
+its residue to that query; `reductionToMigration` provides the converse field
+construction. Thus the query residue is least sufficient in this stated
+preorder. `migrateWithMoreResidue` preserves adequacy when additional residue
+can simulate the old one.
+
+`replaceResidue` uses a trivial certificate to expose the capability result;
+it does not transport the original certificate or claim authenticity.
+The examples show mutually simulating single and duplicate Boolean encodings,
+and that a unit residue can suffice when the visible value already supplies
+the answer but fails when visibility is constant. No minimum bit count, byte
+layout, time, cost, unique carrier, or partial-map preorder follows. Query
+minimality here is a factorization statement, not a new compression theorem.
+
+== Validation and ownership
+
+The complete four-entrypoint gate passed locally with Agda 2.6.4.3 on
+2026-11-07: `tests/check-policy.sh`, `tests/check-proofs.sh`,
+`tests/check-rejections.sh`, and `tests/check-approval-seal-mutations.sh`.
+These are the entrypoints composed by `bash scripts/check.sh`. They checked
+31 source modules, 24 intended semantic rejections, five new valid-prefix
+controls, and the existing four mutation controls.
+The existing exact 23-span warning allowance is unchanged. The four canonical
+Echo integration modules and their source pins are unchanged; their historical
+receipts remain in `partial-recovery.adoc`.
+
+The source and gates were copied byte-for-byte to an isolated ext4 directory
+because WSL startup and the mounted workspace were intermittent. A persistent
+WSL session completed the checks. The missing diagnostic matcher was supplied
+by a user-local extraction of Debian's authenticated `ripgrep=14.1.1-1+b4`
+package; no substitute matcher or warning exception was used. Local logs,
+compiler/tool hashes and source hashes are retained under `_build/`.
+Hosted checks and any later sibling adapters have separate receipts.
+
+These constructions are standard deterministic constructive factorization
+arguments packaged into the owning Epistemic API. The independent source
+review identified and removed a redundant success premise and narrowed the
+arbitrary-request example's claim. Compilation and source review are distinct.
+No new sibling adapter or complete Secret Types semantics bridge is claimed.
+Ordinal work remains excluded.

src/EpistemicTypes/All.agda

@@ -13,6 +13,12 @@ import EpistemicTypes.Kripke.Dependence
 open import EpistemicTypes.EchoBridge public
 import EpistemicTypes.PartialRecovery
 import EpistemicTypes.PartialRecoveryExamples
+import EpistemicTypes.QueryRecovery
+import EpistemicTypes.QueryRecoveryExamples
+import EpistemicTypes.ObserverSafety
+import EpistemicTypes.ObserverSafetyExamples
+import EpistemicTypes.ResidueSufficiency
+import EpistemicTypes.ResidueSufficiencyExamples
 -- Imported (checked) but NOT re-exported publicly: ReadConsistency keeps
 -- its own self-contained ⊥/¬_ (matching the Examples.agda convention),
 -- which would clash with Examples' identically-named helpers if both were

src/EpistemicTypes/ObserverSafety.agda

@@ -0,0 +1,71 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module EpistemicTypes.ObserverSafety where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Maybe using (Maybe; just)
+open import EpistemicTypes.EchoBridge using (Retention)
+open import EpistemicTypes.PartialRecovery using (retainedPair; withDefault)
+open import EpistemicTypes.QueryRecovery using (QueryRecovery; queryConstant)
+
+private
+  sym : {A : Set} {x y : A} -> x ≡ y -> y ≡ x
+  sym refl = refl
+
+  trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
+  trans refl p = p
+
+  cong : {A B : Set} (f : A -> B) {x y : A} -> x ≡ y -> f x ≡ f y
+  cong f refl = refl
+
+-- An explicit deterministic observation of the whole Maybe result, including
+-- success/failure if see exposes it. These results concern GENERATED inputs.
+-- E is a supplied relation; no unproved equivalence laws are silently assumed.
+ObservationNI : {A B R T O : Set} {C : Retention A B R} {q : A -> T} ->
+  QueryRecovery C q -> (Maybe T -> O) -> (A -> A -> Set) -> Set
+ObservationNI {C = C} rec see E = ∀ {x z} -> E x z ->
+  see (QueryRecovery.answer rec (Retention.observe C x) (Retention.retain C x)) ≡
+  see (QueryRecovery.answer rec (Retention.observe C z) (Retention.retain C z))
+
+ReleaseInvariant : {A T O : Set} -> (A -> T) -> (Maybe T -> O) ->
+  (A -> A -> Set) -> Set
+ReleaseInvariant q see E = ∀ {x z} -> E x z -> see (just (q x)) ≡ see (just (q z))
+
+releaseInvariantToNI : {A B R T O : Set} {C : Retention A B R} {q : A -> T}
+  (rec : QueryRecovery C q) (see : Maybe T -> O) (E : A -> A -> Set) ->
+  ReleaseInvariant q see E -> ObservationNI rec see E
+releaseInvariantToNI rec see E invariant {x} {z} related =
+  trans (cong see (QueryRecovery.adequate rec x))
+    (trans (invariant related) (sym (cong see (QueryRecovery.adequate rec z))))
+
+niToReleaseInvariant : {A B R T O : Set} {C : Retention A B R} {q : A -> T}
+  (rec : QueryRecovery C q) (see : Maybe T -> O) (E : A -> A -> Set) ->
+  ObservationNI rec see E -> ReleaseInvariant q see E
+niToReleaseInvariant rec see E invariant {x} {z} related =
+  trans (sym (cong see (QueryRecovery.adequate rec x)))
+    (trans (invariant related) (cong see (QueryRecovery.adequate rec z)))
+
+-- When the whole answer is visible, related sources must have equal queries.
+transparentNIForcesQueryAgreement : {A B R T : Set} {C : Retention A B R} {q : A -> T}
+  (rec : QueryRecovery C q) (E : A -> A -> Set) ->
+  ObservationNI rec (λ result -> result) E -> ∀ {x z} -> E x z -> q x ≡ q z
+transparentNIForcesQueryAgreement {q = q} rec E ni {x} related =
+  cong (withDefault (q x)) (niToReleaseInvariant rec (λ result -> result) E ni related)
+
+-- Taking the query to be the whole source rules out hiding a genuinely
+-- distinct related pair from an observer who sees that recovered source.
+fullRecoveryNIForcesEquality : {A B R : Set} {C : Retention A B R}
+  (rec : QueryRecovery C (λ x -> x)) (E : A -> A -> Set) ->
+  ObservationNI rec (λ result -> result) E -> ∀ {x z} -> E x z -> x ≡ z
+fullRecoveryNIForcesEquality = transparentNIForcesQueryAgreement
+
+-- A separate INPUT-side assumption: if the actual pair hides a relation,
+-- every adequate query must respect it. A private residue need not satisfy
+-- this assumption merely because the visible projection does.
+hiddenPairForcesQueryAgreement : {A B R T : Set} {C : Retention A B R} {q : A -> T}
+  (rec : QueryRecovery C q) (E : A -> A -> Set) ->
+  (∀ {x z} -> E x z -> retainedPair C x ≡ retainedPair C z) ->
+  ∀ {x z} -> E x z -> q x ≡ q z
+hiddenPairForcesQueryAgreement rec E hides related = queryConstant rec (hides related)