proofs: declare the strict flag set in every module

src/EpistemicTypes/Access.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.Access where
 

src/EpistemicTypes/All.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.All where
 

src/EpistemicTypes/Applications/IntegerModel.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Applications / IntegerModel
 --

src/EpistemicTypes/Applications/OrderedGroup.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Applications / OrderedGroup
 --

src/EpistemicTypes/Applications/QCriterion.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Applications / QCriterion
 --

src/EpistemicTypes/Applications/RapidNJExamples.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Applications / RapidNJExamples
 --

src/EpistemicTypes/Applications/RapidNJSkip.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Applications / RapidNJSkip
 --

src/EpistemicTypes/Applications/SortedRow.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Applications / SortedRow
 --

src/EpistemicTypes/Base.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.Base where
 

src/EpistemicTypes/ContinuityExamples.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.ContinuityExamples where
 

src/EpistemicTypes/EchoBridge.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.EchoBridge where
 

src/EpistemicTypes/Examples.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.Examples where
 

src/EpistemicTypes/Kripke/Belief.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 --

src/EpistemicTypes/Kripke/Dependence.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 --

src/EpistemicTypes/Kripke/Frame.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 --

src/EpistemicTypes/Kripke/Indexed.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 --

src/EpistemicTypes/Kripke/Residual.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 --

src/EpistemicTypes/ProofTransport.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Proof statuses carry a successful check and entail a caller-supplied meaning.
 -- Soundness is relative to Meaning and the verifier's explicit soundness proof.

src/EpistemicTypes/ProofTransportExample.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Executable Boolean certificate checks, semantic soundness, and countercases.
 -- ArtifactIsTrue means a Boolean equality, not that a physical action occurred.

src/EpistemicTypes/ReadConsistency.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.ReadConsistency where
 

src/EpistemicTypes/SurrealBridge.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.SurrealBridge where
 

src/EpistemicTypes/Warrant.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.Warrant where
 

tests/check-proofs.sh

@@ -9,6 +9,6 @@ mapfile -t modules < <(find src/EpistemicTypes -name '*.agda' | sort)
 [[ ${#modules[@]} -gt 0 ]] || { echo 'FAIL: no proof modules'; exit 1; }
 for module in "${modules[@]}"; do
   agda --no-libraries --safe --without-K --double-check --ignore-interfaces \
-    -W error -i src "$module"
+    -W error -W noUnsupportedIndexedMatch -i src "$module"
 done
 printf 'PASS: %s source modules checked under the required proof discipline\n' "${#modules[@]}"

tests/check-rejections.sh

@@ -12,7 +12,7 @@ actual_files=$(rg --files tests/reject -g '*.agda' | sort)
 [[ "$actual_files" == "$expected_files" ]] || { echo 'FAIL: rejection manifest differs from files'; exit 1; }
 for fixture in "${fixtures[@]}"; do
   status=0
-  diagnostic=$(agda --no-libraries --safe --without-K --double-check --ignore-interfaces -W error \
+  diagnostic=$(agda --no-libraries --safe --without-K --double-check --ignore-interfaces -W error -W noUnsupportedIndexedMatch \
     -i src -i tests/reject "tests/reject/$fixture.agda" 2>&1) || status=$?
   if [[ "$status" -eq 0 ]]; then
     printf 'FAIL: %s unexpectedly type-checked\n' "$fixture"

tests/reject/BeliefIsKnowledge.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 module BeliefIsKnowledge where

tests/reject/FakeFreshness.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module FakeFreshness where
 open import Agda.Builtin.Equality
 open import EpistemicTypes.ReadConsistency

tests/reject/ForgedAcceptance.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module ForgedAcceptance where
 open import Agda.Builtin.Bool using (true; false)
 open import Agda.Builtin.Equality using (refl)

tests/reject/ForgedResidue.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module ForgedResidue where
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Equality

tests/reject/ForkedHistory.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module ForkedHistory where
 open import EpistemicTypes.ReadConsistency
 import EpistemicTypes.ContinuityExamples as Examples

tests/reject/InventedMigration.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module InventedMigration where
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Equality

tests/reject/LyingVerifier.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module LyingVerifier where
 open import Agda.Builtin.Bool using (true; false)
 open import Agda.Builtin.Equality using (refl)

tests/reject/MismatchedSource.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module MismatchedSource where
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Equality

tests/reject/ReplayedArtifact.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module ReplayedArtifact where
 open import Agda.Builtin.Bool using (false)
 open import EpistemicTypes.ProofTransportExample using (Agent; Claim; Artifact; Meaning; Payload; Alice; ArtifactIsTrue; aliceProof)

tests/reject/ReplayedHolder.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module ReplayedHolder where
 open import Agda.Builtin.Bool using (true)
 open import EpistemicTypes.ProofTransportExample using (Bob; ArtifactIsTrue; module HolderBoundary)

tests/reject/StaleSample.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module StaleSample where
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Equality

tests/reject/UncheckedSkip.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- Rejection control: a skip whose check was not accepted.
 --
 -- The four-taxon scan below is unscannable past its cursor.  With r = 4

tests/reject/UnderstatedBound.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module UnderstatedBound where
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Nat