Prove fixed approval authority and a sticky observed-write seal

PROOF-NEEDS.adoc

@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = epistemic-types — proof needs
-:revdate: 2026-11-01
+:revdate: 2026-11-04
 :toc:
 
 This queue records only obligations that remain relevant to this repository.
@@ -75,6 +75,15 @@ examples; laws must be proved or remain explicit fields | OPEN
 
 == P3 — correspondence and implementation obligations
 
+The approval-seal model added on 2026-11-03 starts P3-2's authority/history
+boundary; it does not close runtime refinement. Its AS-1..AS-8 statements and
+the distinct root-replacement counterexample are recorded in
+link:docs/applications/approval-seal.adoc[]. Cryptographic binding, authorized
+epoch changes, complete observation, receipt authentication and check/use
+correspondence remain OPEN. The new model passed locally with Agda 2.6.4.3
+under the canonical profile, alongside 17 rejections and four mutation controls;
+fresh hosted checking and independent semantic review remain pending.
+
 [cols="1,3,1",options="header"]
 |===
 | ID | Obligation | Status

PROOF-STATUS.adoc

@@ -1,20 +1,36 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = epistemic-types — proof status
-:revdate: 2026-11-01
+:revdate: 2026-11-04
 :toc:
 :sectnums:
 
 [abstract]
 This is the current, source-anchored verification record for the Agda
-formalisation. The authoritative positive tree contains *22 source modules* and
-the negative-control manifest contains *13 expected-rejection fixtures*. The
+formalisation. The authoritative positive tree contains *23 source modules* and
+the negative-control manifest contains *17 expected-rejection fixtures*. The
+2026-11-03 extension adds one module and four fixtures to the previous verified
+22-module/13-fixture baseline, plus 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 2026-11-03 approval-seal extension is locally *AGDA-VERIFIED* under Agda
+2.6.4.3 and the canonical safety profile. `Applications/ApprovalSeal.agda` defines AS-1..AS-8:
+exact approval binding, agent-trace anchor preservation, an irreversible
+observed-write flag, rejection after a write, local-reference irrelevance,
+and clean-state acceptance. See link:docs/applications/approval-seal.adoc[] for
+the exact threat model and the positive counterexample when the adversary can
+replace the root. The baseline gate and extended gate both passed locally;
+23 modules, all 17 expected rejections and 4/4 deterministic mutants were checked.
+The new module needs no warning exception; the existing 23-span warning manifest
+is unchanged. Proof Safety run 41708617511 checked the extended corpus at
+`91038dd6c2a535947178d429fc80ff543f0f32fe`; the earlier receipts below
+remain historical evidence for the preceding 22-module/13-rejection corpus. No runtime,
+independent-review or cryptographic closure is claimed.
+
 This document uses the estate proof-policy vocabulary:
 
 * `PROVEN` — accepted by the named kernel under its safe profile, with no proof
@@ -37,6 +53,7 @@ The policy entry point is `scripts/check.sh`. It runs:
 bash tests/check-policy.sh
 bash tests/check-proofs.sh
 bash tests/check-rejections.sh
+bash tests/check-approval-seal-mutations.sh
 ----
 
 Every first-party Agda entry point is invoked with the canonical theory profile
@@ -48,7 +65,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 22 source modules, 13 rejection fixtures, and the integration
+compares all 23 source modules, 17 rejection fixtures, and the integration
 witness 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
@@ -76,6 +93,22 @@ Agda source, fixture, gate, option, or dependency pin and is itself rerun by the
 same PR workflow. No missing tool, import failure, or unexpected rejection
 counts as a pass.
 
+== Approval-seal hosted receipt
+
+Proof Safety run
+https://github.com/hyperpolymath/epistemic-types/actions/runs/41708617511[41708617511]
+at `91038dd6c2a535947178d429fc80ff543f0f32fe` passed both
+`Proof core and rejection controls` and `Canonical Echo correspondence`.
+The core job checked 23 source modules, 17 expected semantic rejections,
+and all four isolated approval-seal mutants under Agda 2.6.4.3.
+This receipt covers that exact revision, not subsequent edits by implication.
+
+Governance run 41708617122 and Secret Scanner run 41708617124 failed before
+starting jobs. Their failures are not waived by the proof result. Independent
+adversarial review, runtime enforcement, digest binding and authorized approval
+updates remain open. Automated documentation review is not an independent
+validation of the security specification.
+
 == Local proof ledger
 
 All `PROVEN` rows below describe the Agda model only. They are covered by the
@@ -185,7 +218,7 @@ runtime or an unlisted mathematical correspondence.
 | Documentary comparison only; no imported owning definition
 
 | C-1
-| Every one of the 13 intended-invalid constructions is rejected for its
+| Every one of the 17 intended-invalid constructions is rejected for its
   enumerated semantic type mismatch. This is negative-control evidence, not a
   positive theorem.
 | TESTED

coordination.k9

@@ -57,7 +57,7 @@ repo:
   owner: "Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>"
   version: "0.1.0"
   status: "prototype"
-  last_updated: "2026-11-01"
+  last_updated: "2026-11-03"
   kind: "single-tool Agda library"
 
 # Paths the session machinery must treat as load-bearing. Changes under these
@@ -70,7 +70,7 @@ protected_paths:
   - path: ".machine_readable/"
     role: "a2ml + Nickel/k9 machine-readable surface (descriptiles/, proof-transport/)"
   - path: "tests/"
-    role: "proof-policy gate, 13 expected rejections and pinned integration witness"
+    role: "proof-policy gate, 17 expected rejections and pinned integration witness"
   - path: "PROOF-STATUS.adoc"
     role: "current proof ledger and Mathesis grade boundary"
   - path: "Justfile"
@@ -83,7 +83,7 @@ invariants:
   - id: "build-green"
     statement: "The library typechecks: `just check` succeeds."
     command: "just check"
-    expands_to: "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh"
+    expands_to: "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh && bash tests/check-approval-seal-mutations.sh"
     tool: "Agda 2.6.4.3"
   - id: "no-postulates"
     statement: "No postulates or escape hatches. Every first-party module declares --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness."

docs/applications/approval-seal.adoc

@@ -0,0 +1,139 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Approval authority and an observed-write seal
+:revdate: 2026-11-03
+
+== Purpose and exact scope
+
+`Applications/ApprovalSeal.agda` starts the evidence-integrity programme with
+a deliberately small model of authority and observed history. It addresses the
+attack where an implementation agent changes both an artifact and a local
+reference, and the separate attack where it changes and restores the artifact.
+The model is not a deployed gate, a hash implementation, a signature scheme,
+a filesystem monitor, or a proof that an approved program is safe.
+
+The source defines a fixed approval anchor, current artifact identity, writable
+local reference, and a sticky observed-write flag. `Nat` denotes *exact model
+identity*, not a digest and not an assumption that finite hashes are injective.
+Agent actions can write the artifact or local reference. They cannot reanchor
+or clear the flag. These permissions define the threat model; Agda does not
+enforce them on an external operating system.
+
+Acceptance establishes equality with the approval anchor and an intact flag.
+It does not establish the meaning of the approved artifact. Semantic
+certification belongs to `ProofTransport.CertificateCheck`; connecting that
+checker, its exact proposition and this model is a further obligation.
+
+== Theorem inventory
+
+[cols="1,3,3",options="header"]
+|===
+|ID |Declaration |Meaning
+|AS-1 |`accepted-matches-anchor` |Accepted state has the exact anchored artifact.
+|AS-2 |`accepted-is-unbroken` |Acceptance requires an intact observed-write seal.
+|AS-3 |`run-preserves-anchor` |Every finite trace of permitted agent actions preserves the approval anchor.
+|AS-4 |`accepted-trace-matches-original` |Accepted trace endpoints match the original anchor, not a locally substituted reference.
+|AS-5 |`run-keeps-broken` |Once broken, every permitted continuation leaves the seal broken.
+|AS-6 |`write-prevents-acceptance` |An observed artifact write prevents acceptance after every permitted continuation.
+|AS-7 |`local-reseal-irrelevant` |Changing the writable local reference cannot change the protected verdict.
+|AS-8 |`initial-accepted` |All clean initial states are accepted: safety is not obtained by rejecting everything.
+|===
+
+All functions use structural recursion over finite natural values or finite
+action lists under the repository's strict Agda profile. This establishes no
+wall-clock bound, stack bound, external parser termination or arbitrary-program
+termination. Model declarations become checked results only after the recorded
+canonical checker run; the previous baseline receipt does not cover new code.
+
+== Controls and adversary permission boundary
+
+Local verification on 2026-11-03 used Agda 2.6.4.3, extracted from the official
+Debian `agda-bin` and `libghc-agda-dev` packages at version `2.6.4.3-1+b2`.
+The unchanged baseline gate passed (22 modules, 13 rejections); the extended
+gate passed (23 modules, 17 rejections). The new module also passed standalone
+with warnings as errors and no warning suppression. The existing source-warning
+manifest remains unchanged. Hosted Proof Safety run
+https://github.com/hyperpolymath/epistemic-types/actions/runs/41708617511[41708617511]
+passed at `91038dd6c2a535947178d429fc80ff543f0f32fe`, including the four
+mutation controls. See `PROOF-STATUS.adoc` for the separate failing CI checks
+and open independent-review boundary.
+
+`bash tests/check-approval-seal-mutations.sh` first checks the unchanged module,
+then rejects four fixed, isolated semantic mutants: always accepting broken
+seals, replacing the root via the local-reference operation, not latching an
+artifact write, and clearing the latch during resealing. All four returned
+Agda exit 42 with their required semantic diagnostics. Each invocation has a
+20-second timeout; timeout/tool/import failure is not a killed mutant. Only
+the isolated invalid mutants suppress `UnsupportedIndexedMatch` to reach the
+semantic mismatch; the real positive module has no warning exception.
+
+Positive reductions exhibit an attack that fools the writable local comparator;
+an edit/restore trace that fools a protected endpoint comparator; and rejection
+of both by the sticky-seal gate. Four expected-rejection fixtures attempt to
+approve the resealed artifact, erase restoration history, change the anchor
+through agent actions, and infer an intact seal from restored bytes. They must
+reach their precise semantic mismatch with Agda exit 42, not a parser/import
+failure. Existing controls and the positive initial-state theorem remain.
+
+`replacement-root-is-accepted` deliberately demonstrates the limit: if an
+actor can replace the entire state including approval authority and history,
+the newly manufactured state accepts. Record constructors remain public.
+The security statements quantify over traces from a fixed initial state;
+they do not authenticate an arbitrary record supplied by the agent.
+
+Every `writeArtifact`, including a same-value write, breaks the seal. This is
+a conservative *observed-write* policy. An operational implementation must
+decide whether it protects bytes, objects, or attempted operations. No finding
+about malicious intent follows from a broken seal. A legitimate update needs
+a separately authorized approval epoch; that transition is not implemented.
+
+== Relation to sibling work
+
+* JtV halting islands suggest restricting the checker to a total fragment.
+  Termination alone gives neither write protection nor approval authority.
+  No JtV parser, Rust transpiler or theorem is imported here.
+* Absolute Zero's state-preservation models are useful for carefully stated
+  endpoint properties. Endpoint restoration does not establish absence of an
+  intermediate write. OND concerns disclosure relative to observations, not
+  authentication or a persistent tamper latch. No Absolute Zero theorem is
+  imported or counted as an independent proof leg here.
+* Echo retention can explain why a final artifact alone loses history needed
+  by this policy. Retaining an untrusted history is insufficient: the runtime
+  must authenticate its origin and completeness. `MatchesSource` is compatibility,
+  not historical provenance.
+
+== Hashes, signatures and the external root
+
+Changing both an artifact and its local digest needs no hash collision.
+A trusted consumer must obtain its approval anchor outside the agent's write
+authority. The eventual approval must bind the artifact, approved specification,
+checker, policy/configuration and epoch. Canonical serialization and appropriate
+signature/provenance verification are implementation obligations, not consequences
+of Nat equality. An old valid signature also needs freshness/rollback policy.
+
+A final digest detects a persistent change relative to a trusted reference,
+subject to the cryptographic assumptions. It cannot detect every temporary
+edit followed by restoration. A sticky flag requires a trusted, complete event
+source whose state cannot be reset by the adversary. This module assumes the
+listed transitions are the actual observed transitions; it proves no monitor
+coverage, remote log availability, crash persistence or administrator resistance.
+
+Runtime design should reuse established trust-root/provenance mechanisms such
+as TUF/SLSA where applicable rather than invent cryptography. It must also bind
+the bytes checked to the bytes used, closing the check/use race. Deleting a
+receipt, stopping a watcher or exhausting a budget must be unavailable/incomplete,
+not a clean seal. No scanner's CLI exit contract is changed by this module.
+
+== Next bounded obligations
+
+. Independently review this threat model and the literal AS-1..AS-8 statements.
+. Bind approval to exact artifact/specification/checker/configuration/epoch,
+  with a separately authorized update transition and replay controls.
+. Connect a concrete `CertificateCheck` without allowing an agent to replace
+  its `Meaning` predicate or an approved specification.
+. Add coverage-accounting and unknown-status promotion invariants separately.
+. Refine one executable consumer gate against this model, following the estate
+  Rust/Creusot or other applicable implementation policy. Test real enforcement
+  and observed-history completeness independently of these model proofs.
+
+No universal lie detector, end-to-end scanner verification, second-prover
+reconciliation or cryptographic theorem is claimed.

scripts/check.sh

@@ -10,12 +10,13 @@ cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
 
 required_agda=2.6.4.3
 
-# Run the policy, proof and rejection gates in order. A failing gate stops the
-# script with that gate's exit status.
+# Run the policy, proof, rejection and mutation gates in order. A failing gate
+# stops the script with that gate's exit status.
 run_gates() {
   bash tests/check-policy.sh
   bash tests/check-proofs.sh
   bash tests/check-rejections.sh
+  bash tests/check-approval-seal-mutations.sh
 }
 
 # Recursion guard: the Guix environment may resolve a differently named binary;

src/EpistemicTypes/All.agda

@@ -22,6 +22,7 @@ import EpistemicTypes.ContinuityExamples
 -- vocabulary (row entries, scan invariants, a checkability record) that has
 -- no business in the core namespace.  See docs/applications/.
 import EpistemicTypes.Applications.RapidNJExamples
+import EpistemicTypes.Applications.ApprovalSeal
 open import EpistemicTypes.SurrealBridge public
 open import EpistemicTypes.Examples public
 open import EpistemicTypes.ProofTransportExample public