fix(CNO,lib): typecheck CNO.agda under --safe + add agda-lib

Unblocks the Echo<->CNO content-bridge in
hyperpolymath/echo-types#21. Three changes:

1. Adds top-level absolute-zero.agda-lib declaring this repo's
   Agda library so downstream consumers (currently echo-types,
   later VeriSim and others in the hyperpolymath ecosystem) can
   `depend: absolute-zero` and resolve `open import CNO` cleanly.

2. Adds `{-# OPTIONS --safe --without-K #-}` to proofs/agda/CNO.agda
   so it composes with the rest of the verification ecosystem
   (echo-types, VeriSim, etc.), all of which run --safe --without-K.
   Verified clean: `agda --safe CNO.agda` exits 0.

3. Closes three latent issues in CNO.agda that the --safe check
   surfaces:

   * Parse errors at lines 316/323 inside ternary-add and
     crazy-op: `using (_Data.Nat.%_)` is not valid Agda
     (qualifying an operator name inside `using` is rejected by
     the parser). Replaces both helpers with a self-contained
     structural-recursive `mod3` which terminates inside
     --safe --without-K without pulling in Data.Nat.DivMod._%_'s
     NonZero instance noise.

   * Two unfilled holes (`{!!}`) at lines 303/304 in
     cno-composition's cno-identity and cno-pure fields.
     The former filled via state-eq-trans + transport along
     eval-seq-comp. The latter required a new helper `pure-trans`,
     defined via componentwise `trans` on the I/O and memory
     equalities. Both holes now resolve into closed,
     postulate-free IsCNO-record values.

Result: composing two CNO programs is now a constructive theorem
rather than a goal, and cno-composition is a real reusable lemma
for downstream content-bridges.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

absolute-zero.agda-lib

@@ -0,0 +1,3 @@
+name: absolute-zero
+include: proofs/agda
+depend: standard-library

proofs/agda/CNO.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --safe --without-K #-}
+
 {- Certified Null Operations: Agda Formalization
 
    This file provides an Agda formalization of CNO theory.
@@ -13,7 +15,8 @@ module CNO where
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
 open import Data.List using (List; []; _∷_; _++_; length)
 open import Data.Product using (_×_; _,_; proj₁; proj₂; Σ; ∃)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; sym; trans; cong; subst)
 open import Data.Bool using (Bool; true; false; if_then_else_)
 open import Data.Maybe using (Maybe; just; nothing)
 open import Function using (_∘_; id)
@@ -293,34 +296,60 @@ state-eq-trans (m₁ , r₁ , i₁ , p₁) (m₂ , r₂ , i₂ , p₂) =
   trans i₁ i₂ ,
   trans p₁ p₂
 
--- Composition of CNOs is a CNO
+-- Pointwise-transitive purity: agree on I/O and on memory.
+-- Uses `proj₁`/`proj₂` rather than pattern-matching on `_,_`
+-- because `pure` is a definitional `_×_` and the unifier sometimes
+-- declines to unfold it in pattern positions.
+pure-trans : ∀ {s₁ s₂ s₃} → pure s₁ s₂ → pure s₂ s₃ → pure s₁ s₃
+pure-trans p₁₂ p₂₃ =
+  trans (proj₁ p₁₂) (proj₁ p₂₃) ,
+  (λ addr → trans (proj₂ p₁₂ addr) (proj₂ p₂₃ addr))
+
+-- Composition of CNOs is a CNO. The two non-trivial fields
+-- (`cno-identity`, `cno-pure`) chain the per-program lemmas
+-- through `eval p₁ s` and transport along `eval-seq-comp` to the
+-- composite evaluation.
 cno-composition : ∀ {p₁ p₂} → IsCNO p₁ → IsCNO p₂ → IsCNO (seq-comp p₁ p₂)
 cno-composition {p₁} {p₂} cno₁ cno₂ = record
   { cno-terminates = λ s → terminates-always (seq-comp p₁ p₂) s
   ; cno-identity = λ s →
       let eq₁ = IsCNO.cno-identity cno₁ s
           eq₂ = IsCNO.cno-identity cno₂ (eval p₁ s)
-      in {!!}  -- Requires more work with rewrite
-  ; cno-pure = λ s → {!!}
+      in subst (λ x → state-eq x s) (sym (eval-seq-comp p₁ p₂ s))
+              (state-eq-trans eq₂ eq₁)
+  ; cno-pure = λ s →
+      let pu₁ : pure s (eval p₁ s)
+          pu₁ = IsCNO.cno-pure cno₁ s
+          pu₂ : pure (eval p₁ s) (eval p₂ (eval p₁ s))
+          pu₂ = IsCNO.cno-pure cno₂ (eval p₁ s)
+          composed : pure s (eval p₂ (eval p₁ s))
+          composed = pure-trans {s₁ = s} {s₂ = eval p₁ s}
+                                {s₃ = eval p₂ (eval p₁ s)} pu₁ pu₂
+      in subst (pure s) (sym (eval-seq-comp p₁ p₂ s)) composed
   ; cno-reversible = λ s → refl
   }
 
 ----------------------------------------------------------------------------
 -- Malbolge-Specific
 ----------------------------------------------------------------------------
 
--- Ternary operations
+-- Ternary operations: addition mod 3 (Malbolge-flavoured).
+-- Local `mod3` is structural-recursive on its argument, so it
+-- terminates and stays inside `--safe --without-K` without pulling
+-- in `Data.Nat.DivMod._%_` (whose `NonZero` instance lookup adds
+-- noise that this helper does not need).
+mod3 : ℕ → ℕ
+mod3 zero                    = zero
+mod3 (suc zero)              = suc zero
+mod3 (suc (suc zero))        = suc (suc zero)
+mod3 (suc (suc (suc n)))     = mod3 n
+
 ternary-add : ℕ → ℕ → ℕ
-ternary-add a b = (a + b) Data.Nat.% 3
-  where
-    open import Data.Nat.DivMod using (_Data.Nat.%_)
-    -- Simplified for demonstration
+ternary-add a b = mod3 (a + b)
 
--- Crazy operation
+-- Crazy operation (Malbolge crazy op surface; placeholder semantics)
 crazy-op : ℕ → ℕ → ℕ
-crazy-op a b = (a + b) Data.Nat.% 3
-  where
-    open import Data.Nat.DivMod using (_Data.Nat.%_)
+crazy-op a b = mod3 (a + b)
 
 ----------------------------------------------------------------------------
 -- Absolute Zero