feat: SpeckDL v0.2-DP spec with dark provenance primitives

New language members: provenance, review, derives, satisfies, author, source - provenance block: declare intent sources (regulation, design_decision, parent_spec, external_doc) - review directive: mark verification boundaries (manual, auto, hybrid) - derives/satisfies: spec-to-spec and spec-to-requirement edges - author/source: who wrote it and what drove it - Provenance-aware event semantics: runtime events trace back to intent - Updated EBNF grammar, semantics, examples, and JSON-LD mapping - Three new examples: regulated medical device, auto-verified service, compliance audit trail - All primitives optional — Specks without provenance still compile fine
2026-04-28 16:16:04 -07:00 · 2026-04-28 16:16:04 -07:00 · ec1edc9f0f
commit ec1edc9f0f
parent 0ea2204d5b
1 changed files with 706 additions and 0 deletions
--- a/speckdl/SPEC.v2-dp-primitives.md
+++ b/speckdl/SPEC.v2-dp-primitives.md
@ -0,0 +1,706 @@
+# SpeckDL Language Specification v0.2-DP
+
+> The specification-first language for auditable software.
+> **This version adds Dark Provenance primitives: `provenance`, `review`, `derives`, `satisfies`, `author`, `source`.**
+> Part of the [Speckl](https://os.scoble.me/forgejo/sscoble/speckl) project. MIT License.
+
+---
+
+## 1. Introduction
+
+SpeckDL is a domain-specific language for defining system behavior and interfaces. A SpeckDL specification (a **Speck**) describes *what* a system should do, not *how* it should do it. Specks compile through a deterministic pipeline — SpeckDL → Z3 → DST → WASM — producing verified artifacts with full dark provenance.
+
+### Design Goals
+
+- **Human-readable first.** A Speck should be understandable by a domain expert who doesn't write code.
+- **Machine-verifiable.** Every constraint in a Speck compiles to Z3 (SMT solver) input. Verification is automatic.
+- **Provenance-native.** The compilation pipeline records derivation edges automatically. Provenance is not bolted on — it's structural.
+- **Composable.** Specks compose via interfaces. Large systems are built from small, verified Specks.
+- **Deterministic.** Same input, same output. No LLMs in the compilation path.
+
+---
+
+## 2. Syntax
+
+### 2.1 Top-Level Structure
+
+A SpeckDL file consists of one or more Speck definitions:
+
+```
+speck <Name> {
+  <members>
+}
+```
+
+Members are drawn from: `input`, `output`, `constraint`, `verify`, `interface`, `import`, `event`, and **Dark Provenance primitives**: `provenance`, `review`, `derives`, `satisfies`, `author`, `source`.
+
+### 2.2 EBNF Grammar
+
+```ebnf
+file           = { speck_def | import_stmt }
+
+speck_def      = "speck" IDENT "{" { member } "}"
+
+member         = input_def | output_def | constraint_def
+               | verify_def | interface_def | event_def
+               | provenance_def | review_def | derives_def
+               | satisfies_def | author_def | source_def
+
+input_def      = "input" ":" type_expr
+output_def     = "output" ":" type_expr
+
+type_expr      = primitive | compound | IDENT
+primitive      = "Nat" | "Int" | "Real" | "Bool" | "String" | "Bytes"
+compound       = "{" { IDENT ":" type_expr [","] } "}"
+               | "[" type_expr "]"
+
+constraint_def = "constraint" ":" expr
+verify_def     = "verify" ":" temporal_expr
+
+expr           = literal | IDENT | expr op expr | expr "." IDENT
+               | func_call | "(" expr ")"
+op             = "==" | "!=" | "<=" | ">=" | "<" | ">"
+               | "+" | "-" | "*" | "/" | "mod"
+               | "and" | "or" | "not" | "implies"
+func_call      = IDENT "(" [expr { "," expr }] ")"
+
+temporal_expr  = "always" "(" expr ")"
+               | "eventually" "(" expr ")"
+               | "implies" "(" expr "," expr ")"
+
+interface_def  = "interface" IDENT "{" { method_sig } "}"
+method_sig     = IDENT "(" [ { IDENT ":" type_expr "," } ] ")" ":" type_expr
+
+event_def      = "event" IDENT "{" { IDENT ":" type_expr [","] } "}"
+
+provenance_def = "provenance" "{" { provenance_clause } "}"
+provenance_clause = "regulation" ":" STRING
+                  | "design_decision" ":" STRING
+                  | "parent_spec" ":" IDENT
+                  | "external_doc" ":" STRING [ "at" STRING ]
+
+review_def     = "review" ":" review_kind
+review_kind    = "manual" | "auto" | "hybrid"
+
+derives_def    = "derives" "from" IDENT [ "via" STRING ]
+
+satisfies_def  = "satisfies" IDENT [ "clause" STRING ]
+
+author_def     = "author" ":" STRING [ "<" STRING ">" ]
+
+source_def     = "source" ":" source_kind [ "ref" STRING ]
+source_kind    = "conversation" | "meeting" | "document" | "regulation"
+               | "architecture_review" | "threat_model" | "compliance_audit"
+
+import_stmt    = "import" STRING ["as" IDENT]
+
+literal        = NAT_LIT | INT_LIT | REAL_LIT | BOOL_LIT | STRING_LIT
+IDENT          = letter { letter | digit | "_" }
+```
+
+### 2.3 Type System
+
+| Type | Meaning | Z3 Mapping |
+|------|---------|------------|
+| `Nat` | Non-negative integer | `Int` with constraint `>= 0` |
+| `Int` | Signed integer | `Int` |
+| `Real` | Real number | `Real` |
+| `Bool` | Boolean | `Bool` |
+| `String` | UTF-8 string | Uninterpreted sort |
+| `Bytes` | Byte sequence | Uninterpreted sort |
+| `{ ... }` | Record/tuple | Datatype |
+| `[T]` | List of T | Seq(T) |
+
+---
+
+## 3. Semantics
+
+### 3.1 Speck Definitions
+
+A Speck defines a behavioral unit with:
+- **Inputs:** Typed parameters the Speck accepts.
+- **Outputs:** Typed results the Speck produces.
+- **Constraints:** Invariants that must hold for all valid inputs and outputs.
+- **Verification conditions:** Temporal properties that the Z3 solver must prove.
+
+A Speck is *well-formed* if:
+1. All referenced identifiers are in scope.
+2. No two constraints are contradictory (Z3 must report SAT for the conjunction of all constraints).
+3. All verification conditions are provable from the constraints.
+
+### 3.2 Constraint Semantics
+
+A `constraint` defines an invariant that must hold across all valid executions of the Speck. Constraints are compiled to Z3 assertions:
+
+```
+constraint: maxRetries <= 5
+```
+
+becomes:
+
+```smt2
+(assert (<= maxRetries 5))
+```
+
+Constraints are **universally quantified** over all inputs unless explicitly scoped.
+
+### 3.3 Verification Semantics
+
+A `verify` clause defines a property that must be provable from the Speck's constraints:
+
+```
+verify: always(implies(attempt > 1, delay > 0))
+```
+
+becomes:
+
+```smt2
+(assert (=> (> attempt 1) (> delay 0)))
+(check-sat)
+```
+
+If Z3 returns `UNSAT` when asked to negate a verification condition, the condition is proven. If Z3 returns `SAT`, the Speck contains a counterexample — it can be violated.
+
+### 3.4 Interface Semantics
+
+An interface defines a contract between Specks. A Speck that provides an interface must satisfy all constraints of that interface:
+
+```
+interface PaymentProcessor {
+  charge(amount: Real, currency: String): Result
+  refund(transactionId: Nat): Result
+}
+
+speck StripeProcessor {
+  interface: PaymentProcessor
+  input: { apiKey: String }
+  output: Result
+  constraint: amount > 0
+  constraint: currency in ["USD", "EUR", "GBP"]
+}
+```
+
+### 3.5 Event Semantics
+
+Events define state transitions that the provenance graph records:
+
+```
+event RetryAttempted {
+  attemptNumber: Nat
+  delay: Real
+  remainingRetries: Nat
+}
+```
+
+Events are emitted during execution and recorded as nodes in the provenance graph. They do not affect the verification pipeline — they exist for observability.
+
+---
+
+## 3.6 Dark Provenance Semantics (NEW)
+
+Dark Provenance primitives make intent sources and verification boundaries explicit in the specification language. They compile to JSON-LD provenance graph nodes and edges.
+
+### 3.6.1 `provenance` Block Semantics
+
+The `provenance` block declares where a Speck's intent originates:
+
+| Clause | Meaning | JSON-LD Output |
+|--------|---------|----------------|
+| `regulation: "DO-178C"` | Compliance requirement | `prov:wasInformedBy` → Regulation node |
+| `design_decision: "ADR-0017"` | Architecture decision record | `prov:wasDerivedFrom` → Decision node |
+| `parent_spec: ParentSpeck` | Decomposition from another Speck | `prov:wasDerivedFrom` → Parent Speck node |
+| `external_doc: "RFC 8446" at "https://..."` | External reference | `prov:wasInformedBy` → Document node |
+
+Multiple clauses may appear; each creates a separate provenance edge.
+
+### 3.6.2 `review` Directive Semantics
+
+The `review` directive marks verification boundaries:
+
+- `review: manual` — Requires human sign-off before deployment. Compiler emits a `ManualReviewRequired` node in the provenance graph.
+- `review: auto` — Fully automated verification. No human gate required.
+- `review: hybrid` — Automated verification with spot-check sampling. Compiler emits sampling parameters.
+
+Review status is checked at compile time; `manual` Specks without sign-off block the pipeline.
+
+### 3.6.3 `derives` / `satisfies` Semantics
+
+These primitives create explicit edges in the provenance graph:
+
+**`derives from SpecName via "rationale"`**
+- Creates a `prov:wasDerivedFrom` edge from the current Speck to `SpecName`
+- Optional `via` clause records the derivation rationale as `rdfs:comment`
+- Used for: refactoring, decomposition, specialization
+
+**`satisfies RequirementId clause "3.2.1"`**
+- Creates a `speckl:satisfies` edge to a requirement node
+- Optional `clause` specifies the exact subsection
+- Used for: tracing to regulatory requirements, user stories, specs
+
+### 3.6.4 `author` / `source` Metadata Semantics
+
+These primitives capture "who" and "why":
+
+**`author: "Name" <"email@example.com">`**
+- Binds the Speck to an `prov:Agent` node
+- Compiles to `prov:wasAttributedTo` edge
+- Optional email used for agent deduplication in the provenance graph
+
+**`source: kind ref "identifier"`**
+- Records what drove the creation of this Speck
+- `kind`: `conversation`, `meeting`, `document`, `regulation`, `architecture_review`, `threat_model`, `compliance_audit`
+- `ref`: Optional identifier (meeting ID, document URL, ticket number)
+- Compiles to `prov:wasInformedBy` → Source node with `prov:type`
+
+### 3.6.5 Provenance-Aware Event Semantics
+
+Events declared with the standard `event` syntax gain provenance edges automatically:
+
+```
+event DoseCalculated { volume: Real, safe: Bool }
+```
+
+When this event fires at runtime, the provenance graph records:
+- The event instance node (`prov:Activity`)
+- An edge to the declaring Speck (`prov:wasInformedBy`)
+- An edge to the Speck's `provenance` sources (transitive intent tracing)
+- An edge to the runtime WASM module that emitted it (`prov:wasGeneratedBy`)
+
+This creates complete audit trails: Event → Speck → Intent Source → Regulatory Requirement.
+
+## 4. Compilation Pipeline
+
+### 4.1 Stage 1: SpeckDL → Z3
+
+Each Speck is compiled to SMT-LIB2 format:
+
+1. Type declarations become Z3 sort declarations.
+2. Input/output declarations become Z3 constants.
+3. Constraints become `assert` statements.
+4. Verification conditions become `check-sat` queries.
+
+The compiler checks for:
+- **Contradictory constraints:** If the conjunction of all constraints is UNSAT, the Speck is impossible to implement.
+- **Unsatisfiable verification conditions:** If a verify clause can be violated, the compiler reports the counterexample.
+
+### 4.2 Stage 2: Z3 → DST (Decision Structures)
+
+When Z3 reports SAT for a Speck, the model (assignment of values satisfying all constraints) is compiled into a **Decision Structure Tree**:
+
+```
+DSTNode {
+  condition: expr       // branching predicate
+  if_true: DSTNode      // subtree when condition holds
+  if_false: DSTNode     // subtree when condition doesn't hold
+  result: value?        // leaf value (if terminal)
+}
+```
+
+A DST represents the complete behavioral space of a verified Speck. Every possible input maps to exactly one path through the DST, terminating at a leaf with the verified output.
+
+### 4.3 Stage 3: DST → WASM
+
+DSTs compile to WebAssembly via a direct translation:
+
+- Each DST node becomes a `br_if` / `br` instruction pair.
+- Leaf values become `i32.const`, `f64.const`, or structured return values.
+- The resulting WASM module exports a single function matching the Speck's input/output signature.
+
+This compilation is *semantics-preserving by construction*: the WASM module implements exactly the behaviors encoded in the DST, which represents exactly the satisfiable space of the Speck.
+
+### 4.4 Provenance Graph Construction (UPDATED)
+
+At each compilation stage, the pipeline records derivation edges. **Dark Provenance primitives** in the SpeckDL source generate explicit provenance nodes and edges:
+
+```
+Speck "RetryHandler"
+  ├── compiled_to → Z3 assertion set (sha256:abc...)
+  ├── verified_by → Z3 result: SAT
+  ├── compiled_to → DST (sha256:def...)
+  ├── compiled_to → WASM module (sha256:789...)
+  ├── **provenance: {**
+  │     **regulation: "ISO 26262-6"**
+  │     **design_decision: "ADR-0042"**
+  │     **parent_spec: "FaultHandler"**
+  │     **author: "scott"**
+  │     **source: conversation ref "slack://C123/456"**
+  │     **review: manual**
+  │     **derives_from: "FaultHandler"**
+  │     **satisfies: "ASIL-D-REQ-17"**
+  │   **}**
+  ├── **attributed_to → Agent("scott")**
+  ├── **wasDerivedFrom → Speck("FaultHandler")**
+  ├── **satisfies → Requirement("ASIL-D-REQ-17")**
+  ├── **wasInformedBy → Regulation("ISO 26262-6")**
+  ├── **wasInformedBy → Decision("ADR-0042")**
+  └── **requiresReview → ManualReviewRequired**
+```
+
+The provenance graph is serialized as JSON-LD and stored alongside the compiled artifacts.
+
+**Dark Provenance JSON-LD Output:**
+
+```json
+{
+  "@context": {
+    "prov": "http://www.w3.org/ns/prov#",
+    "speckl": "https://os.scoble.me/speckl/ns#",
+    "rdfs": "http://www.w3.org/2000/01/rdf-schema#"
+  },
+  "@id": "speck:RetryHandler",
+  "@type": "speckl:Speck",
+  "prov:wasAttributedTo": {
+    "@id": "agent:scott",
+    "@type": "prov:Agent",
+    "rdfs:label": "scott"
+  },
+  "prov:wasInformedBy": [
+    { "@id": "reg:ISO-26262-6", "@type": "speckl:Regulation" },
+    { "@id": "decision:ADR-0042", "@type": "speckl:DesignDecision" },
+    { "@id": "conv:slack-C123-456", "@type": "speckl:Conversation" }
+  ],
+  "prov:wasDerivedFrom": { "@id": "speck:FaultHandler" },
+  "speckl:satisfies": {
+    "@id": "req:ASIL-D-REQ-17",
+    "speckl:clause": "4.3.2"
+  },
+  "speckl:reviewRequired": {
+    "@type": "speckl:ManualReview",
+    "speckl:status": "pending"
+  }
+}
+```
+
+---
+
+## 5. Examples
+
+### 5.1 Simple: API Rate Limiter
+
+```
+speck RateLimiter {
+  input: { requests: [Request], window: Nat, maxRequests: Nat }
+  output: { allowed: [Bool], remaining: Nat }
+  constraint: maxRequests > 0
+  constraint: window > 0
+  constraint: count(allowed, true) <= maxRequests
+  constraint: remaining == maxRequests - count(allowed, true)
+  verify: always(implies(remaining == 0, not(allowed[current])))
+}
+```
+
+### 5.2 Medium: Data Pipeline with Constraints
+
+```
+speck ETLTransform {
+  input: { source: DataSource, schema: Schema, dedup: Bool }
+  output: { result: Dataset, rejected: Nat }
+  constraint: result.schema == schema
+  constraint: rejected >= 0
+  constraint: implies(dedup, count(result) <= count(source))
+  constraint: implies(not dedup, count(result) == count(source))
+  verify: always(implies(dedup, no_duplicates(result)))
+}
+```
+
+### 5.3 Complex: Regulated Medical Device Function
+
+```
+speck DrugDosageCalculator {
+  input: {
+    patientWeight: Real,
+    drugConcentration: Real,
+    prescribedDose: Real,
+    minDose: Real,
+    maxDose: Real,
+    frequency: Nat
+  }
+  output: {
+    volume: Real,
+    safe: Bool
+  }
+  constraint: patientWeight > 0
+  constraint: drugConcentration > 0
+  constraint: minDose > 0
+  constraint: maxDose > minDose
+  constraint: frequency >= 1
+  constraint: frequency <= 6
+  constraint: implies(safe, volume >= minDose / drugConcentration)
+  constraint: implies(safe, volume <= maxDose / drugConcentration)
+  constraint: implies(not safe, volume == 0)
+  verify: always(implies(
+    prescribedDose >= minDose and prescribedDose <= maxDose,
+    safe
+  ))
+  verify: always(implies(not safe, volume == 0))
+  event DoseCalculated { volume: Real, safe: Bool }
+  event DoseRejected { reason: String }
+}
+```
+
+### 5.4 Edge: Self-Referential Spec
+
+```
+speck SpeckValidator {
+  input: { spec: SpeckDefinition, references: [SpeckDefinition] }
+  output: { valid: Bool, errors: [String] }
+  constraint: implies(valid, count(errors) == 0)
+  constraint: implies(not valid, count(errors) > 0)
+  constraint: forall(ref in references, ref.is_well_formed)
+  verify: always(implies(
+    spec.is_well_formed and forall(r in references, r.is_well_formed),
+    valid
+  ))
+}
+```
+
+### 5.5 Composed: Multi-Speck System
+
+```
+speck PaymentService {
+  import "rate-limiter.speck" as limiter
+  import "retry-handler.speck" as retry
+
+  input: { payment: Payment, apiKey: String }
+  output: Result
+
+  constraint: limiter.maxRequests == 100
+  constraint: limiter.window == 60
+  constraint: retry.maxRetries == 3
+  constraint: implies(not limiter.allowed, output == RateLimited)
+  constraint: implies(limiter.allowed, output in [Success, Failed, RetryExhausted])
+
+  verify: always(implies(
+    limiter.remaining == 0,
+    output == RateLimited
+  ))
+}
+```
+
+### 5.6 Dark Provenance: Regulated Medical Device (NEW)
+
+This example demonstrates all Dark Provenance primitives in a safety-critical context:
+
+```
+speck InfusionPumpController {
+  // Intent sources
+  provenance {
+    regulation: "FDA 21 CFR 820.30"
+    regulation: "IEC 62304 Class C"
+    design_decision: "ADR-0023 Infusion Safety Architecture"
+    external_doc: "AAMI TIR32" at "https://www.aami.org/tir32"
+  }
+
+  // Traceability to system requirements
+  satisfies SYS-REQ-042
+  satisfies SYS-REQ-043 clause "5.2.1"
+
+  // Authorship and origin
+  author: "Dr. Sarah Chen" <"s.chen@meddevice.example">
+  source: architecture_review ref "AR-2024-0315"
+
+  // Verification boundary
+  review: manual
+
+  // Parent spec relationship
+  derives from SafetyCriticalController via "decomposition of dosing logic"
+
+  input: {
+    prescribedRate: Real,
+    vtbi: Real,           // Volume to be infused
+    drugLibraryEntry: DrugProfile,
+    patientWeight: Real,
+    airInLineSensor: Bool
+  }
+
+  output: {
+    motorSpeed: Real,
+    occlusionAlarm: Bool,
+    airInLineAlarm: Bool,
+    complete: Bool
+  }
+
+  // Safety constraints
+  constraint: prescribedRate > 0
+  constraint: prescribedRate <= drugLibraryEntry.maxRate
+  constraint: vtbi > 0
+  constraint: patientWeight > 0
+  constraint: implies(airInLineSensor, motorSpeed == 0)
+  constraint: implies(occlusionAlarm, motorSpeed == 0)
+
+  // Therapeutic constraint: dose must match prescription
+  constraint: motorSpeed == prescribedRate * drugLibraryEntry.conversionFactor
+
+  verify: always(implies(
+    airInLineSensor or occlusionAlarm,
+    motorSpeed == 0
+  ))
+
+  verify: always(implies(
+    complete,
+    vtbi == 0
+  ))
+
+  event DoseStarted {
+    rate: Real
+    remainingVolume: Real
+    timestamp: Nat
+  }
+
+  event AlarmTriggered {
+    alarmType: String
+    severity: Nat
+    automaticResponse: String
+  }
+
+  event InfusionComplete {
+    totalVolumeDelivered: Real
+    duration: Real
+  }
+}
+```
+
+### 5.7 Dark Provenance: Auto-Verified Service (NEW)
+
+This example shows `review: auto` for internal services with no manual gate:
+
+```
+speck InternalMetricsCollector {
+  provenance {
+    parent_spec: ObservabilityPlatform
+    design_decision: "ADR-0056 Unified Telemetry"
+  }
+
+  author: "Platform Team" <"platform@example.com">
+  source: meeting ref "zoom://2024-04-15/platform-sync"
+
+  satisfies PLATFORM-REQ-12
+  derives from ObservabilityPlatform via "metrics ingestion path"
+
+  review: auto
+
+  input: {
+    serviceName: String,
+    metricBatch: [Metric],
+    apiKey: String
+  }
+
+  output: { accepted: Nat, rejected: Nat, latencyMs: Nat }
+
+  constraint: count(metricBatch) <= 1000
+  constraint: accepted + rejected == count(metricBatch)
+  constraint: latencyMs <= 100
+
+  verify: always(implies(
+    count(metricBatch) > 0,
+    accepted + rejected == count(metricBatch)
+  ))
+}
+```
+
+### 5.8 Dark Provenance: Compliance Audit Trail (NEW)
+
+This example demonstrates provenance for audit and compliance scenarios:
+
+```
+speck AuditLogValidator {
+  provenance {
+    regulation: "SOX Section 404"
+    regulation: "PCI-DSS v4.0 Requirement 10"
+  }
+
+  author: "Compliance Engineering"
+  source: compliance_audit ref "AUDIT-2024-Q1"
+
+  satisfies COMPLIANCE-REQ-08 clause "10.3"
+  review: hybrid
+
+  input: {
+    logEntry: LogEntry,
+    previousHash: String,
+    validatorKeys: [String]
+  }
+
+  output: { valid: Bool, tamperDetected: Bool, newHash: String }
+
+  constraint: implies(tamperDetected, not valid)
+  constraint: newHash == hash(logEntry, previousHash)
+  constraint: implies(valid, signatureValid(logEntry, validatorKeys))
+
+  verify: always(implies(
+    logEntry.hash != hash(logEntry.payload),
+    tamperDetected
+  ))
+
+  event IntegrityCheckFailed {
+    logId: String
+    expectedHash: String
+    actualHash: String
+    severity: Nat
+  }
+}
+```
+
+---
+
+## 6. Tooling
+
+### Reference Compiler
+
+The reference compiler (`speckl-compile`) is a Node.js/TypeScript application that:
+
+1. Parses SpeckDL files into an AST.
+2. Type-checks the AST against the type system defined in §3.
+3. Compiles constraints and verification conditions to SMT-LIB2.
+4. Invokes Z3 and interprets results.
+5. Compiles verified models to DSTs.
+6. Compiles DSTs to WASM.
+7. Emits provenance graph metadata (JSON-LD) at each stage.
+
+### Planned Tooling
+
+| Tool | Purpose | Status |
+|------|---------|--------|
+| `speckl-compile` | Reference compiler | Spec only |
+| `speckl-lsp` | Language Server Protocol (IDE support) | Planned |
+| `speckl-playground` | Browser-based spec editor + live verification | Planned |
+| `speckl-fmt` | Formatter | Planned |
+| `speckl-doc` | Documentation generator from Specks | Planned |
+
+---
+
+## Appendix A: Z3 Mapping Reference
+
+| SpeckDL Construct | SMT-LIB2 |
+|---|---|
+| `Nat n` | `(declare-const n Int)` + `(assert (>= n 0))` |
+| `Int n` | `(declare-const n Int)` |
+| `Real r` | `(declare-const r Real)` |
+| `Bool b` | `(declare-const b Bool)` |
+| `constraint: e` | `(assert e)` |
+| `verify: always(e)` | `(assert (not e))` + `(check-sat)` — expect UNSAT |
+| `verify: eventually(e)` | Not directly expressible; requires bounded model checking |
+| `a == b` | `(= a b)` |
+| `a implies b` | `(=> a b)` |
+| `a and b` | `(and a b)` |
+| `forall(x in S, e)` | `(forall ((x T)) (=> (member x S) e))` |
+
+## Appendix B: Dark Provenance JSON-LD Reference (NEW)
+
+| SpeckDL Primitive | JSON-LD Output | PROV-O Mapping |
+|---|---|---|
+| `provenance { regulation: X }` | Node with `prov:wasInformedBy` → Regulation | `prov:Entity` → `prov:Activity` |
+| `provenance { design_decision: X }` | Node with `prov:wasInformedBy` → Decision | `prov:Entity` → `prov:Activity` |
+| `provenance { parent_spec: X }` | Node with `prov:wasDerivedFrom` → Speck | `prov:Entity` → `prov:Entity` |
+| `provenance { external_doc: X at Y }` | Node with `prov:wasInformedBy` → Document | `prov:Entity` → `prov:Activity` |
+| `author: Name <email>` | Agent node + `prov:wasAttributedTo` | `prov:Agent` |
+| `source: kind ref X` | Source node + `prov:wasInformedBy` | `prov:Activity` with `prov:type` |
+| `derives from X via Y` | `prov:wasDerivedFrom` edge | `prov:wasDerivedFrom` |
+| `satisfies X clause Y` | `speckl:satisfies` edge + clause property | Extension property |
+| `review: manual` | `speckl:ManualReview` requirement node | Extension |
+| `review: auto` | No additional nodes (default path) | N/A |
+| `review: hybrid` | `speckl:HybridReview` with sampling params | Extension |
+
+---
+
+*This is a v0.2-DP specification. Dark Provenance primitives are optional but recommended for safety-critical and regulated systems. Feedback welcome via the [Speckl repository](https://os.scoble.me/forgejo/sscoble/speckl).*