fix(formal): make the local Coq assumptions gate capable of failing (#202)

fix(formal): make the local Coq assumptions gate capable of failing

`just -f formal/Justfile check-assumptions` returned 0 whether or not
anything compiled, so a green local proof gate was not evidence of a
proof. Demonstrated by putting a stub `coqc` that exits 127 on PATH:

    $ PATH=/tmp/fakebin:$PATH just -f formal/Justfile check-planner
    coqc: not found
    OK(Planner): Q1-lite 3 theorems x 4 axioms whitelisted
    exit=0

Cause: every compile recipe was `coqc -q X.v | tee X.out`. A pipeline's
exit status is its *last* command's, so `just` saw `tee`'s 0 and moved
on; `coqc`'s diagnostics go to stderr, which `tee` never captures. The
guard then ran awk over an empty `X.out`, found no axioms, and reported
OK.

Fixed by redirecting instead of piping: `coqc -q X.v > X.out`. The exit
status is now `coqc`'s and `just` aborts the recipe.

Note this is deliberately NOT fixed with `set shell := [... "pipefail"
...]`.
The guards are shaped `awk | sort -u | grep -vE '<whitelist>' | { ...
}`,
and `grep -v` exits 1 precisely when it filters everything out — i.e. on
the success path, where every axiom is whitelisted. Enabling pipefail
would turn every passing check into a failure.
`.github/workflows/coq-build.yml`
already handles this correctly (`set -euo pipefail` *and* `|| true` on
each
grep), so CI was never affected; this was a local-only divergence.

Also adds `Set Printing Width 400.` to all nine modules. Both the CI and
Justfile guards match axiom names with `awk '/^[A-Za-z_][A-Za-z0-9_]*
:/'`,
which only fires when the name and its colon share a line. Coq wraps at
~78 columns and `Planner.out`'s longest line was **77** — one character
from silently escaping the check. With the directive, statements print
in
full (Normalizer 75 -> 157, WAL 62 -> 127, Octad 62 -> 127,
PlannerSemantic
74 -> 113, Drift 72 -> 95).

To be precise about what this did and did not find: comparing the axiom
names visible to the guard with and without the directive shows **no
difference today**. Nothing was being hidden; this closes a latent
escape
before it opens, it does not fix an active one.

Verified: with a broken `coqc` the gate now exits 127 ("recipe `planner`
failed on line 29"); with the real coqc 8.20.1 all nine modules compile
and
`check-assumptions` exits 0 with 9/9 OK lines. `reuse lint` still
compliant.

Author: hyperpolymath

formal/Drift.v

@@ -27,6 +27,15 @@
 
 Require Import Coq.Init.Logic.
 
+(* 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. *)
+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 *)
 
 (** Opaque score type. In the Rust source this is [f64]. *)

formal/Justfile

@@ -17,31 +17,31 @@ all: provenance drift transaction planner wal normalizer vcl planner-semantic oc
 # --- Per-module compile recipes -------------------------------------------
 
 provenance:
-    {{COQC}} -q Provenance.v | tee Provenance.out
+    {{COQC}} -q Provenance.v > Provenance.out
 
 drift:
-    {{COQC}} -q Drift.v | tee Drift.out
+    {{COQC}} -q Drift.v > Drift.out
 
 transaction:
-    {{COQC}} -q Transaction.v | tee Transaction.out
+    {{COQC}} -q Transaction.v > Transaction.out
 
 planner:
-    {{COQC}} -q Planner.v | tee Planner.out
+    {{COQC}} -q Planner.v > Planner.out
 
 wal:
-    {{COQC}} -q WAL.v | tee WAL.out
+    {{COQC}} -q WAL.v > WAL.out
 
 normalizer:
-    {{COQC}} -q Normalizer.v | tee Normalizer.out
+    {{COQC}} -q Normalizer.v > Normalizer.out
 
 vcl:
-    {{COQC}} -q VCL.v | tee VCL.out
+    {{COQC}} -q VCL.v > VCL.out
 
 planner-semantic:
-    {{COQC}} -q PlannerSemantic.v | tee PlannerSemantic.out
+    {{COQC}} -q PlannerSemantic.v > PlannerSemantic.out
 
 octad:
-    {{COQC}} -q Octad.v | tee Octad.out
+    {{COQC}} -q Octad.v > Octad.out
 
 # --- Whitelist guards -----------------------------------------------------
 # Each module declares its own set of Parameters/Axioms; the guard greps

formal/Normalizer.v

@@ -47,6 +47,15 @@
 Require Import Coq.Logic.FunctionalExtensionality.
 Require Import Coq.Bool.Bool.
 
+(* 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. *)
+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 *)
 
 Parameter modality : Type.

formal/Octad.v

@@ -89,6 +89,15 @@
 Require Import Coq.Lists.List.
 Require Import Coq.Bool.Bool.
 Require Import Coq.Logic.FunctionalExtensionality.
+
+(* 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. *)
+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

formal/Planner.v

@@ -32,6 +32,15 @@
 
 Require Import Coq.Lists.List.
 Require Import Coq.Sorting.Permutation.
+
+(* 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. *)
+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 *)

formal/PlannerSemantic.v

@@ -50,6 +50,15 @@
 
 Require Import Coq.Lists.List.
 Require Import Coq.Sorting.Permutation.
+
+(* 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. *)
+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) *)

formal/Provenance.v

@@ -35,6 +35,15 @@
 *)
 
 Require Import Coq.Lists.List.
+
+(* 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. *)
+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 *)

formal/Transaction.v

@@ -38,6 +38,15 @@
 
 Require Import Coq.Init.Logic.
 
+(* 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. *)
+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 *)
 
 Inductive txn_state : Type :=

formal/VCL.v

@@ -43,6 +43,15 @@
 
 Require Import Coq.Init.Logic.
 
+(* 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. *)
+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 *)
 
 Inductive ty : Type :=

formal/WAL.v

@@ -45,6 +45,15 @@
 
 Require Import Coq.Lists.List.
 Require Import Coq.Logic.FunctionalExtensionality.
+
+(* 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. *)
+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 *)