diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index a808750..c288d3f 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -3,7 +3,7 @@ # Copyright (c) Jonathan D.A. Jewell # # Proof verification CI for the ACTIVE proof stack (owner ruling 2026-10-10): -# * Agda — CNO + OND + EchoBridge (--safe --without-K) +# * Agda — CNO + OND + EchoBridge (PROOF-POLICY 2.1 invocation + strict flags) # * Z3 — CNO + OND bounded checks (expect-annotated) # * Idris 2 — the ABI package (absolute-zero-abi.ipkg) # Each is an INDEPENDENT job, so one flaking never blocks the others. @@ -66,14 +66,19 @@ jobs: mkdir -p "$HOME/.agda" echo "$HOME/agda-stdlib/standard-library.agda-lib" > "$HOME/.agda/libraries" echo "standard-library" > "$HOME/.agda/defaults" - - name: Type-check CNO + OND + EchoBridge (4 modules, --safe --without-K) + - name: Type-check CNO + OND + EchoBridge (4 modules, PROOF-POLICY 2.1 + strict flags) working-directory: proofs/agda + # The canonical invocation (standards PROOF-POLICY 2.1) is + # `agda --safe --without-K --cubical-compatible`. The other strict + # language flags (--exact-split --no-sized-types --no-guardedness) + # are declared in each module's OPTIONS pragma, not here, so they do + # not also apply to the standard library. run: | agda --version - agda --safe --without-K CNO.agda - agda --safe --without-K OND.agda - agda --safe --without-K EchoBridgeScaffold.agda - agda --safe --without-K EchoBridgeCNO.agda + agda --safe --without-K --cubical-compatible --double-check -W error -W noUnsupportedIndexedMatch CNO.agda + agda --safe --without-K --cubical-compatible --double-check -W error -W noUnsupportedIndexedMatch OND.agda + agda --safe --without-K --cubical-compatible --double-check -W error -W noUnsupportedIndexedMatch EchoBridgeScaffold.agda + agda --safe --without-K --cubical-compatible --double-check -W error -W noUnsupportedIndexedMatch EchoBridgeCNO.agda echo "✓ Agda: CNO + OND + EchoBridgeScaffold + EchoBridgeCNO type-check" z3: diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 5d5ebfc..c2527b8 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -9,7 +9,7 @@ This file backs every factual claim in link:README.adoc[README.adoc] with code p [IMPORTANT] ==== -*Archive notice (2026-10-10, reconciled 2026-11-01).* The active proof stack is Agda (`proofs/agda/`, `--safe --without-K`, zero postulates) + Z3 as a bounded-check solver + the Idris 2 ABI. Coq, Lean 4, Isabelle/HOL and Mizar now live under `archive/proofs/`; paths below of the form `proofs/coq/…` / `proofs/lean4/…` refer to the *archived* trees (`archive/proofs/coq/…` etc.), and counts such as "115 Qed / 61 Axioms" are *historical* figures of those archived trees. The canonical active-vs-archived proof-status table is link:PROOF-STATUS.adoc[PROOF-STATUS.adoc], which also records the estate proof grades (mathesis `estate-mathematical-architecture` §5) and the closed ledger vocabulary of `hyperpolymath/standards` (`proven` / `proven-with-postulates` / `tested-only` / `argued` / `open`): the active Agda proofs are `proven` at **Grade 3** (local strict-flag check, no independent-foundation translation), the Z3 bounded checks are `tested-only`, and OND-6 is `open`. +*Archive notice (2026-10-10, reconciled 2026-11-01).* The active proof stack is Agda (`proofs/agda/`, `--safe --without-K`, zero postulates) + Z3 as a bounded-check solver + the Idris 2 ABI. Coq, Lean 4, Isabelle/HOL and Mizar now live under `archive/proofs/`; paths below of the form `proofs/coq/…` / `proofs/lean4/…` refer to the *archived* trees (`archive/proofs/coq/…` etc.), and counts such as "115 Qed / 61 Axioms" are *historical* figures of those archived trees. The canonical active-vs-archived proof-status table is link:PROOF-STATUS.adoc[PROOF-STATUS.adoc], which also records Proof Witness Grades (standards PROOF-POLICY §8) and the closed ledger vocabulary of `hyperpolymath/standards` (`proven` / `proven-with-postulates` / `tested-only` / `argued` / `open`): the active Agda proofs are `proven` and `ungraded` (no PWG-3 receipt recorded yet), the Z3 bounded checks are `tested-only`, and OND-6 is `open`. Its 2026-11-09 design audit records that the active Agda `IsCNO` was degenerate (termination and reversibility held by construction) and how it was restated over a pc-driven machine the same day. ==== == Claim-to-implementation map @@ -55,10 +55,10 @@ Caveat:: ____Verify CNO properties in six independent proof systems.____ How this is implemented:: -Artefacts exist for Coq, Lean 4, Agda, Z3, Isabelle, and Mizar in `link:proofs/[]`. `link:proofs/verify-all-provers.sh[]` orchestrates verification. CI gates Coq, Lean 4, and Agda. +Active artefacts are Agda, Z3 and the Idris 2 ABI in `link:proofs/[]`, run by `link:proofs/verify-active-provers.sh[]` and CI. Coq, Lean 4, Isabelle and Mizar are archived under `archive/proofs/` and are not built or gated. Caveat:: -**Z3, Isabelle, and Mizar are generated but not yet run in CI.** The artefacts exist but are not evidence until machine-executed and green. The "six prover" claim describes the target architecture, not the current CI gate. +**Isabelle and Mizar are archived and not run in CI.** Z3 runs in CI (the `z3` job in `.github/workflows/proofs.yml`) as bounded, `tested-only` checks. The "six prover" claim describes the target architecture, not the current CI gate. === Thermodynamic reversibility follows from Landauer's principle diff --git a/GLOSSARY.adoc b/GLOSSARY.adoc index 9752e8d..362532f 100644 --- a/GLOSSARY.adoc +++ b/GLOSSARY.adoc @@ -12,7 +12,7 @@ Cross-reference glossary for link:README.adoc[README.adoc], link:EXPLAINME.adoc[ [[cno]] CNO (Certified Null Effect):: A program that does nothing to the world: terminates, maps input state to identical output state, is pure, and is thermodynamically reversible. The conserved quantity is state. - *Classification:* **novel assembly** (standard concepts combined into this specific 4-field record). + *Classification:* **novel assembly** (standard concepts combined; the intended notion has four parts, while the active Agda `IsCNO` record has two fields, see <>). [[ond]] OND (Observational Null Disclosure):: @@ -28,7 +28,7 @@ Coupling dial:: [[is-cno]] IsCNO(p):: - The core predicate: `Terminates(p, σ) ∧ FinalState(p, σ) = σ ∧ NoSideEffects(p) ∧ ThermodynamicallyReversible(p)`. + The core predicate. Intended notion: `Terminates(p, σ) ∧ FinalState(p, σ) = σ ∧ NoSideEffects(p) ∧ ThermodynamicallyReversible(p)`. Active Agda (`proofs/agda/CNO.agda`): from every state the pc-driven machine stops normally (`cno-terminates`), and every normal stop is `obs-eq` to the start (`cno-identity`). Purity and observational reversibility are derived; no thermodynamic claim is made. *Classification:* **project-specific** (formalisation). [[landauer-principle]] @@ -38,7 +38,7 @@ Landauer's principle:: [[reversible-computing]] Reversible computing:: - Computation that can be undone with zero energy cost (Bennett 1973). A required field of `IsCNO`. + Computation that can be undone with zero energy cost (Bennett 1973). Part of the intended CNO notion; the active Agda proves only observational reversibility (`cno-left-inverse`), not an energy bound. *Classification:* **standard** (Bennett 1973). == OND concepts diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 62aa215..9c86a6b 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -45,14 +45,17 @@ ground truth** — see "Role of this repository" below. `hyperpolymath/standards` (`3-practice/PROOF-POLICY.adoc` §5 and `docs/README-EXPLAINME-STANDARD.adoc` §5): `proven`, `proven-with-postulates`, `tested-only`, `argued`, `open` — recorded exactly, never flattened into a -percentage. Estate grades follow mathesis's `estate-mathematical-architecture` -§5–6: **Grade 3** = type-checks locally in Agda under strict flags but not yet -translated to an independent foundational system; **Grade 2i/2ii** = -translation to one/two independent foundations (2ii requires a non-DTT -second system, e.g. Isabelle/HOL); **Grade 1** = headless CI via verified -checker APIs. Verification receipts are tied to commit hashes; superseded -claims are marked historical, not silently dropped, and axiom dependence -(`Print Assumptions` / `#print axioms`) is tracked per row. +percentage. Grades are Proof Witness Grades (PWG) as defined in +PROOF-POLICY §8 (owner ruling 2026-11-04), which supersedes the "Grade +3/2i/2ii/1" ladder of mathesis's `estate-mathematical-architecture` brief +that this file used until 2026-11-09. `PWG-3` needs an Agda receipt under the +§2.1 invocation `agda --safe --without-K --cubical-compatible`, recording the +Agda version, standard-library pin, flags in force, import cone and source +commit; `PWG-2i`/`PWG-2ii` additionally need one/both Rocq and Lean legs whose +§2.2 correspondence state is `RECONCILED`. A theorem below `PWG-3` is +`ungraded`. A status token and a grade are separate fields and are never +written in one cell. Superseded claims are marked historical, not silently +dropped, and axiom dependence is tracked per row. [cols="2,1,2,3",options="header"] |=== @@ -60,12 +63,12 @@ claims are marked historical, not silently dropped, and axiom dependence | `proofs/agda/` — `CNO.agda`, `OND.agda`, `EchoBridgeScaffold.agda`, `EchoBridgeCNO.agda` | ACTIVE (CI `agda` job; `proofs/verify-active-provers.sh`) -| `proven` — **Grade 3**: type-checked locally in Agda, zero postulates, every file `{-# OPTIONS --safe --without-K #-}`; EchoBridge takes funext as an *explicit hypothesis*, not a global postulate. Not translated to any independent foundation, so not Grade 2+ -| Domain formalisation of both pillars; discharges OND-1..5; contains no OND-6. Open obligation: recheck under the 2026-11-01 canonical profile `agda --safe --without-K --cubical-compatible` (standards PROOF-POLICY §2.1) — prior `--safe --without-K` receipts are not receipts for the combined profile +| Status: `proven` for each stated Agda term — zero postulates, every file `{-# OPTIONS --safe --without-K #-}`; EchoBridge takes funext as an *explicit hypothesis*, not a global postulate. Grade: `ungraded` (no PWG-3 receipt recorded; see the 2026-11-09 audit below). *What the CNO terms state is narrower than the pillar description*: see "Design audit (2026-11-09)" below before citing any CNO result +| Domain formalisation of both pillars; discharges OND-1..5; contains no OND-6. The canonical profile `agda --safe --without-K --cubical-compatible` (standards PROOF-POLICY §2.1) passes locally (2026-11-09) and is the CI invocation from 2026-11-09. Open obligation: a PWG-3 receipt for that profile | `proofs/z3/` — `ond/OND_checks.smt2` via `proofs/z3/verify.sh` | ACTIVE as bounded-check solver (CI `z3` job) -| `tested-only` — bounded SMT checks, no proof grade; every `(check-sat)` carries a `; expect sat|unsat` annotation. Receipt reproduced in this sandbox 2026-11-01 (z3 5.3.3, `Z3-CHECK OK`, sat/unsat/sat) — see receipts below +| `tested-only` — bounded SMT checks, no proof grade; every `(check-sat)` carries a `; expect sat|unsat` annotation. Receipt reproduced in this sandbox 2026-11-01 (`z3` 4.16.0, `Z3-CHECK OK`, sat/unsat/sat) — see receipts below | Bounds: finite/bounded programs under a finite declared `O`; not a general proof | `src/abi/` + `absolute-zero-abi.ipkg` (Idris 2) @@ -104,9 +107,69 @@ claims are marked historical, not silently dropped, and axiom dependence | Declared observation models `+O+` and residue lists; every OND certificate is relative to its declared `+O+` |=== +=== Design audit (2026-11-09) + +A statement-level review of the active Agda (`proofs/agda/` at `cbe9ae9`) +against the claims in this file, README, EXPLAINME and `docs/TWO-PILLARS.adoc`. +The terms all type-check: on 2026-11-09 the four modules at `cbe9ae9` were rechecked cold +with Agda 2.6.3 and agda-stdlib 2.3 (CI pairs Agda 2.6.3 with agda-stdlib 1.7.3) under +`agda --safe --without-K --cubical-compatible`, and all passed. That is a local check, not a CI +receipt. The findings concern what the terms *state*. + +[cols="2,3,2",options="header"] +|=== +| Item | What the Agda actually states | Honest label + +| `IsCNO` (`CNO.agda`) +| `state-eq` includes `state-pc`. `step` advances the PC on `Nop`, `Load`, +`Store` and `Add` and sets it on `Jump`; `eval` never restores it. So +`cno-identity : ∀ s → state-eq (eval p s) s` holds only for programs made +of `Halt` instructions (and the empty program). The archived Coq fixed +the same defect on 2026-05-18 by excluding the PC from `state_eq`; the +active Agda did not. +| `IsCNO` is a degenerate class in the active stack. `halt-is-cno`, +`cno-composition` and every result quantified over `IsCNO` are `proven` +but about that class only. *Resolved 2026-11-09:* `IsCNO` now judges a run by `obs-eq` (memory, registers, I/O; no PC). `nop-is-cno` and `jump-exit-is-cno` show the class is not Halt-only; `load-not-cno` shows it is not everything. `state-eq` keeps the PC and is still the full equality. + +| `terminates`, `terminates-always` +| `terminates p s = ∃ s′. eval p s ≡ s′`, inhabited by `(eval p s , refl)` +for every program. `eval` is a total fold over the instruction list. +| Holds by construction; *not* a termination result. *Resolved 2026-11-09:* `eval` is replaced by a pc-driven machine: a big-step relation `_⊢_⇓_` and a fuel interpreter `run`, related by `run-sound` and `run-complete`. `Terminates p s` asks for a normal stop from pc 0, and `jump-self-diverges` shows `Jump 0` never stops. A Store or Add on a missing register faults and does not terminate. + +| `thermodynamically-reversible`, `energy-dissipated` +| `energy-dissipated _ _ _ = zero`, so every program, reversible or not, +satisfies it. `reversible` is defined but never used. +| Holds by construction; *not* a Landauer/Bennett result. The archived Coq +`StatMech`/`LandauerDerivation` development is the only thermodynamic +formalisation, and it is archived. *Resolved 2026-11-09:* `energy-dissipated`, `thermodynamically-reversible` and the unused `reversible` are removed. `cno-left-inverse` proves observational reversibility (running any CNO after a CNO restores memory, registers and I/O) as a consequence of the identity law, and claims nothing thermodynamic. + +| OND-5 "mirrored in Lean 4, Agda, Z3" +| Agda states OND-5 under `O-out`; the archived Coq and Lean state it under +`O_all`. Both are true; they are different propositions. +| Correspondence state `unassessed` (PROOF-POLICY §2.2). The rows are not +mirrors of one theorem. + +| OND-3 "anchored to `is_CNO`" +| `OND.agda` uses a local `is-null` and never imports `CNO`. The anchoring +(`writer_program_not_core_CNO`, `skip_program_is_core_CNO`) exists only in +the archived Coq. +| The active Agda OND-3 is *not* anchored to `IsCNO`. + +| EchoBridge +| The `≡`-form results (`echo-from-cno-program-≡`, `absolute-zero-echo-≡`) +take funext as a hypothesis; the `EchoRel` results do not. The echo is the +fixed-point witness `(s , cno-identity)`. +| `proven`, conditional on funext where stated; inherits the `IsCNO` +degeneracy above. *Resolved 2026-11-09:* restated over `cno-result` and `obs-eq`; the `≡` form is now on the observable projection `observe`, and `program-state-model` is a `CNOModel` over observable states. +|=== + +Downstream: `hyperpolymath/echo-types` imports `CNO` (`EchoCNOBridge`, +`EchoCNOSemantics`, `EchoThermodynamicsArbitrary`, `EchoCNOPackaging`); its +CNO-facing results inherit these limits. + === Reproduction receipts (this environment, 2026-11-01) -* *Z3 — REPRODUCED HERE.* `z3` 5.3.3 (64-bit, via the `z3-solver` PyPI wheel, +* *Z3 — REPRODUCED HERE.* `z3` 4.16.0 (64-bit, via the `z3-solver` PyPI wheel, the only package host reachable from this sandbox) running `bash proofs/z3/verify.sh` → `Z3-CHECK OK`: 1 file (`proofs/z3/ond/OND_checks.smt2`), 3 `(check-sat)` verdicts `sat unsat sat`, @@ -134,7 +197,7 @@ be cited as proof status for any other repository. *Cross-repo note (2026-11-01).* `epistemic-types` (at `5422cd5`) is an *independent* proof library with **no dependency on absolute-zero**. Any cross-repo claim must therefore name the exact theorem, its scope, and its -assumptions (e.g. "OND-1..5, `proven`, Grade 3, Agda `--safe --without-K`, +assumptions (e.g. "OND-1..5, `proven`, `ungraded`, Agda `--safe --without-K`, relative to a declared `O`") — never a bare count imported from this repo. Mathesis (the estate mathematical knowledge commons) may *catalogue* these receipts and grades, but per its own architecture the original repositories diff --git a/README.adoc b/README.adoc index 7aa1739..b1094ba 100644 --- a/README.adoc +++ b/README.adoc @@ -54,9 +54,17 @@ Secret→observable channel |=== -Both pillars are machine-checked. OND obligations OND-1..5 are proved -with zero axioms in Coq, mirrored in Lean 4, Agda, and Z3. The -independence theorem is anchored to `+is_CNO+`. OND-6 (conditional +OND obligations OND-1..5 are proved with zero axioms in the active Agda +(`proofs/agda/OND.agda`); archived Coq and Lean developments and bounded Z3 +checks exist, but the Agda and Coq/Lean OND-5 statements are different +propositions, and the anchoring of the independence theorem to `+is_CNO+` +exists only in the archived Coq. The active Agda CNO definition was +degenerate until 2026-11-09 (Halt-only, with termination and +reversibility holding by construction). It is now stated over a +pc-driven machine: termination is a real property, identity is up to +observable state (memory, registers, I/O), and nothing thermodynamic is +claimed. See the 2026-11-09 design audit in +link:PROOF-STATUS.adoc[PROOF-STATUS.adoc]. OND-6 (conditional composition, the research capstone) remains open by design. == What is standard and what is ours @@ -188,10 +196,10 @@ The *canonical* proof-status table — separating active, archived, proved, axiomatic and generated artefacts, with OND-6 explicitly open — lives in link:PROOF-STATUS.adoc[PROOF-STATUS.adoc]. Figures quoted above for archived provers are historical counts of those archived trees, not active status. -Estate proof grades (mathesis `estate-mathematical-architecture` §5) are -recorded there too: the active Agda proofs are **Grade 3** (local, -strict-flag, zero-postulate — not yet translated to an independent -foundation), the Z3 checks are `tested-only` (bounded), and OND-6 is `open`. +Proof Witness Grades (standards PROOF-POLICY §8) are recorded there too: +the active Agda proofs are `proven` but `ungraded` until a PWG-3 receipt +is recorded, the Z3 checks are `tested-only` (bounded), and OND-6 is +`open`. == [CAUTION] diff --git a/docs/TWO-PILLARS.adoc b/docs/TWO-PILLARS.adoc index 906283c..daec857 100644 --- a/docs/TWO-PILLARS.adoc +++ b/docs/TWO-PILLARS.adoc @@ -61,6 +61,19 @@ Agda, Isabelle, Mizar), `is_CNO p` bundles four properties: 4. *Thermodynamic reversibility* — zero energy dissipation by Landauer's principle (logical reversibility ⇒ no entropy increase, via Bennett). +[WARNING] +.Active Agda status (2026-11-09) +==== +These four properties describe the intended notion. The active Agda +(`proofs/agda/CNO.agda`, restated 2026-11-09) formalises (1) as a normal stop +of a pc-driven machine, (2) up to memory, registers and I/O (not the program +counter), and (3) as a consequence of (2). It formalises (4) only as +observational reversibility (`cno-left-inverse`), with no energy model. Before +that date (1) and (4) held by construction and `IsCNO` was Halt-only. See the +design audit in +link:../PROOF-STATUS.adoc[PROOF-STATUS.adoc]. +==== + The defining feature of CNO is that *everything it talks about is inside the model*. State is a modelled object; "the output state equals the input state" is a closed mathematical statement, provable without reference to any physical diff --git a/proofs/agda/CNO.agda b/proofs/agda/CNO.agda index 5b52d65..424dcc9 100644 --- a/proofs/agda/CNO.agda +++ b/proofs/agda/CNO.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} {- Certified Null Operations: Agda Formalization @@ -10,16 +10,20 @@ License: AGPL-3.0 / Palimpsest 0.5 -} + 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 Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; _<_; z≤n; s≤s) +open import Data.Nat.Properties using (+-comm; ≤-antisym) +open import Data.List using (List; []; _∷_; _++_; length; map) +open import Data.Product using (_×_; _,_; proj₁; proj₂; Σ) +open import Data.Sum using (_⊎_; inj₁; inj₂) +open import Data.Empty using (⊥; ⊥-elim) +open import Relation.Nullary using (¬_) 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) +open import Data.Maybe using (Maybe; just; nothing) renaming (map to maybe-map) ---------------------------------------------------------------------------- -- Memory Model @@ -76,7 +80,7 @@ record ProgramState : Set where open ProgramState --- State equality +-- Full state equality, program counter included. state-eq : ProgramState → ProgramState → Set state-eq s₁ s₂ = mem-eq (state-memory s₁) (state-memory s₂) × @@ -84,6 +88,30 @@ state-eq s₁ s₂ = state-io s₁ ≡ state-io s₂ × state-pc s₁ ≡ state-pc s₂ +-- Observable state equality: memory, registers and I/O. The program +-- counter is control state, not an observable effect, so a CNO is judged +-- by this relation. (Until 2026-11-09 `IsCNO` used `state-eq`, which +-- made every program that advances the counter, `Nop` included, fail to +-- be a CNO.) +obs-eq : ProgramState → ProgramState → Set +obs-eq s₁ s₂ = + mem-eq (state-memory s₁) (state-memory s₂) × + state-registers s₁ ≡ state-registers s₂ × + state-io s₁ ≡ state-io s₂ + +obs-eq-refl : ∀ s → obs-eq s s +obs-eq-refl s = (λ _ → refl) , refl , refl + +obs-eq-sym : ∀ {s₁ s₂} → obs-eq s₁ s₂ → obs-eq s₂ s₁ +obs-eq-sym (m , r , i) = (λ a → sym (m a)) , sym r , sym i + +obs-eq-trans : ∀ {s₁ s₂ s₃} → obs-eq s₁ s₂ → obs-eq s₂ s₃ → obs-eq s₁ s₃ +obs-eq-trans (m₁ , r₁ , i₁) (m₂ , r₂ , i₂) = + (λ a → trans (m₁ a) (m₂ a)) , trans r₁ r₂ , trans i₁ i₂ + +state-eq→obs-eq : ∀ {s₁ s₂} → state-eq s₁ s₂ → obs-eq s₁ s₂ +state-eq→obs-eq (m , r , i , _) = m , r , i + ---------------------------------------------------------------------------- -- Instructions ---------------------------------------------------------------------------- @@ -94,9 +122,9 @@ data Instruction : Set where Load : ℕ → ℕ → Instruction -- Load mem[addr] to reg Store : ℕ → ℕ → Instruction -- Store reg to mem[addr] Add : ℕ → ℕ → ℕ → Instruction -- r3 := r1 + r2 - Jump : ℕ → Instruction + Jump : ℕ → Instruction -- absolute jump: pc := target --- A program is a list of instructions +-- A program is a list of instructions, addressed from 0 by the pc. Program : Set Program = List Instruction @@ -116,58 +144,199 @@ set-reg [] _ _ = [] set-reg (_ ∷ rs) zero val = val ∷ rs set-reg (r ∷ rs) (suc n) val = r ∷ set-reg rs n val ----------------------------------------------------------------------------- --- Operational Semantics ----------------------------------------------------------------------------- - -open import Data.Nat using (_≡ᵇ_) - --- Single step evaluation -step : ProgramState → Instruction → ProgramState -step s Nop = record s { state-pc = suc (state-pc s) } - -step s Halt = s - -step s (Load addr reg) = - let val = state-memory s addr - in record s - { state-registers = set-reg (state-registers s) reg val - ; state-pc = suc (state-pc s) - } - -step s (Store addr reg) with get-reg (state-registers s) reg -... | just val = record s - { state-memory = mem-update (state-memory s) addr val - ; state-pc = suc (state-pc s) - } -... | nothing = s -- Error case - -step s (Add r₁ r₂ r₃) with get-reg (state-registers s) r₁ | get-reg (state-registers s) r₂ -... | just v₁ | just v₂ = record s - { state-registers = set-reg (state-registers s) r₃ (v₁ + v₂) - ; state-pc = suc (state-pc s) - } -... | _ | _ = s -- Error case - -step s (Jump target) = record s { state-pc = target } +-- The instruction at a program counter, if any. +fetch : Program → ℕ → Maybe Instruction +fetch [] _ = nothing +fetch (i ∷ _) zero = just i +fetch (_ ∷ is) (suc n) = fetch is n + +---------------------------------------------------------------------------- +-- Operational Semantics: a pc-driven machine +---------------------------------------------------------------------------- + +-- What one instruction does to the machine. `fault` is a Store or Add +-- that names a missing register: the machine stops abnormally, so a +-- faulting run does not terminate in the sense of `_⊢_⇓_`. +data Ctl : Set where + halt : Ctl + fault : Ctl + go : ProgramState → Ctl + +store-at : ProgramState → ℕ → Maybe ℕ → Ctl +store-at s addr (just v) = go (record s + { state-memory = mem-update (state-memory s) addr v + ; state-pc = suc (state-pc s) + }) +store-at s addr nothing = fault + +add-at : ProgramState → ℕ → Maybe ℕ → Maybe ℕ → Ctl +add-at s r₃ (just v₁) (just v₂) = go (record s + { state-registers = set-reg (state-registers s) r₃ (v₁ + v₂) + ; state-pc = suc (state-pc s) + }) +add-at s r₃ (just _) nothing = fault +add-at s r₃ nothing _ = fault + +-- Single step. +step : ProgramState → Instruction → Ctl +step s Nop = go (record s { state-pc = suc (state-pc s) }) +step s Halt = halt +step s (Load addr reg) = go (record s + { state-registers = set-reg (state-registers s) reg (state-memory s addr) + ; state-pc = suc (state-pc s) + }) +step s (Store addr reg) = store-at s addr (get-reg (state-registers s) reg) +step s (Add r₁ r₂ r₃) = + add-at s r₃ (get-reg (state-registers s) r₁) (get-reg (state-registers s) r₂) +step s (Jump target) = go (record s { state-pc = target }) + +-- Big-step semantics. `p ⊢ s ⇓ s'`: started in `s`, program `p` stops +-- normally in `s'`, either by running off the end (no instruction at the +-- pc) or by executing `Halt`. +infix 4 _⊢_⇓_ +data _⊢_⇓_ (p : Program) : ProgramState → ProgramState → Set where + ⇓-end : ∀ {s} → fetch p (state-pc s) ≡ nothing → p ⊢ s ⇓ s + ⇓-halt : ∀ {s i} → fetch p (state-pc s) ≡ just i → step s i ≡ halt → + p ⊢ s ⇓ s + ⇓-step : ∀ {s i s₁ s'} → fetch p (state-pc s) ≡ just i → + step s i ≡ go s₁ → p ⊢ s₁ ⇓ s' → p ⊢ s ⇓ s' + +-- Fuel-bounded interpreter: the executable form of the same machine. +-- `run n p s` performs at most `n` non-halting steps; `nothing` means +-- out of fuel or a fault. +run : ℕ → Program → ProgramState → Maybe ProgramState +run-from : ℕ → Program → ProgramState → Maybe Instruction → Maybe ProgramState +run-ctl : Ctl → ℕ → Program → ProgramState → Maybe ProgramState + +run n p s = run-from n p s (fetch p (state-pc s)) + +run-from n p s nothing = just s +run-from n p s (just i) = run-ctl (step s i) n p s + +run-ctl halt n p s = just s +run-ctl fault n p s = nothing +run-ctl (go s₁) zero p s = nothing +run-ctl (go s₁) (suc n) p s = run n p s₁ + +-- Every program starts at pc 0. +start : ProgramState → ProgramState +start s = record s { state-pc = 0 } + +---------------------------------------------------------------------------- +-- Small lemmas +---------------------------------------------------------------------------- + +just-inj : ∀ {A : Set} {x y : A} → just x ≡ just y → x ≡ y +just-inj refl = refl + +go-inj : ∀ {s₁ s₂} → go s₁ ≡ go s₂ → s₁ ≡ s₂ +go-inj refl = refl + +nothing≢just : ∀ {A : Set} {x : A} → ¬ (nothing ≡ just x) +nothing≢just () + +halt≢go : ∀ {s} → ¬ (halt ≡ go s) +halt≢go () + +fetch-nothing : ∀ p n → fetch p n ≡ nothing → length p ≤ n +fetch-nothing [] n e = z≤n +fetch-nothing (i ∷ p) zero () +fetch-nothing (i ∷ p) (suc n) e = s≤s (fetch-nothing p n e) + +fetch-just : ∀ p n {i} → fetch p n ≡ just i → n < length p +fetch-just [] n () +fetch-just (i ∷ p) zero e = s≤s z≤n +fetch-just (i ∷ p) (suc n) e = s≤s (fetch-just p n e) + +fetch-++-left : ∀ p q n {i} → fetch p n ≡ just i → fetch (p ++ q) n ≡ just i +fetch-++-left [] q n () +fetch-++-left (x ∷ p) q zero e = e +fetch-++-left (x ∷ p) q (suc n) e = fetch-++-left p q n e + +fetch-++-right : ∀ p q j → fetch (p ++ q) (length p + j) ≡ fetch q j +fetch-++-right [] q j = refl +fetch-++-right (x ∷ p) q j = fetch-++-right p q j + +fetch-map : ∀ (f : Instruction → Instruction) q j → + fetch (map f q) j ≡ maybe-map f (fetch q j) +fetch-map f [] j = refl +fetch-map f (x ∷ q) zero = refl +fetch-map f (x ∷ q) (suc j) = fetch-map f q j + +---------------------------------------------------------------------------- +-- Adequacy: the interpreter and the big-step relation agree +---------------------------------------------------------------------------- + +run-sound : ∀ n p s {s'} → run n p s ≡ just s' → p ⊢ s ⇓ s' +from-sound : ∀ n p s m {s'} → fetch p (state-pc s) ≡ m → + run-from n p s m ≡ just s' → p ⊢ s ⇓ s' +ctl-sound : ∀ c n p s i {s'} → fetch p (state-pc s) ≡ just i → + step s i ≡ c → run-ctl c n p s ≡ just s' → p ⊢ s ⇓ s' + +run-sound n p s h = from-sound n p s (fetch p (state-pc s)) refl h + +from-sound n p s nothing e refl = ⇓-end e +from-sound n p s (just i) e h = ctl-sound (step s i) n p s i e refl h + +ctl-sound halt n p s i e g refl = ⇓-halt e g +ctl-sound fault n p s i e g () +ctl-sound (go s₁) zero p s i e g () +ctl-sound (go s₁) (suc n) p s i e g h = ⇓-step e g (run-sound n p s₁ h) + +run-complete : ∀ {p s s'} → p ⊢ s ⇓ s' → Σ ℕ (λ n → run n p s ≡ just s') +run-complete {p} {s} (⇓-end e) = 0 , cong (run-from 0 p s) e +run-complete {p} {s} (⇓-halt e g) = + 0 , trans (cong (run-from 0 p s) e) (cong (λ c → run-ctl c 0 p s) g) +run-complete {p} {s} (⇓-step e g d) with run-complete d +... | n , h = suc n , trans (cong (run-from (suc n) p s) e) + (trans (cong (λ c → run-ctl c (suc n) p s) g) h) + +-- The machine is deterministic. +⇓-det : ∀ {p s a b} → p ⊢ s ⇓ a → p ⊢ s ⇓ b → a ≡ b +⇓-det (⇓-end e) (⇓-end e') = refl +⇓-det (⇓-end e) (⇓-halt e' _) = ⊥-elim (nothing≢just (trans (sym e) e')) +⇓-det (⇓-end e) (⇓-step e' _ _) = ⊥-elim (nothing≢just (trans (sym e) e')) +⇓-det (⇓-halt e _) (⇓-end e') = ⊥-elim (nothing≢just (trans (sym e') e)) +⇓-det (⇓-halt e _) (⇓-halt _ _) = refl +⇓-det {s = s} (⇓-halt e h) (⇓-step e' g _) = + ⊥-elim (halt≢go (trans (sym h) + (trans (cong (step s) (just-inj (trans (sym e) e'))) g))) +⇓-det (⇓-step e _ _) (⇓-end e') = ⊥-elim (nothing≢just (trans (sym e') e)) +⇓-det {s = s} (⇓-step e g _) (⇓-halt e' h) = + ⊥-elim (halt≢go (trans (sym h) + (trans (cong (step s) (just-inj (trans (sym e') e))) g))) +⇓-det {p} {s} {b = b} (⇓-step e g d) (⇓-step e' g' d') = + ⇓-det d (subst (λ x → p ⊢ x ⇓ b) (sym s₁≡s₂) d') + where + s₁≡s₂ = go-inj (trans (sym g) + (trans (cong (step s) (just-inj (trans (sym e) e'))) g')) --- Multi-step evaluation -eval : Program → ProgramState → ProgramState -eval [] s = s -eval (i ∷ is) s = eval is (step s i) +-- A run stops either off the end or at an instruction that halts. +⇓-final : ∀ {p s s'} → p ⊢ s ⇓ s' → + (fetch p (state-pc s') ≡ nothing) ⊎ + Σ Instruction (λ i → fetch p (state-pc s') ≡ just i × step s' i ≡ halt) +⇓-final (⇓-end e) = inj₁ e +⇓-final (⇓-halt e h) = inj₂ (_ , e , h) +⇓-final (⇓-step _ _ d) = ⇓-final d ---------------------------------------------------------------------------- -- Termination ---------------------------------------------------------------------------- --- A program terminates if evaluation produces a result --- For finite programs, this is always true -terminates : Program → ProgramState → Set -terminates p s = ∃ λ s' → eval p s ≡ s' +-- `p` terminates from `s` when the machine, started at pc 0, stops +-- normally. Programs can loop (`jump-self-diverges` below) or fault, so +-- this is a real property, not a consequence of evaluation being total. +Terminates : Program → ProgramState → Set +Terminates p s = Σ ProgramState (λ s' → p ⊢ start s ⇓ s') --- Termination proof for any program -terminates-always : ∀ (p : Program) (s : ProgramState) → terminates p s -terminates-always p s = eval p s , refl +-- The same notion through the fuel interpreter. +terminates→fuel : ∀ {p s} → Terminates p s → + Σ ℕ (λ n → Σ ProgramState (λ s' → run n p (start s) ≡ just s')) +terminates→fuel (s' , d) with run-complete d +... | n , h = n , s' , h + +fuel→terminates : ∀ {p s} n {s'} → run n p (start s) ≡ just s' → Terminates p s +fuel→terminates {p} {s} n {s'} h = s' , run-sound n p (start s) h ---------------------------------------------------------------------------- -- Side Effects @@ -185,154 +354,303 @@ no-memory-alloc s₁ s₂ = mem-eq (state-memory s₁) (state-memory s₂) pure : ProgramState → ProgramState → Set pure s₁ s₂ = no-io s₁ s₂ × no-memory-alloc s₁ s₂ ----------------------------------------------------------------------------- --- Reversibility ----------------------------------------------------------------------------- - --- A program is reversible if there exists an inverse -reversible : Program → Set -reversible p = ∃ λ p-inv → ∀ s → eval p-inv (eval p s) ≡ s - ----------------------------------------------------------------------------- --- Thermodynamic Reversibility ----------------------------------------------------------------------------- - --- Energy dissipated (simplified model) -energy-dissipated : Program → ProgramState → ProgramState → ℕ -energy-dissipated _ _ _ = zero - --- Thermodynamically reversible programs dissipate no energy -thermodynamically-reversible : Program → Set -thermodynamically-reversible p = - ∀ s → energy-dissipated p s (eval p s) ≡ zero - ---------------------------------------------------------------------------- -- CNO Definition ---------------------------------------------------------------------------- --- A Certified Null Operation +-- A Certified Null Operation: from every state the machine stops +-- normally, and every normal stop leaves memory, registers and I/O as +-- they were. Purity and reversibility are consequences, proved below. record IsCNO (p : Program) : Set where field - cno-terminates : ∀ s → terminates p s - cno-identity : ∀ s → state-eq (eval p s) s - cno-pure : ∀ s → pure s (eval p s) - cno-reversible : thermodynamically-reversible p + cno-terminates : ∀ s → Terminates p s + cno-identity : ∀ {s s'} → p ⊢ start s ⇓ s' → obs-eq s' s + +-- Build a CNO certificate from one witnessing run per state; determinism +-- extends the identity to every run. +cno-from-runs : ∀ {p} → + (∀ s → Σ ProgramState (λ s' → p ⊢ start s ⇓ s' × obs-eq s' s)) → IsCNO p +cno-from-runs f = record + { cno-terminates = λ s → proj₁ (f s) , proj₁ (proj₂ (f s)) + ; cno-identity = λ {s} d → + subst (λ x → obs-eq x s) (⇓-det (proj₁ (proj₂ (f s))) d) + (proj₂ (proj₂ (f s))) + } ---------------------------------------------------------------------------- --- Basic Theorems +-- CNO Properties ---------------------------------------------------------------------------- --- The empty program is a CNO -empty-is-cno : IsCNO [] -empty-is-cno = record - { cno-terminates = λ s → terminates-always [] s - ; cno-identity = λ s → (λ addr → refl) , refl , refl , refl - ; cno-pure = λ s → refl , (λ addr → refl) - ; cno-reversible = λ s → refl - } - --- Nop preserves most state (modulo PC) -nop-preserves-memory : ∀ s → mem-eq (state-memory (eval (Nop ∷ []) s)) - (state-memory s) -nop-preserves-memory s = λ addr → refl +cno-terminates-thm : ∀ {p} → IsCNO p → ∀ s → Terminates p s +cno-terminates-thm cno = IsCNO.cno-terminates cno -nop-preserves-registers : ∀ s → state-registers (eval (Nop ∷ []) s) - ≡ state-registers s -nop-preserves-registers s = refl +-- The final state of a CNO's run. +cno-result : ∀ {p} → IsCNO p → ProgramState → ProgramState +cno-result cno s = proj₁ (IsCNO.cno-terminates cno s) -nop-preserves-io : ∀ s → state-io (eval (Nop ∷ []) s) ≡ state-io s -nop-preserves-io s = refl - --- Halt is a perfect CNO -halt-is-cno : IsCNO (Halt ∷ []) -halt-is-cno = record - { cno-terminates = λ s → terminates-always (Halt ∷ []) s - ; cno-identity = λ s → (λ addr → refl) , refl , refl , refl - ; cno-pure = λ s → refl , (λ addr → refl) - ; cno-reversible = λ s → refl - } - ----------------------------------------------------------------------------- --- CNO Properties ----------------------------------------------------------------------------- +cno-result-run : ∀ {p} (cno : IsCNO p) s → p ⊢ start s ⇓ cno-result cno s +cno-result-run cno s = proj₂ (IsCNO.cno-terminates cno s) --- CNOs always terminate -cno-terminates-thm : ∀ {p} → IsCNO p → ∀ s → terminates p s -cno-terminates-thm {p} cno s = IsCNO.cno-terminates cno s +cno-preserves-state : ∀ {p} (cno : IsCNO p) s → obs-eq (cno-result cno s) s +cno-preserves-state cno s = IsCNO.cno-identity cno {s} (cno-result-run cno s) --- CNOs preserve state -cno-preserves-state : ∀ {p} → IsCNO p → ∀ s → state-eq (eval p s) s -cno-preserves-state {p} cno s = IsCNO.cno-identity cno s +-- CNOs are pure: no I/O, no memory change. +cno-pure-thm : ∀ {p s s'} → IsCNO p → p ⊢ start s ⇓ s' → pure s s' +cno-pure-thm {s = s} cno d with IsCNO.cno-identity cno {s} d +... | m , _ , i = sym i , (λ a → sym (m a)) --- CNOs are pure -cno-pure-thm : ∀ {p} → IsCNO p → ∀ s → pure s (eval p s) -cno-pure-thm {p} cno s = IsCNO.cno-pure cno s +-- Observational reversibility: running `q` after `p` restores every +-- observable component. This is a consequence of the identity law, not +-- a thermodynamic statement; the Landauer accounting lives in echo-types +-- (`EchoThermodynamics`). +ObsLeftInverse : Program → Program → Set +ObsLeftInverse p q = + ∀ {s s₁ s₂} → p ⊢ start s ⇓ s₁ → q ⊢ start s₁ ⇓ s₂ → obs-eq s₂ s --- CNOs are thermodynamically reversible -cno-thermo-rev : ∀ {p} → IsCNO p → thermodynamically-reversible p -cno-thermo-rev {p} cno = IsCNO.cno-reversible cno +cno-left-inverse : ∀ {p q} → IsCNO p → IsCNO q → ObsLeftInverse p q +cno-left-inverse cp cq {s} {s₁} {s₂} d₁ d₂ = + obs-eq-trans {s₂} {s₁} {s} + (IsCNO.cno-identity cq {s₁} d₂) (IsCNO.cno-identity cp {s} d₁) ---------------------------------------------------------------------------- -- Composition ---------------------------------------------------------------------------- --- Sequential composition +-- Jumps are absolute, so the second program is relocated by the length +-- of the first. +shift-instr : ℕ → Instruction → Instruction +shift-instr k (Jump t) = Jump (t + k) +shift-instr k Nop = Nop +shift-instr k Halt = Halt +shift-instr k (Load a r) = Load a r +shift-instr k (Store a r) = Store a r +shift-instr k (Add a b c) = Add a b c + seq-comp : Program → Program → Program -seq-comp p₁ p₂ = p₁ ++ p₂ - --- Evaluation of composition -eval-seq-comp : ∀ p₁ p₂ s → eval (seq-comp p₁ p₂) s ≡ eval p₂ (eval p₁ s) -eval-seq-comp [] p₂ s = refl -eval-seq-comp (i ∷ is) p₂ s = eval-seq-comp is p₂ (step s i) - --- Helper lemma for composition -state-eq-refl : ∀ s → state-eq s s -state-eq-refl s = (λ addr → refl) , refl , refl , refl - -state-eq-trans : ∀ {s₁ s₂ s₃} → state-eq s₁ s₂ → state-eq s₂ s₃ → state-eq s₁ s₃ -state-eq-trans (m₁ , r₁ , i₁ , p₁) (m₂ , r₂ , i₂ , p₂) = - (λ addr → trans (m₁ addr) (m₂ addr)) , - trans r₁ r₂ , - trans i₁ i₂ , - trans p₁ p₂ - --- 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 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 - } +seq-comp p₁ p₂ = p₁ ++ map (shift-instr (length p₁)) p₂ + +-- A program is closed when no jump leaves it except to its end. Without +-- this, a jump past the end of `p₁` lands inside `p₂` in the composite +-- (`closedness-needed` below). +Closed : Program → Set +Closed p = ∀ {n t} → fetch p n ≡ just (Jump t) → t ≤ length p + +shift-pc : ℕ → ProgramState → ProgramState +shift-pc k s = record s { state-pc = state-pc s + k } + +shift-ctl : ℕ → Ctl → Ctl +shift-ctl k halt = halt +shift-ctl k fault = fault +shift-ctl k (go s) = go (shift-pc k s) + +obs-shift : ∀ k s → obs-eq (shift-pc k s) s +obs-shift k s = obs-eq-refl s + +store-shift : ∀ k s a m → store-at (shift-pc k s) a m ≡ shift-ctl k (store-at s a m) +store-shift k s a (just v) = refl +store-shift k s a nothing = refl + +add-shift : ∀ k s r m₁ m₂ → + add-at (shift-pc k s) r m₁ m₂ ≡ shift-ctl k (add-at s r m₁ m₂) +add-shift k s r (just v₁) (just v₂) = refl +add-shift k s r (just v₁) nothing = refl +add-shift k s r nothing m₂ = refl + +step-shift : ∀ k s i → step (shift-pc k s) (shift-instr k i) ≡ shift-ctl k (step s i) +step-shift k s Nop = refl +step-shift k s Halt = refl +step-shift k s (Load a r) = refl +step-shift k s (Store a r) = store-shift k s a (get-reg (state-registers s) r) +step-shift k s (Add a b c) = + add-shift k s c (get-reg (state-registers s) a) (get-reg (state-registers s) b) +step-shift k s (Jump t) = refl + +store-pc : ∀ s a m {s₁} → store-at s a m ≡ go s₁ → state-pc s₁ ≡ suc (state-pc s) +store-pc s a (just v) refl = refl +store-pc s a nothing () + +add-pc : ∀ s r m₁ m₂ {s₁} → add-at s r m₁ m₂ ≡ go s₁ → + state-pc s₁ ≡ suc (state-pc s) +add-pc s r (just v₁) (just v₂) refl = refl +add-pc s r (just v₁) nothing () +add-pc s r nothing m₂ () + +-- In a closed program every step keeps the pc within `0 .. length p`. +step-pc-bound : ∀ {p s i s₁} → Closed p → fetch p (state-pc s) ≡ just i → + step s i ≡ go s₁ → state-pc s₁ ≤ length p +step-pc-bound {p} {s} {Nop} cl e g = + subst (λ x → x ≤ length p) (cong state-pc (go-inj g)) (fetch-just p _ e) +step-pc-bound {p} {s} {Halt} cl e () +step-pc-bound {p} {s} {Load a r} cl e g = + subst (λ x → x ≤ length p) (cong state-pc (go-inj g)) (fetch-just p _ e) +step-pc-bound {p} {s} {Store a r} cl e g = + subst (λ x → x ≤ length p) + (sym (store-pc s a (get-reg (state-registers s) r) g)) + (fetch-just p _ e) +step-pc-bound {p} {s} {Add a b c} cl e g = + subst (λ x → x ≤ length p) + (sym (add-pc s c (get-reg (state-registers s) a) + (get-reg (state-registers s) b) g)) + (fetch-just p _ e) +step-pc-bound {p} {s} {Jump t} cl e g = + subst (λ x → x ≤ length p) (cong state-pc (go-inj g)) (cl e) + +⇓-pc-bound : ∀ {p s s'} → Closed p → state-pc s ≤ length p → + p ⊢ s ⇓ s' → state-pc s' ≤ length p +⇓-pc-bound cl b (⇓-end _) = b +⇓-pc-bound cl b (⇓-halt _ _) = b +⇓-pc-bound {p} cl b (⇓-step e g d) = + ⇓-pc-bound {p} cl (step-pc-bound {p} cl e g) d + +-- Phase 1: a run of `p` is a prefix of a run of `p ++ q`. +prefix : ∀ {p q s s' s''} → p ⊢ s ⇓ s' → (p ++ q) ⊢ s' ⇓ s'' → (p ++ q) ⊢ s ⇓ s'' +prefix (⇓-end _) k = k +prefix (⇓-halt _ _) k = k +prefix {p} {q} {s} (⇓-step e g d) k = + ⇓-step (fetch-++-left p q (state-pc s) e) g (prefix d k) + +-- Phase 2: a run of `p₂` is a run of the relocated copy in the composite. +module Seq (p₁ p₂ : Program) where + k : ℕ + k = length p₁ + + fetch-comp : ∀ j → fetch (seq-comp p₁ p₂) (j + k) + ≡ maybe-map (shift-instr k) (fetch p₂ j) + fetch-comp j = + trans (cong (fetch (seq-comp p₁ p₂)) (+-comm j k)) + (trans (fetch-++-right p₁ (map (shift-instr k) p₂) j) + (fetch-map (shift-instr k) p₂ j)) + + phase2 : ∀ {t t'} → p₂ ⊢ t ⇓ t' → seq-comp p₁ p₂ ⊢ shift-pc k t ⇓ shift-pc k t' + phase2 {t} (⇓-end e) = + ⇓-end (trans (fetch-comp (state-pc t)) (cong (maybe-map (shift-instr k)) e)) + phase2 {t} (⇓-halt {i = i} e h) = + ⇓-halt (trans (fetch-comp (state-pc t)) (cong (maybe-map (shift-instr k)) e)) + (trans (step-shift k t i) (cong (shift-ctl k) h)) + phase2 {t} (⇓-step {i = i} e g d) = + ⇓-step (trans (fetch-comp (state-pc t)) (cong (maybe-map (shift-instr k)) e)) + (trans (step-shift k t i) (cong (shift-ctl k) g)) + (phase2 d) + +shift-start : ∀ {k} s → state-pc s ≡ k → shift-pc k (start s) ≡ s +shift-start (mk-state m r io pc) e = cong (mk-state m r io) (sym e) + +-- Sequential composition of CNOs is a CNO when the first is closed. +cno-composition : ∀ {p₁ p₂} → Closed p₁ → IsCNO p₁ → IsCNO p₂ → + IsCNO (seq-comp p₁ p₂) +cno-composition {p₁} {p₂} cl c₁ c₂ = cno-from-runs runs + where + open Seq p₁ p₂ + + comp : Program + comp = seq-comp p₁ p₂ + + runs : ∀ s → Σ ProgramState (λ s' → comp ⊢ start s ⇓ s' × obs-eq s' s) + runs s with IsCNO.cno-terminates c₁ s + ... | s₁ , d₁ with ⇓-final d₁ + ... | inj₂ (i , e , h) = + s₁ , + prefix d₁ (⇓-halt (fetch-++-left p₁ _ (state-pc s₁) e) h) , + IsCNO.cno-identity c₁ {s} d₁ + ... | inj₁ e with IsCNO.cno-terminates c₂ s₁ + ... | t' , d₂ = + shift-pc k t' , + prefix d₁ (subst (λ x → comp ⊢ x ⇓ shift-pc k t') + (shift-start s₁ pc≡k) (phase2 d₂)) , + obs-eq-trans {shift-pc k t'} {t'} {s} (obs-shift k t') + (obs-eq-trans {t'} {s₁} {s} + (IsCNO.cno-identity c₂ {s₁} d₂) (IsCNO.cno-identity c₁ {s} d₁)) + where + pc≡k : state-pc s₁ ≡ k + pc≡k = ≤-antisym (⇓-pc-bound {p₁} cl z≤n d₁) (fetch-nothing p₁ _ e) + +---------------------------------------------------------------------------- +-- Witnesses +---------------------------------------------------------------------------- + +-- The empty program is a CNO +empty-is-cno : IsCNO [] +empty-is-cno = cno-from-runs (λ s → start s , ⇓-end refl , obs-eq-refl s) + +-- Halt is a CNO +halt-is-cno : IsCNO (Halt ∷ []) +halt-is-cno = cno-from-runs (λ s → start s , ⇓-halt refl refl , obs-eq-refl s) + +-- Nop advances the pc and is a CNO: the class is not Halt-only. +nop-is-cno : IsCNO (Nop ∷ []) +nop-is-cno = + cno-from-runs (λ s → _ , ⇓-step refl refl (⇓-end refl) , obs-eq-refl s) + +-- A jump to the end is a CNO. +jump-exit-is-cno : IsCNO (Jump 1 ∷ []) +jump-exit-is-cno = + cno-from-runs (λ s → _ , ⇓-step refl refl (⇓-end refl) , obs-eq-refl s) + +nop-closed : Closed (Nop ∷ []) +nop-closed {zero} () +nop-closed {suc n} () + +-- Composition at work: Nop ; Nop. +nop-nop-is-cno : IsCNO (seq-comp (Nop ∷ []) (Nop ∷ [])) +nop-nop-is-cno = cno-composition {Nop ∷ []} {Nop ∷ []} (λ {n} {t} → nop-closed {n} {t}) nop-is-cno nop-is-cno + +-- A self-loop never stops: termination is not automatic. +loop : Program +loop = Jump 0 ∷ [] + +loop-stuck : ∀ {t t'} → state-pc t ≡ 0 → ¬ (loop ⊢ t ⇓ t') +loop-stuck {t} pc0 (⇓-end e) = + nothing≢just (trans (sym e) (cong (fetch loop) pc0)) +loop-stuck {t} pc0 (⇓-halt e h) = + halt≢go (trans (sym h) + (cong (step t) (just-inj (trans (sym e) (cong (fetch loop) pc0))))) +loop-stuck {t} pc0 (⇓-step e g d) = + loop-stuck (sym (cong state-pc (go-inj (trans (sym + (cong (step t) (just-inj (trans (sym e) (cong (fetch loop) pc0))))) g)))) d + +jump-self-diverges : ∀ s → ¬ Terminates loop s +jump-self-diverges s (_ , d) = loop-stuck refl d + +-- A Load that changes a register is not a CNO: the class is not +-- everything. +load-prog : Program +load-prog = Load 0 0 ∷ [] + +load-not-cno : ¬ IsCNO load-prog +load-not-cno cno with IsCNO.cno-identity cno + {s = mk-state empty-memory (5 ∷ []) [] 0} + (⇓-step refl refl (⇓-end refl)) +... | _ , () , _ + +-- The closedness side condition is needed. `Jump 2` and +-- `Jump 2 ; Load 0 0` are both CNOs, but in the composite the first +-- jump lands on the relocated Load. +jump2 : Program +jump2 = Jump 2 ∷ [] + +jump2-load : Program +jump2-load = Jump 2 ∷ Load 0 0 ∷ [] + +closedness-needed : + IsCNO jump2 × IsCNO jump2-load × ¬ Closed jump2 × ¬ IsCNO (seq-comp jump2 jump2-load) +closedness-needed = + cno-from-runs (λ s → _ , ⇓-step refl refl (⇓-end refl) , obs-eq-refl s) , + cno-from-runs (λ s → _ , ⇓-step refl refl (⇓-end refl) , obs-eq-refl s) , + (λ cl → two≰one (cl {0} refl)) , + bad + where + two≰one : ¬ (2 ≤ 1) + two≰one (s≤s ()) + + bad : ¬ IsCNO (seq-comp jump2 jump2-load) + bad cno with IsCNO.cno-identity cno + {s = mk-state empty-memory (5 ∷ []) [] 0} + (⇓-step refl refl (⇓-step refl refl (⇓-end refl))) + ... | _ , () , _ ---------------------------------------------------------------------------- -- Malbolge-Specific ---------------------------------------------------------------------------- - -- 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 diff --git a/proofs/agda/CNOTests.agda b/proofs/agda/CNOTests.agda new file mode 100644 index 0000000..a33d27e --- /dev/null +++ b/proofs/agda/CNOTests.agda @@ -0,0 +1,200 @@ +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} + +-- Unit regressions for the pc-driven machine. Each equality is checked by +-- normalization; expected states are explicit, rather than computed by step. +-- Run from proofs/agda using the CI Agda invocation, targeting CNOTests.agda. +module CNOTests where + +open import CNO +open ProgramState +open import Data.Nat using (ℕ; suc) +open import Data.List using ([]; _∷_) +open import Data.Maybe using (just; nothing) +open import Data.Product using (_,_; proj₁; proj₂) +open import Relation.Nullary using (¬_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) + +-- Nonempty memory, registers and I/O expose accidental resets or clobbers. +mem : Memory +mem = mem-update empty-memory 4 11 + +io : IOState +io = ReadOp 3 ∷ WriteOp 8 ∷ [] + +at : ℕ → ProgramState +at pc = mk-state mem (2 ∷ 5 ∷ 9 ∷ []) io pc + +empty-needs-no-fuel : run 0 [] (at 7) ≡ just (at 7) +empty-needs-no-fuel = refl + +halt-needs-no-fuel : run 0 (Halt ∷ []) (at 0) ≡ just (at 0) +halt-needs-no-fuel = refl + +halt-skips-effects : run 10 (Halt ∷ Store 4 0 ∷ []) (at 0) ≡ just (at 0) +halt-skips-effects = refl + +pc-selects-instruction : + run 0 (Store 4 0 ∷ Halt ∷ []) (at 1) ≡ just (at 1) +pc-selects-instruction = refl + +pc-at-end : run 0 (Nop ∷ []) (at 1) ≡ just (at 1) +pc-at-end = refl + +pc-beyond-end : run 0 (Nop ∷ []) (at 8) ≡ just (at 8) +pc-beyond-end = refl + +nop-needs-fuel : run 0 (Nop ∷ []) (at 0) ≡ nothing +nop-needs-fuel = refl + +nop-exact-fuel : run 1 (Nop ∷ []) (at 0) ≡ just (at 1) +nop-exact-fuel = refl + +halt-after-last-fuel : run 1 (Nop ∷ Halt ∷ []) (at 0) ≡ just (at 1) +halt-after-last-fuel = refl + +load-existing : step (at 3) (Load 4 1) ≡ + go (mk-state mem (2 ∷ 11 ∷ 9 ∷ []) io 4) +load-existing = refl + +load-default-memory : step (at 3) (Load 7 2) ≡ + go (mk-state mem (2 ∷ 5 ∷ 0 ∷ []) io 4) +load-default-memory = refl + +-- Missing destinations retain the register list under the existing set-reg +-- contract; only missing source registers fault. +load-missing-destination : step (at 3) (Load 4 3) ≡ go (at 4) +load-missing-destination = refl + +store-existing : step (at 3) (Store 4 2) ≡ + go (mk-state (mem-update mem 4 9) (2 ∷ 5 ∷ 9 ∷ []) io 4) +store-existing = refl + +store-missing : step (at 3) (Store 4 3) ≡ fault +store-missing = refl + +store-empty-registers : step (mk-state mem [] io 0) (Store 4 0) ≡ fault +store-empty-registers = refl + +add-existing : step (at 3) (Add 0 1 2) ≡ + go (mk-state mem (2 ∷ 5 ∷ 7 ∷ []) io 4) +add-existing = refl + +add-aliases-source : step (at 3) (Add 0 0 0) ≡ + go (mk-state mem (4 ∷ 5 ∷ 9 ∷ []) io 4) +add-aliases-source = refl + +add-missing-left : step (at 3) (Add 3 0 1) ≡ fault +add-missing-left = refl + +add-missing-right : step (at 3) (Add 0 3 1) ≡ fault +add-missing-right = refl + +add-missing-both : step (at 3) (Add 3 4 1) ≡ fault +add-missing-both = refl + +add-missing-destination : step (at 3) (Add 0 1 3) ≡ go (at 4) +add-missing-destination = refl + +fault-is-not-normal-stop : run 5 (Store 4 3 ∷ Halt ∷ []) (at 0) ≡ nothing +fault-is-not-normal-stop = refl + +add-fault-is-not-normal-stop : run 5 (Add 0 3 1 ∷ Halt ∷ []) (at 0) ≡ nothing +add-fault-is-not-normal-stop = refl + +-- A multi-instruction data dependency tests fetch and state threading. +arithmetic : Program +arithmetic = Load 4 0 ∷ Add 0 1 2 ∷ Store 7 2 ∷ Halt ∷ [] + +arithmetic-short-fuel : run 2 arithmetic (at 0) ≡ nothing +arithmetic-short-fuel = refl + +arithmetic-exact-fuel : run 3 arithmetic (at 0) ≡ + just (mk-state (mem-update mem 7 16) (11 ∷ 5 ∷ 16 ∷ []) io 3) +arithmetic-exact-fuel = refl + +stored-address : mem-update mem 7 16 7 ≡ 16 +stored-address = refl + +other-address-preserved : mem-update mem 7 16 4 ≡ 11 +other-address-preserved = refl + +jump-skips-fault : run 1 (Jump 2 ∷ Store 4 3 ∷ Halt ∷ []) (at 0) ≡ just (at 2) +jump-skips-fault = refl + +jump-beyond-end : run 1 (Jump 20 ∷ []) (at 0) ≡ just (at 20) +jump-beyond-end = refl + +jump-is-absolute : step (at 7) (Jump 2) ≡ go (at 2) +jump-is-absolute = refl + +-- Universal fuel regression: a backward jump never becomes a normal stop. +self-loop-no-fuel : ∀ n → run n loop (at 0) ≡ nothing +self-loop-no-fuel 0 = refl +self-loop-no-fuel (suc n) = self-loop-no-fuel n + +backward-loop : run 8 (Nop ∷ Jump 0 ∷ []) (at 0) ≡ nothing +backward-loop = refl + +start-resets-only-pc : start (at 19) ≡ at 0 +start-resets-only-pc = refl + +nop-result-starts-at-zero : cno-result nop-is-cno (at 19) ≡ at 1 +nop-result-starts-at-zero = refl + +pc-not-observable : obs-eq (at 1) (at 19) +pc-not-observable = (λ _ → refl) , refl , refl + +pc-still-in-full-equality : ¬ state-eq (at 1) (at 19) +pc-still-in-full-equality (_ , _ , _ , ()) + +memory-change-observable : ¬ obs-eq (mk-state empty-memory (2 ∷ 5 ∷ 9 ∷ []) io 0) (at 0) +memory-change-observable (m , _ , _) with m 4 +... | () + +register-change-observable : ¬ obs-eq (mk-state mem [] io 0) (at 0) +register-change-observable (_ , () , _) + +io-change-observable : ¬ obs-eq (mk-state mem (2 ∷ 5 ∷ 9 ∷ []) [] 0) (at 0) +io-change-observable (_ , _ , ()) + +-- Exercise adequacy on a run with real control flow, and determinism across +-- two fuel budgets, rather than only on the empty program witnesses. +skip : Program +skip = Jump 2 ∷ Store 4 3 ∷ Halt ∷ [] + +skip-derivation : skip ⊢ at 0 ⇓ at 2 +skip-derivation = run-sound 1 skip (at 0) refl + +complete-roundtrip : + run (proj₁ (run-complete skip-derivation)) skip (at 0) ≡ just (at 2) +complete-roundtrip = proj₂ (run-complete skip-derivation) + +fuel-independent : at 2 ≡ at 2 +fuel-independent = ⇓-det skip-derivation (run-sound 8 skip (at 0) refl) + +termination-resets-pc : Terminates skip (at 19) +termination-resets-pc = fuel→terminates {p = skip} {s = at 19} 1 refl + +-- Relocate jumps only in the second component; its local exit must become +-- the composite exit, rather than a self-loop at the second instruction. +relocated-layout : seq-comp (Nop ∷ []) + (Jump 2 ∷ Load 4 0 ∷ []) ≡ Nop ∷ Jump 3 ∷ Load 4 0 ∷ [] +relocated-layout = refl + +relocated-run : run 2 (seq-comp (Nop ∷ []) (Jump 2 ∷ Load 4 0 ∷ [])) (at 0) ≡ just (at 3) +relocated-run = refl + +relocation-preserves-other-instructions : + seq-comp (Nop ∷ []) (Nop ∷ Halt ∷ Load 4 0 ∷ Store 7 1 ∷ Add 0 1 2 ∷ []) ≡ + Nop ∷ Nop ∷ Halt ∷ Load 4 0 ∷ Store 7 1 ∷ Add 0 1 2 ∷ [] +relocation-preserves-other-instructions = refl + +halt-prefix-skips-second : + run 0 (seq-comp (Halt ∷ []) (Store 4 3 ∷ [])) (at 0) ≡ just (at 0) +halt-prefix-skips-second = refl + +-- Observable regression witnessing why composition requires Closed. +unclosed-prefix-changes-register : + run 2 (seq-comp jump2 jump2-load) (at 0) ≡ + just (mk-state mem (0 ∷ 5 ∷ 9 ∷ []) io 3) +unclosed-prefix-changes-register = refl diff --git a/proofs/agda/EchoBridgeCNO.agda b/proofs/agda/EchoBridgeCNO.agda index 06db811..f246346 100644 --- a/proofs/agda/EchoBridgeCNO.agda +++ b/proofs/agda/EchoBridgeCNO.agda @@ -1,18 +1,30 @@ -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} --- Concrete Echo/CNO instantiation against CNO.Program and CNO.eval. +-- Concrete Echo/CNO instantiation against CNO's pc-driven machine. -- --- Primary bridge: use CNO.state-eq directly as the relation in EchoRel. --- Secondary bridge: recover propositional equality with extensionality. +-- A CNO certificate fixes a total result function `cno-result`, and its +-- identity law is stated up to `CNO.obs-eq` (memory, registers, I/O; the +-- program counter is control state). So: +-- +-- * primary bridge: relation-based echoes via `EchoRel ... CNO.obs-eq` +-- (no extensionality needed); +-- * secondary bridge: propositional `Echo` on the observable projection, +-- given function extensionality for memory, plus a `CNOModel` instance +-- over observable states. +-- +-- Until 2026-11-09 this module used the old list-walking `eval` and +-- `state-eq`, under which only Halt-only programs were CNOs. module EchoBridgeCNO where open import Level using (zero) -open import Data.Product using (_,_) -open import Relation.Binary.PropositionalEquality using (_≡_; refl) +open import Data.Product using (Σ; _×_; _,_) +open import Data.Unit using (⊤; tt) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) open import Axiom.Extensionality.Propositional using (Extensionality) import CNO +module PS = CNO.ProgramState open import EchoBridgeScaffold using ( CNOModel ; Echo @@ -21,21 +33,51 @@ open import EchoBridgeScaffold using ; echo-from-rel ) +---------------------------------------------------------------------------- +-- Primary: up to observable equality +---------------------------------------------------------------------------- + echo-from-cno-program-rel : (p : CNO.Program) → - CNO.IsCNO p → + (cno : CNO.IsCNO p) → (s : CNO.ProgramState) → - EchoRel (CNO.eval p) CNO.state-eq s + EchoRel (CNO.cno-result cno) CNO.obs-eq s echo-from-cno-program-rel p cno s = - echo-from-rel (CNO.eval p) CNO.state-eq s s - (CNO.IsCNO.cno-identity cno s) + echo-from-rel (CNO.cno-result cno) CNO.obs-eq s s + (CNO.cno-preserves-state cno s) absolute-zero-echo-rel : (s : CNO.ProgramState) → - EchoRel (CNO.eval CNO.absolute-zero) CNO.state-eq s + EchoRel (CNO.cno-result CNO.absolute-zero-is-cno) CNO.obs-eq s absolute-zero-echo-rel s = echo-from-cno-program-rel CNO.absolute-zero CNO.absolute-zero-is-cno s +---------------------------------------------------------------------------- +-- Secondary: propositional equality on observable states +---------------------------------------------------------------------------- + +Obs : Set +Obs = CNO.Memory × CNO.Registers × CNO.IOState + +observe : CNO.ProgramState → Obs +observe s = PS.state-memory s , PS.state-registers s , PS.state-io s + +-- An observable state, placed at pc 0. +inject : Obs → CNO.ProgramState +inject (m , r , io) = CNO.mk-state m r io 0 + +observe-inject : ∀ o → observe (inject o) ≡ o +observe-inject (m , r , io) = refl + +obs-eq→≡ : + Extensionality zero zero → + ∀ {s₁ s₂ : CNO.ProgramState} → + CNO.obs-eq s₁ s₂ → observe s₁ ≡ observe s₂ +obs-eq→≡ ext {CNO.mk-state m₁ r₁ i₁ pc₁} {CNO.mk-state m₂ r₂ i₂ pc₂} + (m-eq , r-eq , io-eq) + rewrite ext m-eq | r-eq | io-eq = refl + +-- Full state equality still yields propositional equality. state-eq→≡ : Extensionality zero zero → ∀ {s₁ s₂ : CNO.ProgramState} → @@ -44,27 +86,49 @@ state-eq→≡ ext {CNO.mk-state m₁ r₁ i₁ pc₁} {CNO.mk-state m₂ r₂ i (m-eq , r-eq , io-eq , pc-eq) rewrite ext m-eq | r-eq | io-eq | pc-eq = refl -program-state-model : Extensionality zero zero → CNOModel CNO.ProgramState -program-state-model ext = record - { Op = CNO.Program - ; run = CNO.eval - ; IsCNO = CNO.IsCNO - ; cno-identity = λ cno s → - state-eq→≡ ext (CNO.IsCNO.cno-identity cno s) - } - echo-from-cno-program-≡ : (ext : Extensionality zero zero) → (p : CNO.Program) → - CNO.IsCNO p → + (cno : CNO.IsCNO p) → (s : CNO.ProgramState) → - Echo (CNO.eval p) s + Echo (λ x → observe (CNO.cno-result cno x)) (observe s) echo-from-cno-program-≡ ext p cno s = - echo-from-cno (program-state-model ext) p cno s + s , obs-eq→≡ ext {CNO.cno-result cno s} {s} (CNO.cno-preserves-state cno s) absolute-zero-echo-≡ : (ext : Extensionality zero zero) → (s : CNO.ProgramState) → - Echo (CNO.eval CNO.absolute-zero) s + Echo (λ x → observe (CNO.cno-result CNO.absolute-zero-is-cno x)) (observe s) absolute-zero-echo-≡ ext s = echo-from-cno-program-≡ ext CNO.absolute-zero CNO.absolute-zero-is-cno s + +-- Certified programs act on observable states as the identity. The +-- certificate travels with the operation, so the model's own `IsCNO` +-- predicate is trivial. +CertifiedProgram : Set +CertifiedProgram = Σ CNO.Program CNO.IsCNO + +run-obs : CertifiedProgram → Obs → Obs +run-obs (p , cno) o = observe (CNO.cno-result cno (inject o)) + +program-state-model : Extensionality zero zero → CNOModel Obs +program-state-model ext = record + { Op = CertifiedProgram + ; run = run-obs + ; IsCNO = λ _ → ⊤ + ; cno-identity = λ { {p , cno} _ o → + trans′ (obs-eq→≡ ext {CNO.cno-result cno (inject o)} {inject o} + (CNO.cno-preserves-state cno (inject o))) + (observe-inject o) } + } + where + trans′ : ∀ {a b c : Obs} → a ≡ b → b ≡ c → a ≡ c + trans′ refl q = q + +echo-from-certified-program : + (ext : Extensionality zero zero) → + (cp : CertifiedProgram) → + (o : Obs) → + Echo (run-obs cp) o +echo-from-certified-program ext cp o = + echo-from-cno (program-state-model ext) cp tt o diff --git a/proofs/agda/EchoBridgeCNOTests.agda b/proofs/agda/EchoBridgeCNOTests.agda new file mode 100644 index 0000000..b66cef9 --- /dev/null +++ b/proofs/agda/EchoBridgeCNOTests.agda @@ -0,0 +1,67 @@ +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} + +-- Bridge regressions use a nonzero initial pc and nonempty observables. +module EchoBridgeCNOTests where + +open import CNO +open ProgramState +open import EchoBridgeCNO +open import EchoBridgeScaffold using (CNOModel) +open import CNOTests using (at; mem; io) +open import Data.List using ([]; _∷_) +open import Data.Product using (_,_; proj₁; proj₂) +open import Data.Unit using (tt) +open import Level using (zero) +open import Axiom.Extensionality.Propositional using (Extensionality) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +visible : Obs +visible = mem , (2 ∷ 5 ∷ 9 ∷ []) , io + +projection-discards-pc : observe (at 19) ≡ visible +projection-discards-pc = refl + +injection-starts-at-zero : inject visible ≡ at 0 +injection-starts-at-zero = refl + +projection-roundtrip : observe (inject visible) ≡ visible +projection-roundtrip = observe-inject visible + +injection-roundtrip-resets-pc : inject (observe (at 19)) ≡ start (at 19) +injection-roundtrip-resets-pc = refl + +nop-certified : CertifiedProgram +nop-certified = (Nop ∷ []) , nop-is-cno + +certified-nop-observables : run-obs nop-certified visible ≡ visible +certified-nop-observables = refl + +certified-composition-observables : + run-obs (seq-comp (Nop ∷ []) (Nop ∷ []) , nop-nop-is-cno) visible ≡ visible +certified-composition-observables = refl + +relational-echo-retains-input : + proj₁ (echo-from-cno-program-rel (Nop ∷ []) nop-is-cno (at 19)) ≡ at 19 +relational-echo-retains-input = refl + +relational-echo-certifies-observables : + obs-eq (cno-result nop-is-cno (at 19)) (at 19) +relational-echo-certifies-observables = + proj₂ (echo-from-cno-program-rel (Nop ∷ []) nop-is-cno (at 19)) + +-- Extensionality stays an explicit parameter, never a test postulate. +model-uses-certified-run : (ext : Extensionality zero zero) → + CNOModel.run (program-state-model ext) nop-certified visible ≡ visible +model-uses-certified-run ext = refl + +model-identity : (ext : Extensionality zero zero) → + run-obs nop-certified visible ≡ visible +model-identity ext = CNOModel.cno-identity (program-state-model ext) {op = nop-certified} tt visible + +certified-echo-retains-observables : (ext : Extensionality zero zero) → + proj₁ (echo-from-certified-program ext nop-certified visible) ≡ visible +certified-echo-retains-observables ext = refl + +propositional-echo-retains-input : (ext : Extensionality zero zero) → + proj₁ (echo-from-cno-program-≡ ext (Nop ∷ []) nop-is-cno (at 19)) ≡ at 19 +propositional-echo-retains-input ext = refl diff --git a/proofs/agda/EchoBridgeScaffold.agda b/proofs/agda/EchoBridgeScaffold.agda index 60c227a..7b28d41 100644 --- a/proofs/agda/EchoBridgeScaffold.agda +++ b/proofs/agda/EchoBridgeScaffold.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} -- Echo/CNO Agda bridge scaffold. -- diff --git a/proofs/agda/OND.agda b/proofs/agda/OND.agda index baa32be..3f96e7f 100644 --- a/proofs/agda/OND.agda +++ b/proofs/agda/OND.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe --without-K #-} +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} {- Observational Null Operations (OND): The Disclosure Pillar — Agda diff --git a/proofs/agda/README.adoc b/proofs/agda/README.adoc index b6c17ff..e413531 100644 --- a/proofs/agda/README.adoc +++ b/proofs/agda/README.adoc @@ -4,9 +4,9 @@ This directory currently contains: -* `CNO.agda` — main Agda CNO development (compiles locally). +* `CNO.agda` — main Agda CNO development: a pc-driven machine (`_⊢_⇓_`, fuel interpreter `run`, adequacy both ways), `IsCNO` up to observable state, composition under a closedness condition, and witnesses for and against. * `EchoBridgeScaffold.agda` — compile-safe interface layer for bridging CNO identity witnesses to the echo/fiber shape used in `echo-types`. -* `EchoBridgeCNO.agda` — concrete model instantiation from `CNO.Program` / `eval` into the scaffold interface. +* `EchoBridgeCNO.agda` — concrete model instantiation from certified programs and `cno-result` into the scaffold interface. == Purpose of `EchoBridgeScaffold.agda` @@ -21,17 +21,14 @@ It provides: == Purpose of `EchoBridgeCNO.agda` -This module imports `CNO.agda` and instantiates `CNOModel` concretely with: +This module imports `CNO.agda`. `CNO.cno-identity` is phrased as `obs-eq` +(memory, registers and I/O, with function-valued memory; the program counter is +not compared), so the bridge provides two layers: -* `Op = Program` -* `run = eval` -* `IsCNO = IsCNO` - -Because `CNO.cno-identity` is phrased as `state-eq` (with function-valued memory), -the bridge provides two layers: - -* primary: relation-based echoes via `EchoRel ... CNO.state-eq` (no extensionality needed); -* secondary: propositional `Echo` corollaries via a function-extensionality parameter. +* primary: relation-based echoes via `EchoRel (cno-result cno) CNO.obs-eq` (no extensionality needed); +* secondary: propositional `Echo` on the observable projection `observe`, via a + function-extensionality parameter, and a `CNOModel` instance over observable + states with `Op = Σ Program IsCNO` and `run = run-obs`. == Integration plan