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

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 *)