feat(formal): discharge optimize_is_permutation — axiom to theorem, in both modules

.github/workflows/coq-build.yml

@@ -154,18 +154,26 @@ jobs:
         working-directory: formal
         run: |
           set -euo pipefail
-          # Whitelist: modality, condition, optimize, optimize_is_permutation
+          # Whitelist: condition, node_cost.
+          #
+          # Tightened 2026-07-28. Was: modality, condition, optimize,
+          # optimize_is_permutation. `optimize_is_permutation` is now a Theorem
+          # discharged from Coq.Sorting.Mergesort's Permuted_sort, and both
+          # `modality` and `optimize` are concrete definitions, so all three
+          # must NOT reappear here. Re-adding any of them would let the axiom
+          # come back silently -- this list is the acceptance test for that
+          # work, not bookkeeping.
           UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Planner.out \
             | sort -u \
-            | grep -vE '^(modality|condition|optimize|optimize_is_permutation)$' || true)
+            | grep -vE '^(condition|node_cost)$' || 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"
+          echo "OK(Planner): Q1-lite 3 theorems x 2 parameters whitelisted (0 propositional axioms)"
 
       - name: Verify WAL assumptions whitelist
         working-directory: formal
@@ -219,7 +227,7 @@ jobs:
           set -euo pipefail
           UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' PlannerSemantic.out \
             | sort -u \
-            | grep -vE '^(modality|condition|octad|exec_node|exec_node_comm|optimize|optimize_is_permutation)$' || true)
+            | grep -vE '^(condition|node_cost|octad|exec_node|exec_node_comm)$' || true)
           if [ -n "$UNEXPECTED" ]; then
             echo "ERROR(PlannerSemantic): unexpected axiom(s):"
             echo "$UNEXPECTED"

formal/Justfile

@@ -37,7 +37,7 @@ normalizer:
 vcl:
     {{COQC}} -q VCL.v > VCL.out
 
-planner-semantic:
+planner-semantic: planner
     {{COQC}} -q PlannerSemantic.v > PlannerSemantic.out
 
 octad:
@@ -81,11 +81,11 @@ check-transaction: transaction
 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)$' \
+      | grep -vE '^(condition|node_cost)$' \
       | { 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"; \
+            echo "OK(Planner): Q1-lite 3 theorems x 2 parameters whitelisted (0 propositional axioms)"; \
           fi; }
 
 check-wal: wal
@@ -120,7 +120,7 @@ check-vcl: vcl
 check-planner-semantic: planner-semantic
     @awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' PlannerSemantic.out \
       | sort -u \
-      | grep -vE '^(modality|condition|octad|exec_node|exec_node_comm|optimize|optimize_is_permutation)$' \
+      | grep -vE '^(condition|node_cost|octad|exec_node|exec_node_comm)$' \
       | { if read -r line; then \
             echo "ERROR(PlannerSemantic): unexpected axiom: $line"; cat; exit 1; \
           else \

formal/Planner.v

@@ -20,18 +20,58 @@
     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.
+    [optimize_is_permutation] was an [Axiom] until 2026-07-28. It is now a
+    [Theorem]. The change matters because, as an axiom over a [Parameter]
+    [optimize], it was not merely unproven — it was *unprovable*: nothing
+    constrained [optimize], so [fun _ => []] inhabited the parameter and
+    refuted the statement. Assuming it was therefore assuming the conclusion.
+
+    The discharge replaces the parameter with a definition, which is what
+    makes the statement provable at all:
+
+      - [modality] becomes an [Inductive] mirroring [crate::Modality]'s six
+        constructors, with [execution_priority] transcribing the Rust match
+        arms exactly (verisim-planner/src/lib.rs).
+      - [optimize] becomes [Mergesort]'s [sort] over a decidable total order
+        on nodes: execution priority first, cost as tie-breaker — the same
+        key [Optimizer::optimize]'s [sort_by] comparator uses.
+      - The permutation property is then discharged by the standard library's
+        [Permuted_sort], which is itself closed under the global context.
+
+    Two [Parameter]s remain by design, and being parametric in them makes the
+    result stronger rather than weaker — the theorem holds for *any* condition
+    representation and *any* cost function:
+
+      - [condition] : the Rust [ConditionKind] has nine constructors carrying
+        [String]/[usize] payloads; none of that is relevant to a permutation.
+      - [node_cost] : abstracts [CostModel::estimate]'s [time_ms]. Modelling
+        the real cost model would constrain the theorem to one cost function
+        for no gain.
+
+    Two honest gaps between this model and the Rust, neither affecting the
+    permutation property, both worth stating rather than eliding:
+
+      - [node_cost] returns [nat]; the Rust tie-breaker is [f64] compared with
+        [partial_cmp(...).unwrap_or(Equal)]. A NaN would make that comparator
+        non-transitive and break [sort_by]'s contract. NaN is unreachable today
+        (the only division in [CostModel::estimate] is guarded and feeds
+        [selectivity], not [time_ms]) but nothing in the Rust types enforces it.
+      - The Rust [optimize] is partial — it returns [PlannerError::EmptyPlan]
+        for an empty plan — whereas [sort []] is [[]]. Total here, partial there.
+
+    Full Q1 (semantic equivalence) remains MODERATE and open; [exec_node_comm]
+    in PlannerSemantic.v is a genuine spec axiom needing per-operator semantics,
+    not something this change touches.
 
     Tracking issue: hyperpolymath/verisimdb#77.
 *)
 
 Require Import Coq.Lists.List.
 Require Import Coq.Sorting.Permutation.
+Require Import Coq.Sorting.Mergesort.
+Require Import Coq.Structures.Orders.
+Require Import Coq.Arith.PeanoNat.
+Require Import Lia.
 
 (* Keep Print Assumptions output on one line per axiom: the CI and Justfile
    guards match /^name :/ with awk, and Coq's default ~78-column wrap would
@@ -42,9 +82,38 @@ Import ListNotations.
 
 (** ** Domain *)
 
-(** Opaque modality and condition types. Mirrors [crate::Modality]
-    and [crate::plan::Condition] in the Rust source. *)
-Parameter modality : Type.
+(** [modality] mirrors [crate::Modality] (verisim-planner/src/lib.rs).
+
+    Six constructors, not the octad's eight: the planner declares its own
+    canonical enum and does not cover Provenance or Spatial, even though both
+    are full crates. That gap is real and tracked separately; this module
+    mirrors the Rust as it is rather than as it should be, because a model
+    that covered eight would no longer describe the code it validates. *)
+Inductive modality : Type :=
+  | Graph
+  | Vector
+  | Tensor
+  | Semantic
+  | Document
+  | Temporal.
+
+(** Transcribes [Modality::execution_priority] arm for arm. Lower runs
+    earlier: Temporal first (often cached), Vector/Document next (selective
+    indexes), Graph middle, Tensor moderate, Semantic last (ZKP expensive). *)
+Definition execution_priority (m : modality) : nat :=
+  match m with
+  | Temporal => 10
+  | Vector   => 20
+  | Document => 30
+  | Graph    => 40
+  | Tensor   => 50
+  | Semantic => 90
+  end.
+
+(** Conditions stay opaque. [crate::plan::ConditionKind] has nine constructors
+    (Equality, Range, Fulltext, Similarity, Traversal, AtTime,
+    ProofVerification, TensorOp, Predicate), none of whose structure bears on
+    whether the optimizer reorders or loses nodes. *)
 Parameter condition : Type.
 
 (** A plan node is a (modality, condition list) pair. *)
@@ -60,14 +129,53 @@ Definition logical_plan : Type := list node.
     structural-preservation property below. *)
 Definition physical_plan : Type := list node.
 
-(** ** Optimizer contract
+(** ** Optimizer
 
-    The optimizer is a permutation: it reorders the input nodes but
-    neither adds nor drops any. *)
-Parameter optimize : logical_plan -> physical_plan.
+    [CostModel::estimate]'s [time_ms], abstracted. See the header for why this
+    stays a [Parameter] and what the [nat]-vs-[f64] gap is. *)
+Parameter node_cost : node -> nat.
 
-Axiom optimize_is_permutation :
+(** The comparator from [Optimizer::optimize]'s [sort_by]: execution priority
+    first, total cost as tie-breaker. *)
+Definition node_leb (a b : node) : bool :=
+  if Nat.ltb (execution_priority (fst a)) (execution_priority (fst b)) then true
+  else if Nat.ltb (execution_priority (fst b)) (execution_priority (fst a)) then false
+  else Nat.leb (node_cost a) (node_cost b).
+
+(** Totality — the property [f64] with [unwrap_or(Equal)] cannot guarantee, and
+    the reason the cost carrier is [nat] here. *)
+Lemma node_leb_total : forall a b, node_leb a b = true \/ node_leb b a = true.
+Proof.
+  intros a b. unfold node_leb.
+  destruct (Nat.ltb (execution_priority (fst a)) (execution_priority (fst b))) eqn:Hab.
+  - left; reflexivity.
+  - destruct (Nat.ltb (execution_priority (fst b)) (execution_priority (fst a))) eqn:Hba.
+    + right; reflexivity.
+    + apply Nat.ltb_ge in Hab. apply Nat.ltb_ge in Hba.
+      destruct (Nat.leb_spec (node_cost a) (node_cost b)) as [H|H].
+      * left; reflexivity.
+      * right. apply Nat.leb_le. lia.
+Qed.
+
+Module PlanOrder <: TotalLeBool.
+  Definition t := node.
+  Definition leb := node_leb.
+  Infix "<=?" := leb (at level 70, no associativity).
+  Theorem leb_total : forall a1 a2, leb a1 a2 = true \/ leb a2 a1 = true.
+  Proof. exact node_leb_total. Qed.
+End PlanOrder.
+
+Module PlanSort := Sort PlanOrder.
+
+(** The optimizer: a stable mergesort under [node_leb]. *)
+Definition optimize (lp : logical_plan) : physical_plan := PlanSort.sort lp.
+
+(** The former axiom, now discharged from [Permuted_sort]. *)
+Theorem optimize_is_permutation :
   forall lp, Permutation lp (optimize lp).
+Proof.
+  intro lp. apply PlanSort.Permuted_sort.
+Qed.
 
 (** ** Q1-lite corollaries *)
 

formal/PlannerSemantic.v

@@ -50,6 +50,7 @@
 
 Require Import Coq.Lists.List.
 Require Import Coq.Sorting.Permutation.
+Require Import Planner.
 
 (* Keep Print Assumptions output on one line per axiom: the CI and Justfile
    guards match /^name :/ with awk, and Coq's default ~78-column wrap would
@@ -58,14 +59,21 @@ Set Printing Width 400.
 
 Import ListNotations.
 
-(** ** Domain (reusing Planner.v abstractions) *)
+(** ** Domain
+
+    This module said "reusing Planner.v abstractions" while in fact
+    re-declaring its own [modality], [condition], [node], [optimize] and a
+    second copy of [optimize_is_permutation]. The two files agreed only by
+    coincidence, and the duplicated axiom meant discharging it in Planner.v
+    would have left an identical assumption standing here.
+
+    It now genuinely imports Planner.v, so [modality] (an [Inductive]),
+    [node], [optimize] (a [Definition]) and the discharged
+    [optimize_is_permutation] [Theorem] all come from one place. *)
 
-Parameter modality : Type.
-Parameter condition : Type.
 Parameter octad : Type.
 
-Definition node : Type := (modality * list condition)%type.
-Definition plan : Type := list node.
+Definition plan : Type := logical_plan.
 Definition state : Type := list octad.
 
 (** ** Per-node execution semantics
@@ -93,12 +101,12 @@ Fixpoint exec_plan (p : plan) (s : state) : state :=
   | n :: rest => exec_plan rest (exec_node n s)
   end.
 
-(** ** Optimizer (axiomatised from Planner.v) *)
-
-Parameter optimize : plan -> plan.
+(** ** Optimizer
 
-Axiom optimize_is_permutation :
-  forall p, Permutation p (optimize p).
+    Imported from Planner.v, where [optimize] is [Mergesort]'s [sort] under a
+    decidable total order and [optimize_is_permutation] is a [Theorem]
+    discharged from [Permuted_sort]. Previously both were re-declared here as
+    a [Parameter] and an [Axiom]. *)
 
 (** ** Helper: exec_plan is invariant under permutation of nodes *)
 Theorem exec_plan_perm_invariant :