SIL Compiler Spec Bundle v0.1 — Normative Core + Implementation Notes
- Original Source: https://huggingface.co/datasets/kanaria007/agi-structural-intelligence-protocols/blob/main/spec/sil-compiler-spec-bundle-v0.1.md
- Conformance Kit: https://huggingface.co/datasets/kanaria007/agi-structural-intelligence-protocols/blob/main/spec/sil-compiler-conformance-kit-v0.1.md
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 +
.sirrevreversibility 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 isCONif 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 variantsenum, genericsfn 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 mapio,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/typingare 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
goalfield 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;bringsN::alias into scope. Imports are acyclic at compile time.
Phase A import resolution (Normative):
useresolves 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 withuse 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
varonly 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 Hmeta.effectsis an array from{pure,io,state,unsafe}.goal: optional numeric telemetry; if present, optimizer MUST NOT lowergoalin 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_hashandpost_hash.
Frame labels do not contribute totraced_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" }- Source span map: IR node id →
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
vandlang_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 +
.sirrevwith 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/*.silwith 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 gateSIL0007: ambiguous import (two exports with same name; alias required)SIL0008: unresolved import / cycle (Phase A) (external package not available)SIL0010: illegal operands for operatorSIL0012: effect violation (impure call in pure context)SIL0017: nondeterministic op used in DET layerSIL0021: 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.func→module__func(ASCII) by default; backends MAY override.
4.2 WASM Notes
- Target
wasm32-wasias 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
DETblocks; 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_hashand tool versions in every unit.
7) Versioning & Governance (Normative)
- SemVer for
lang_versionand IRv. - Feature gates: experimental features MUST be gated and off by default.
- Changes tracked in
VERSIONING.md; patent policy inSPEC-PATENT-POLICY.md.
Appendix A — Complete EBNF (Normative)
Note (Normative cross-reference): Operator precedence & associativity are defined in §1.6.
The EBNF uses a flatexpr := 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 onlyconstraintgoal→ may callgoalorconstraintdet→ may calldet|goal|constraintop→ 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 →
SIL0012with hint “lowering not allowed”- H-MERGE → backend IR must show the strictest layer; missing ⇒
SIL0021if 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 emitSIL0017with 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
opblock and pass the value as data intogoal/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-reorderfor 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. |