feat(formal): foundation-pack D2 + Q1-lite — drift detector + planner permutation (#93)

hyperpolymath · web-flow · commit 6987d9a7c0c0 · 2026-06-01T13:51:01.000+01:00
## Summary Lands two more foundation-pack theorems from #77, on top of #87 (P2+P3) and #90 (D1+C2). **Brings foundation pack to 5 of 8 closed**; the remaining 3 (C7, N2, V2) are documented as blocked on spec gaps in #89, #91, #92. ## What lands ### D2: Drift detector iff threshold (Drift.v extension) | Theorem | Statement | |---|---| | `detect_drift_sound` | detector returns true ⇒ score > threshold | | `detect_drift_complete` | detector returns false ⇒ score ≤ threshold | Mirrors `DriftDetector::record` in `verisim-drift/src/lib.rs` line 419. The trichotomy-via-`le_or_gt` axiom avoids classical reasoning; faithful to the f64 total order in the Rust source (modulo NaN, ruled out by D1 clamps proved in #90). ### Q1-lite: Planner is a permutation (Planner.v, new module) | Theorem | Statement | |---|---| | `planner_preserves_node_count` | `length lp = length (optimize lp)` | | `planner_preserves_membership` | `In n lp ↔ In n (optimize lp)` | | `planner_preserves_multiset` | `Permutation lp (optimize lp)` | Audit findings (recorded in PR #90) found `Planner::optimize` is a deterministic single-pass `stable_sort_by` over logical plan nodes — never adds, never drops. We axiomatize this as `optimize_is_permutation` and derive three structural-preservation corollaries. **Full Q1** (semantic equivalence: same input data yields same result set under logical vs physical) requires per-operator semantics (`Similarity` HNSW k-NN, `Traversal` graph reachability, `ProofVerification` contract check) and is deferred until those are formalised. Structural preservation here lays the foundation: any future semantic-equivalence proof can compose with `planner_preserves_multiset` to argue executing the physical plan yields the same multiset of per-node results as executing the logical plan. ## Cumulative foundation-pack progress | # | Theorem | Module | Status | PR | |---|---|---|---|---| | 1 | P2 record_verify_iff_unchanged | Provenance.v | ✓ MERGED | #87 | | 2 | P3 chain_linked_step + chain_linked | Provenance.v | ✓ MERGED | #87 | | 3 | D1 drift_score_in_unit_interval | Drift.v | ✓ MERGED | #90 | | 4 | C2 txn_state_machine_well_formed | Transaction.v | ✓ MERGED | #90 | | 5 | **D2 detect_drift_sound + complete** | **Drift.v** | **THIS PR** | #93 | | 6 | **Q1-lite planner_preserves_*** | **Planner.v** | **THIS PR** | #93 | | 7 | C7 wal_replay_idempotent | _todo_ | blocked | #89 | | 8 | N2 normalize_idempotent | _todo_ | blocked | #91 | | 9 | V2 vql_preservation | _todo_ | blocked | #92 | 5 of 8 foundation-pack theorems landed (P3 + D1 + D2 + C2 + Q1-lite); 3 blocked on spec gaps with concrete remediation paths filed. ## Whitelist guards (updated) - **Drift.v**: D1 + D2 set of axioms — adds `f_detect_drift`, `strictly_greater`, `le_or_gt`, `le_gt_exclusive`, `detector_iff_threshold` - **Planner.v**: `modality`, `condition`, `optimize`, `optimize_is_permutation` (4 total) ## 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 ``` ## Test plan - [x] All 4 modules compile under Coq 8.18.0 with no errors or admits - [x] Per-module Print Assumptions matches declared whitelist - [x] Transaction.v guard still asserts zero axioms - [ ] CI workflow `Coq Build Oracle` passes (verify on PR) Refs #77 (foundation pack tracking).
diff --git a/.github/workflows/coq-build.yml b/.github/workflows/coq-build.yml
@@ -60,6 +60,12 @@ jobs:
           set -euo pipefail
           coqc -q Transaction.v | tee Transaction.out
 
+      - name: Compile Planner.v
+        working-directory: formal
+        run: |
+          set -euo pipefail
+          coqc -q Planner.v | tee Planner.out
+
       - name: Verify Provenance assumptions whitelist
         working-directory: formal
         run: |
@@ -81,18 +87,20 @@ jobs:
         working-directory: formal
         run: |
           set -euo pipefail
-          # Whitelist: 5 ordering Parameters + 3 ordering axioms + 9 f_*_drift Parameters
+          # D1 whitelist: 5 ordering Parameters + 3 ordering axioms + 9 f_*_drift
+          # D2 whitelist additions: f_detect_drift, strictly_greater, le_or_gt,
+          # le_gt_exclusive, detector_iff_threshold
           UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Drift.out \
             | sort -u \
-            | grep -vE '^(score|zero|one|le|clamp|le_refl|clamp_lower|clamp_upper|f_semantic_vector_drift|f_graph_document_drift|f_temporal_consistency_drift|f_tensor_drift|f_provenance_drift|f_spatial_drift|f_schema_drift|f_quality_drift|f_quality_drift_octad)$' || true)
+            | grep -vE '^(score|zero|one|le|clamp|le_refl|clamp_lower|clamp_upper|f_semantic_vector_drift|f_graph_document_drift|f_temporal_consistency_drift|f_tensor_drift|f_provenance_drift|f_spatial_drift|f_schema_drift|f_quality_drift|f_quality_drift_octad|f_detect_drift|strictly_greater|le_or_gt|le_gt_exclusive|detector_iff_threshold)$' || true)
           if [ -n "$UNEXPECTED" ]; then
             echo "ERROR(Drift): unexpected axiom(s) in Print Assumptions:"
             echo "$UNEXPECTED"
             echo "---"
             cat Drift.out
             exit 1
           fi
-          echo "OK(Drift): whitelisted Parameters + 9 drift fns"
+          echo "OK(Drift): D1 (9 fns) + D2 (detector iff threshold) whitelisted"
 
       - name: Verify Transaction assumptions (must be empty)
         working-directory: formal
@@ -110,3 +118,20 @@ jobs:
             exit 1
           fi
           echo "OK(Transaction): 3 theorems closed under global context (0 axioms)"
+
+      - name: Verify Planner assumptions whitelist
+        working-directory: formal
+        run: |
+          set -euo pipefail
+          # Whitelist: modality, condition, optimize, optimize_is_permutation
+          UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Planner.out \
+            | sort -u \
+            | grep -vE '^(modality|condition|optimize|optimize_is_permutation)$' || true)
+          if [ -n "$UNEXPECTED" ]; then
+            echo "ERROR(Planner): unexpected axiom(s) in Print Assumptions:"
+            echo "$UNEXPECTED"
+            echo "---"
+            cat Planner.out
+            exit 1
+          fi
+          echo "OK(Planner): Q1-lite 3 theorems x 4 axioms whitelisted"
diff --git a/formal/Drift.v b/formal/Drift.v
@@ -130,12 +130,74 @@ Theorem quality_drift_octad_in_unit_interval :
   forall input, in_unit_interval (quality_drift_octad input).
 Proof. intros. apply clamped_in_unit_interval. Qed.
 
+(** ** D2: detect_drift_sound + detect_drift_complete
+
+    The drift detector signals iff the score exceeds the threshold.
+    Mirrors [DriftDetector::record] in
+    [rust-core/verisim-drift/src/lib.rs], which returns [Some event]
+    when [score > threshold] and [None] otherwise.
+
+    This is the BOUNDARY direction — soundness ("if event then over
+    threshold") plus completeness ("if no event then within
+    threshold") at the threshold comparison. The deeper question of
+    whether threshold-exceedance corresponds to a real consistency
+    violation is the [score ↔ violation] gap (issue #80 territory).
+    See verisimdb#77 D2 row + audit transcript in PR description. *)
+
+(** The detector function: takes a score and a threshold and returns
+    whether to emit a drift event. *)
+Parameter f_detect_drift : score -> score -> bool.
+
+(** Strict ordering. *)
+Parameter strictly_greater : score -> score -> Prop.
+
+(** Total ordering on [score]: for every pair [s, t], either [s <= t]
+    or [s > t]. Faithful to the [f64] total order in the Rust source
+    (modulo NaN, which the drift code rules out via clamp). *)
+Axiom le_or_gt :
+  forall s t, le s t \/ strictly_greater s t.
+
+(** Strict-greater and weak-less-or-equal are mutually exclusive. *)
+Axiom le_gt_exclusive :
+  forall s t, ~ (le s t /\ strictly_greater s t).
+
+(** The detector contract: [f_detect_drift score threshold = true]
+    iff [score > threshold]. The Rust source implements this with
+    an [if score > threshold] guard at lib.rs line 419. *)
+Axiom detector_iff_threshold :
+  forall s t, f_detect_drift s t = true <-> strictly_greater s t.
+
+(** D2 soundness: a positive detector signal implies threshold is
+    strictly exceeded (no false positives at the comparison boundary). *)
+Theorem detect_drift_sound :
+  forall s t, f_detect_drift s t = true -> strictly_greater s t.
+Proof.
+  intros s t Hdet. apply detector_iff_threshold. exact Hdet.
+Qed.
+
+(** D2 completeness: a negative detector signal implies the score is
+    within threshold (no false negatives at the comparison boundary). *)
+Theorem detect_drift_complete :
+  forall s t, f_detect_drift s t = false -> le s t.
+Proof.
+  intros s t Hdet.
+  destruct (le_or_gt s t) as [Hle | Hgt].
+  - exact Hle.
+  - exfalso.
+    apply detector_iff_threshold in Hgt.
+    rewrite Hgt in Hdet. discriminate.
+Qed.
+
 (** ** Print Assumptions guard
 
     Each theorem must close under the global context. The whitelist
     in the CI workflow allows: score, zero, one, le, clamp, le_refl,
-    clamp_lower, clamp_upper, and the 9 [f_*_drift] parameters. *)
+    clamp_lower, clamp_upper, the 9 [f_*_drift] parameters, plus
+    [f_detect_drift], [strictly_greater], [strictly_greater_iff_not_le],
+    [detector_iff_threshold], [classic_le] (D2 additions). *)
 
 Print Assumptions clamped_in_unit_interval.
 Print Assumptions semantic_vector_drift_in_unit_interval.
 Print Assumptions quality_drift_octad_in_unit_interval.
+Print Assumptions detect_drift_sound.
+Print Assumptions detect_drift_complete.
diff --git a/formal/Justfile b/formal/Justfile
@@ -12,7 +12,7 @@
 COQC := "coqc"
 
 # Compile every proof module.
-all: provenance drift transaction
+all: provenance drift transaction planner
 
 # --- Per-module compile recipes -------------------------------------------
 
@@ -25,11 +25,14 @@ drift:
 transaction:
     {{COQC}} -q Transaction.v | tee Transaction.out
 
+planner:
+    {{COQC}} -q Planner.v | tee Planner.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-assumptions: check-provenance check-drift check-transaction check-planner
 
 check-provenance: provenance
     @awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Provenance.out \
@@ -44,11 +47,11 @@ check-provenance: provenance
 check-drift: drift
     @awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Drift.out \
       | sort -u \
-      | grep -vE '^(score|zero|one|le|clamp|le_refl|clamp_lower|clamp_upper|f_semantic_vector_drift|f_graph_document_drift|f_temporal_consistency_drift|f_tensor_drift|f_provenance_drift|f_spatial_drift|f_schema_drift|f_quality_drift|f_quality_drift_octad)$' \
+      | grep -vE '^(score|zero|one|le|clamp|le_refl|clamp_lower|clamp_upper|f_semantic_vector_drift|f_graph_document_drift|f_temporal_consistency_drift|f_tensor_drift|f_provenance_drift|f_spatial_drift|f_schema_drift|f_quality_drift|f_quality_drift_octad|f_detect_drift|strictly_greater|le_or_gt|le_gt_exclusive|detector_iff_threshold)$' \
       | { if read -r line; then \
             echo "ERROR(Drift): unexpected axiom: $line"; cat; exit 1; \
           else \
-            echo "OK(Drift): whitelisted Parameters + 9 drift fns"; \
+            echo "OK(Drift): D1 (9 fns) + D2 (detector iff threshold) whitelisted"; \
           fi; }
 
 check-transaction: transaction
@@ -60,6 +63,16 @@ check-transaction: transaction
             echo "OK(Transaction): 3 theorems closed under global context (0 axioms)"; \
           fi; }
 
+check-planner: planner
+    @awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Planner.out \
+      | sort -u \
+      | grep -vE '^(modality|condition|optimize|optimize_is_permutation)$' \
+      | { if read -r line; then \
+            echo "ERROR(Planner): unexpected axiom: $line"; cat; exit 1; \
+          else \
+            echo "OK(Planner): Q1-lite 3 theorems x 4 axioms whitelisted"; \
+          fi; }
+
 # Remove all build artefacts.
 clean:
     rm -f *.vo *.vos *.vok *.glob .*.aux *.out
diff --git a/formal/Planner.v b/formal/Planner.v
@@ -0,0 +1,106 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
+
+(** * VeriSimDB Planner — Logical/Physical Plan Equivalence (Q1-lite)
+
+    Mechanises Q1 [planner_logical_physical_equivalence] for the query
+    planner in [rust-core/verisim-planner/src/optimizer.rs].
+
+    Audit finding (verisimdb#77, recorded in PR #90 description): the
+    optimizer is a deterministic single-pass [stable_sort_by] over the
+    logical plan nodes, ordered by [Modality::execution_priority] with
+    cost as a tie-breaker. Nodes are mapped 1:1 to physical steps;
+    [conditions] are preserved verbatim as [pushed_predicates].
+
+    Full Q1 (semantic equivalence: same input data yields same result
+    set under logical vs physical) is MODERATE — blocked on
+    formalising the semantics of [Similarity] (HNSW k-NN),
+    [Traversal] (graph reachability), and [ProofVerification]. See
+    verisimdb#77 Q1 row. This module proves the STRUCTURAL preservation
+    direction: optimize is a permutation. Semantic equivalence then
+    follows once per-operator semantics are formalised.
+
+    Declared axiom: [optimize_is_permutation]. This is a structural
+    contract on the Rust optimizer enforced by inspection of
+    [Planner::optimize] (no node insertion, no node deletion, only
+    reordering via [Vec::sort_by]). A property test added alongside
+    Provenance.v's chain-link integrity check would exercise this in
+    Rust.
+
+    Tracking issue: hyperpolymath/verisimdb#77.
+*)
+
+Require Import Coq.Lists.List.
+Require Import Coq.Sorting.Permutation.
+Import ListNotations.
+
+(** ** Domain *)
+
+(** Opaque modality and condition types. Mirrors [crate::Modality]
+    and [crate::plan::Condition] in the Rust source. *)
+Parameter modality : Type.
+Parameter condition : Type.
+
+(** A plan node is a (modality, condition list) pair. *)
+Definition node : Type := (modality * list condition)%type.
+
+(** A logical plan is a list of nodes. *)
+Definition logical_plan : Type := list node.
+
+(** A physical plan, at this layer of abstraction, has the same
+    shape — each step records its modality and the conditions it
+    pushes down. The Rust [PhysicalPlan.steps] enriches each step
+    with cost and an optimization hint; those are orthogonal to the
+    structural-preservation property below. *)
+Definition physical_plan : Type := list node.
+
+(** ** Optimizer contract
+
+    The optimizer is a permutation: it reorders the input nodes but
+    neither adds nor drops any. *)
+Parameter optimize : logical_plan -> physical_plan.
+
+Axiom optimize_is_permutation :
+  forall lp, Permutation lp (optimize lp).
+
+(** ** Q1-lite corollaries *)
+
+(** Q1-lite (a): the optimizer preserves node count. *)
+Theorem planner_preserves_node_count :
+  forall lp, length lp = length (optimize lp).
+Proof.
+  intros lp. apply Permutation_length. apply optimize_is_permutation.
+Qed.
+
+(** Q1-lite (b): every node in the logical plan appears in the
+    physical plan, and vice versa. *)
+Theorem planner_preserves_membership :
+  forall lp (n : node),
+    In n lp <-> In n (optimize lp).
+Proof.
+  intros lp n. split.
+  - intros H. eapply Permutation_in.
+    + apply optimize_is_permutation.
+    + exact H.
+  - intros H. eapply Permutation_in.
+    + apply Permutation_sym. apply optimize_is_permutation.
+    + exact H.
+Qed.
+
+(** Q1-lite (c): the multiset of nodes is preserved. This is the
+    strongest structural property short of pointwise equivalence —
+    same nodes, possibly reordered. *)
+Theorem planner_preserves_multiset :
+  forall lp, Permutation lp (optimize lp).
+Proof.
+  intros lp. apply optimize_is_permutation.
+Qed.
+
+(** ** Print Assumptions guard
+
+    Allowed axioms/parameters: modality, condition, optimize,
+    optimize_is_permutation. Anything else fails the CI guard. *)
+
+Print Assumptions planner_preserves_node_count.
+Print Assumptions planner_preserves_membership.
+Print Assumptions planner_preserves_multiset.
