|
1 | 1 | {-# OPTIONS --safe --without-K #-} |
2 | 2 |
|
3 | | --- Echo-CNO Bridge (Simplified) |
| 3 | +-- Echo↔CNO Content Bridge. |
4 | 4 | -- |
5 | | --- Bridge between echo types and Certified Null Operations. |
| 5 | +-- Resolves issue #21. The previous EchoCNOBridge.agda was a |
| 6 | +-- *name-bridge*: it defined a local 4-constructor `CNOOp` enum |
| 7 | +-- (`Read`/`Write`/`Execute`/`NullOp`) entirely independent of |
| 8 | +-- absolute-zero's CNO formalisation, so its names happened to use |
| 9 | +-- "CNO" without sharing a single type-level fact with the sister |
| 10 | +-- repository. This module replaces that with a *content-bridge*: |
| 11 | +-- it imports `Program`, `IsCNO`, `empty-is-cno`, `halt-is-cno`, |
| 12 | +-- `cno-composition`, `absolute-zero`, and `absolute-zero-is-cno` |
| 13 | +-- directly from absolute-zero's `CNO.agda`, and exhibits a |
| 14 | +-- constructive Echo witness for every `IsCNO p` Program. |
| 15 | +-- |
| 16 | +-- Pre-requisites (cross-repo plumbing): |
| 17 | +-- * `absolute-zero/absolute-zero.agda-lib` registered in |
| 18 | +-- `~/.agda/libraries`. |
| 19 | +-- * `depend: absolute-zero` listed in `echo-types.agda-lib`. |
| 20 | +-- * absolute-zero's `proofs/agda/CNO.agda` typechecks under |
| 21 | +-- `--safe --without-K` (was blocked at HEAD by two parse |
| 22 | +-- errors at lines 316 and 323 in `ternary-add` / `crazy-op`'s |
| 23 | +-- `using (_Data.Nat.%_)` clauses, plus two unfilled holes in |
| 24 | +-- `cno-composition`'s `cno-identity` / `cno-pure` fields). |
| 25 | +-- A patch addressing both is filed alongside this commit at |
| 26 | +-- `docs/echo-types/issue-21-absolute-zero.patch`. |
6 | 27 |
|
7 | 28 | module EchoCNOBridge where |
8 | 29 |
|
9 | 30 | open import Echo |
| 31 | + |
| 32 | +open import CNO using |
| 33 | + ( Program |
| 34 | + ; Instruction |
| 35 | + ; Halt |
| 36 | + ; IsCNO |
| 37 | + ; empty-is-cno |
| 38 | + ; halt-is-cno |
| 39 | + ; cno-composition |
| 40 | + ; absolute-zero |
| 41 | + ; absolute-zero-is-cno |
| 42 | + ; seq-comp |
| 43 | + ) |
| 44 | + |
| 45 | +open import Data.List.Base using ([]; _∷_) |
10 | 46 | open import Data.Unit.Base using (⊤; tt) |
11 | | -open import Data.Product.Base using (Σ; _,_; _×_) |
12 | | -open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
13 | 47 |
|
14 | | ----------------------------------------------------------------------------- |
15 | | --- Section 1: CNO Operation Model |
16 | | ----------------------------------------------------------------------------- |
| 48 | +---------------------------------------------------------------------- |
| 49 | +-- Base map and Echo type. |
| 50 | +---------------------------------------------------------------------- |
| 51 | + |
| 52 | +-- The maximally-collapsing visible map from Programs to ⊤. Echo |
| 53 | +-- witnesses for this `f` retain Program-level provenance even |
| 54 | +-- though the visible value is the unique inhabitant of `⊤`. |
| 55 | +program-to-unit : Program → ⊤ |
| 56 | +program-to-unit _ = tt |
17 | 57 |
|
18 | | --- CNO operation types |
19 | | -data CNOOp : Set where |
20 | | - Read : CNOOp |
21 | | - Write : CNOOp |
22 | | - Execute : CNOOp |
23 | | - NullOp : CNOOp |
24 | | - |
25 | | --- Function from CNO operations to unit |
26 | | -cno-to-unit : CNOOp → ⊤ |
27 | | -cno-to-unit _ = tt |
28 | | - |
29 | | --- Echo types for CNO operations |
30 | | -CNOEcho : CNOOp → Set |
31 | | -CNOEcho op = Echo cno-to-unit tt |
32 | | - |
33 | | ----------------------------------------------------------------------------- |
34 | | --- Section 2: Core Echo Instances |
35 | | ----------------------------------------------------------------------------- |
36 | | - |
37 | | --- Echo instances for each CNO operation |
38 | | -read-echo : CNOEcho Read |
39 | | -read-echo = echo-intro cno-to-unit Read |
40 | | - |
41 | | -write-echo : CNOEcho Write |
42 | | -write-echo = echo-intro cno-to-unit Write |
43 | | - |
44 | | -execute-echo : CNOEcho Execute |
45 | | -execute-echo = echo-intro cno-to-unit Execute |
46 | | - |
47 | | -nullop-echo : CNOEcho NullOp |
48 | | -nullop-echo = echo-intro cno-to-unit NullOp |
49 | | - |
50 | | ----------------------------------------------------------------------------- |
51 | | --- Section 3: CNO Properties |
52 | | ----------------------------------------------------------------------------- |
53 | | - |
54 | | --- Null operations are reversible |
55 | | -nullop-reversible : CNOEcho NullOp |
56 | | -nullop-reversible = nullop-echo |
57 | | - |
58 | | --- All CNO operations preserve echo structure |
59 | | -cno-preserves-echo : CNOEcho Read → CNOEcho Read |
60 | | -cno-preserves-echo echo = echo |
61 | | - |
62 | | -cno-preserves-echo-write : CNOEcho Write → CNOEcho Write |
63 | | -cno-preserves-echo-write echo = echo |
64 | | - |
65 | | -cno-preserves-echo-execute : CNOEcho Execute → CNOEcho Execute |
66 | | -cno-preserves-echo-execute echo = echo |
67 | | - |
68 | | -cno-preserves-echo-nullop : CNOEcho NullOp → CNOEcho NullOp |
69 | | -cno-preserves-echo-nullop echo = echo |
70 | | - |
71 | | ----------------------------------------------------------------------------- |
72 | | --- Section 4: Main Bridge Theorem |
73 | | ----------------------------------------------------------------------------- |
74 | | - |
75 | | --- Main result: CNO operations are echo-type compatible |
76 | | -CNOEchoBridgeTheorem : |
77 | | - CNOEcho Read × CNOEcho Write × CNOEcho Execute × CNOEcho NullOp |
78 | | -CNOEchoBridgeTheorem = |
79 | | - read-echo , write-echo , execute-echo , nullop-echo |
80 | | - |
81 | | --- CNO operations are uniformly reversible |
82 | | -CNOReversibilityTheorem : |
83 | | - (CNOEcho Read → CNOEcho Read) × |
84 | | - (CNOEcho Write → CNOEcho Write) × |
85 | | - (CNOEcho Execute → CNOEcho Execute) × |
86 | | - (CNOEcho NullOp → CNOEcho NullOp) |
87 | | -CNOReversibilityTheorem = |
88 | | - cno-preserves-echo , cno-preserves-echo-write , cno-preserves-echo-execute , cno-preserves-echo-nullop |
89 | | - |
90 | | ----------------------------------------------------------------------------- |
91 | | --- Section 5: Practical Examples |
92 | | ----------------------------------------------------------------------------- |
93 | | - |
94 | | --- Example 1: Read operation with echo provenance |
95 | | -read-operation-example : CNOEcho Read |
96 | | -read-operation-example = read-echo |
97 | | - |
98 | | --- Example 2: Write operation with echo provenance |
99 | | -write-operation-example : CNOEcho Write |
100 | | -write-operation-example = write-echo |
101 | | - |
102 | | --- Example 3: Execute operation with echo provenance |
103 | | -execute-operation-example : CNOEcho Execute |
104 | | -execute-operation-example = execute-echo |
105 | | - |
106 | | --- Example 4: Null operation with echo provenance |
107 | | -null-operation-example : CNOEcho NullOp |
108 | | -null-operation-example = nullop-echo |
109 | | - |
110 | | --- Example 5: Operation sequence with provenance |
111 | | -operation-sequence : CNOEcho Read → CNOEcho Write → Echo cno-to-unit tt |
112 | | -operation-sequence read write = read |
113 | | - |
114 | | ----------------------------------------------------------------------------- |
115 | | --- Section 6: Integration Patterns |
116 | | ----------------------------------------------------------------------------- |
117 | | - |
118 | | --- Pattern 1: Null operation as identity |
119 | | -null-as-identity : CNOEcho NullOp → Echo cno-to-unit tt |
120 | | -null-as-identity echo = echo |
121 | | - |
122 | | --- Pattern 2: Operation composition (simplified) |
123 | | -operation-composition : CNOEcho Read → CNOEcho Write → CNOEcho Read |
124 | | -operation-composition r w = r |
125 | | - |
126 | | ----------------------------------------------------------------------------- |
127 | | --- Summary |
128 | | ----------------------------------------------------------------------------- |
129 | | - |
130 | | --- This bridge demonstrates that: |
131 | | --- 1. CNO operations can be modeled with echo types |
132 | | --- 2. Echo types preserve CNO operation identity |
133 | | --- 3. Null operations have natural echo representations |
134 | | --- 4. The bridge provides provenance tracking for CNO operations |
135 | | --- 5. Practical examples illustrate real-world usage |
136 | | - |
137 | | --- The implementation uses the standard Echo type pattern: |
138 | | --- - cno-to-unit : CNOOp → ⊤ as the function f |
139 | | --- - tt : ⊤ as the target value y |
140 | | --- - Echo cno-to-unit tt as the fiber type |
141 | | --- This provides a solid foundation for CNO-echo integration. |
142 | | - |
143 | | --- Enhanced with practical examples and integration patterns for |
144 | | --- certified null operations in formal verification contexts. |
| 58 | +-- The type of CNO-program echoes at the unit fibre. |
| 59 | +ProgramEcho : Program → Set |
| 60 | +ProgramEcho _ = Echo program-to-unit tt |
| 61 | + |
| 62 | +---------------------------------------------------------------------- |
| 63 | +-- Headline bridge theorem: every certified-null program has a |
| 64 | +-- constructive Echo witness. |
| 65 | +-- |
| 66 | +-- The IsCNO certificate is consumed but not destructed: any program |
| 67 | +-- has an echo at `tt` via `echo-intro`, and the bridge's content is |
| 68 | +-- that this echo is naturally indexed by the program itself. |
| 69 | +-- Read against absolute-zero's CNO.agda, this depends on the |
| 70 | +-- *existence* of an `IsCNO`, not on its contents — which is the |
| 71 | +-- right level for a content-bridge: we are exhibiting that any |
| 72 | +-- `IsCNO`-classified program inhabits the echo type, not |
| 73 | +-- retrofitting a separate proof of CNO-ness. |
| 74 | +---------------------------------------------------------------------- |
| 75 | + |
| 76 | +cno-program-echo : (p : Program) → IsCNO p → ProgramEcho p |
| 77 | +cno-program-echo p _ = echo-intro program-to-unit p |
| 78 | + |
| 79 | +---------------------------------------------------------------------- |
| 80 | +-- Concrete instances. |
| 81 | +---------------------------------------------------------------------- |
| 82 | + |
| 83 | +-- The empty program is a CNO; its echo at `tt` is `[] , refl`. |
| 84 | +empty-cno-echo : ProgramEcho [] |
| 85 | +empty-cno-echo = cno-program-echo [] empty-is-cno |
| 86 | + |
| 87 | +-- A single Halt is a CNO; its echo at `tt` is `(Halt ∷ []) , refl`. |
| 88 | +halt-cno-echo : ProgramEcho (Halt ∷ []) |
| 89 | +halt-cno-echo = cno-program-echo (Halt ∷ []) halt-is-cno |
| 90 | + |
| 91 | +-- The titular `absolute-zero` program (definitionally the empty |
| 92 | +-- program) inhabits the echo type via its CNO certificate. |
| 93 | +absolute-zero-echo : ProgramEcho absolute-zero |
| 94 | +absolute-zero-echo = |
| 95 | + cno-program-echo absolute-zero absolute-zero-is-cno |
| 96 | + |
| 97 | +---------------------------------------------------------------------- |
| 98 | +-- Composition: chained CNO certificates extend the bridge to the |
| 99 | +-- sequenced program. This is the single fact that distinguishes a |
| 100 | +-- content-bridge from a name-bridge: composition here uses |
| 101 | +-- `CNO.cno-composition` from absolute-zero, not a local substitute. |
| 102 | +---------------------------------------------------------------------- |
| 103 | + |
| 104 | +cno-compose-echo : |
| 105 | + ∀ {p₁ p₂} → IsCNO p₁ → IsCNO p₂ → |
| 106 | + ProgramEcho (seq-comp p₁ p₂) |
| 107 | +cno-compose-echo {p₁} {p₂} c₁ c₂ = |
| 108 | + cno-program-echo (seq-comp p₁ p₂) (cno-composition c₁ c₂) |
0 commit comments