From 065f9d964aacbd94c63a4a308da48981882953ba Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 19:59:08 +0000
Subject: [PATCH 01/18] Prove approval authority and sticky observed-write
 seal: docs/applications/approval-seal.adoc

---
 docs/applications/approval-seal.adoc | 135 +++++++++++++++++++++++++++
 1 file changed, 135 insertions(+)
 create mode 100644 docs/applications/approval-seal.adoc

diff --git a/docs/applications/approval-seal.adoc b/docs/applications/approval-seal.adoc
new file mode 100644
index 0000000..7ac50dc
--- /dev/null
+++ b/docs/applications/approval-seal.adoc
@@ -0,0 +1,135 @@
+// 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 rechecking is pending.
+
+`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.

From 0ed78e68c09803ba20a2be036a308e6a16e7b530 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 19:59:15 +0000
Subject: [PATCH 02/18] Prove approval authority and sticky observed-write
 seal: src/EpistemicTypes/Applications/ApprovalSeal.agda

---
 .../Applications/ApprovalSeal.agda            | 166 ++++++++++++++++++
 1 file changed, 166 insertions(+)
 create mode 100644 src/EpistemicTypes/Applications/ApprovalSeal.agda

diff --git a/src/EpistemicTypes/Applications/ApprovalSeal.agda b/src/EpistemicTypes/Applications/ApprovalSeal.agda
new file mode 100644
index 0000000..425d3d8
--- /dev/null
+++ b/src/EpistemicTypes/Applications/ApprovalSeal.agda
@@ -0,0 +1,166 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+
+-- A small authority/history model, not cryptographic or filesystem verification.
+-- Nat represents exact model artifact identity, NOT a collision-free hash.
+module EpistemicTypes.Applications.ApprovalSeal where
+
+open import Agda.Builtin.Bool using (Bool; true; false)
+open import Agda.Builtin.Nat using (Nat; zero; suc)
+open import Agda.Builtin.List using (List; []; _∷_)
+open import Agda.Builtin.Equality using (_≡_; refl)
+
+data Impossible : Set where
+
+private
+  cong : {A B : Set} (f : A -> B) {x y : A} -> x ≡ y -> f x ≡ f y
+  cong f refl = refl
+
+  trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
+  trans refl q = q
+
+  sym : {A : Set} {x y : A} -> x ≡ y -> y ≡ x
+  sym refl = refl
+
+  false-not-true : false ≡ true -> Impossible
+  false-not-true ()
+
+same : Nat -> Nat -> Bool
+same zero zero = true
+same zero (suc _) = false
+same (suc _) zero = false
+same (suc x) (suc y) = same x y
+
+same-reflexive : (x : Nat) -> same x x ≡ true
+same-reflexive zero = refl
+same-reflexive (suc x) = same-reflexive x
+
+same-sound : (x y : Nat) -> same x y ≡ true -> x ≡ y
+same-sound zero zero _ = refl
+same-sound zero (suc _) ()
+same-sound (suc _) zero ()
+same-sound (suc x) (suc y) p = cong suc (same-sound x y p)
+
+record State : Set where
+  constructor state
+  field
+    anchor : Nat
+    artifact : Nat
+    localReference : Nat
+    broken : Bool
+open State public
+
+-- These are ALL agent actions in this model. There is no reset or reanchor.
+-- Record constructors are public: the theorem concerns traces from a fixed
+-- initial state, not arbitrary records supplied by an untrusted caller.
+data AgentAction : Set where
+  writeArtifact : Nat -> AgentAction
+  writeLocalReference : Nat -> AgentAction
+
+step : AgentAction -> State -> State
+step (writeArtifact x) s = state (anchor s) x (localReference s) true
+step (writeLocalReference x) s = state (anchor s) (artifact s) x (broken s)
+
+run : List AgentAction -> State -> State
+run [] s = s
+run (a ∷ rest) s = run rest (step a s)
+
+initial : Nat -> State
+initial x = state x x x false
+
+data Verdict : Set where
+  accepted mismatch sealBroken : Verdict
+
+matchVerdict : Bool -> Verdict
+matchVerdict true = accepted
+matchVerdict false = mismatch
+
+gate : State -> Verdict
+gate (state a x _ false) = matchVerdict (same x a)
+gate (state _ _ _ true) = sealBroken
+
+-- A deliberately inadequate comparator: both arguments are agent-writable.
+localGate : State -> Bool
+localGate s = same (artifact s) (localReference s)
+
+-- A protected endpoint comparator still cannot detect intermediate writes.
+endpointGate : State -> Bool
+endpointGate s = same (artifact s) (anchor s)
+
+private
+  match-accepted : (b : Bool) -> matchVerdict b ≡ accepted -> b ≡ true
+  match-accepted true _ = refl
+  match-accepted false ()
+
+-- AS-1: acceptance binds the exact model artifact to the protected anchor.
+accepted-matches-anchor : (s : State) -> gate s ≡ accepted -> artifact s ≡ anchor s
+accepted-matches-anchor (state a x _ false) p = same-sound x a (match-accepted (same x a) p)
+accepted-matches-anchor (state _ _ _ true) ()
+
+-- AS-2: an accepted state has an intact seal.
+accepted-is-unbroken : (s : State) -> gate s ≡ accepted -> broken s ≡ false
+accepted-is-unbroken (state _ _ _ false) _ = refl
+accepted-is-unbroken (state _ _ _ true) ()
+
+step-preserves-anchor : (a : AgentAction) (s : State) -> anchor (step a s) ≡ anchor s
+step-preserves-anchor (writeArtifact _) _ = refl
+step-preserves-anchor (writeLocalReference _) _ = refl
+
+-- AS-3: no finite agent trace changes the protected authority.
+run-preserves-anchor : (actions : List AgentAction) (s : State) -> anchor (run actions s) ≡ anchor s
+run-preserves-anchor [] _ = refl
+run-preserves-anchor (a ∷ rest) s = trans (run-preserves-anchor rest (step a s)) (step-preserves-anchor a s)
+
+-- AS-4: the accepted endpoint of any trace is bound to its ORIGINAL anchor.
+accepted-trace-matches-original : (actions : List AgentAction) (s : State) ->
+  gate (run actions s) ≡ accepted -> artifact (run actions s) ≡ anchor s
+accepted-trace-matches-original actions s p =
+  trans (accepted-matches-anchor (run actions s) p) (run-preserves-anchor actions s)
+
+step-keeps-broken : (a : AgentAction) (s : State) -> broken s ≡ true -> broken (step a s) ≡ true
+step-keeps-broken (writeArtifact _) _ _ = refl
+step-keeps-broken (writeLocalReference _) _ p = p
+
+-- AS-5: once broken, all subsequent agent traces leave the seal broken.
+run-keeps-broken : (actions : List AgentAction) (s : State) -> broken s ≡ true -> broken (run actions s) ≡ true
+run-keeps-broken [] _ p = p
+run-keeps-broken (a ∷ rest) s p = run-keeps-broken rest (step a s) (step-keeps-broken a s p)
+
+-- AS-6: any observed artifact write prevents acceptance after ANY continuation.
+write-prevents-acceptance : (x : Nat) (rest : List AgentAction) (s : State) ->
+  gate (run rest (step (writeArtifact x) s)) ≡ accepted -> Impossible
+write-prevents-acceptance x rest s p = false-not-true
+  (trans (sym (accepted-is-unbroken (run rest (step (writeArtifact x) s)) p))
+    (run-keeps-broken rest (step (writeArtifact x) s) refl))
+
+-- AS-7: regenerating the local reference cannot affect the protected verdict.
+local-reseal-irrelevant : (x : Nat) (s : State) -> gate (step (writeLocalReference x) s) ≡ gate s
+local-reseal-irrelevant _ (state _ _ _ false) = refl
+local-reseal-irrelevant _ (state _ _ _ true) = refl
+
+-- AS-8: positive control; the gate does not achieve safety by rejecting all.
+initial-accepted : (x : Nat) -> gate (initial x) ≡ accepted
+initial-accepted x = cong matchVerdict (same-reflexive x)
+
+-- Concrete attacks and limits. These are checked reductions, not crypto tests.
+resealed : State
+resealed = run (writeArtifact 1 ∷ writeLocalReference 1 ∷ []) (initial 0)
+
+local-reseal-fools-local-gate : localGate resealed ≡ true
+local-reseal-fools-local-gate = refl
+
+local-reseal-breaks-protected-seal : gate resealed ≡ sealBroken
+local-reseal-breaks-protected-seal = refl
+
+restored : State
+restored = run (writeArtifact 1 ∷ writeArtifact 0 ∷ []) (initial 0)
+
+restoration-fools-endpoint-gate : endpointGate restored ≡ true
+restoration-fools-endpoint-gate = refl
+
+restoration-does-not-repair-seal : gate restored ≡ sealBroken
+restoration-does-not-repair-seal = refl
+
+-- An actor allowed to replace the root AND the history can manufacture a new
+-- accepted state. This is outside AgentAction, and an explicit trust boundary.
+replacement-root-is-accepted : gate (state 1 1 1 false) ≡ accepted
+replacement-root-is-accepted = refl

From 61ec0757b501e746eb3603b3df9172be76fa9a56 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 19:59:22 +0000
Subject: [PATCH 03/18] Prove approval authority and sticky observed-write
 seal: tests/check-approval-seal-mutations.sh

---
 tests/check-approval-seal-mutations.sh | 55 ++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100644 tests/check-approval-seal-mutations.sh

diff --git a/tests/check-approval-seal-mutations.sh b/tests/check-approval-seal-mutations.sh
new file mode 100644
index 0000000..264ad45
--- /dev/null
+++ b/tests/check-approval-seal-mutations.sh
@@ -0,0 +1,55 @@
+#!/usr/bin/env bash
+# Deterministic theorem-sensitivity controls, isolated from the real source tree.
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+source_file=src/EpistemicTypes/Applications/ApprovalSeal.agda
+flags=(--no-libraries --safe --without-K --cubical-compatible --exact-split
+  --no-sized-types --no-guardedness --double-check --ignore-interfaces -W error)
+
+# A missing checker or universally rejecting checker must fail the positive leg.
+timeout 20s agda "${flags[@]}" -i src "$source_file"
+tmpdir=$(mktemp -d)
+trap 'rm -rf "$tmpdir"' EXIT
+
+mutate() {
+  local name=$1 original=$2 replacement=$3 expected=$4 status=0 diagnostic
+  local root="$tmpdir/$name"
+  local target="$root/EpistemicTypes/Applications/ApprovalSeal.agda"
+  mkdir -p -- "$(dirname -- "$target")"
+  # Refuse to run a stale mutation against zero or several matching lines.
+  awk -v old="$original" -v new="$replacement" '
+    $0 == old { print new; replacements++; next }
+    { print }
+    END { if (replacements != 1) exit 1 }
+  ' "$source_file" > "$target"
+
+  # Only isolated invalid mutants suppress the transport warning so they reach
+  # their semantic error. The unchanged positive module has no suppression.
+  diagnostic=$(timeout 20s agda "${flags[@]}" -W noUnsupportedIndexedMatch \
+    -i "$root" "$target" 2>&1) || status=$?
+  if [[ $status -ne 42 ]] || ! rg -q -- "$expected" <<< "$diagnostic" || \
+      ! rg -q 'when checking' <<< "$diagnostic"; then
+    printf 'FAIL: %s did not produce the required semantic rejection (exit %s)\n%s\n' \
+      "$name" "$status" "$diagnostic"
+    exit 1
+  fi
+  printf 'PASS: %s rejected with Agda exit 42 and its expected semantic diagnostic\n' "$name"
+}
+
+mutate always-accept \
+  'gate (state _ _ _ true) = sealBroken' \
+  'gate (state _ _ _ true) = accepted' \
+  'should be empty, but the following constructor patterns are valid'
+mutate local-root-replacement \
+  'step (writeLocalReference x) s = state (anchor s) (artifact s) x (broken s)' \
+  'step (writeLocalReference x) s = state x (artifact s) x (broken s)' \
+  'x != anchor s'
+mutate write-without-latch \
+  'step (writeArtifact x) s = state (anchor s) x (localReference s) true' \
+  'step (writeArtifact x) s = state (anchor s) x (localReference s) (broken s)' \
+  'broken s != true'
+mutate clear-on-reseal \
+  'step (writeLocalReference x) s = state (anchor s) (artifact s) x (broken s)' \
+  'step (writeLocalReference x) s = state (anchor s) (artifact s) x false' \
+  'broken s != false'
+printf 'PASS: 4/4 fixed approval-seal mutants rejected; 20-second bound per invocation\n'

From 0e29c32c8e4276022158bca36a50330af44b5466 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 19:59:28 +0000
Subject: [PATCH 04/18] Prove approval authority and sticky observed-write
 seal: tests/reject/AgentChangesAnchor.agda

---
 tests/reject/AgentChangesAnchor.agda | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 tests/reject/AgentChangesAnchor.agda

diff --git a/tests/reject/AgentChangesAnchor.agda b/tests/reject/AgentChangesAnchor.agda
new file mode 100644
index 0000000..ca88370
--- /dev/null
+++ b/tests/reject/AgentChangesAnchor.agda
@@ -0,0 +1,7 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+module AgentChangesAnchor where
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import EpistemicTypes.Applications.ApprovalSeal
+
+forged : anchor resealed ≡ 1
+forged = refl

From 92edc0cdf2a4b3b65474c9cb1f30e2c89f657d1f Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 19:59:35 +0000
Subject: [PATCH 05/18] Prove approval authority and sticky observed-write
 seal: tests/reject/FinalStateProvesNoTouch.agda

---
 tests/reject/FinalStateProvesNoTouch.agda | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 tests/reject/FinalStateProvesNoTouch.agda

diff --git a/tests/reject/FinalStateProvesNoTouch.agda b/tests/reject/FinalStateProvesNoTouch.agda
new file mode 100644
index 0000000..e2b35cf
--- /dev/null
+++ b/tests/reject/FinalStateProvesNoTouch.agda
@@ -0,0 +1,8 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+module FinalStateProvesNoTouch where
+open import Agda.Builtin.Bool using (false)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import EpistemicTypes.Applications.ApprovalSeal
+
+forged : broken restored ≡ false
+forged = refl

From 68e89b3c4e536859412a4fd8e906d4b68352a3e0 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 19:59:41 +0000
Subject: [PATCH 06/18] Prove approval authority and sticky observed-write
 seal: tests/reject/ResealApprovesChange.agda

---
 tests/reject/ResealApprovesChange.agda | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 tests/reject/ResealApprovesChange.agda

diff --git a/tests/reject/ResealApprovesChange.agda b/tests/reject/ResealApprovesChange.agda
new file mode 100644
index 0000000..ce70769
--- /dev/null
+++ b/tests/reject/ResealApprovesChange.agda
@@ -0,0 +1,7 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+module ResealApprovesChange where
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import EpistemicTypes.Applications.ApprovalSeal
+
+forged : gate resealed ≡ accepted
+forged = refl

From 503b1a35fd09ac1ab47aec76dd0d9ffb36335eb7 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 19:59:48 +0000
Subject: [PATCH 07/18] Prove approval authority and sticky observed-write
 seal: tests/reject/RestoreErasesHistory.agda

---
 tests/reject/RestoreErasesHistory.agda | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 tests/reject/RestoreErasesHistory.agda

diff --git a/tests/reject/RestoreErasesHistory.agda b/tests/reject/RestoreErasesHistory.agda
new file mode 100644
index 0000000..f4d330e
--- /dev/null
+++ b/tests/reject/RestoreErasesHistory.agda
@@ -0,0 +1,7 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+module RestoreErasesHistory where
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import EpistemicTypes.Applications.ApprovalSeal
+
+forged : gate restored ≡ accepted
+forged = refl

From 273ea18d61b3de7e3a5dfdbd85362c6eb78acd9f Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 19:59:55 +0000
Subject: [PATCH 08/18] Prove approval authority and sticky observed-write
 seal: PROOF-NEEDS.adoc

---
 PROOF-NEEDS.adoc | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc
index a4c9310..430fdbc 100644
--- a/PROOF-NEEDS.adoc
+++ b/PROOF-NEEDS.adoc
@@ -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

From 50f7d0779e38d5b965e7522bffab33782193663c Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 20:00:01 +0000
Subject: [PATCH 09/18] Prove approval authority and sticky observed-write
 seal: PROOF-STATUS.adoc

---
 PROOF-STATUS.adoc | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 9b2a7de..1cc28d4 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -1,13 +1,15 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = epistemic-types — proof status
-:revdate: 2026-11-01
+:revdate: 2026-11-03
 :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
@@ -15,6 +17,19 @@ 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. Hosted receipts below cover the preceding 22-module,
+13-rejection corpus only; a fresh hosted receipt is pending. 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 +52,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

From 750bbed9654cb6ddbf3d0b959d721ce37249ecc7 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 20:00:07 +0000
Subject: [PATCH 10/18] Prove approval authority and sticky observed-write
 seal: coordination.k9

---
 coordination.k9 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/coordination.k9 b/coordination.k9
index 6064238..0fa7c92 100644
--- a/coordination.k9
+++ b/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."

From 20fd31edf17ef1ff80ce66e608caf662e181b6f9 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 20:00:14 +0000
Subject: [PATCH 11/18] Prove approval authority and sticky observed-write
 seal: scripts/check.sh

---
 scripts/check.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/scripts/check.sh b/scripts/check.sh
index 422db86..f668e0d 100755
--- a/scripts/check.sh
+++ b/scripts/check.sh
@@ -16,6 +16,7 @@ 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;

From 980ad3c8a503f34117b513d761a4e59889bc0250 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 20:00:21 +0000
Subject: [PATCH 12/18] Prove approval authority and sticky observed-write
 seal: src/EpistemicTypes/All.agda

---
 src/EpistemicTypes/All.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/EpistemicTypes/All.agda b/src/EpistemicTypes/All.agda
index b9af38e..bce43d0 100644
--- a/src/EpistemicTypes/All.agda
+++ b/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

From 54cd0d890f5c10148196eba21bd90233eba700ea Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 20:00:28 +0000
Subject: [PATCH 13/18] Prove approval authority and sticky observed-write
 seal: tests/check-policy.sh

---
 tests/check-policy.sh | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/tests/check-policy.sh b/tests/check-policy.sh
index d381d29..4d7f9ec 100755
--- a/tests/check-policy.sh
+++ b/tests/check-policy.sh
@@ -9,6 +9,7 @@ required_options='{-# OPTIONS --safe --without-K --cubical-compatible --exact-sp
 expected_source_modules=(
   src/EpistemicTypes/Access.agda
   src/EpistemicTypes/All.agda
+  src/EpistemicTypes/Applications/ApprovalSeal.agda
   src/EpistemicTypes/Applications/IntegerModel.agda
   src/EpistemicTypes/Applications/OrderedGroup.agda
   src/EpistemicTypes/Applications/QCriterion.agda
@@ -32,8 +33,10 @@ expected_source_modules=(
 )
 # shellcheck disable=SC2034 # consumed through require_exact_inventory namerefs
 expected_rejection_fixtures=(
+  tests/reject/AgentChangesAnchor.agda
   tests/reject/BeliefIsKnowledge.agda
   tests/reject/FakeFreshness.agda
+  tests/reject/FinalStateProvesNoTouch.agda
   tests/reject/ForgedAcceptance.agda
   tests/reject/ForgedResidue.agda
   tests/reject/ForkedHistory.agda
@@ -42,6 +45,8 @@ expected_rejection_fixtures=(
   tests/reject/MismatchedSource.agda
   tests/reject/ReplayedArtifact.agda
   tests/reject/ReplayedHolder.agda
+  tests/reject/ResealApprovesChange.agda
+  tests/reject/RestoreErasesHistory.agda
   tests/reject/StaleSample.agda
   tests/reject/UncheckedSkip.agda
   tests/reject/UnderstatedBound.agda

From 91038dd6c2a535947178d429fc80ff543f0f32fe Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 3 Nov 2026 20:00:35 +0000
Subject: [PATCH 14/18] Prove approval authority and sticky observed-write
 seal: tests/check-rejections.sh

---
 tests/check-rejections.sh | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/tests/check-rejections.sh b/tests/check-rejections.sh
index 82c2127..565e893 100644
--- a/tests/check-rejections.sh
+++ b/tests/check-rejections.sh
@@ -6,7 +6,8 @@ cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
 # unrelated parse failures must fail this gate rather than count as rejection.
 fixtures=(LyingVerifier ForgedAcceptance ReplayedArtifact ReplayedHolder \
   StaleSample FakeFreshness ForkedHistory ForgedResidue MismatchedSource \
-  UnderstatedBound InventedMigration UncheckedSkip BeliefIsKnowledge)
+  UnderstatedBound InventedMigration UncheckedSkip BeliefIsKnowledge \
+  AgentChangesAnchor FinalStateProvesNoTouch ResealApprovesChange RestoreErasesHistory)
 expected_files=$(printf 'tests/reject/%s.agda\n' "${fixtures[@]}" | sort)
 actual_files=$(rg --files tests/reject -g '*.agda' | sort)
 [[ "$actual_files" == "$expected_files" ]] || { echo 'FAIL: rejection manifest differs from files'; exit 1; }
@@ -33,6 +34,9 @@ for fixture in "${fixtures[@]}"; do
     UnderstatedBound) expected='1 != 0' ;;
     InventedMigration) expected='true != .*false' ;;
     BeliefIsKnowledge) expected='w₁ != .*w₀' ;;
+    AgentChangesAnchor) expected='0 != 1' ;;
+    FinalStateProvesNoTouch) expected='true != .*false' ;;
+    ResealApprovesChange|RestoreErasesHistory) expected='sealBroken != .*accepted' ;;
   esac
   if [[ "$status" -ne 42 ]] || ! rg -q "$expected" <<< "$diagnostic" || \
       ! rg -q 'when checking' <<< "$diagnostic"; then

From c8bdaf594edbeec7c440e2242cc1e9e3858a622e Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 4 Nov 2026 09:02:40 +0000
Subject: [PATCH 15/18] docs: reconcile approval-seal verification counts and
 hosted receipt

---
 PROOF-STATUS.adoc | 27 ++++++++++++++++++++++-----
 1 file changed, 22 insertions(+), 5 deletions(-)

diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 1cc28d4..8374aec 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = epistemic-types — proof status
-:revdate: 2026-11-03
+:revdate: 2026-11-04
 :toc:
 :sectnums:
 
@@ -26,8 +26,9 @@ 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. Hosted receipts below cover the preceding 22-module,
-13-rejection corpus only; a fresh hosted receipt is pending. No runtime,
+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:
@@ -64,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
@@ -92,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
@@ -201,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

From 39452e366b3e397bf4fba0e529ff44193d46cb30 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 4 Nov 2026 09:02:49 +0000
Subject: [PATCH 16/18] docs: reconcile approval-seal verification counts and
 hosted receipt

---
 PROOF-NEEDS.adoc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc
index 430fdbc..9398fd7 100644
--- a/PROOF-NEEDS.adoc
+++ b/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.

From 7fb3ec65246507f3a4ce628520247a83ae433207 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 4 Nov 2026 09:02:56 +0000
Subject: [PATCH 17/18] docs: reconcile approval-seal verification counts and
 hosted receipt

---
 docs/applications/approval-seal.adoc | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/docs/applications/approval-seal.adoc b/docs/applications/approval-seal.adoc
index 7ac50dc..a2b79c6 100644
--- a/docs/applications/approval-seal.adoc
+++ b/docs/applications/approval-seal.adoc
@@ -51,7 +51,11 @@ 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 rechecking is pending.
+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

From 8065be69cd6dddb5a55fc06c436439a332d4fedc Mon Sep 17 00:00:00 2001
From: "coderabbitai[bot]"
 <136622811+coderabbitai[bot]@users.noreply.github.com>
Date: Wed, 4 Nov 2026 09:15:39 +0000
Subject: [PATCH 18/18] docs(approval-seal): clarify state transitions, gate
 semantics, and mutation checks

<!-- coderabbit-ai-generated:v1 -->
---
 scripts/check.sh                                  |  4 ++--
 src/EpistemicTypes/Applications/ApprovalSeal.agda | 13 +++++++++++--
 2 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/scripts/check.sh b/scripts/check.sh
index f668e0d..84c4820 100755
--- a/scripts/check.sh
+++ b/scripts/check.sh
@@ -10,8 +10,8 @@ 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
diff --git a/src/EpistemicTypes/Applications/ApprovalSeal.agda b/src/EpistemicTypes/Applications/ApprovalSeal.agda
index 425d3d8..c22392a 100644
--- a/src/EpistemicTypes/Applications/ApprovalSeal.agda
+++ b/src/EpistemicTypes/Applications/ApprovalSeal.agda
@@ -56,14 +56,19 @@ data AgentAction : Set where
   writeArtifact : Nat -> AgentAction
   writeLocalReference : Nat -> AgentAction
 
+-- An artifact write breaks the seal, even if the identity is unchanged.
+-- A local-reference write leaves the artifact and seal unchanged.
 step : AgentAction -> State -> State
 step (writeArtifact x) s = state (anchor s) x (localReference s) true
 step (writeLocalReference x) s = state (anchor s) (artifact s) x (broken s)
 
+-- Apply actions in list order; an empty trace leaves the state unchanged.
 run : List AgentAction -> State -> State
 run [] s = s
 run (a ∷ rest) s = run rest (step a s)
 
+-- Start with the given identity as anchor, artifact and local reference, and
+-- an intact seal.
 initial : Nat -> State
 initial x = state x x x false
 
@@ -74,15 +79,19 @@ matchVerdict : Bool -> Verdict
 matchVerdict true = accepted
 matchVerdict false = mismatch
 
+-- A broken seal takes precedence; otherwise accept exactly when the artifact
+-- matches the anchor, returning mismatch when it does not.
 gate : State -> Verdict
 gate (state a x _ false) = matchVerdict (same x a)
 gate (state _ _ _ true) = sealBroken
 
--- A deliberately inadequate comparator: both arguments are agent-writable.
+-- A deliberately inadequate comparator: both the artifact and the local
+-- reference are agent-writable, and the seal is ignored.
 localGate : State -> Bool
 localGate s = same (artifact s) (localReference s)
 
--- A protected endpoint comparator still cannot detect intermediate writes.
+-- Compare the artifact with the anchor, ignoring the seal; this endpoint
+-- comparator cannot detect intermediate writes.
 endpointGate : State -> Bool
 endpointGate s = same (artifact s) (anchor s)