From ec1edc9f0f701352ba33d8d56ce42d2f9a45ca3e Mon Sep 17 00:00:00 2001 From: Content Agent Date: Tue, 28 Apr 2026 16:16:04 -0700 Subject: [PATCH] feat: SpeckDL v0.2-DP spec with dark provenance primitives MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- speckdl/SPEC.v2-dp-primitives.md | 706 +++++++++++++++++++++++++++++++ 1 file changed, 706 insertions(+) create mode 100644 speckdl/SPEC.v2-dp-primitives.md diff --git a/speckdl/SPEC.v2-dp-primitives.md b/speckdl/SPEC.v2-dp-primitives.md new file mode 100644 index 0000000..df34c4f --- /dev/null +++ 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 { + +} +``` + +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 ` | 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).* \ No newline at end of file