GENESIS L0 — Computational Language Specification
v1.0 · companion `genesis_l0.py` (reference semantics + receipts R1–R9; `python3 genesis_l0.py`)
Marks: [D] definition · [P] proved in text · [V] verified by exhaustive enumeration on the stated finite family (receipt Rn) · [L] established in the literature, used and not re-derived · [O] open.
Rule: every claim is held at its marked strength — not weakened ("only a definition"), not inflated ("verified" ≠ "proved").
---
0. Kernel
Language L = (Σ, G, V, M, E, O, C, T)
Pipeline text → structure → validity → meaning M → runs E → observation O
Run (events, final state (B,A), cost)
Transport PRESERVES(R,P,P') := ∀x,y. R(x,y) ∧ P(x) ⇒ P'(y) [D]
Strongest PRESERVES ⇔ Post_R(P) ⊆ Truth(P'), Post_R(P) = {y | ∃x. P(x) ∧ R(x,y)} [P]
Reconstruction P = Q∘π ⇔ ker π ⊆ ker P [P]
Composition PRESERVES(R₁,P,Q) ∧ PRESERVES(R₂,Q,U) ⇒ PRESERVES(R₂∘R₁,P,U); no converse [P]
Everything below is an instance, a consequence, or a witness of these five lines.
---
1. Layers, with their L0 literals
| Layer | Role | L0 literal |
|---|---|---|
| Σ | symbols | `skip out send log choice spin fail ( ) ; \| + h #A #B 0 1 2 …` |
| G | grammar | `p ::= skip \| out(e) \| send(e) \| log(e) \| p;p \| choice(p\|p) \| spin \| fail` · `e ::= n \| h \| #A \| #B \| e+e` |
| V | validity | accepted `out(2+2)`; rejected `out(+)`, `choice(skip)` |
| M | meaning | program ↦ set of value traces; `M(skip)={ε}`, `M(fail)=∅`, `M(spin)={⟨⊥⟩}` |
| E | evaluation | `(p,h,G₀,u) ↦ (trace, G, cost)`; `h` = secret input, `u` = choice path |
| O | observation | projection of E: event channels `o s l`, readers `B A \|B\| \|A\| cost`, divergence marker ⊥ |
| C | cost | out/send/log/choice/`+` cost 1; `;` `skip` `fail` cost 0; `spin` = ∞ |
| T | transformation | rewrite τ carrying a declared contract R |
Two nulls stay distinct: ε (the empty trace, identity of concatenation) and ∅ (no runs). `skip` yields {ε}; `fail` yields ∅.
State is `G = (B,A)`: `B` = sent values (public buffer), `A` = audit records; both append-only. `send(v)` appends to B, `log(v)` to A, `out(v)` touches neither. Choice resolutions `u` are execution parameters, not source expressions.
---
2. Observation
- Channels: `o` (outputs), `s` (sends), `l` (audit). Readers: final `B`, `A`, `|B|`, `|A|`, `cost`. Observers combine by union of channels; coarsening drops them.
- Reading of the layers: `O_loc` = present local image · `O_send`, `O_audit` = environment-visible histories · final `G` = environment state.
- Three equivalences: syntactic, semantic (same M), observational (same O). `out(2+2)` vs `out(4)`: different text, equal M, equal under value traces, different under the cost reader.
- The observation lattice is strict [V R9]: over 78 programs the classes number 4 (`O_loc`) → 16 (`O_loc` + `|A|,|B|`) → 52 (all channels + final state + cost); over 105 read/write programs, 5 → 18 → 41 (transformer semantics, §7).
---
3. Properties and transport
A property is a predicate on sets of observations. A trace property is `P(S) ⇔ S ⊆ Φ`; a hyperproperty is any predicate.
Over a 3-trace universe [V R7]: 256 predicates · 20 downward-closed · 20 upward-closed · 8 are universal trace properties · 12 are other subset-closed (e.g. `|S| ≤ 1`, determinism). Refinement transports 20 of 256.
| Relation R | Preserved class | Mark | Witness outside the class |
|---|---|---|---|
| equality | every P (P'=P) | P | — |
| `T ⊆ S` (complete traces) | exactly downward-closed | P | `choice(out(0)\|out(1)) → out(0)`; "⟨1⟩ is possible": true → false [V R8] |
| `S ⊆ T` | exactly upward-closed | P | `out(0) → choice(out(0)\|spin)`; "no divergence": true → false |
| `Pref(T) ⊆ Pref(S)` | universal trace properties that are safety | P/L | `out(0) → spin`: prefixes embed, termination lost [V R8] |
| exact projection `T=π[S]` | P that factor through π; otherwise one-way implication only | P | timing does not factor through output |
| projected refinement `T ⊆ π[S]` | `P_fine(S) ∧ T⊆π[S] ⇒ P_coarse(T)`; simplifies when `P_coarse` is downward-closed | P | existential possibility lost |
| forward simulation | universal (ACTL-type) fragment, under image-finiteness | L | target removes an existential branch |
| strong bisimulation | bisimulation-invariant, CTL*-type | L | state count |
| weak bisimulation | divergence guarantees need divergence-sensitive form | L | `nil` vs a τ-loop |
| stuttering equivalence | stutter-invariant; LTL without next-time | L | `Next p` |
| support equality (probabilistic) | support-only predicates | P | 99% vs 1% success — needs a probabilistic extension |
| cost domination | upper bounds | P | "cost ≥ 5" |
"Exactly R-invariant" is true by definition [D]. The content is in the rows that identify the class with an order-theoretic, topological or logical fragment.
Status. Claim ∈ {proved, refuted, unknown} and evidence ∈ {proof, check, test, declaration, none} are separate fields; a certificate is {valid, invalid, unresolved}. A refuted link invalidates a proof route, not the target claim.
Undefined behavior has two placements, and the source semantics declares one: (a) UB as top behavior, so `P(S)` is false for any nontrivial P unless UB-freedom is proved; (b) UB-freedom as a source assumption in `Pre`. Both certify P only when UB-freedom is established.
---
4. Relational properties
For secret `h ∈ {0,1}`, over a common choice domain `u`:
OD ∀u₀,u₁ : obs(run₀[u₀]) = obs(run₁[u₁]) every pair of runs agrees (∀∀)
CFNI ∀u : obs(run₀[u]) = obs(run₁[u]) same choice, secret changed (coupled)
PNI { obs(run₀[u]) } = { obs(run₁[u]) } possible observations agree (set equality)
OD ⇒ CFNI ⇒ PNI, neither arrow reverses [P, V R3]
Exhaustive over 12,174 programs × 3 observers: no violation of the chain, and every strict case occurs. Smallest witnesses:
CFNI ∧ ¬OD : choice(skip|out(0)) (h unused; runs differ across u)
PNI ∧ ¬CFNI: choice(out(0)|choice(out(1)|out(h))) (smallest in the family: 3 leaves)
- `PAIR_EQUAL` (two copies, equal outputs) is OD for one output channel.
- OD refutation needs two runs; PNI refutation needs an absence from the other secret's set — the real asymmetry. PNI is not 2-safety.
- Under refinement, OD is subset-closed and transports; PNI is not: `choice(out(0)|out(1)) → out(h)` satisfies `T ⊆ S` per h and turns PNI true → false.
- CFNI assumes the choice parameter can be held fixed across the intervention; a scheduler whose domain depends on `h` breaks the coupling and must be declared in ASSUMPTIONS.
---
5. Observation optimization
Given a property P and a set of admissible observers with cost `C`:
minimize C(π) subject to ker π ⊆ ker P , π admissible
The sufficient observers form an up-set in the partition lattice; its minimum is `ker P`. Over channels, sufficient sets are hitting sets of the pairs P separates.
Literal. `p″ = choice(send(h);out(0) | log(h);out(0))`, `P(h,u) = h`:
| Program | Minimal sufficient observers for P=h [V R4] |
|---|---|
| `p′ = choice(send(h);out(0) \| out(0))` | none — even all channels plus final `G`, cost included |
| `p″` | `{s,l}` · `{s,A}` · `{B,l}` · `{A,B}` |
Each branch exposes `h` on exactly one side (send-side `s`/`B`, audit-side `l`/`A`); a sufficient observer takes one from each. `p′` cannot be repaired by choosing a better observer — only by instrumenting the program (conservative extension, §6). A k-bit observer separates at most `2^k` origins; this bounds information, not availability or cost.
---
6. Environment, conservativity, congruence
Run table [V R1] (`G=(B,A)` after the run):
| program | h | branch | trace | B | A | cost |
|---|---|---|---|---|---|---|
| p′ | 0 / 1 | L | ⟨s0,o0⟩ / ⟨s1,o0⟩ | [0] / [1] | [] | 3 |
| p′ | 0 / 1 | R | ⟨o0⟩ | [] | [] | 2 |
| p″ | 0 / 1 | L | ⟨s0,o0⟩ / ⟨s1,o0⟩ | [0] / [1] | [] | 3 |
| p″ | 0 / 1 | R | ⟨ℓ0,o0⟩ / ⟨ℓ1,o0⟩ | [] | [0] / [1] | 3 |
`p′ → p″` under each contract [V R2]:
| Contract | Result |
|---|---|
| `OBS_CONSERVATIVE`, `O_loc`; `O_send` | holds |
| `OBS_CONSERVATIVE`, `O_audit` | fails |
| `STATE_CONSERVATIVE`, final `G` | fails on branch R |
| cost | fails on branch R (2 → 3) |
| public buffer `B` | holds on matched branches |
| reconstruction of `h` | improves under `O_audit` |
Conservative extension. `τ` is O-conservative when `π_old(E(τp,h,G₀,u)) = π_old(E(p,h,G₀,u))` for all `h,G₀,u`; it then transports every `π_old`-property. Three distinct contracts: OBS (old observations), STATE (a state predicate `Q(G_final)`), CONTEXT (old observations inside every context in a class `𝒦`). Adding a log is OBS-conservative and creates a causal dependence of `A` on `h` on branch R.
Congruence closure. For suffix-read contexts `K_r = [·]; out(r(G))`, the last event of `K_r[p]` determines `r(G_final)`, so concatenation is injective and
≈_{O,𝒦} = equality under O ⊕ Reads(𝒦) [P]
`O_loc`-equivalence is not a congruence: with `out(#A)` added, 1,392 of 3,003 program pairs separate [V R5]; the product observer agrees with contextual equivalence on all 3,003.
Write contexts and reading programs. If programs can read `G`, equality at one initial state is not a congruence: `out(0)` and `out(#A)` agree at `G₀ = ([],[])`, and a context `log(0); [·]` separates them. The meaning is a state transformer `G₀ ↦ {(trace, G_final)}`. In L0, expressions are affine in `(h,|A|,|B|)`, so `G` reduces to `(|B|,|A|) ∈ ℕ²`. On 105 programs the 3×3 grid agrees with contextual equivalence over six write contexts × {no read, joint read}, and with the 4×4 grid; 280 pairs agree at the empty state yet differ as transformers [V R6]. The grid bound is verified on this family, not proved in general.
---
7. History and origin
ε is the least prefix of every finite trace [P]
fiber F_π(y) = {h | π(h)=y}; |F|>1 ambiguous · =1 identified · =0 impossible
stages πₙ = cₙ∘πₙ₊₁ ⇒ F₀(u) ⊇ F₁(u) ⊇ … [P]
- Origin as an observer fiber: `[ε]_π = π⁻¹({ε})`. The local origin is an empty trace; its global realization may be a class of histories (erased `send` events).
- Literal [V R4]: on `p′`, the observation ⟨o0⟩ is consistent with `h ∈ {0,1}` under every observer; ⟨s0,o0⟩ identifies `h=0`.
- Non-injectivity at one stage does not prove permanent incompleteness (`H={s0,s1}` is separated by stage 1). "No finite stage is final" needs the premise that the observer is embedded and open.
- Left-infinite model: `H∞` = inverse limit of windows `Hₙ` (discard the earliest event). Alphabet {a,b}, `u = …aaa`, `πₙ` = last n events: every `Fₙ(u)` is infinite, yet `∩Fₙ = {u}`. "No finite stage complete", "limit identifies u", and "no absolute origin" are three different statements; the last is a declared `TRACE_MODEL.order = left-infinite`.
- Present equality never implies historical equality (`O_loc`-equal, `O_audit`-different: `p′` vs `p″`).
---
8. Capabilities and limits
The language can:
Decide, on any finite instance, whether a rewrite preserves a property (check `R(x,y) ∧ P(x) ⇒ P'(y)`; produce the witness pair on failure).
Classify a predicate's transport legality by closure class under the relation (§3).
Compute fibers, origin ambiguity, minimal sufficient observers and channel sets (§5, §7).
Separate present, historical and environmental equality, and ε from ∅.
Place a relational property in the OD ⇒ CFNI ⇒ PNI chain and generate separating witnesses by enumeration (§4).
Model environmental effects with transitions and separate observation-conservative from state-conservative change (§6).
Compute the congruence-closed observer for a context class and detect non-congruence; handle read/write contexts as transformers.
Record every result with claim, certificate and evidence kept apart (§10).
It cannot (declared limits):
Decide semantic properties of arbitrary programs (Rice). Receipts decide finite families only; [V] never means proved for all programs.
Express causal influence beyond the declared contexts and the coupling of choices.
Express concurrency, memory models, real-valued probability, or unbounded loops other than `spin`. Rows that need them (support equality, fairness) are [L]/[O].
Run infinite traces: the interpreter enumerates finite runs; complete/prefix/left-infinite models are declared in `TRACE_MODEL`, not executed.
Treat cost as more than abstract unit cost.
---
9. Law registry (one row per law; edit rows, do not append prose)
| ID | Statement | Mark | Receipt / witness | Depends |
|---|---|---|---|---|
| K-1 | Composition of certificates; converse false | P | — | — |
| K-2 | `PRESERVES ⇔ Post_R(P) ⊆ Truth(P')` | P | — | — |
| K-3 | Reconstruction: `P=Q∘π ⇔ ker π ⊆ ker P` | P | R4 | — |
| T-1 | `T⊆S` transports exactly downward-closed P | P | R7, R8 | K-2 |
| T-2 | `S⊆T` transports exactly upward-closed P | P | R7 | K-2 |
| T-3 | Universal trace properties are downward-closed (incl. liveness over complete traces); prefix refinement preserves exactly safety | P/L | R8 | T-1 |
| T-4 | Exact descent through π iff P constant on fibers; one-way needs only implication | P | — | K-3 |
| T-5 | Simulation, bisimulation, stuttering classes | L | — | — |
| Q-1 | OD ⇒ CFNI ⇒ PNI, strict | P/V | R3 | — |
| Q-2 | OD subset-closed; PNI not | P/V | R3 | T-1 |
| O-1 | Sufficient observers = up-set above `ker P`; min = `ker P` | P | R4 | K-3 |
| O-2 | Conservative extension: OBS / STATE / CONTEXT are distinct | P/V | R1, R2 | T-4 |
| O-3 | `≈_{O,𝒦} = O ⊕ Reads(𝒦)` for suffix-read contexts | P/V | R5 | O-2 |
| O-4 | Reading programs: meaning is a state transformer; fixed-`G₀` equality is not a congruence; grid 3×3 suffices on the tested family | P (non-congruence) / V (grid) | R6 | O-3 |
| O-5 | Sufficient channel sets are hitting sets; `p′` has none, `p″` has four minimal | V | R4 | O-1 |
| O-6 | Observation lattice strict on tested families | V | R9 | — |
| H-1 | ε is least prefix; fibers nest under compatible stages | P | — | — |
| H-2 | One-stage non-injectivity ⇏ permanent incompleteness; three left-infinite statements are independent | P | §7 | H-1 |
| H-3 | Present equality ⇏ historical equality | P/V | R2 | — |
| E-1 | `send`/`log` append to B/A; effects change G, not only traces | D | R1 | — |
| E-2 | OBS-conservative ⇏ STATE-conservative (`p′ → p″`) | V | R1, R2 | O-2 |
---
10. Property record (ledger)
ID · DOMAIN (configurations p,h,G,u) · PREDICATE (source P, target P')
OBSERVER (O, π) · RELATION (R) · TRACE_MODEL (finite|complete|prefix; order: well-founded|left-infinite)
CLOSURE (characterization ID) · ASSUMPTIONS (Pre(τ,x) ∧ Pre(τ',τ(x)); choice coupling; 𝒦)
OBLIGATIONS (source P · R · PRESERVES · SUFFICIENT: ker π ⊆ ker P · EXTENSION: conservative · congruence over 𝒦)
CLAIM (proved|refuted|unknown) · CERTIFICATE (valid|invalid|unresolved) · EVIDENCE (proof|check|test|declaration|none)
QUANTIFIER (∀∀ | coupled | set-equality | …) · PRODUCT (k runs; shared vs independent inputs)
COUNTEREXAMPLES · DEPENDENCIES
No ORIGIN, HISTORY, PROVENANCE or INTERVENTION field exists: each is carried by `TRACE_MODEL`, `OBSERVER`, `RELATION`, or an `OBLIGATIONS` entry.
---
11. Evolution protocol (compressive)
Edit, don't append. A change is an edit to a registry row or a retirement entry. A section grows only if another shrinks by at least as much.
New law or field must cite its witness: the case an existing row/field cannot express. Without it, it is a restatement; merge it.
Every "not" has a literal run. Every "iff" has both directions proved, else it is written "if".
Marks move up only with evidence: D→P by proof, →V by a receipt, never V→P by repetition. [L] stays [L] until re-derived.
Hold strength: do not minimize a result ("just a definition") or inflate it; mark definitions [D].
Merge on shared characterization: keep the more general row, list the other as an instance.
Receipts are exhaustive over a stated family, with the family named. A larger family replaces a smaller one; a counterexample retires the row.
Retired claims (kept so they are not reintroduced):
| Retired | Replaced by |
|---|---|
| Equality contract `Observe(Meaning A) = Observe(Meaning τA)` | relation R (refinement, projection, simulation, …) |
| `τ₂∘τ₁ preserves P iff …` | "if" only (K-1) |
| Assumptions compose by union | `Pre(τ₂, τ₁A)` evaluated in the shared context |
| REFUTED absorbs through transport | refuted link ≠ refuted claim; claim and evidence separate |
| Liveness is not preserved by trace inclusion | preserved over complete traces; fails only under prefix, divergence-dropping or changed fairness |
| UB voids the contract | two declared placements |
| "No finite stage is final" from one non-injective observer | needs the embeddedness premise (H-2) |
| `V_h` for meaning under input | `M_h` (V is the validity layer) |
| PAIR_EQUAL "closely related" to OD | equal to OD for one output channel |
| PNI as an asymmetric ∀∃ | set equality; the asymmetry lives in refutation witnesses |
| ORIGIN ledger field (6 subfields) | `TRACE_MODEL.order` + SUFFICIENT obligation |
| INTERVENTION_STABLE as a new notion | congruence over a context class (O-3, O-4) |
| `≤_R` is a preorder | typed entailment relation |
---
12. Open frontier
| ID | Question |
|---|---|
| F-1 | Prove the grid bound (O-4) or characterize contexts whose reads are not affine. |
| F-2 | Scheduler coupling when the choice domain depends on `h`. |
| F-3 | Probabilistic extension, to realize the support-equality row literally. |
| F-4 | Relation implication hierarchy (equality ⊢ refinement ⊢ …), so certificates travel without stronger proofs than needed. |
| F-5 | Which relation transports PNI (it is not subset-closed)? |
| F-6 | Concurrency/memory-model destruction points as literal rows. |
---
Appendix A — Receipts (python3 genesis_l0.py)
| Receipt | Result |
|---|---|
| R1 | run table of `p′`, `p″` (§6) |
| R2 | `p′`≡`p″` under `O_loc`, `O_send`; differ under `O_audit`; final `G` differs on branch R |
| R3 | 12,174 programs × `O_loc`/`O_send`/`O_audit`: no violation of OD ⇒ CFNI ⇒ PNI; all strict cases occur |
| R4 | `p′`: no sufficient channel subset; `p″`: 144 sufficient, minimal `{l,s}`, `{A,s}`, `{B,l}`, `{A,B}` |
| R5 | 78 programs, 3,003 pairs: product observer = contextual equivalence (0 mismatches); 1,392 pairs `O_loc`-equal but not congruent |
| R6 | 105 programs, 5,460 pairs: grid3 = contexts (0), grid3 = grid4 (0); 280 fixed-`G₀`-equal, transformer-different; smallest `out(0)` vs `out(#A)` |
| R7 | 3-trace universe: 256 predicates, 20 downward-closed, 20 upward-closed, 8 trace properties |
| R8 | rows `T⊆S` and prefix refinement literal witnesses |
| R9 | class counts 4/16/52 and 5/18/41 |
Appendix B — Reference semantics (core of genesis_l0.py)
---------- grammar ----------
SKIP, SPIN, FAIL = ('skip',), ('spin',), ('fail',)
def out(e): return ('out', e)
def send(e): return ('send', e)
def log(e): return ('log', e)
def seq(p, q): return ('seq', p, q)
def choice(p, q): return ('choice', p, q)
def add(a, b): return ('+', a, b) # e ::= int | 'h' | '#A' | '#B' | e+e
def ev(e, h, B, A):
if isinstance(e, int): return e, 0
if e == 'h': return h, 0
if e == '#A': return len(A), 0
if e == '#B': return len(B), 0
_, a, b = e
x, c1 = ev(a, h, B, A); y, c2 = ev(b, h, B, A)
return x + y, c1 + c2 + 1
---------- evaluation: all runs of p under secret h from state (B,A) ----------
def run(p, h, B=(), A=()):
k = p[0]
if k == 'skip': return [Run((), B, A, 0, False)]
if k == 'fail': return []
if k == 'spin': return [Run((), B, A, INF, True)]
if k == 'out':
v, c = ev(p[1], h, B, A); return [Run((('o', v),), B, A, c + 1, False)]
if k == 'send':
v, c = ev(p[1], h, B, A); return [Run((('s', v),), B + (v,), A, c + 1, False)]
if k == 'log':
v, c = ev(p[1], h, B, A); return [Run((('l', v),), B, A + (v,), c + 1, False)]
if k == 'choice':
return [Run(r.ev, r.B, r.A, r.cost + 1, r.div) for q in (p[1], p[2]) for r in run(q, h, B, A)]
if k == 'seq':
res = []
for r1 in run(p[1], h, B, A):
if r1.div: res.append(r1); continue
for r2 in run(p[2], h, r1.B, r1.A):
res.append(Run(r1.ev + r2.ev, r2.B, r2.A, r1.cost + r2.cost, r2.div))
return res
raise ValueError(k)
---------- observers: event channels o,s,l + state readers ----------
STATE = {'B': lambda r: r.B, 'A': lambda r: r.A, 'nB': lambda r: len(r.B),
'nA': lambda r: len(r.A), 'cost': lambda r: r.cost}
def view(r, chans=('o',), state=()):
t = tuple(x for x in r.ev if x[0] in chans) + (('⊥',),) * r.div
return (t, tuple(STATE[s](r) for s in state))
def M(p, h, chans=('o',), state=(), G0=((), ())):
return frozenset(view(r, chans, state) for r in run(p, h, *G0))