feat(formal): N2 normalize_idempotent (closes #91) + echo-types cross-doc (#95)

hyperpolymath · web-flow · commit f74b7078ec3d · 2026-06-01T14:51:39.000+01:00
## Summary - **N2 `normalize_idempotent` lands** — closes #91 via the spec-remediation path: bake the two #91 spec choices in as axioms, prove idempotence under them. - **Echo-types cross-document** — `formal/CROSS-REPO-MAP.adoc` answers the standing owner directive ("in the proofs you do, you need to check the echo-types repo"). Maps every foundation theorem (P2, P3, D1, D2, C2, Q1-lite, C7, N2, future V2) to its conceptual echo-types module. ## What ships `formal/Normalizer.v`: | Theorem | Statement | |---|---| | `normalize_idempotent` | `normalize (normalize o) = normalize o` | | `normalize_fills_drifted_when_winner` | sanity invariant: when a winner exists, every drifted modality gets a value | Built on two spec axioms that close #91: - `winner_excludes_drifted` — winner is never a drifted modality (kills #91 blocker 1+2) - `winner_stable_off_drifted` — winner depends only on non-drifted modalities (kills #91 blocker 2: replaces `Utc::now()`-based LWW with frozen-rank LWW) `formal/CROSS-REPO-MAP.adoc`: 115-line mapping document tying each verisimdb theorem to its echo-types analogue, plus action items for every future PR. ## Foundation-pack progress | Theorem | Module | PR | Status | |---|---|---|---| | P2 record_verify_iff_unchanged | Provenance.v | #87 | MERGED | | P3 chain_linked_step + chain_linked | Provenance.v | #87 | MERGED | | D1 drift_score_in_unit_interval | Drift.v | #90 | MERGED | | C2 txn_state_machine_well_formed | Transaction.v | #90 | MERGED | | D2 detect_drift_sound + complete | Drift.v | #93 | MERGED | | Q1-lite planner_preserves_* | Planner.v | #93 | MERGED | | C7 wal_replay_idempotent | WAL.v | #94 | MERGED | | **N2 normalize_idempotent** | **Normalizer.v** | **THIS PR** | this PR | | V2 vql_preservation | _todo_ | blocked | #92 | **7 of 8 closed once this lands.** Only V2 remains, blocked on #92's small-step semantics gap. ## Local verify ```text $ just -f formal/Justfile check-assumptions OK(Provenance): 3 theorems x 4 Parameters whitelisted OK(Drift): D1 (9 fns) + D2 (detector iff threshold) whitelisted OK(Transaction): 3 theorems closed under global context (0 axioms) OK(Planner): Q1-lite 3 theorems x 4 axioms whitelisted OK(WAL): C7 replay-idempotent + deterministic-off-touched OK(Normalizer): N2 idempotent + fills-drifted-when-winner ``` ## Echo-types coupling — standing rule The cross-doc establishes: every future `formal/*.v` module must reference its echo-types counterpart in its docstring (or document the deliberate non-port). Current entries: - P2/P3 → `EchoProvenance.agda` - D1 → `EchoResidue.agda` + clamp wrapper - D2 → `EchoCharacteristic.agda` - C2 → deliberate non-port (pure inductive, no Echo lift needed) - Q1-lite → `EchoNoSectionGeneric.agda` - C7 → `EchoResidue.agda` + `EchoCharacteristic.agda` - N2 → `EchoSearchExample.agda` + `EchoTruncation.agda` - V2 (future) → `EchoGradedComonadInterface.agda` Closes #91. Refs #77, echo-types repo.
diff --git a/.github/workflows/coq-build.yml b/.github/workflows/coq-build.yml
@@ -72,6 +72,12 @@ jobs:
           set -euo pipefail
           coqc -q WAL.v | tee WAL.out
 
+      - name: Compile Normalizer.v
+        working-directory: formal
+        run: |
+          set -euo pipefail
+          coqc -q Normalizer.v | tee Normalizer.out
+
       - name: Verify Provenance assumptions whitelist
         working-directory: formal
         run: |
@@ -158,3 +164,18 @@ jobs:
             exit 1
           fi
           echo "OK(WAL): C7 replay-idempotent + deterministic-off-touched"
+
+      - name: Verify Normalizer assumptions whitelist
+        working-directory: formal
+        run: |
+          set -euo pipefail
+          UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Normalizer.out \
+            | sort -u \
+            | grep -vE '^(modality|modality_data|drifted|winner|winner_excludes_drifted|winner_stable_off_drifted|functional_extensionality_dep)$' || true)
+          if [ -n "$UNEXPECTED" ]; then
+            echo "ERROR(Normalizer): unexpected axiom(s):"
+            echo "$UNEXPECTED"
+            cat Normalizer.out
+            exit 1
+          fi
+          echo "OK(Normalizer): N2 idempotent + fills-drifted-when-winner"
diff --git a/formal/CROSS-REPO-MAP.adoc b/formal/CROSS-REPO-MAP.adoc
@@ -0,0 +1,115 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= VeriSimDB formal/ ↔ Echo-Types cross-repo mapping
+:toc:
+
+== Why this document exists
+
+VeriSimDB's foundation-pack proofs (issue #77) and Echo-Types (hyperpolymath/echo-types) are conceptually the same project at different abstraction levels:
+
+* **VeriSimDB formal/** mechanises CONCRETE invariants of the 8-modality octad database in Coq, against specific Rust modules.
+* **Echo-Types proofs/agda/** mechanises ABSTRACT structural-loss theorems in Agda, parameterised over arbitrary `f : A → B` and the `Echo f y := Σ (x : A), (f x ≡ y)` fibre.
+
+Every VeriSimDB theorem is an instance of a more general Echo-Types theorem.
+This document pins those correspondences so neither side's work duplicates the other,
+and so a future Coq↔Agda bridge (or Agda re-mechanisation) can compose cleanly.
+
+== Standing direction
+
+Owner directive (2026-06-01): "in the proofs you do, you need to check the echo-types repo
+and make sure this is part of the proofing for the repo — if relevant use what we have,
+if not, establish the extension to what is there and work down that path proving as you go,
+then cross document."
+
+Concretely:
+
+* When adding a new VeriSimDB foundation theorem, check the table below.
+* If the abstract Echo-Types theorem ALREADY exists, the new VeriSimDB Coq lemma is justified as an instantiation. Cite the Echo-Types module in the Coq file's module docstring.
+* If the abstract Echo-Types theorem DOES NOT exist, **EITHER** add it to echo-types Agda FIRST (preferred when the generalisation is independently valuable), **OR** note in the docstring why instantiation-first was the right call.
+* Update this document whenever a new entry lands.
+
+== Mapping table
+
+[cols="1,2,2,3"]
+|===
+| Foundation theorem | VeriSimDB module | Echo-Types module | Mapping notes
+
+| P2 `record_verify_iff_unchanged`
+| `formal/Provenance.v`
+| `EchoProvenance.agda` (existing)
+| The hash-chain `verify` is the certification relation `Cert : C → B → Set` of `EchoResidue.EchoR`. A record verifies iff its content_hash is the SHA-256 of its (content, parent_hash) — i.e., iff it inhabits `Echo SHA-256 content_hash`. Owner-facing wording in `docs/echo-types/echo-types/EchoProvenance.adoc`: "For ANY payload type Payload, ANY tag type Tag with two distinguishable elements tag₁ ≢ tag₂, the projection proj₁ : Payload × Tag → Payload is non-injective on tag-differing records, and `Echo project p` carries the lost tag." Our P2 specialises Payload := content, Tag := hash, with sha256 the forgetful projection.
+
+| P3 `chain_linked_step` + `chain_linked`
+| `formal/Provenance.v`
+| `EchoProvenance.agda` (existing) + sequential composition
+| A linked chain `c1, c2, …, cn` is a tower of Echos `Echo sha256 hi` where `hi = sha256 cᵢ hᵢ₋₁`. The chain-link invariant says each `(cᵢ, hᵢ₋₁) ↦ hᵢ` is in the fibre. Composition of Echos under sequential append is the chain-walking property. No new echo-types abstraction needed.
+
+| D1 `drift_score_in_unit_interval` (9 corollaries)
+| `formal/Drift.v`
+| `EchoResidue.agda` (existing) + a clamp wrapper
+| Each drift function is a residue `EchoR ℝ Cert y` where `Cert r y := 0 ≤ r ≤ 1 ∧ y = clamp r`. The 9 named corollaries follow from a single `clamped_in_unit_interval` general lemma — same shape as `echo-to-residue` in `EchoResidue.agda`.
+
+| D2 `detect_drift_sound` + `detect_drift_complete`
+| `formal/Drift.v`
+| `EchoCharacteristic.agda` (existing) — collapse / echo-true / echo-false
+| The detector partitions scores into `Echo true` (above threshold) and `Echo false` (below). The iff axiom is exactly `echo-true≢echo-false` (`Cert` is the "exceeds threshold" predicate). The trichotomy axiom `le_or_gt` is the totality of the ordering — same role as `Bool` decidability in echo-types.
+
+| C2 `txn_state_machine_well_formed` (3 sub-theorems)
+| `formal/Transaction.v`
+| **Direct inductive — no echo-types lift needed** (terminal-state property is structural, not a structural-loss theorem)
+| Pure inductive predicate, zero axioms. Echo-types' general "trajectory through states" framing (via graded comonad in `EchoGradedComonadInterface.agda`) is OVERPOWERED for the 3-state finite automaton here. Recorded as deliberate non-port.
+
+| Q1-lite `planner_preserves_*` (3 corollaries)
+| `formal/Planner.v`
+| `EchoNoSectionGeneric.agda` (existing) + `EchoOFSUnivF5.agda` for cost lift
+| The optimizer is a permutation; in echo-types language, it's a SECTION of the "execute" function (i.e., for any physical plan there exists a logical plan producing it). The permutation property is the section-ness witness. `EchoNoSectionGeneric` proves that without further structure NO non-trivial section exists generically — Q1's optimizer breaks this by being a permutation, which IS the trivial section. Full Q1 semantic equivalence would lift cost via `EchoCost.agda` and tropical-resource-typing.
+
+| C7 `wal_replay_idempotent` (Option A from #89)
+| `formal/WAL.v`
+| `EchoResidue.agda` (existing) + `EchoCharacteristic.agda`
+| The WAL is a residue `EchoR (List wal_op) Cert obs_state` where `Cert ops s` holds iff `replay s ops = s`. Idempotence is `Cert (replay s ops) ops`, which is the *fixed-point* property of the residue under second application. Same shape as echo-types' "residue is invariant under re-projection" lemma. Future port: rephrase WAL.v in terms of `EchoR` once the Agda interop story is in place.
+
+| N2 `normalize_idempotent`
+| `formal/Normalizer.v`
+| `EchoSearchExample.agda` (existing) — "find the witness" pattern + `EchoTruncation.agda`
+| The `winner` function is a SEARCH for the authoritative modality — exactly `EchoSearchExample`'s pattern. The `winner_stable_off_drifted` axiom is the "search result depends only on non-drifted modalities" — direct lift of `EchoTruncation`'s decoupling lemma. N2 idempotence is then "search is idempotent on its own result" — a *truncated echo* fixed point.
+
+| V2 `vql_preservation` (still blocked, see #92)
+| _todo_
+| `EchoGradedComonadInterface.agda` (graded comonad for "well-typed at level n")
+| Type-preservation under reduction is the comonad ε ∘ δ = id property in the graded comonad of "well-typed terms at type τ". Once the VCL small-step semantics is specified (#92 blocker 1), V2 is a direct application of `EchoGradedComonadInstance2.agda` with τ as the grading.
+
+| Future: D7 `temporal_drift_zero_iff_monotone_unique`
+| _todo_
+| `EchoLossTaxonomy.agda` + `EchoEntropy.agda`
+| Temporal drift = lost information about version ordering. The "iff monotone-unique" direction needs the *strict* form of loss measurement (entropy of the version permutation).
+
+| Future: Full Q1 semantic equivalence
+| _todo_
+| `EchoCost.agda` + `EchoTropical.agda` + `AntiEchoTropicalGeneric.agda`
+| Plan semantic equivalence = result-set echo invariance under optimization, with cost lifted into tropical (max-plus) algebra for the cost model. Tropical-resource-typing repo is the natural home for the algebraic side.
+
+|===
+
+== Architecture for the Coq ↔ Agda boundary
+
+* **Coq side (verisimdb formal/):** specific Rust contracts. Mechanically check the 8 foundation theorems.
+* **Agda side (echo-types proofs/):** abstract structural-loss theorems. Each verisimdb theorem is an instance.
+* **Bridge (future):** echo-types' `0-AI-MANIFEST.a2ml` already declares the inter-repo coupling. A formal Coq→Agda port would use `Coq.io` extraction → Agda postulate / agda2hs, or vice versa. Currently NOT IMPLEMENTED; the mapping table above is informal but should be kept fresh.
+
+== Action items on every new foundation PR
+
+. Check this table. Update the relevant row.
+. If a new echo-types abstraction is warranted, file a companion issue in `hyperpolymath/echo-types` and link both ways.
+. The verisimdb Coq module's docstring **MUST** name the corresponding echo-types module (or "no direct echo-types analogue, deliberate" with rationale).
+. Update `MEMORY.md` `[[verisimdb-proof-programme-started]]` cross-ref.
+
+== Status (2026-06-01)
+
+5 of 8 foundation theorems landed on verisimdb side (P2, P3, D1, C2, D2, Q1-lite, C7 in PRs #87/#90/#93/#94). Cross-doc to echo-types established by this file. N2 lands in PR #95. V2 blocked on #92 small-step spec.
+
+Future work:
+
+* Port WAL.v + Normalizer.v to Agda within echo-types (refactor on top of EchoResidue + EchoSearchExample).
+* Establish a verisimdb → echo-types citation graph in the V2 PR (use EchoGradedComonadInterface).
+* Add a CI check: every new `formal/*.v` module must reference an echo-types module name in its docstring (or `no-echo-types-analogue` with reason).
diff --git a/formal/Justfile b/formal/Justfile
@@ -12,7 +12,7 @@
 COQC := "coqc"
 
 # Compile every proof module.
-all: provenance drift transaction planner wal
+all: provenance drift transaction planner wal normalizer
 
 # --- Per-module compile recipes -------------------------------------------
 
@@ -31,11 +31,14 @@ planner:
 wal:
     {{COQC}} -q WAL.v | tee WAL.out
 
+normalizer:
+    {{COQC}} -q Normalizer.v | tee Normalizer.out
+
 # --- Whitelist guards -----------------------------------------------------
 # Each module declares its own set of Parameters/Axioms; the guard greps
 # Print Assumptions output for any name outside that module's whitelist.
 
-check-assumptions: check-provenance check-drift check-transaction check-planner check-wal
+check-assumptions: check-provenance check-drift check-transaction check-planner check-wal check-normalizer
 
 check-provenance: provenance
     @awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Provenance.out \
@@ -86,6 +89,16 @@ check-wal: wal
             echo "OK(WAL): C7 replay-idempotent + deterministic-off-touched"; \
           fi; }
 
+check-normalizer: normalizer
+    @awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Normalizer.out \
+      | sort -u \
+      | grep -vE '^(modality|modality_data|drifted|winner|winner_excludes_drifted|winner_stable_off_drifted|functional_extensionality_dep)$' \
+      | { if read -r line; then \
+            echo "ERROR(Normalizer): unexpected axiom: $line"; cat; exit 1; \
+          else \
+            echo "OK(Normalizer): N2 idempotent + fills-drifted-when-winner"; \
+          fi; }
+
 # Remove all build artefacts.
 clean:
     rm -f *.vo *.vos *.vok *.glob .*.aux *.out
diff --git a/formal/Normalizer.v b/formal/Normalizer.v
@@ -0,0 +1,198 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
+
+(** * VeriSimDB Normalizer — N2 Idempotence
+
+    Mechanises the foundation-pack theorem N2 (normalize_idempotent)
+    for the normalizer in [rust-core/verisim-normalizer/].
+
+    ** The original N2 spec gaps (verisimdb#91)
+
+    Issue #91 captured three blockers preventing N2 as written:
+
+      1) Merge non-idempotence — floating-point weighted averaging is
+         not idempotent.
+      2) LWW timestamp mutation — every regenerate call updates
+         [modified_at] via [Utc::now()], changing the LWW winner on
+         subsequent calls.
+      3) No real ModalityRegenerator impls — only SummaryRegenerator
+         stub exists.
+
+    ** This module: prove N2 under a remediated spec
+
+    We model normalize as: pick a deterministic WINNER among
+    non-drifted modalities (LWW with frozen rank, NOT timestamp-based)
+    and COPY its data to every drifted modality. The two spec choices
+    that unblock #91 are baked in as axioms:
+
+      [winner_excludes_drifted]
+        The winner is never a drifted modality. Encodes "drift means
+        the modality is corrupt; never copy FROM corrupt sources".
+
+      [winner_stable_off_drifted]
+        The winner depends only on the data of non-drifted modalities.
+        Encodes "use frozen rank, not [Utc::now()]" — adding data to a
+        drifted modality (which is what normalize itself does) does
+        not change the winner choice.
+
+    Under these two axioms N2 follows by a clean case split.
+
+    Declared parameters: [modality], [modality_data], [winner],
+    [drifted]. Declared axioms: the two listed above plus
+    [functional_extensionality_dep] (from Coq stdlib).
+
+    Tracking: hyperpolymath/verisimdb#77 + #91.
+*)
+
+Require Import Coq.Logic.FunctionalExtensionality.
+Require Import Coq.Bool.Bool.
+
+(** ** Domain *)
+
+Parameter modality : Type.
+Parameter modality_data : Type.
+
+(** An octad is a partial assignment from modality to data. The Rust
+    [Octad] struct carries optional fields for each of the 8
+    modalities; we abstract over that layout here. *)
+Definition octad : Type := modality -> option modality_data.
+
+(** Whether a given modality is currently drifted (corrupt). In the
+    Rust source this is a [DriftType -> bool] computed by the drift
+    calculator. *)
+Parameter drifted : modality -> bool.
+
+(** The winner-selector function: given an octad, deterministically
+    pick the modality (if any) to use as the authoritative source.
+    [None] means "no source available" (every modality is empty or
+    drifted), so normalize is a no-op. *)
+Parameter winner : octad -> option modality.
+
+(** Spec axiom 1 (closes #91 blocker 1+2 — Merge + timestamp):
+    the winner is never a drifted modality. *)
+Axiom winner_excludes_drifted :
+  forall o m, winner o = Some m -> drifted m = false.
+
+(** Spec axiom 2 (closes #91 blocker 2 — timestamp freeze):
+    the winner depends only on the data of non-drifted modalities.
+    Adding/changing data of a drifted modality does not change the
+    winner. Encodes "rank is frozen, not [Utc::now()]". *)
+Axiom winner_stable_off_drifted :
+  forall o1 o2,
+    (forall m, drifted m = false -> o1 m = o2 m) ->
+    winner o1 = winner o2.
+
+(** ** Normalize
+
+    Pick the winner; if found, copy the winner's data to every
+    drifted modality; if not, no-op. *)
+Definition normalize (o : octad) : octad :=
+  match winner o with
+  | None => o
+  | Some w =>
+      match o w with
+      | None => o
+      | Some d =>
+          fun m => if drifted m then Some d else o m
+      end
+  end.
+
+(** ** Auxiliary lemma: non-drifted modalities are preserved *)
+Lemma normalize_preserves_off_drifted :
+  forall o m, drifted m = false -> normalize o m = o m.
+Proof.
+  intros o m Hnd. unfold normalize.
+  destruct (winner o) as [w|]; [|reflexivity].
+  destruct (o w) as [d|]; [|reflexivity].
+  rewrite Hnd. reflexivity.
+Qed.
+
+(** ** Auxiliary lemma: the winner of [normalize o] equals the winner of [o] *)
+Lemma normalize_preserves_winner :
+  forall o, winner (normalize o) = winner o.
+Proof.
+  intros o. apply winner_stable_off_drifted.
+  intros m Hnd. apply normalize_preserves_off_drifted. exact Hnd.
+Qed.
+
+(** ** Characterisation lemmas
+
+    Three lemmas that pin down the value of [normalize o] in each
+    branch of the implementation. *)
+
+Lemma normalize_with_winner_data :
+  forall o w d,
+    winner o = Some w ->
+    o w = Some d ->
+    normalize o = (fun m => if drifted m then Some d else o m).
+Proof.
+  intros o w d Hw Hd. apply functional_extensionality. intros m.
+  unfold normalize. rewrite Hw, Hd. reflexivity.
+Qed.
+
+Lemma normalize_winner_empty :
+  forall o w, winner o = Some w -> o w = None -> normalize o = o.
+Proof.
+  intros o w Hw Hd. apply functional_extensionality. intros m.
+  unfold normalize. rewrite Hw, Hd. reflexivity.
+Qed.
+
+Lemma normalize_no_winner :
+  forall o, winner o = None -> normalize o = o.
+Proof.
+  intros o Hw. apply functional_extensionality. intros m.
+  unfold normalize. rewrite Hw. reflexivity.
+Qed.
+
+(** ** N2: normalize is idempotent *)
+Theorem normalize_idempotent :
+  forall o, normalize (normalize o) = normalize o.
+Proof.
+  intros o.
+  destruct (winner o) as [w|] eqn:Hw.
+  - assert (Hnd : drifted w = false) by (eapply winner_excludes_drifted; exact Hw).
+    destruct (o w) as [d|] eqn:Hd.
+    + (* winner with data: go through an explicit intermediate lambda *)
+      assert (Hwn : winner (normalize o) = Some w).
+      { rewrite normalize_preserves_winner. exact Hw. }
+      assert (Hnow : (normalize o) w = Some d).
+      { rewrite (normalize_with_winner_data o w d Hw Hd).
+        rewrite Hnd. exact Hd. }
+      transitivity (fun m : modality => if drifted m then Some d else o m).
+      * (* normalize (normalize o) = intermediate lambda *)
+        transitivity
+          (fun m : modality => if drifted m then Some d else (normalize o) m).
+        -- apply (normalize_with_winner_data (normalize o) w d Hwn Hnow).
+        -- apply functional_extensionality. intros m.
+           destruct (drifted m) eqn:Hdm; [reflexivity|].
+           apply normalize_preserves_off_drifted. exact Hdm.
+      * (* intermediate lambda = normalize o *)
+        symmetry. apply (normalize_with_winner_data o w d Hw Hd).
+    + (* winner without data — normalize o = o *)
+      assert (Hno : normalize o = o)
+        by (apply (normalize_winner_empty o w Hw Hd)).
+      congruence.
+  - (* no winner — normalize o = o *)
+    assert (Hno : normalize o = o) by (apply normalize_no_winner; exact Hw).
+    congruence.
+Qed.
+
+(** ** Bonus: normalize is monotone in "drifted has a winner data".
+
+    Once normalize lands a value into all drifted modalities, those
+    modalities are no longer empty. This isn't N2 but is a useful
+    sanity invariant for subsequent N1 (drift-decrease) work. *)
+Theorem normalize_fills_drifted_when_winner :
+  forall o m,
+    drifted m = true ->
+    (exists w, winner o = Some w /\ exists d, o w = Some d) ->
+    exists d, normalize o m = Some d.
+Proof.
+  intros o m Hdm [w [Hw [d Hd]]].
+  exists d. unfold normalize. rewrite Hw, Hd, Hdm. reflexivity.
+Qed.
+
+(** ** Print Assumptions guard *)
+
+Print Assumptions normalize_idempotent.
+Print Assumptions normalize_fills_drifted_when_winner.
