From 6e10d9d04aefe1b80ead05e4a767b67b7a5010f9 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 19:29:50 +0100 Subject: [PATCH 1/2] docs(formal): remove the duplicated Set Printing Width comment (9 modules) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #202 landed the same three-line explanatory comment twice in every module — once above `Set Printing Width 400.` where it belongs, and once orphaned immediately below it. My fault: I ran the insertion, then deleted only the `Set Printing Width 400.` line to A/B-test whether the ~78-column wrap was actually hiding any axiom from the guard, then re-ran the insertion. The sed that undid the test matched only the directive, not its comment, so the second pass stacked a fresh copy on top of the leftover. Comment-only; no directive, no proof and no guard changes. `formal/Justfile` is untouched. To be accurate about scope, since the obvious worry is that a text edit near the imports clipped something: it did not. `Import ListNotations.` and every `Require Import` are intact in all nine modules — verified before and after. (A *different* cleanup attempt of mine did briefly eat that import by skipping a fixed three lines past the marker, which in `Planner.v` overran the comment. That version was reset and never committed; it is mentioned only so the next person knows the offset-based approach is the wrong tool here. This commit removes the second matched block specifically, keyed on occurrence count.) Verified: real coqc 8.20.1 -> `check-assumptions` exits 0, 9/9 OK; stub coqc -> exit 127, so the gate from #202 still fails when it should; `Normalizer.out` still prints at 157 columns, so the wrap fix is unaffected; `reuse lint` compliant. --- formal/Drift.v | 3 --- formal/Normalizer.v | 3 --- formal/Octad.v | 3 --- formal/Planner.v | 3 --- formal/PlannerSemantic.v | 3 --- formal/Provenance.v | 3 --- formal/Transaction.v | 3 --- formal/VCL.v | 3 --- formal/WAL.v | 3 --- 9 files changed, 27 deletions(-) diff --git a/formal/Drift.v b/formal/Drift.v index d9730be..6d7ce59 100644 --- a/formal/Drift.v +++ b/formal/Drift.v @@ -32,9 +32,6 @@ Require Import Coq.Init.Logic. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* 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 - split a longer axiom type across lines and silently escape the check. *) (** ** Domain *) diff --git a/formal/Normalizer.v b/formal/Normalizer.v index b86c7d6..0d7dadd 100644 --- a/formal/Normalizer.v +++ b/formal/Normalizer.v @@ -52,9 +52,6 @@ Require Import Coq.Bool.Bool. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* 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 - split a longer axiom type across lines and silently escape the check. *) (** ** Domain *) diff --git a/formal/Octad.v b/formal/Octad.v index cf4154f..f3f13e3 100644 --- a/formal/Octad.v +++ b/formal/Octad.v @@ -95,9 +95,6 @@ Require Import Coq.Logic.FunctionalExtensionality. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* 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 - split a longer axiom type across lines and silently escape the check. *) Import ListNotations. (** ** [def:modset] — Modality Set diff --git a/formal/Planner.v b/formal/Planner.v index 093eb6a..56e9072 100644 --- a/formal/Planner.v +++ b/formal/Planner.v @@ -38,9 +38,6 @@ Require Import Coq.Sorting.Permutation. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* 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 - split a longer axiom type across lines and silently escape the check. *) Import ListNotations. (** ** Domain *) diff --git a/formal/PlannerSemantic.v b/formal/PlannerSemantic.v index 81cf126..95fe4b9 100644 --- a/formal/PlannerSemantic.v +++ b/formal/PlannerSemantic.v @@ -56,9 +56,6 @@ Require Import Coq.Sorting.Permutation. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* 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 - split a longer axiom type across lines and silently escape the check. *) Import ListNotations. (** ** Domain (reusing Planner.v abstractions) *) diff --git a/formal/Provenance.v b/formal/Provenance.v index 8caaefd..7bb1bfb 100644 --- a/formal/Provenance.v +++ b/formal/Provenance.v @@ -41,9 +41,6 @@ Require Import Coq.Lists.List. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* 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 - split a longer axiom type across lines and silently escape the check. *) Import ListNotations. (** ** Domain *) diff --git a/formal/Transaction.v b/formal/Transaction.v index b100dc6..1753771 100644 --- a/formal/Transaction.v +++ b/formal/Transaction.v @@ -43,9 +43,6 @@ Require Import Coq.Init.Logic. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* 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 - split a longer axiom type across lines and silently escape the check. *) (** ** Domain *) diff --git a/formal/VCL.v b/formal/VCL.v index 4530de9..86db14b 100644 --- a/formal/VCL.v +++ b/formal/VCL.v @@ -48,9 +48,6 @@ Require Import Coq.Init.Logic. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* 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 - split a longer axiom type across lines and silently escape the check. *) (** ** Syntax *) diff --git a/formal/WAL.v b/formal/WAL.v index 4df1c67..ec7b890 100644 --- a/formal/WAL.v +++ b/formal/WAL.v @@ -51,9 +51,6 @@ Require Import Coq.Logic.FunctionalExtensionality. split a longer axiom type across lines and silently escape the check. *) Set Printing Width 400. -(* 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 - split a longer axiom type across lines and silently escape the check. *) Import ListNotations. (** ** Domain *) From 7be83ed6230a4b5ab59769046576854119194f45 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 19:43:00 +0100 Subject: [PATCH 2/2] =?UTF-8?q?feat(formal):=20discharge=20optimize=5Fis?= =?UTF-8?q?=5Fpermutation=20=E2=80=94=20axiom=20to=20theorem,=20in=20both?= =?UTF-8?q?=20modules?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `optimize_is_permutation` was an `Axiom` in `formal/Planner.v` and, separately, a second identical `Axiom` in `formal/PlannerSemantic.v`. Both are now gone. **It was not merely unproven — it was unprovable.** `optimize` was a `Parameter`, so nothing constrained it: `fun _ => []` inhabits the parameter and refutes `forall lp, Permutation lp (optimize lp)`. Assuming the statement was assuming the conclusion, and no amount of proof effort against that signature would have worked. Discharging it *requires* replacing the parameter with a definition, which is what this does: * `modality` becomes an `Inductive` with the six constructors of `crate::Modality`, and `execution_priority` transcribes the Rust match arms (Temporal 10, Vector 20, Document 30, Graph 40, Tensor 50, Semantic 90). * `optimize` becomes `Coq.Sorting.Mergesort`'s `sort` under `node_leb` — execution priority first, cost as tie-breaker, i.e. the key `Optimizer::optimize`'s `sort_by` comparator actually uses. * The permutation property falls out of the standard library's `Permuted_sort`, which is itself closed under the global context. All five call sites were left untouched and still compile: the theorem statement is character-for-character what the axiom asserted. `PlannerSemantic.v` claimed in a comment to be "reusing Planner.v abstractions" while in fact re-declaring its own `modality`, `condition`, `node`, `optimize` and a duplicate axiom. The two files agreed only by coincidence, and the duplicate meant discharging Planner's axiom would have left an identical assumption standing next door. It now genuinely `Require Import Planner`, and `formal/Justfile` gains the `planner-semantic: planner` dependency edge that this makes necessary. **Whitelists tightened — this is the acceptance test, not bookkeeping.** The guards enforce "exactly these assumptions", never "no assumptions", so leaving `optimize_is_permutation` listed would have let it return silently: * Planner: `modality|condition|optimize|optimize_is_permutation` -> `condition|node_cost` * PlannerSemantic: drops `modality`, `optimize`, `optimize_is_permutation` Both `formal/Justfile` and `.github/workflows/coq-build.yml` updated together. Two `Parameter`s remain **by design**, and being parametric in them makes the result stronger, not weaker — it holds for *any* condition representation and *any* cost function: `condition` (the Rust `ConditionKind`'s nine constructors are irrelevant to whether nodes are reordered or lost) and `node_cost` (abstracts `CostModel::estimate`'s `time_ms`). Two honest model-vs-code gaps, both recorded in the module header rather than elided, neither affecting the permutation property: * `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 violate `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 that. * Rust `optimize` is partial (`PlannerError::EmptyPlan`); `sort []` is `[]`. `exec_node_comm` deliberately stays. It is a genuine spec axiom over an uninterpreted `exec_node` and needs per-operator semantics to discharge — not something this change touches, and it should not look like collateral. Verified: * Clean build: `just -f formal/Justfile all` and `check-assumptions` both exit 0, 9/9 OK, with the tightened whitelists. * `optimize_is_permutation` appears zero times in either module's `Print Assumptions` output, and no `Axiom optimize_is_permutation` remains anywhere (was 2). * **Negative control** — reintroducing an axiom a theorem depends on is caught: `ERROR(Planner): unexpected axiom: sneaky_regression`, gate exit 1. The tightened whitelist genuinely fails rather than passing vacuously. * Stub `coqc` still drives the gate to exit 127, so #202's fix is intact. * `reuse lint` compliant. --- .github/workflows/coq-build.yml | 16 +++- formal/Justfile | 8 +- formal/Planner.v | 136 ++++++++++++++++++++++++++++---- formal/PlannerSemantic.v | 28 ++++--- 4 files changed, 156 insertions(+), 32 deletions(-) diff --git a/.github/workflows/coq-build.yml b/.github/workflows/coq-build.yml index 84a137d..410fac9 100644 --- a/.github/workflows/coq-build.yml +++ b/.github/workflows/coq-build.yml @@ -154,10 +154,18 @@ 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" @@ -165,7 +173,7 @@ jobs: 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" diff --git a/formal/Justfile b/formal/Justfile index bc4eef6..8c8da8a 100644 --- a/formal/Justfile +++ b/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 \ diff --git a/formal/Planner.v b/formal/Planner.v index 56e9072..720eecd 100644 --- a/formal/Planner.v +++ b/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 *) diff --git a/formal/PlannerSemantic.v b/formal/PlannerSemantic.v index 95fe4b9..a58d157 100644 --- a/formal/PlannerSemantic.v +++ b/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 :