SIL Compiler Spec Bundle v0.1 — Normative Core + Implementation Notes

Community Article Published October 25, 2025

Purpose. Provide a compact, patent‑safe specification set that lets multiple implementers build compatible SIL compilers beyond the Kickstart article. This bundle fixes the language surface, the IR & reversibility format, and conformance/diagnostics, while leaving room for creativity in backends and optimizations.

Status. v0.1, implementable now. Normative sections are explicitly marked. Everything else is informative.

Licensing. Text © 2025 under CC BY 4.0. Code/pseudocode under MIT (see SPEC-LICENSE). Patent posture: RF on Essential Claims as defined in project policy.

Packaging note (v0.1). This release is a single-file specification bundle.
No auxiliary directories, test files, or runner scripts are shipped.
All examples in this document are informative / non-normative.

Conformance policy. This specification does not ship a normative reference implementation.
Formal conformance is determined solely by the golden conformance corpus published in the SIL Compiler Conformance Kit v0.1 (normative). Implementers MUST pass that corpus.


0) Overview & Scope (Normative)

  • In scope: (a) SIL language surface sufficient for portable programs; (b) SIR IR + .sirrev reversibility map; (c) conformance tests and diagnostic catalog.
  • Out of scope: backend internals, register allocators, concrete optimizer implementations, vendor‑specific extensions.
  • Keywords: MUST/SHOULD/MAY per RFC‑2119.

Compilation pipeline (conceptual)

flowchart LR
A[SIL Source] --> B[Syntactic & Semantic Analysis]
B --> C[SIR (SSA) + Metadata]
C --> D[.sirrev Reverse Map]
C --> E[Backend Lowering (LLVM/WASM/C ABI)]
E --> F[Objects/Binaries]

1) SIL Language Reference (Normative)

1.1 Syntax (summary)

A complete EBNF is provided in Appendix A. Highlights:

  • Modules: module <ident> { ... }; imports: use <module> [as <alias>];
  • Bindings: let x: T = expr; (immutable by default), var x: T = expr; (mutable)
  • Functions: fn name(param: T, ...): U { ... }
  • Effects (decl annotation): @effect(pure|io|state|unsafe); multiple effects allowed via @effect(io,state).

    Safety default (informative). Unannotated code compiles as CON. Vendors SHOULD NOT change this default, which serves as the project’s strict safety baseline for v0.1.

  • Layers (structural intent): @layer(DET|CON|GOAL|AS); default is CON if unspecified. Synonyms used in Appendix H: CON≡constraint, GOAL≡goal, DET≡det, AS≡op.
  • Frames (audit/rollback marks): @frame(begin|end|mark("label")) on blocks; implicit function prologue/epilogue are marks.
  • Types: primitives (i32, u64, f64, bool, str), records {a:T, b:U}, algebraic variants enum, generics fn f<T>(x:T) -> T.

1.2 Typing (HM‑style with ascription)

  • Type inference is HM‑style; ascriptions MUST be enforced.
  • Purity & effects refine the judgment: Γ ⊢ e : T ! ε where ε is an effect row (e.g., {io,state} or {} for pure).
  • Calls MUST respect effect subtyping: {} ⊑ {io} ⊑ {io,state} ⊑ {unsafe}.

Effect rows & inference (normative clarifications).

  • Effect rows form a finite set lattice with partial order ⊑ defined as subset; join = ∪, meet = ∩.
  • Bottom (⊥) = {} (pure), Top (⊤) = {unsafe}. Implementations MAY internally map io,state ⊑ unsafe.
  • Row polymorphism MAY quantify over row variables; defaulting MUST preserve principal types.
  • Typing judgment is Γ ⊢ e : T ! ε where ε is a row; principal types MUST exist for closed terms.
  • Implementations MAY use algorithm W or equivalents extended with row variables; unification respects set‑lattice laws.
  • Where ambiguity remains, the reference typing tests in tests/golden/typing are normative: passing them is required for conformance.

1.3 Layers & Structural Rules

  • DET layer code MUST NOT invoke non‑deterministic primitives; see determinism table (Appendix F). Violations are diagnostics SIL0017.
  • Goal telemetry (informative). Compilers MAY emit a numeric goal field in SIR for analysis. No normative monotonicity requirement in v0.1; any optimization MUST still preserve frame mark ordering and effect semantics.

1.4 Frames (execution marks)

  • A frame is a verifiable region for Reflexia/rollback. Entrypoints and returns are implicit marks; @frame(mark("label")) inserts named marks. Optimizers MUST preserve mark order relative to effectful ops.

1.5 Name Resolution & Imports

  • Lexical scoping, module‑qualified names (M::f). use M as N; brings N:: alias into scope. Imports are acyclic at compile time.

Phase A import resolution (Normative):

  • use resolves modules within the current compilation workspace only (same invocation).
  • Import graph MUST be acyclic in Phase A.
  • External/package resolution is deferred to Phase B.

Diagnostics (add):

  • SIL0007: ambiguous import — two or more candidates export the same name (remedy: alias with use M as X;).
  • SIL0008: unresolved import / cycle in Phase A — external package not available (remedy: defer to Phase B or vendor config).

1.6 Operators (precedence & associativity)

From highest to lowest: unary ! - (right) → * / % (left) → + - (left) → comparisons < <= > >= (left) → equality == != (left) → logical && (left) → || (left).

Note (v0.1): There is no assignment expression. Re-assignment is statement-level for var only and not part of the expression operator table.

1.7 Versioning & Gates

  • Source files MUST declare lang_version = "0.1". Feature gates via @feature(name); unknown gates MUST be rejected (SIL0003).

1.8 Operator typing (Normative, SIL-0)

Operator Operand Types Result Notes
+ i32+i32 i32 integer addition
+ str+str str string concatenation (lowers to sil_text_concat)
==,!= T==T (T ∈ {i32,u64,f64,bool,str}) bool equality/inequality
<,<=,>,>= numeric pairs only (i32,u64,f64) bool ordered comparisons only

All other operand combinations are a compile-time error: SIL0010 illegal operands for operator.

1.9 Reserved keywords (Normative, SIL-0)

module, use, as, type, let, var, fn, return, if, else, match, enum Identifiers MUST NOT use these spellings.


2) SIR IR + .sirrev Format (Normative)

2.1 Encoding

  • Canonical encoding is JSON Lines (one IR entity per line). Binary CBOR is allowed; if used, an ASCII JSON export MUST be provided.
  • Field names are snake_case (e.g., lang_version, sirrev_ref). Unknown fields MUST be ignored (forward-compat) but preserved when round-tripped (if present in .sirrev).

2.2 Top‑level IR object

// SPDX-License-Identifier: MIT
{
  "v":"1",
  "module":"m.example",
  "lang_version":"0.1",
  "types":[],
  "const_pool":[],
  "funcs":[{"name":"add","sig":"(i32,i32)->i32","blocks":[/* see 2.3 */],
             "meta":{"layer":"DET","effects":[],"frames":["prologue","epilogue"]}}],
  "env_hash":"sha256:...",
  "determinism":{"level":"DCL-1","epsilon":1e-6},
  "sirrev_ref":"sirrev://m.example/1234"
}

2.3 Blocks & Instructions (minimal set)

  • SSA form; each block has label, phis, instrs, term.
  • Minimal instructions (extensible): iconst/fconst, load/store, binop(add,sub,mul,div,cmp), call, select, phi, mark, trap, ret.
  • Lowering note (informative): field projection, pattern matching, and closures SHOULD be lowered into the minimal set (records + select + branches) in v0.1. This set is extensible; future structured ops MAY be added without breaking existing IR.

2.4 Metadata (normative fields)

  • meta.layer ∈ {DET,CON,GOAL,AS} // see mapping in §1.1 and Appendix H
  • meta.effects is an array from {pure,io,state,unsafe}.
  • goal: optional numeric telemetry; if present, optimizer MUST NOT lower goal in DET regions.
  • ethics: optional policy ref; effectful ops crossing an ethics barrier MUST be marked.

2.5 .sirrev Reverse Map (proof‑preserving)

Coverage metric (normative): SCover = |traced_nodes| / |total_nodes|.

  • total_nodes: count of IR instructions and terminators across all blocks (exclude labels/metadata/phi).

  • traced_nodes: IR nodes (instr/term) that have either (a) a source span entry, or (b) a transform trace mapping.

  • Frames: every frame entry MUST carry both pre_hash and post_hash.
    Frame labels do not contribute to traced_nodes (coverage) but are mandatory for validity.

  • Purpose: enable rollback, audit, and structured replay.

  • Required contents:

    • Source span map: IR node id → {file, line, col, len}
    • Transform trace: pass id → list of {src_node, dst_node, rule}
    • Dataflow anchors: frame marks with pre/post hashes

    Build manifest (Normative, adjacent to object files): Each produced object MUST have a JSON entry with the following keys:

    {
      "manifest_version": 1,
      "path": "out/obj/hello.o",
      "sirrev_sidecar": "out/obj/hello.o.sirrev.jsonl",
      "sirrev_sha256": "sha256:...",
      "compiler": "silc 0.1.0",
      "lang_version": "0.1",
      "frame_policy": "constraint-first"
    }
    
  • Coverage target: SCover ≥ 0.90 (PoC), computed as traced_nodes / total_nodes.

Example (excerpt)

{
  "v":"1",
  "unit":"m.example",
  "spans":[{"ir":"b1.i3","src":{"file":"main.sil","line":7,"col":12,"len":5}}],
  "transforms":[{"pass":"cse","map":[{"src":"b1.i3","dst":"b1.i1","rule":"cse.merge"}]}],
  "frames":[{"label":"prologue","pre_hash":"sha256:...","post_hash":"sha256:..."}]
}

2.6 Stability & Migration

  • SemVer for v and lang_version. Backward compatible additions MAY add optional fields. Breaking changes require a bump and a migration note.

3) Conformance & Diagnostics (Normative)

3.1 Acceptance Phases

  • Phase A (Front‑end): parse + type; emit diagnostics; produce SIR skeleton; pass golden source → IR tests.
  • Phase B (IR + sirrev): emit full SIR + .sirrev with SCover ≥ 0.90; preserve marks; pass determinism checks in DET blocks.
  • Phase C (Backend smoke): lower a defined subset (arith/call/branch) to chosen backend; run provided fixtures.

3.2 Golden Tests

  • Canonical test set: tests/golden/*.sil with expected *.sir.jsonl. Comparison ignores object field ordering and requires value equality.
  • Array order: Unless stated otherwise, arrays are compared order-sensitive. The conformance profile MAY mark specific arrays as order-insensitive (e.g., meta.effects) and those MUST be compared as sets.

3.3 Diagnostics Catalog (IDs & format)

  • Machine format (normative, JSONL) — emitted by compilers and used by golden diff:

    {"id":"SIL0012","msg":"effect violation: ...","file":"demo.sil","line":1,"col":12}
    
  • Human format (informative)SIL####: short_reason — file:line:col (hint)

  • Examples:

    • SIL0001: parse error (show unexpected token & nearest production)
    • SIL0003: unknown feature gate
    • SIL0007: ambiguous import (two exports with same name; alias required)
    • SIL0008: unresolved import / cycle (Phase A) (external package not available)
    • SIL0010: illegal operands for operator
    • SIL0012: effect violation (impure call in pure context)
    • SIL0017: nondeterministic op used in DET layer
    • SIL0021: lost frame mark across optimization

3.4 Telemetry Metrics (normative)

  • CAS: Causality Alignment Score (DET replays produce identical decisions)
  • SCover: structural coverage (sirrev traced / total)
  • RIR: rollback integrity rate (revert+reapply success / 1k)
  • EAI: ethics pass ratio on effectful ops

Extraction (PoC)

nos audit export --window 24h > eval.jsonl
si-bench collect eval.jsonl --out compiler_bench.json

3.5 Reporting Schema (JSON excerpt)

{
  "lang_version":"0.1",
  "phase":"B",
  "metrics":{"CAS":0.999,"SCover":0.94,"RIR":0.9995,"EAI":0.997},
  "errors":[{"id":"SIL0017","count":0}],
  "golden_pass":true
}

3.6 Conformance Authority (No Normative Implementation) — Normative

  • Where algorithmic details are under-specified, the golden test suite SHALL resolve behavior. Passing the suite is required for conformance.
  • No normative reference implementation is provided. Editors SHALL NOT ship normative code. Educational examples may exist but are non-normative.
  • Implementers are free to choose algorithms and internal representations, provided that emitted SIR/.sirrev/diagnostics and externally-observable behavior match the normative golden outputs.

4) Backend ABI & Runtime Notes (Informative)

4.1 C/LLVM ABI (minimal)

  • Calling conv: C default; integers/floats per target ABI; structs by pointer unless ≤ two registers.
  • Data layout: compiler MUST pin the LLVM datalayout string in artifacts.
  • Name mangling: module.funcmodule__func (ASCII) by default; backends MAY override.

4.2 WASM Notes

  • Target wasm32-wasi as baseline. Memory via linear heap; host I/O behind capability shims. Frame marks exported as custom sections.

4.3 Memory Model

  • Front‑end assumes sequentially consistent semantics for DET blocks; backends SHOULD not introduce UB via reordering across frame marks.

5) Optimization & Reversibility Guide (Informative)

5.1 Sirrev‑preserving Transform Table

Transform Allowed? Conditions
CSE YES Preserve source map; update .sirrev.transforms
Inlining YES Must copy marks and merge frame metadata
DCE YES If effect row is {} and no mark removed
Loop unroll YES Keep iteration anchors; update spans
FP reassoc NO in DET Only in CON/AS or with @effect(unsafe)
Hoisting IO NO Never move across marks/ethics gates

5.2 Typical Pitfalls

  • Losing a mark during block merge → SIL0021.
  • Emitting non‑canonical JSONL ordering → golden diff noise.

6) Security & Safety Considerations (Informative)

  • Proof‑preserving redaction for logs; optional ethics policy hook on effectful intrinsics.
  • Supply‑chain: sign artifacts; include env_hash and tool versions in every unit.

7) Versioning & Governance (Normative)

  • SemVer for lang_version and IR v.
  • Feature gates: experimental features MUST be gated and off by default.
  • Changes tracked in VERSIONING.md; patent policy in SPEC-PATENT-POLICY.md.

Appendix A — Complete EBNF (Normative)

Note (Normative cross-reference): Operator precedence & associativity are defined in §1.6.
The EBNF uses a flat expr := primary { op primary } form for readability; conforming parsers MUST implement precedence/associativity exactly as in §1.6.

ident      = /[A-Za-z_][A-Za-z0-9_]*/  -  ("module"|"use"|"as"|"type"|"let"|"var"|"fn"|"return"|"if"|"else"|"match"|"enum") ;
module     = "module" ident "{" { decl } "}" ;
decl       = use | let | var | fn | enum | type ;
use        = "use" ident {"::" ident} ["as" ident] ";" ;
let        = "let" ident ":" type "=" expr ";" ;
var        = "var" ident ":" type "=" expr ";" ;
fn         = [layer] [effect] "fn" ident "(" [params] ")" [":" type] block ;
layer      = "@layer(" ("DET"|"CON"|"GOAL"|"AS") ")" ;
effect     = "@effect(" effect_list ")" ;
effect_list= ident {"," ident} ;
params     = param {"," param} ;
param      = ident ":" type ;
block      = "{" { stmt } "}" ;
stmt       = let | var | expr ";" | frame ;
frame      = "@frame(" ("begin" | "end" | ("mark(" , string , ")")) ")" ;
expr       = primary { op primary } ;
op         = "+" | "-" | "*" | "/" | "%" | "==" | "!=" | "<" | "<=" | ">" | ">=" | "&&" | "||" ;
primary    = ident | number | string | call | group ;
call       = ident "(" [args] ")" ;
args       = expr {"," expr} ;
number     = /[0-9]+(\.[0-9]+)?/ ;
string     = '"' { /[^\"]/ } '"' ;
type       = ident | ident "<" type {"," type} ">" | record ;
record     = "{" ident ":" type {"," ident ":" type} "}" ;

Appendix B — SIR JSON Schema (Excerpt, Normative)

{
  "$schema":"https://json-schema.org/draft/2020-12/schema",
  "type":"object",
  "required":["v","module","funcs"],
  "properties":{
    "v":{"const":"1"},
    "module":{"type":"string"},
    "lang_version":{"type":"string"},
    "funcs":{"type":"array"},
    "env_hash":{"type":"string"},
    "determinism":{"type":"object"},
    "sirrev_ref":{"type":"string"}
  }
}

Appendix C — Golden Test (Example)

module demo {
  @layer(DET) @effect(pure)
  fn add(a:i32, b:i32): i32 {
    @frame(begin)
    let c:i32 = a + b;
    @frame(end)
    c
  }
}

Expected IR (excerpt):

{"v":"1","module":"demo","funcs":[{"name":"add","meta":{"layer":"DET","effects":[]}}]}

Appendix D — Diagnostic Table (Excerpt)

ID Title When Remedy
SIL0001 Parse error unexpected token check EBNF & punctuation
SIL0003 Unknown feature gate @feature(x) not known remove or bump lang_version
SIL0010 Illegal operands operator/type mismatch fix operand types or add overload
SIL0012 Effect violation impure call in pure context add @effect(io) or refactor
SIL0017 Nondeterminism in DET disallowed op move to CON or change op
SIL0021 Lost frame mark optimization removed mark fix pass to preserve marks

Appendix E — Licensing Snippets

  • Text: CC BY 4.0. Code: MIT.
  • SPDX headers SHOULD be present in every code block intended for reuse: // SPDX-License-Identifier: MIT.

Appendix F — Determinism Table (Normative for DET) & Notes (Informative)

F.1 Determinism Table (Normative for DET layer)

Category Examples DET CON AS Required flags / notes
FP reassociation / fast‑math -ffast-math, FMA merge, algebraic reorder NO YES YES Enforce IEEE‑754 strict; disable fast‑math/FMA unless proven bit‑identical.
Order‑unstable parallel reductions GPU atomic add on float, non‑tree reductions NO* YES YES *Allowed only if reduction is commutative & order‑fixed (deterministic tree/barrier). Provide pass proof.
Stochastic ops without fixed seed Dropout, data augmentation RNG NO YES YES In DET require fixed seeds recorded in DecisionFrame; otherwise classify as CON.
Async kernel reordering Streams that reorder accumulation NO YES YES Use deterministic queues/barriers; disable autotuning in DET.
Variable‑length loops (data‑dependent) Early exit by data IF YES YES Allowed in DET only if bounded and seeds fixed; else CON.
Time/clock/entropy reads clock_gettime, RDRAND, /dev/urandom NO YES YES Treat as io; not permitted in DET.
I/O & networking File/socket ops NO YES YES Effect row must include io; mark ethics barriers as needed.
Denormals/FTZ/DAZ modes Flush‑to‑zero differences IF YES YES Pin FP mode; record in env_hash.
Library determinism cuDNN/oneDNN nondeterministic kernels IF YES YES In DET set deterministic paths; pin versions in env_hash.
Custom kernels Hand‑written CUDA/OpenCL IF YES YES Provide a determinism statement; otherwise treat as CON.
Integer atomics (commutative) atomicAdd(int), atomicMin/Max IF YES YES Allowed if commutative & order‑insensitive; document.

Legend: YES allowed; NO forbidden; IF allowed under stated constraints.

F.2 Notes (Informative)

  • Mapping to DCL levels (see Appendix I): operations that violate any NO row force the frame ≤ DCL‑1; satisfying all DET constraints enables DCL‑2/3; hardware‑enforced order (e.g., SI‑GSPU) enables DCL‑4.
  • Practical tip: Start with host‑only DET (DCL‑2), then graduate to deterministic‑GPU paths (DCL‑3) once kernels are audited.

Appendix G — Normative Reference to the Golden Corpus

This specification binds to the SIL Compiler Conformance Kit v0.1 as the normative golden corpus.
Conformance claims to this spec MUST reference and pass that kit’s golden tests (including its profiles/golden_profile.json comparison rules).

Version binding (v0.1): SIL Compiler Conformance Kit v0.1 (release tag: v0.1).
If the corpus changes, its version MUST be bumped, and conforming compilers SHALL reference the new tag.

Appendix H — Layer Interaction Matrix (Normative)

Purpose. Make cross-layer calls predictable and checkable. Layers are context labels carried in IR (meta.layer). The active layer of an expression is the maximum strictness of all open layer blocks in scope.

H.1 Layers & Ordering

We define a total order by strictness:

constraint  >  goal  >  det  >  op
   3            2        1      0     // ordinal (higher = stricter)

H.2 Call Rule (H-CALL)

In context layer Lctx, a call to a function annotated with Lfn is permitted iff

ord(Lfn) ≥ ord(Lctx)

Examples:

  • constraint → may call only constraint
  • goal → may call goal or constraint
  • det → may call det|goal|constraint
  • op → may call any (subject to effects)

H.3 Allowed Effects per Layer (H-EFF)

Minimal requirements (effects are rows over {state, io, unsafe, …}):

layer       allowed effects
--------------------------------
constraint  {}                         // pure only
goal        {}                         // pure only
det         {}  + determinism (§I)     // pure; must meet DET constraints
op          {state, io} (no unsafe*)   // *unsafe only behind feature gate + ethics

Effect subtyping is enforced in addition to H-CALL. A program in constraint that syntactically appears pure but calls an op function will fail both H-CALL and effect checks with SIL0012.

H.4 Raising/Lowering (H-TRANS)

Entering a stricter sub-block (e.g., with_goal { … }) is allowed; leaving it does not authorize looser calls in the outer scope. Lowering a callee’s declared layer is forbidden. Compilers MUST reject any implicit lowering.

H.5 Conflict Resolution (H-MERGE)

When multiple annotations compose, the active layer is the maximum ordinal (strictest wins). IR MUST reflect the active layer in meta.layer for functions and blocks emitted.

Conformance hooks. Violations MUST surface as diagnostics:

  • H-CALL/H-EFF → SIL0012 (effect/layer violation)
  • H-TRANS → SIL0012 with hint “lowering not allowed”
  • H-MERGE → backend IR must show the strictest layer; missing ⇒ SIL0021 if marks/layer lost.

Appendix I — Determinism Constraints for DET (Normative)

Applies when meta.layer = "DET" (or stricter contexts that delegate into DET). The following are forbidden unless explicitly whitelisted by the determinism profile:

I-F1. Non-det RNG (no fixed seed captured in unit) → SIL0017
I-F2. Floating-point reassociation / “fast-math” / non-IEEE-strict → SIL0017
I-F3. Non-det library kernels (e.g., race-prone reductions) → SIL0017
I-F4. Atomics unless mathematically commutative and deterministic reduction is proven → SIL0017
I-F5. Parallel iteration with unspecified order; map/dict with non-stable iteration order → SIL0017
I-F6. Wall-clock/time, randomness from OS, environment-dependent values → SIL0017
I-F7. I/O and external state mutation (handled already by effects; repeat as hard prohibition) → SIL0012
I-F8. Data-dependent thread geometry / kernel launch shapes (unless recorded and replayed) → SIL0017

Implementations MUST provide the following positives in emitted unit metadata when DET is active:

I-R1. determinism.level = "DCL-k" (k per §F)
I-R2. determinism.seed present when any pseudo-RNG used
I-R3. determinism.epsilon present if numerical tolerance is part of replay contract
I-R4. Deterministic flags enabled for vendor libraries (e.g., oneDNN/cuDNN equivalents)

Test protocol (I-TP). Replay N=30 with identical inputs; the set of decision hashes must match (CAS ≥ 0.999). Failures SHALL emit SIL0017 with a hint to the first violated clause (I-F*).


Appendix J — Remedy Hints (Informative)

These are non-normative editor hints mapped to diagnostic IDs.

SIL0012 (effect/layer violation)

  • Move the side-effect to an op block and pass the value as data into goal/constraint/det.
  • Replace impure callee with a pure adapter; or split evaluation (compute → pass literal/struct).

SIL0017 (non-det in DET)

  • Use a fixed-seed RNG; enable deterministic vendor kernels; disable fast-math; use stable sort.
  • Record thread geometry and reduction order; replace atomics with ordered scans if needed.

SIL0021 (lost/moved frame or layer mark)

  • Mark blocks as no-reorder for passes that might sink/hoist; ensure marks are attached after CSE/DCE.

SIL0007 (ambiguous import)

  • Disambiguate with use foo as bar; prefer explicit re-exports from one owner module.

SIL0008 (unresolved import / cycle) (Phase A)

  • Break the cycle by extracting an interface module; or delay resolution to Phase B with a stub gate.

SIL0001 (parse/duplicate symbol)

  • Rename or scope the symbol; ensure EBNF terminals are not consumed by keywords.

Appendix K — Theory Mappings (Informative)

SIL concern Theory that backs it How it’s specialized in SIL
constraint layer semantics CLP / Constraint Stores Treat constraints as a monotone store; entailment/consistency checks are pure; no I/O.
goal layer search Abductive / Non-monotonic reasoning Goal sets are finite labels in v0.1; search/plans are represented as pure transformations; conflicts resolved by H-MERGE (strictest layer wins).
Cross-layer logic Modal / Multi-context systems Layers are modalities with total order (§H.1). H-CALL/H-TRANS give the structural rules.
Determinism Program logics for FP / concurrency DET forbids non-associative rewrites and order-sensitive races; replay contract captured by seed/epsilon.
Audit / frames Trace semantics Frame marks are observable events; .sirrev preserves them; loss is SIL0021.

Community

Sign up or log in to comment