From f4600da71278ca2b45934d811402af09394b0d17 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 03:37:58 +0000 Subject: [PATCH] proofs: declare the strict flag set in every module that can take it Adds --cubical-compatible --exact-split --no-sized-types --no-guardedness to the OPTIONS pragma of 141 modules, keeping --safe --without-K. #355 made the code compatible; this declares it, so downstream repos that adopt the strict set (choreographic-types, through experimental/echo-additive/Grade.agda) can import these modules: --cubical-compatible is coinfective. Left unchanged, for these reasons: - EchoCNOBridge, EchoThermodynamicsArbitrary: import absolute-zero's CNO, which does not declare --cubical-compatible yet. - All, Smoke: import those two. - EchoImageFactorizationPropCubical (--cubical island) and EchoImageFactorizationPropPostulated (quarantined postulate): exempt. scripts/kernel-guard.sh: the safety-relaxing-flag check matched `--cubical` inside `--cubical-compatible`. It now matches whole flags only. Planting --cubical, --sized-types or --guardedness in Echo.agda still fails it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- proofs/agda/AntiEcho.agda | 2 +- proofs/agda/AntiEchoTropical.agda | 2 +- proofs/agda/AntiEchoTropicalGeneric.agda | 2 +- proofs/agda/Dyadic.agda | 2 +- proofs/agda/DyadicEchoBridge.agda | 2 +- proofs/agda/Echo.agda | 2 +- proofs/agda/Echo/Index/ThinPoset.agda | 2 +- proofs/agda/Echo/Measure/Examples.agda | 2 +- proofs/agda/Echo/Measure/Interface.agda | 2 +- proofs/agda/Echo/Modality/Core.agda | 2 +- proofs/agda/Echo/Modality/Interface.agda | 2 +- proofs/agda/Echo/Separation/NotResourceInstance.agda | 2 +- proofs/agda/EchoAbstractionBarrier.agda | 2 +- proofs/agda/EchoAccess.agda | 2 +- proofs/agda/EchoAggregation.agda | 2 +- proofs/agda/EchoApprox.agda | 2 +- proofs/agda/EchoApproxInstance.agda | 2 +- proofs/agda/EchoBitNarrowingNumeric.agda | 2 +- proofs/agda/EchoCanonicalIdentitySuite.agda | 2 +- proofs/agda/EchoCategorical.agda | 2 +- proofs/agda/EchoCharacteristic.agda | 2 +- proofs/agda/EchoChoreo.agda | 2 +- proofs/agda/EchoCost.agda | 2 +- proofs/agda/EchoCostInstance.agda | 2 +- proofs/agda/EchoDecidable.agda | 2 +- proofs/agda/EchoDecorationBridge.agda | 2 +- proofs/agda/EchoDecorationStructure.agda | 2 +- proofs/agda/EchoDeniability.agda | 2 +- proofs/agda/EchoDifferential.agda | 2 +- proofs/agda/EchoDisplayed.agda | 2 +- proofs/agda/EchoEntropy.agda | 2 +- proofs/agda/EchoEphapaxBridge.agda | 2 +- proofs/agda/EchoEpistemic.agda | 2 +- proofs/agda/EchoEpistemicResidue.agda | 2 +- proofs/agda/EchoExampleAbsInt.agda | 2 +- proofs/agda/EchoExampleBitNarrowing.agda | 2 +- proofs/agda/EchoExampleParser.agda | 2 +- proofs/agda/EchoExampleProvenance.agda | 2 +- proofs/agda/EchoExampleSignAnalysis.agda | 2 +- proofs/agda/EchoExampleTruncation.agda | 2 +- proofs/agda/EchoExamples.agda | 2 +- proofs/agda/EchoFiberBridge.agda | 2 +- proofs/agda/EchoFiberCount.agda | 2 +- proofs/agda/EchoFiberTriangulation.agda | 2 +- proofs/agda/EchoFidelity.agda | 2 +- proofs/agda/EchoGraded.agda | 2 +- proofs/agda/EchoGradedComonad.agda | 2 +- proofs/agda/EchoGradedComonadF1.agda | 2 +- proofs/agda/EchoGradedComonadInstance1.agda | 2 +- proofs/agda/EchoGradedComonadInstance2.agda | 2 +- proofs/agda/EchoGradedComonadInterface.agda | 2 +- proofs/agda/EchoHaplotypeCollapsing.agda | 2 +- proofs/agda/EchoImageFactorization.agda | 2 +- proofs/agda/EchoImageFactorizationProp.agda | 2 +- proofs/agda/EchoIndexed.agda | 2 +- proofs/agda/EchoIntegration.agda | 2 +- proofs/agda/EchoJanusBridge.agda | 2 +- proofs/agda/EchoKernel.agda | 2 +- proofs/agda/EchoLLEncoding.agda | 2 +- proofs/agda/EchoLinear.agda | 2 +- proofs/agda/EchoLossTaxonomy.agda | 2 +- proofs/agda/EchoNoSectionGeneric.agda | 2 +- proofs/agda/EchoOFSUnivF5.agda | 2 +- proofs/agda/EchoOFSUnivF5Diag.agda | 2 +- proofs/agda/EchoOFSUnivF5Iso.agda | 2 +- proofs/agda/EchoObservationalEquivalence.agda | 2 +- proofs/agda/EchoOrdinal.agda | 2 +- proofs/agda/EchoOrthogonalFactorizationSystem.agda | 2 +- proofs/agda/EchoProbabilisticSupport.agda | 2 +- proofs/agda/EchoProvenance.agda | 2 +- proofs/agda/EchoPullback.agda | 2 +- proofs/agda/EchoPullbackUnivF4.agda | 2 +- proofs/agda/EchoRelModel.agda | 2 +- proofs/agda/EchoRelational.agda | 2 +- proofs/agda/EchoResidue.agda | 2 +- proofs/agda/EchoResidueCell.agda | 2 +- proofs/agda/EchoResidueTaxonomy.agda | 2 +- proofs/agda/EchoReversibilityBridge.agda | 2 +- proofs/agda/EchoScope.agda | 2 +- proofs/agda/EchoSearch.agda | 2 +- proofs/agda/EchoSearchExample.agda | 2 +- proofs/agda/EchoSearchInstance.agda | 2 +- proofs/agda/EchoSecurity.agda | 2 +- proofs/agda/EchoSelectiveProjection.agda | 2 +- proofs/agda/EchoSeparating.agda | 2 +- proofs/agda/EchoStabilityTests.agda | 2 +- proofs/agda/EchoStepNDModelF2.agda | 2 +- proofs/agda/EchoThermoCollapseImpossible.agda | 2 +- proofs/agda/EchoThermodynamics.agda | 2 +- proofs/agda/EchoThermodynamicsFinite.agda | 2 +- proofs/agda/EchoTotalCompletion.agda | 2 +- proofs/agda/EchoTransaction.agda | 2 +- proofs/agda/EchoTropical.agda | 2 +- proofs/agda/EchoTruncation.agda | 2 +- proofs/agda/EchoVariance.agda | 2 +- proofs/agda/MinimalCNO.agda | 2 +- proofs/agda/NarrowingSmoke.agda | 2 +- proofs/agda/Ordinal/Buchholz/Syntax.agda | 2 +- proofs/agda/Ordinal/OmegaMarkers.agda | 2 +- proofs/agda/SimpleTest.agda | 2 +- proofs/agda/VecRotation.agda | 2 +- proofs/agda/WorkingCNO.agda | 2 +- proofs/agda/characteristic/All.agda | 2 +- proofs/agda/characteristic/ChoreoInjective.agda | 2 +- proofs/agda/characteristic/IntegrationAudit.agda | 2 +- proofs/agda/characteristic/InteractionTest.agda | 2 +- proofs/agda/characteristic/ModeGraded.agda | 2 +- proofs/agda/characteristic/N5Falsifier.agda | 2 +- proofs/agda/characteristic/NonTruncatable.agda | 2 +- proofs/agda/characteristic/RecipeNonTriviality.agda | 2 +- proofs/agda/characteristic/RecipeSpec.agda | 2 +- proofs/agda/characteristic/RecipeTheorem.agda | 2 +- proofs/agda/characteristic/RoleGraded.agda | 2 +- proofs/agda/characteristic/RoleMode.agda | 2 +- proofs/agda/characteristic/RoleModeGrade.agda | 2 +- proofs/agda/characteristic/RoleRole.agda | 2 +- proofs/agda/characteristic/VisibleConstraintAudit.agda | 2 +- proofs/agda/examples/All.agda | 2 +- proofs/agda/examples/EchoVsSigma.agda | 2 +- proofs/agda/examples/EpistemicUpdate.agda | 2 +- proofs/agda/examples/LinearErasure.agda | 2 +- proofs/agda/examples/Transport.agda | 2 +- proofs/agda/examples/TropicalArgmin.agda | 2 +- proofs/agda/experimental/echo-additive/All.agda | 2 +- proofs/agda/experimental/echo-additive/Grade.agda | 2 +- proofs/agda/experimental/echo-additive/GradedAdjunction.agda | 2 +- proofs/agda/experimental/echo-additive/GradedCarrier.agda | 2 +- .../experimental/echo-additive/GradedCarrierFaithful.agda | 2 +- proofs/agda/experimental/echo-additive/GradedComonad.agda | 2 +- proofs/agda/experimental/echo-additive/GradedMonad.agda | 2 +- proofs/agda/experimental/echo-additive/VarianceGate.agda | 2 +- scripts/kernel-guard.sh | 5 +++-- tutorial/All.agda | 2 +- tutorial/epistemic_erasure/All.agda | 2 +- tutorial/epistemic_erasure/EpistemicErasure.agda | 2 +- tutorial/epistemic_erasure/Smoke.agda | 2 +- tutorial/provenance_debugging/All.agda | 2 +- tutorial/provenance_debugging/ProvenanceDebugging.agda | 2 +- tutorial/provenance_debugging/Smoke.agda | 2 +- tutorial/region_exit_audit/All.agda | 2 +- tutorial/region_exit_audit/RegionExitAudit.agda | 2 +- tutorial/region_exit_audit/Smoke.agda | 2 +- 142 files changed, 144 insertions(+), 143 deletions(-) diff --git a/proofs/agda/AntiEcho.agda b/proofs/agda/AntiEcho.agda index 7760d95e..15c58599 100644 --- a/proofs/agda/AntiEcho.agda +++ b/proofs/agda/AntiEcho.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/AntiEchoTropical.agda b/proofs/agda/AntiEchoTropical.agda index 1fd01024..b6f5af9b 100644 --- a/proofs/agda/AntiEchoTropical.agda +++ b/proofs/agda/AntiEchoTropical.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/AntiEchoTropicalGeneric.agda b/proofs/agda/AntiEchoTropicalGeneric.agda index 6037945c..08e3fb1b 100644 --- a/proofs/agda/AntiEchoTropicalGeneric.agda +++ b/proofs/agda/AntiEchoTropicalGeneric.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/Dyadic.agda b/proofs/agda/Dyadic.agda index 20363e1b..8f7f61a4 100644 --- a/proofs/agda/Dyadic.agda +++ b/proofs/agda/Dyadic.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/DyadicEchoBridge.agda b/proofs/agda/DyadicEchoBridge.agda index 49ee41f3..3b5ed2fe 100644 --- a/proofs/agda/DyadicEchoBridge.agda +++ b/proofs/agda/DyadicEchoBridge.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/Echo.agda b/proofs/agda/Echo.agda index 86745cd6..1ce9cfcf 100644 --- a/proofs/agda/Echo.agda +++ b/proofs/agda/Echo.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/Echo/Index/ThinPoset.agda b/proofs/agda/Echo/Index/ThinPoset.agda index 805eb3d2..c6c579a9 100644 --- a/proofs/agda/Echo/Index/ThinPoset.agda +++ b/proofs/agda/Echo/Index/ThinPoset.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/Echo/Measure/Examples.agda b/proofs/agda/Echo/Measure/Examples.agda index 5065d80e..e169a020 100644 --- a/proofs/agda/Echo/Measure/Examples.agda +++ b/proofs/agda/Echo/Measure/Examples.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/Echo/Measure/Interface.agda b/proofs/agda/Echo/Measure/Interface.agda index 04e8dc39..e965bbbe 100644 --- a/proofs/agda/Echo/Measure/Interface.agda +++ b/proofs/agda/Echo/Measure/Interface.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/Echo/Modality/Core.agda b/proofs/agda/Echo/Modality/Core.agda index 60b6932d..d55f6784 100644 --- a/proofs/agda/Echo/Modality/Core.agda +++ b/proofs/agda/Echo/Modality/Core.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/Echo/Modality/Interface.agda b/proofs/agda/Echo/Modality/Interface.agda index 97771576..2d66ad73 100644 --- a/proofs/agda/Echo/Modality/Interface.agda +++ b/proofs/agda/Echo/Modality/Interface.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/Echo/Separation/NotResourceInstance.agda b/proofs/agda/Echo/Separation/NotResourceInstance.agda index 8b0334c6..1f056df3 100644 --- a/proofs/agda/Echo/Separation/NotResourceInstance.agda +++ b/proofs/agda/Echo/Separation/NotResourceInstance.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoAbstractionBarrier.agda b/proofs/agda/EchoAbstractionBarrier.agda index a33f52d1..038c673f 100644 --- a/proofs/agda/EchoAbstractionBarrier.agda +++ b/proofs/agda/EchoAbstractionBarrier.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoAccess.agda b/proofs/agda/EchoAccess.agda index e0e98208..5f680ad7 100644 --- a/proofs/agda/EchoAccess.agda +++ b/proofs/agda/EchoAccess.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoAggregation.agda b/proofs/agda/EchoAggregation.agda index 0b545a30..8dca6722 100644 --- a/proofs/agda/EchoAggregation.agda +++ b/proofs/agda/EchoAggregation.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoApprox.agda b/proofs/agda/EchoApprox.agda index 3a863f85..3ca4fe20 100644 --- a/proofs/agda/EchoApprox.agda +++ b/proofs/agda/EchoApprox.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoApproxInstance.agda b/proofs/agda/EchoApproxInstance.agda index 3ec3b309..c40f05dc 100644 --- a/proofs/agda/EchoApproxInstance.agda +++ b/proofs/agda/EchoApproxInstance.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoBitNarrowingNumeric.agda b/proofs/agda/EchoBitNarrowingNumeric.agda index c1931498..619991d3 100644 --- a/proofs/agda/EchoBitNarrowingNumeric.agda +++ b/proofs/agda/EchoBitNarrowingNumeric.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 -- Numeric specification for the typed-wasm-echo receipt. This proves the diff --git a/proofs/agda/EchoCanonicalIdentitySuite.agda b/proofs/agda/EchoCanonicalIdentitySuite.agda index 4f51b3bb..7b7570af 100644 --- a/proofs/agda/EchoCanonicalIdentitySuite.agda +++ b/proofs/agda/EchoCanonicalIdentitySuite.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoCategorical.agda b/proofs/agda/EchoCategorical.agda index 886f4f83..0a538dce 100644 --- a/proofs/agda/EchoCategorical.agda +++ b/proofs/agda/EchoCategorical.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoCharacteristic.agda b/proofs/agda/EchoCharacteristic.agda index 7a6ad9d3..4f18d64e 100644 --- a/proofs/agda/EchoCharacteristic.agda +++ b/proofs/agda/EchoCharacteristic.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoChoreo.agda b/proofs/agda/EchoChoreo.agda index 07446cd8..4d2c4b1a 100644 --- a/proofs/agda/EchoChoreo.agda +++ b/proofs/agda/EchoChoreo.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoCost.agda b/proofs/agda/EchoCost.agda index c37c6226..ae6adef5 100644 --- a/proofs/agda/EchoCost.agda +++ b/proofs/agda/EchoCost.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoCostInstance.agda b/proofs/agda/EchoCostInstance.agda index 4a977a10..b6dc882a 100644 --- a/proofs/agda/EchoCostInstance.agda +++ b/proofs/agda/EchoCostInstance.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoDecidable.agda b/proofs/agda/EchoDecidable.agda index 9a1e75ce..38d06e05 100644 --- a/proofs/agda/EchoDecidable.agda +++ b/proofs/agda/EchoDecidable.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoDecorationBridge.agda b/proofs/agda/EchoDecorationBridge.agda index 039ba455..ea7eec29 100644 --- a/proofs/agda/EchoDecorationBridge.agda +++ b/proofs/agda/EchoDecorationBridge.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoDecorationStructure.agda b/proofs/agda/EchoDecorationStructure.agda index 1ec753f3..e188f7b8 100644 --- a/proofs/agda/EchoDecorationStructure.agda +++ b/proofs/agda/EchoDecorationStructure.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoDeniability.agda b/proofs/agda/EchoDeniability.agda index 44599b9b..55f27d96 100644 --- a/proofs/agda/EchoDeniability.agda +++ b/proofs/agda/EchoDeniability.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoDifferential.agda b/proofs/agda/EchoDifferential.agda index f7e88331..b2fef3e4 100644 --- a/proofs/agda/EchoDifferential.agda +++ b/proofs/agda/EchoDifferential.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoDisplayed.agda b/proofs/agda/EchoDisplayed.agda index a47f2c5a..2da6ab39 100644 --- a/proofs/agda/EchoDisplayed.agda +++ b/proofs/agda/EchoDisplayed.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoEntropy.agda b/proofs/agda/EchoEntropy.agda index fc5d7c16..8e01fc1d 100644 --- a/proofs/agda/EchoEntropy.agda +++ b/proofs/agda/EchoEntropy.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoEphapaxBridge.agda b/proofs/agda/EchoEphapaxBridge.agda index e61250d4..02fab9c4 100644 --- a/proofs/agda/EchoEphapaxBridge.agda +++ b/proofs/agda/EchoEphapaxBridge.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoEpistemic.agda b/proofs/agda/EchoEpistemic.agda index 09f717cc..4a1f9bcd 100644 --- a/proofs/agda/EchoEpistemic.agda +++ b/proofs/agda/EchoEpistemic.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoEpistemicResidue.agda b/proofs/agda/EchoEpistemicResidue.agda index 245e50c0..97e0a3b7 100644 --- a/proofs/agda/EchoEpistemicResidue.agda +++ b/proofs/agda/EchoEpistemicResidue.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoExampleAbsInt.agda b/proofs/agda/EchoExampleAbsInt.agda index 4ac3174d..3f4ab49f 100644 --- a/proofs/agda/EchoExampleAbsInt.agda +++ b/proofs/agda/EchoExampleAbsInt.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoExampleBitNarrowing.agda b/proofs/agda/EchoExampleBitNarrowing.agda index 334c7cd8..d0981e8c 100644 --- a/proofs/agda/EchoExampleBitNarrowing.agda +++ b/proofs/agda/EchoExampleBitNarrowing.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 diff --git a/proofs/agda/EchoExampleParser.agda b/proofs/agda/EchoExampleParser.agda index 95fcc902..f5f9d2d8 100644 --- a/proofs/agda/EchoExampleParser.agda +++ b/proofs/agda/EchoExampleParser.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoExampleProvenance.agda b/proofs/agda/EchoExampleProvenance.agda index 6484e2f6..25a9de83 100644 --- a/proofs/agda/EchoExampleProvenance.agda +++ b/proofs/agda/EchoExampleProvenance.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoExampleSignAnalysis.agda b/proofs/agda/EchoExampleSignAnalysis.agda index ee0a3188..7b52550f 100644 --- a/proofs/agda/EchoExampleSignAnalysis.agda +++ b/proofs/agda/EchoExampleSignAnalysis.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoExampleTruncation.agda b/proofs/agda/EchoExampleTruncation.agda index 82e9407e..91f00343 100644 --- a/proofs/agda/EchoExampleTruncation.agda +++ b/proofs/agda/EchoExampleTruncation.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoExamples.agda b/proofs/agda/EchoExamples.agda index 6291a169..6c2d6a71 100644 --- a/proofs/agda/EchoExamples.agda +++ b/proofs/agda/EchoExamples.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoFiberBridge.agda b/proofs/agda/EchoFiberBridge.agda index 15b2544d..83ef2ad6 100644 --- a/proofs/agda/EchoFiberBridge.agda +++ b/proofs/agda/EchoFiberBridge.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoFiberCount.agda b/proofs/agda/EchoFiberCount.agda index 181a8159..a3a2683b 100644 --- a/proofs/agda/EchoFiberCount.agda +++ b/proofs/agda/EchoFiberCount.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoFiberTriangulation.agda b/proofs/agda/EchoFiberTriangulation.agda index b237d2bc..72c7212b 100644 --- a/proofs/agda/EchoFiberTriangulation.agda +++ b/proofs/agda/EchoFiberTriangulation.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoFidelity.agda b/proofs/agda/EchoFidelity.agda index 04e09cab..3850d73d 100644 --- a/proofs/agda/EchoFidelity.agda +++ b/proofs/agda/EchoFidelity.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 -- -- STATUS: type-checks under Agda 2.6.3 / agda-stdlib 2.3 (`--safe diff --git a/proofs/agda/EchoGraded.agda b/proofs/agda/EchoGraded.agda index 38f4787a..b3bd5bfc 100644 --- a/proofs/agda/EchoGraded.agda +++ b/proofs/agda/EchoGraded.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoGradedComonad.agda b/proofs/agda/EchoGradedComonad.agda index f928545c..c6a560f5 100644 --- a/proofs/agda/EchoGradedComonad.agda +++ b/proofs/agda/EchoGradedComonad.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoGradedComonadF1.agda b/proofs/agda/EchoGradedComonadF1.agda index 30c399f0..b69fc00f 100644 --- a/proofs/agda/EchoGradedComonadF1.agda +++ b/proofs/agda/EchoGradedComonadF1.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoGradedComonadInstance1.agda b/proofs/agda/EchoGradedComonadInstance1.agda index 1aa3791a..fe7ad623 100644 --- a/proofs/agda/EchoGradedComonadInstance1.agda +++ b/proofs/agda/EchoGradedComonadInstance1.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoGradedComonadInstance2.agda b/proofs/agda/EchoGradedComonadInstance2.agda index 7c4d5bb9..815e81fa 100644 --- a/proofs/agda/EchoGradedComonadInstance2.agda +++ b/proofs/agda/EchoGradedComonadInstance2.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoGradedComonadInterface.agda b/proofs/agda/EchoGradedComonadInterface.agda index f2641c7b..90c19038 100644 --- a/proofs/agda/EchoGradedComonadInterface.agda +++ b/proofs/agda/EchoGradedComonadInterface.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoHaplotypeCollapsing.agda b/proofs/agda/EchoHaplotypeCollapsing.agda index 225cd1a4..a7c90b05 100644 --- a/proofs/agda/EchoHaplotypeCollapsing.agda +++ b/proofs/agda/EchoHaplotypeCollapsing.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoImageFactorization.agda b/proofs/agda/EchoImageFactorization.agda index 7536f867..5384e22c 100644 --- a/proofs/agda/EchoImageFactorization.agda +++ b/proofs/agda/EchoImageFactorization.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoImageFactorizationProp.agda b/proofs/agda/EchoImageFactorizationProp.agda index 1ffb73bd..871f2a8c 100644 --- a/proofs/agda/EchoImageFactorizationProp.agda +++ b/proofs/agda/EchoImageFactorizationProp.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoIndexed.agda b/proofs/agda/EchoIndexed.agda index 67bce2ea..e6c83f38 100644 --- a/proofs/agda/EchoIndexed.agda +++ b/proofs/agda/EchoIndexed.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoIntegration.agda b/proofs/agda/EchoIntegration.agda index 116d193d..18e5a771 100644 --- a/proofs/agda/EchoIntegration.agda +++ b/proofs/agda/EchoIntegration.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoJanusBridge.agda b/proofs/agda/EchoJanusBridge.agda index ee7a1402..6b04c7f7 100644 --- a/proofs/agda/EchoJanusBridge.agda +++ b/proofs/agda/EchoJanusBridge.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoKernel.agda b/proofs/agda/EchoKernel.agda index a7ba21a7..fc849737 100644 --- a/proofs/agda/EchoKernel.agda +++ b/proofs/agda/EchoKernel.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoLLEncoding.agda b/proofs/agda/EchoLLEncoding.agda index 9f9458eb..063bd4e8 100644 --- a/proofs/agda/EchoLLEncoding.agda +++ b/proofs/agda/EchoLLEncoding.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoLinear.agda b/proofs/agda/EchoLinear.agda index c6867171..9b260f55 100644 --- a/proofs/agda/EchoLinear.agda +++ b/proofs/agda/EchoLinear.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoLossTaxonomy.agda b/proofs/agda/EchoLossTaxonomy.agda index 16c00204..bc117ef6 100644 --- a/proofs/agda/EchoLossTaxonomy.agda +++ b/proofs/agda/EchoLossTaxonomy.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoNoSectionGeneric.agda b/proofs/agda/EchoNoSectionGeneric.agda index 14c68096..3ac5b58e 100644 --- a/proofs/agda/EchoNoSectionGeneric.agda +++ b/proofs/agda/EchoNoSectionGeneric.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoOFSUnivF5.agda b/proofs/agda/EchoOFSUnivF5.agda index e3237adb..f18774e9 100644 --- a/proofs/agda/EchoOFSUnivF5.agda +++ b/proofs/agda/EchoOFSUnivF5.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoOFSUnivF5Diag.agda b/proofs/agda/EchoOFSUnivF5Diag.agda index 5cdae356..f1ec1c7a 100644 --- a/proofs/agda/EchoOFSUnivF5Diag.agda +++ b/proofs/agda/EchoOFSUnivF5Diag.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoOFSUnivF5Iso.agda b/proofs/agda/EchoOFSUnivF5Iso.agda index 53898584..51430e8f 100644 --- a/proofs/agda/EchoOFSUnivF5Iso.agda +++ b/proofs/agda/EchoOFSUnivF5Iso.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoObservationalEquivalence.agda b/proofs/agda/EchoObservationalEquivalence.agda index 1accfcd5..c42d188d 100644 --- a/proofs/agda/EchoObservationalEquivalence.agda +++ b/proofs/agda/EchoObservationalEquivalence.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoOrdinal.agda b/proofs/agda/EchoOrdinal.agda index 5b4eaf74..81d3c457 100644 --- a/proofs/agda/EchoOrdinal.agda +++ b/proofs/agda/EchoOrdinal.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoOrthogonalFactorizationSystem.agda b/proofs/agda/EchoOrthogonalFactorizationSystem.agda index 7b2ff7bb..046d4795 100644 --- a/proofs/agda/EchoOrthogonalFactorizationSystem.agda +++ b/proofs/agda/EchoOrthogonalFactorizationSystem.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoProbabilisticSupport.agda b/proofs/agda/EchoProbabilisticSupport.agda index 7966b392..0207eb26 100644 --- a/proofs/agda/EchoProbabilisticSupport.agda +++ b/proofs/agda/EchoProbabilisticSupport.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoProvenance.agda b/proofs/agda/EchoProvenance.agda index fb2329c9..510e8887 100644 --- a/proofs/agda/EchoProvenance.agda +++ b/proofs/agda/EchoProvenance.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoPullback.agda b/proofs/agda/EchoPullback.agda index 4b73d41e..14ecc7fc 100644 --- a/proofs/agda/EchoPullback.agda +++ b/proofs/agda/EchoPullback.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoPullbackUnivF4.agda b/proofs/agda/EchoPullbackUnivF4.agda index 787f7c0e..41cc045d 100644 --- a/proofs/agda/EchoPullbackUnivF4.agda +++ b/proofs/agda/EchoPullbackUnivF4.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoRelModel.agda b/proofs/agda/EchoRelModel.agda index 010027ff..b0c2b56c 100644 --- a/proofs/agda/EchoRelModel.agda +++ b/proofs/agda/EchoRelModel.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoRelational.agda b/proofs/agda/EchoRelational.agda index d19feac9..15f5af9d 100644 --- a/proofs/agda/EchoRelational.agda +++ b/proofs/agda/EchoRelational.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoResidue.agda b/proofs/agda/EchoResidue.agda index 880f05a3..e7715697 100644 --- a/proofs/agda/EchoResidue.agda +++ b/proofs/agda/EchoResidue.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoResidueCell.agda b/proofs/agda/EchoResidueCell.agda index 696903b3..d5761b1a 100644 --- a/proofs/agda/EchoResidueCell.agda +++ b/proofs/agda/EchoResidueCell.agda @@ -26,7 +26,7 @@ -- `holding` cell before consuming) — that needs the `(1 e)` quantity / an -- `@0`-style erasure encoding and remains the documented next slice. -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} module EchoResidueCell where diff --git a/proofs/agda/EchoResidueTaxonomy.agda b/proofs/agda/EchoResidueTaxonomy.agda index ab3112c3..ea2026ed 100644 --- a/proofs/agda/EchoResidueTaxonomy.agda +++ b/proofs/agda/EchoResidueTaxonomy.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoReversibilityBridge.agda b/proofs/agda/EchoReversibilityBridge.agda index 8f14078b..23e45db8 100644 --- a/proofs/agda/EchoReversibilityBridge.agda +++ b/proofs/agda/EchoReversibilityBridge.agda @@ -25,7 +25,7 @@ -- under `--safe --without-K` with zero postulates. The Agda here is the -- source of truth; 007's Rust checker and Idris2 spec mirror this model. -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} module EchoReversibilityBridge where diff --git a/proofs/agda/EchoScope.agda b/proofs/agda/EchoScope.agda index 5c36d534..e75876aa 100644 --- a/proofs/agda/EchoScope.agda +++ b/proofs/agda/EchoScope.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoSearch.agda b/proofs/agda/EchoSearch.agda index dbfca39d..3b80e0f3 100644 --- a/proofs/agda/EchoSearch.agda +++ b/proofs/agda/EchoSearch.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoSearchExample.agda b/proofs/agda/EchoSearchExample.agda index 9653f229..555814ac 100644 --- a/proofs/agda/EchoSearchExample.agda +++ b/proofs/agda/EchoSearchExample.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoSearchInstance.agda b/proofs/agda/EchoSearchInstance.agda index d1cda76a..845a7a90 100644 --- a/proofs/agda/EchoSearchInstance.agda +++ b/proofs/agda/EchoSearchInstance.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoSecurity.agda b/proofs/agda/EchoSecurity.agda index 46d8f1c0..a5dd5674 100644 --- a/proofs/agda/EchoSecurity.agda +++ b/proofs/agda/EchoSecurity.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoSelectiveProjection.agda b/proofs/agda/EchoSelectiveProjection.agda index 670c5f5a..568d4f34 100644 --- a/proofs/agda/EchoSelectiveProjection.agda +++ b/proofs/agda/EchoSelectiveProjection.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoSeparating.agda b/proofs/agda/EchoSeparating.agda index 52f2c952..dac95b10 100644 --- a/proofs/agda/EchoSeparating.agda +++ b/proofs/agda/EchoSeparating.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoStabilityTests.agda b/proofs/agda/EchoStabilityTests.agda index 22cc2ef4..2ee13f62 100644 --- a/proofs/agda/EchoStabilityTests.agda +++ b/proofs/agda/EchoStabilityTests.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoStepNDModelF2.agda b/proofs/agda/EchoStepNDModelF2.agda index c6f7e5a9..de424c49 100644 --- a/proofs/agda/EchoStepNDModelF2.agda +++ b/proofs/agda/EchoStepNDModelF2.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoThermoCollapseImpossible.agda b/proofs/agda/EchoThermoCollapseImpossible.agda index ca5aeb2a..93c433b9 100644 --- a/proofs/agda/EchoThermoCollapseImpossible.agda +++ b/proofs/agda/EchoThermoCollapseImpossible.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoThermodynamics.agda b/proofs/agda/EchoThermodynamics.agda index 3148ce27..41ca32a4 100644 --- a/proofs/agda/EchoThermodynamics.agda +++ b/proofs/agda/EchoThermodynamics.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoThermodynamicsFinite.agda b/proofs/agda/EchoThermodynamicsFinite.agda index 5bb3bf2e..31a34f32 100644 --- a/proofs/agda/EchoThermodynamicsFinite.agda +++ b/proofs/agda/EchoThermodynamicsFinite.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoTotalCompletion.agda b/proofs/agda/EchoTotalCompletion.agda index 59a48f14..dc490acf 100644 --- a/proofs/agda/EchoTotalCompletion.agda +++ b/proofs/agda/EchoTotalCompletion.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoTransaction.agda b/proofs/agda/EchoTransaction.agda index c5f1cb6f..61aa8584 100644 --- a/proofs/agda/EchoTransaction.agda +++ b/proofs/agda/EchoTransaction.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoTropical.agda b/proofs/agda/EchoTropical.agda index fd896727..f3aa1272 100644 --- a/proofs/agda/EchoTropical.agda +++ b/proofs/agda/EchoTropical.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoTruncation.agda b/proofs/agda/EchoTruncation.agda index cc388310..64bc5752 100644 --- a/proofs/agda/EchoTruncation.agda +++ b/proofs/agda/EchoTruncation.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/EchoVariance.agda b/proofs/agda/EchoVariance.agda index 0779c4df..963fdef7 100644 --- a/proofs/agda/EchoVariance.agda +++ b/proofs/agda/EchoVariance.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/MinimalCNO.agda b/proofs/agda/MinimalCNO.agda index 8a66daff..1993fdd3 100644 --- a/proofs/agda/MinimalCNO.agda +++ b/proofs/agda/MinimalCNO.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/NarrowingSmoke.agda b/proofs/agda/NarrowingSmoke.agda index a7a2b776..cb62e852 100644 --- a/proofs/agda/NarrowingSmoke.agda +++ b/proofs/agda/NarrowingSmoke.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 -- Focused entrypoint for the Wasm narrowing model and numeric contract. diff --git a/proofs/agda/Ordinal/Buchholz/Syntax.agda b/proofs/agda/Ordinal/Buchholz/Syntax.agda index ea5f908f..e3ab590b 100644 --- a/proofs/agda/Ordinal/Buchholz/Syntax.agda +++ b/proofs/agda/Ordinal/Buchholz/Syntax.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/Ordinal/OmegaMarkers.agda b/proofs/agda/Ordinal/OmegaMarkers.agda index dee20cdc..f74e5a40 100644 --- a/proofs/agda/Ordinal/OmegaMarkers.agda +++ b/proofs/agda/Ordinal/OmegaMarkers.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/SimpleTest.agda b/proofs/agda/SimpleTest.agda index 7487286e..4fd7b660 100644 --- a/proofs/agda/SimpleTest.agda +++ b/proofs/agda/SimpleTest.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/VecRotation.agda b/proofs/agda/VecRotation.agda index f5912616..8d0d5fd1 100644 --- a/proofs/agda/VecRotation.agda +++ b/proofs/agda/VecRotation.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/WorkingCNO.agda b/proofs/agda/WorkingCNO.agda index e76c1f31..6ec21338 100644 --- a/proofs/agda/WorkingCNO.agda +++ b/proofs/agda/WorkingCNO.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/All.agda b/proofs/agda/characteristic/All.agda index 980b26da..edac45e8 100644 --- a/proofs/agda/characteristic/All.agda +++ b/proofs/agda/characteristic/All.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/ChoreoInjective.agda b/proofs/agda/characteristic/ChoreoInjective.agda index 015f9a0d..dfd08431 100644 --- a/proofs/agda/characteristic/ChoreoInjective.agda +++ b/proofs/agda/characteristic/ChoreoInjective.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/IntegrationAudit.agda b/proofs/agda/characteristic/IntegrationAudit.agda index fe30976a..248f6726 100644 --- a/proofs/agda/characteristic/IntegrationAudit.agda +++ b/proofs/agda/characteristic/IntegrationAudit.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/InteractionTest.agda b/proofs/agda/characteristic/InteractionTest.agda index f4bd3e51..011067b7 100644 --- a/proofs/agda/characteristic/InteractionTest.agda +++ b/proofs/agda/characteristic/InteractionTest.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/ModeGraded.agda b/proofs/agda/characteristic/ModeGraded.agda index 1c3d0938..7d2c856b 100644 --- a/proofs/agda/characteristic/ModeGraded.agda +++ b/proofs/agda/characteristic/ModeGraded.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/N5Falsifier.agda b/proofs/agda/characteristic/N5Falsifier.agda index 52d8ec3e..042df70e 100644 --- a/proofs/agda/characteristic/N5Falsifier.agda +++ b/proofs/agda/characteristic/N5Falsifier.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/NonTruncatable.agda b/proofs/agda/characteristic/NonTruncatable.agda index 28df91a0..dcb496dd 100644 --- a/proofs/agda/characteristic/NonTruncatable.agda +++ b/proofs/agda/characteristic/NonTruncatable.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/RecipeNonTriviality.agda b/proofs/agda/characteristic/RecipeNonTriviality.agda index ce02eb2c..dadd32cd 100644 --- a/proofs/agda/characteristic/RecipeNonTriviality.agda +++ b/proofs/agda/characteristic/RecipeNonTriviality.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/RecipeSpec.agda b/proofs/agda/characteristic/RecipeSpec.agda index 41325a50..71c83afa 100644 --- a/proofs/agda/characteristic/RecipeSpec.agda +++ b/proofs/agda/characteristic/RecipeSpec.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/RecipeTheorem.agda b/proofs/agda/characteristic/RecipeTheorem.agda index 94263db9..f49e5135 100644 --- a/proofs/agda/characteristic/RecipeTheorem.agda +++ b/proofs/agda/characteristic/RecipeTheorem.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/RoleGraded.agda b/proofs/agda/characteristic/RoleGraded.agda index a5b6c3e5..e94490fe 100644 --- a/proofs/agda/characteristic/RoleGraded.agda +++ b/proofs/agda/characteristic/RoleGraded.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/RoleMode.agda b/proofs/agda/characteristic/RoleMode.agda index e99569ea..971eae47 100644 --- a/proofs/agda/characteristic/RoleMode.agda +++ b/proofs/agda/characteristic/RoleMode.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/RoleModeGrade.agda b/proofs/agda/characteristic/RoleModeGrade.agda index 8ff75f61..df2eb2c8 100644 --- a/proofs/agda/characteristic/RoleModeGrade.agda +++ b/proofs/agda/characteristic/RoleModeGrade.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/RoleRole.agda b/proofs/agda/characteristic/RoleRole.agda index a0fa64d0..6531a360 100644 --- a/proofs/agda/characteristic/RoleRole.agda +++ b/proofs/agda/characteristic/RoleRole.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/characteristic/VisibleConstraintAudit.agda b/proofs/agda/characteristic/VisibleConstraintAudit.agda index 6356d91c..4b913da7 100644 --- a/proofs/agda/characteristic/VisibleConstraintAudit.agda +++ b/proofs/agda/characteristic/VisibleConstraintAudit.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/examples/All.agda b/proofs/agda/examples/All.agda index b6dcfe23..426cf131 100644 --- a/proofs/agda/examples/All.agda +++ b/proofs/agda/examples/All.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/examples/EchoVsSigma.agda b/proofs/agda/examples/EchoVsSigma.agda index 76aad452..483a9e02 100644 --- a/proofs/agda/examples/EchoVsSigma.agda +++ b/proofs/agda/examples/EchoVsSigma.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/examples/EpistemicUpdate.agda b/proofs/agda/examples/EpistemicUpdate.agda index 3df11366..2f92bf6a 100644 --- a/proofs/agda/examples/EpistemicUpdate.agda +++ b/proofs/agda/examples/EpistemicUpdate.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/examples/LinearErasure.agda b/proofs/agda/examples/LinearErasure.agda index 663c59f5..7a1d56ce 100644 --- a/proofs/agda/examples/LinearErasure.agda +++ b/proofs/agda/examples/LinearErasure.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/examples/Transport.agda b/proofs/agda/examples/Transport.agda index f7c9ebb5..93a476f9 100644 --- a/proofs/agda/examples/Transport.agda +++ b/proofs/agda/examples/Transport.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/examples/TropicalArgmin.agda b/proofs/agda/examples/TropicalArgmin.agda index c99427fc..5e8e4db7 100644 --- a/proofs/agda/examples/TropicalArgmin.agda +++ b/proofs/agda/examples/TropicalArgmin.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: 2025-2026 Jonathan D.A. Jewell diff --git a/proofs/agda/experimental/echo-additive/All.agda b/proofs/agda/experimental/echo-additive/All.agda index c71a56a8..b0b1594a 100644 --- a/proofs/agda/experimental/echo-additive/All.agda +++ b/proofs/agda/experimental/echo-additive/All.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} -- EXPERIMENTAL aggregate root for CI only. -- diff --git a/proofs/agda/experimental/echo-additive/Grade.agda b/proofs/agda/experimental/echo-additive/Grade.agda index 309258e7..d28eca5a 100644 --- a/proofs/agda/experimental/echo-additive/Grade.agda +++ b/proofs/agda/experimental/echo-additive/Grade.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} -- EXPERIMENTAL — R0 deliverable. -- ℕ ∪ {∞} grade semiring for the echo-types additive tower. diff --git a/proofs/agda/experimental/echo-additive/GradedAdjunction.agda b/proofs/agda/experimental/echo-additive/GradedAdjunction.agda index 54a6192b..6563a882 100644 --- a/proofs/agda/experimental/echo-additive/GradedAdjunction.agda +++ b/proofs/agda/experimental/echo-additive/GradedAdjunction.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} -- EXPERIMENTAL — R4 deliverable: the F_r ⊣ U_r ADJUNCTION ATTEMPT on the -- CONTENT-FAITHFUL carrier (terminating-condition (ii) discriminator). diff --git a/proofs/agda/experimental/echo-additive/GradedCarrier.agda b/proofs/agda/experimental/echo-additive/GradedCarrier.agda index 678c5b85..267502ad 100644 --- a/proofs/agda/experimental/echo-additive/GradedCarrier.agda +++ b/proofs/agda/experimental/echo-additive/GradedCarrier.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} -- EXPERIMENTAL — R2 deliverable (SHARED CARRIER). -- Carrier D : Grade → Set → Set for the echo-additive composition lines, diff --git a/proofs/agda/experimental/echo-additive/GradedCarrierFaithful.agda b/proofs/agda/experimental/echo-additive/GradedCarrierFaithful.agda index 84f597f6..5b45e579 100644 --- a/proofs/agda/experimental/echo-additive/GradedCarrierFaithful.agda +++ b/proofs/agda/experimental/echo-additive/GradedCarrierFaithful.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} -- EXPERIMENTAL — R4 deliverable (CONTENT-FAITHFUL CARRIER). -- The variant carrier named in GradedComonad §7: a finite layer carries a diff --git a/proofs/agda/experimental/echo-additive/GradedComonad.agda b/proofs/agda/experimental/echo-additive/GradedComonad.agda index deb7ecac..1bb2f8b4 100644 --- a/proofs/agda/experimental/echo-additive/GradedComonad.agda +++ b/proofs/agda/experimental/echo-additive/GradedComonad.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} -- EXPERIMENTAL — R3 SECONDARY LINE (comonadic δ). -- Colaxator δ_{r,s} : D (r +g s) A → D r (D s A), the SPLITTING direction, diff --git a/proofs/agda/experimental/echo-additive/GradedMonad.agda b/proofs/agda/experimental/echo-additive/GradedMonad.agda index 26791be1..1bd411d9 100644 --- a/proofs/agda/experimental/echo-additive/GradedMonad.agda +++ b/proofs/agda/experimental/echo-additive/GradedMonad.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} -- EXPERIMENTAL — R3 PRIMARY LINE: the graded monad multiplication φ. -- AUTHOR-GATED comparative variance protocol (R2/R3). NOT merged to main (W6). diff --git a/proofs/agda/experimental/echo-additive/VarianceGate.agda b/proofs/agda/experimental/echo-additive/VarianceGate.agda index ddf31d87..8e45839e 100644 --- a/proofs/agda/experimental/echo-additive/VarianceGate.agda +++ b/proofs/agda/experimental/echo-additive/VarianceGate.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} -- EXPERIMENTAL — R1 deliverable: variance gate framing. -- This file contains NO proven theorems. Every type signature below is diff --git a/scripts/kernel-guard.sh b/scripts/kernel-guard.sh index 50504233..319798d9 100644 --- a/scripts/kernel-guard.sh +++ b/scripts/kernel-guard.sh @@ -75,8 +75,9 @@ for src in "$ECHO_SRC" "$KERNEL_SRC"; do head -1 "$src" | grep -q -- '--without-K' \ || fail "$src: missing --without-K in the OPTIONS pragma" - # No safety-relaxing flag, anywhere. - if grep -nE -- '--(type-in-type|cubical|rewriting|sized-types|guardedness|injective-type-constructors|no-positivity-check|no-termination-check|allow-unsolved-metas)' "$src" >/dev/null; then + # No safety-relaxing flag, anywhere. Whole flags only: `--cubical-compatible` + # (which strengthens, not relaxes) must not match `--cubical`. + if grep -nE -- '--(type-in-type|cubical|erased-cubical|rewriting|sized-types|guardedness|injective-type-constructors|no-positivity-check|no-termination-check|allow-unsolved-metas)([[:space:]]|#|$)' "$src" >/dev/null; then fail "$src: a safety-relaxing OPTIONS flag is present" fi diff --git a/tutorial/All.agda b/tutorial/All.agda index 4fcc2063..9de7d9c9 100644 --- a/tutorial/All.agda +++ b/tutorial/All.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: 2025-2026 Jonathan D.A. Jewell diff --git a/tutorial/epistemic_erasure/All.agda b/tutorial/epistemic_erasure/All.agda index cc2c3c84..c86c82d8 100644 --- a/tutorial/epistemic_erasure/All.agda +++ b/tutorial/epistemic_erasure/All.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: 2025-2026 Jonathan D.A. Jewell diff --git a/tutorial/epistemic_erasure/EpistemicErasure.agda b/tutorial/epistemic_erasure/EpistemicErasure.agda index f8934a4c..f7e99f05 100644 --- a/tutorial/epistemic_erasure/EpistemicErasure.agda +++ b/tutorial/epistemic_erasure/EpistemicErasure.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: 2025-2026 Jonathan D.A. Jewell diff --git a/tutorial/epistemic_erasure/Smoke.agda b/tutorial/epistemic_erasure/Smoke.agda index 9b06b276..0692fe00 100644 --- a/tutorial/epistemic_erasure/Smoke.agda +++ b/tutorial/epistemic_erasure/Smoke.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: 2025-2026 Jonathan D.A. Jewell diff --git a/tutorial/provenance_debugging/All.agda b/tutorial/provenance_debugging/All.agda index 38b34743..af23125c 100644 --- a/tutorial/provenance_debugging/All.agda +++ b/tutorial/provenance_debugging/All.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: 2025-2026 Jonathan D.A. Jewell diff --git a/tutorial/provenance_debugging/ProvenanceDebugging.agda b/tutorial/provenance_debugging/ProvenanceDebugging.agda index 2cd9a509..59bdda23 100644 --- a/tutorial/provenance_debugging/ProvenanceDebugging.agda +++ b/tutorial/provenance_debugging/ProvenanceDebugging.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: 2025-2026 Jonathan D.A. Jewell diff --git a/tutorial/provenance_debugging/Smoke.agda b/tutorial/provenance_debugging/Smoke.agda index dffd0e15..1d813dd8 100644 --- a/tutorial/provenance_debugging/Smoke.agda +++ b/tutorial/provenance_debugging/Smoke.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: 2025-2026 Jonathan D.A. Jewell diff --git a/tutorial/region_exit_audit/All.agda b/tutorial/region_exit_audit/All.agda index 6dcaba2e..3dfd67ef 100644 --- a/tutorial/region_exit_audit/All.agda +++ b/tutorial/region_exit_audit/All.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: 2025-2026 Jonathan D.A. Jewell diff --git a/tutorial/region_exit_audit/RegionExitAudit.agda b/tutorial/region_exit_audit/RegionExitAudit.agda index 579a67ff..7d597288 100644 --- a/tutorial/region_exit_audit/RegionExitAudit.agda +++ b/tutorial/region_exit_audit/RegionExitAudit.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: 2025-2026 Jonathan D.A. Jewell diff --git a/tutorial/region_exit_audit/Smoke.agda b/tutorial/region_exit_audit/Smoke.agda index 1fdd842d..fa6b73b7 100644 --- a/tutorial/region_exit_audit/Smoke.agda +++ b/tutorial/region_exit_audit/Smoke.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: 2025-2026 Jonathan D.A. Jewell