sscoble/speckl
1
0
Fork 0
Code Issues 2 Pull requests Projects Releases Packages Wiki Activity Actions

Merge v0.2-DP into SPEC.md — unified v0.2 spec

Browse source 
- Integrated §3.6 Dark Provenance primitives (provenance, review, derives, satisfies, author, source)
- Added §3.6.5 Provenance-Aware Event Semantics
- Added §3.6.6 SpeckBOM (bom block)
- Added §3.6.7 Import Version Pinning
- Expanded §4.4 Provenance Graph with PROV-O node/edge types
- Added §4.5 Compilation Manifest with dual CycloneDX v1.6 + SPDX 3.0.1 output
- Updated EBNF grammar with all new primitives
- Updated examples 5.3 and 5.5 with provenance/bom/import-pinning
- Added Appendix B reference tables (B.1-B.4)
- Updated tooling section with CLI flags and speckl-compile status
- Preserved v0.2-DP reference file (not deleted)
This commit is contained in:
Scott Scoble 2026-04-29 15:05:26 -07:00
parent 712ec94495
commit 448819104a
1 changed files with 391 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

400
speckdl/SPEC.md
View file

@ -1,4 +1,4 @@
# SpeckDL Language Specification v0.1
# SpeckDL Language Specification v0.2
> The specification-first language for auditable software.
> Part of the [Speckl](https://os.scoble.me/forgejo/sscoble/speckl) project. MIT License.
@ -31,7 +31,7 @@ speck <Name> {
}
```
Members are drawn from: `input`, `output`, `constraint`, `verify`, `interface`, `import`, and `event`.
Members are drawn from: `input`, `output`, `constraint`, `verify`, `interface`, `import`, `event`, and the Dark Provenance primitives: `provenance`, `review`, `derives`, `satisfies`, `author`, `source`, and the SpeckBOM primitive: `bom`.
### 2.2 EBNF Grammar
@ -42,6 +42,9 @@ 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
| bom_def
input_def = "input" ":" type_expr
output_def = "output" ":" type_expr
@ -70,7 +73,33 @@ method_sig = IDENT "(" [ { IDENT ":" type_expr "," } ] ")" ":" type_expr
event_def = "event" IDENT "{" { IDENT ":" type_expr [","] } "}"
import_stmt = "import" STRING ["as" IDENT]
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"
bom_def = "bom" "{" { bom_clause } "}"
bom_clause = "compiler" ":" STRING ["version" STRING]
| "solver" ":" STRING ["version" STRING]
| "runtime" ":" STRING ["version" STRING]
| "license" ":" STRING
| "hash" ":" STRING
import_stmt = "import" STRING ["as" IDENT] ["version" STRING] ["hash" STRING]
literal = NAT_LIT | INT_LIT | REAL_LIT | BOOL_LIT | STRING_LIT
IDENT = letter { letter | digit | "_" }
@ -172,6 +201,128 @@ event RetryAttempted {
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
Dark Provenance primitives make intent sources and verification boundaries explicit in the specification language. They compile to JSON-LD provenance graph nodes and edges. These primitives are optional — bare Specks (without any provenance annotations) still compile — but they are recommended for safety-critical and regulated systems.
#### 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 a `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.
#### 3.6.6 SpeckBOM: Bill of Materials
A **SpeckBOM** is the specification analog of a Software Bill of Materials (SBOM). Where an SBOM lists software components, versions, and licenses, a SpeckBOM lists the complete dependency and artifact tree for a Speck system.
The `bom` block declares **toolchain dependencies** — what compiler, solver, and runtime a Speck requires. Combined with `import`, `derives`, and `satisfies`, it provides a full bill of materials:
| SpeckBOM concern | SpeckDL primitive | What it captures |
|---|---|---|
| **Spec dependencies** | `import` | Which other Specks this one depends on (with content hashes) |
| **Toolchain** | `bom { compiler, solver, runtime }` | What tools produced the verified artifacts |
| **Intent lineage** | `derives from`, `satisfies` | Which specs/requirements this one traces to |
| **Authorship** | `author`, `source` | Who wrote it and what drove it |
| **Artifact hashes** | `bom { hash }` | Content hash of the Speck source itself |
| **License** | `bom { license }` | Under what terms this spec can be used |
| **Compilation output** | *(auto-generated)* | Z3, DST, WASM hashes and solver results (see §4.5) |
**Why this matters.** In regulated environments (DO-178C, IEC 62304), an auditor needs to know not just "what code runs" but "what was the complete chain from requirement to deployed artifact." The SpeckBOM answers this declaratively — it's machine-readable, hash-pinned, and queriable.
**Example:**
```
speck DrugDosageCalculator {
bom {
compiler: "speckl-compile" version "0.2.0"
solver: "z3" version "4.12.5"
runtime: "wasm-runtime" version "1.0.0"
license: "MIT"
hash: "sha256:e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
}
import "retry-handler.speck" as retry
...
}
```
#### 3.6.7 Import Version Pinning
The `import` statement supports optional `version` and `hash` fields for reproducible builds:
```
import "retry-handler.speck" as retry
version "1.2.0"
hash "sha256:abcdef1234567890..."
```
- **`version`**: Semantic version of the imported Speck. The compiler verifies the imported file declares this version in its `bom` block.
- **`hash`**: Content hash of the imported file. The compiler computes the hash at parse time and fails if it doesn't match.
Version pinning is optional for local development but required for Specks with `review: manual` or `review: hybrid` — the compiler enforces that all imports are hash-pinned before allowing manual review sign-off.
---
## 4. Compilation Pipeline
@ -227,12 +378,128 @@ Speck "RetryHandler"
└── provenance: {
author: "scott",
timestamp: "2026-04-28T09:00:00Z",
tool: "speckl-compiler v0.1",
tool: "speckl-compiler v0.2",
z3_version: "4.12.5"
}
```
The provenance graph is serialized as JSON-LD and stored alongside the compiled artifacts.
The provenance graph is serialized as **JSON-LD using the W3C PROV-O vocabulary** and stored alongside the compiled artifacts.
#### 4.4.1 PROV-O Namespace and Context
The JSON-LD output uses the standard PROV-O namespace:
```json
{
"@context": {
"prov": "http://www.w3.org/ns/prov#",
"speckl": "https://speckl.scoble.me/ns/v0.2#",
"rdfs": "http://www.w3.org/2000/01/rdf-schema#"
}
}
```
#### 4.4.2 Provenance Node Types
| Node Type | PROV-O Class | Description |
|-----------|---------------|-------------|
| Speck | `prov:Entity` | The specification itself |
| Z3 Assertion Set | `prov:Entity` | Compiled SMT-LIB2 |
| DST | `prov:Entity` | Decision structure tree |
| WASM Module | `prov:Entity` | Compiled binary |
| Z3 Solver | `prov:Agent` | The verification tool |
| Compiler | `prov:Agent` | The compilation tool |
| Compilation Act | `prov:Activity` | A compilation stage |
| Author | `prov:Agent` | Person (from `author` primitive) |
| Source | `prov:Activity` | Intent origin (from `source` primitive) |
| Regulation | `prov:Entity` | Compliance requirement |
| Design Decision | `prov:Entity` | Architecture decision record |
#### 4.4.3 Provenance Edge Types
| Edge | PROV-O Property | From → To |
|------|-----------------|-----------|
| Compiled to | `prov:wasGeneratedBy` | Artifact → Compilation Act |
| Used tool | `prov:used` | Compilation Act → Tool (Agent) |
| Derived from | `prov:wasDerivedFrom` | Speck → Parent Speck |
| Informed by | `prov:wasInformedBy` | Speck → Regulation / Source |
| Attributed to | `prov:wasAttributedTo` | Speck → Author |
| Satisfies | `speckl:satisfies` | Speck → Requirement |
### 4.5 Compilation Manifest: Dual BOM Output
The compiler produces a **compilation manifest** containing both provenance and bill-of-materials data. The manifest supports two output formats:
- **CycloneDX v1.6** (JSON) — OWASP standard, ECMA-424
- **SPDX 3.0.1** (JSON-LD) — ISO 5962:2023
The `--bom-format` flag controls output: `cdx`, `spdx`, or `both` (default: `both`).
#### 4.5.1 Output Files
For a Speck named `Name`, the compiler produces:
| File | Format | Content |
|------|--------|---------|
| `Name.prov.jsonld` | JSON-LD / PROV-O | Intent provenance graph |
| `Name.specbom.cdx.json` | CycloneDX v1.6 JSON | Composition BOM (CycloneDX) |
| `Name.specbom.spdx.json` | SPDX 3.0.1 JSON-LD | Composition BOM (SPDX) |
#### 4.5.2 CycloneDX v1.6 Mapping
| SpeckDL Primitive | CycloneDX Location | Field |
|---|---|---|
| `bom { compiler }`, `bom { solver }`, `bom { runtime }` | `metadata.tools[]` | Standard tool entries |
| `bom { license }` | `metadata.component.licenses[]` | SPDX expression |
| `bom { hash }` | `metadata.component.hashes[]` | SHA-256 |
| `import "X" as Y hash H version V` | `components[]` | Component entry with purl, hashes, properties |
| `derives from X` | `component.properties[]` | `speckl:derivesFrom` |
| `satisfies X clause Y` | `component.properties[]` | `speckl:satisfies` |
| `author: Name <email>` | `annotations[]` | `speckl:provenanceType: author` |
| `source: kind ref X` | `annotations[]` | `speckl:provenanceType: source` |
| `provenance { regulation: X }` | `annotations[]` | `speckl:provenanceType: regulation` |
| `review: manual` | `annotations[]` | `speckl:reviewType: manual` |
| `review: auto` | No additional annotation | N/A |
| `review: hybrid` | `annotations[]` | `speckl:reviewType: hybrid` |
| Compilation artifacts (Z3, DST, WASM) | `components[]` (nested) | Type + hash |
| Verification results (SAT/UNSAT) | `metadata.component.properties[]` | `speckl:verificationResult` |
| Reproducibility status | `metadata.component.properties[]` | `speckl:reproducible` |
#### 4.5.3 SPDX 3.0.1 Mapping
| SpeckDL Primitive | SPDX Location | Field |
|---|---|---|
| `bom { compiler }`, `bom { solver }`, `bom { runtime }` | `spdx:Build` (in `builtBy`) | Tool name + version |
| `bom { license }` | `spdx:licenseConcluded` | SPDX expression (native) |
| `bom { hash }` | `spdx:hash` | SHA-256 |
| `import "X" hash H version V` | `spdx:Software` element | Package with version + hash |
| `derives from X` | `spdx:Relationship` (derivesFrom) | Standard SPDX relationship |
| `satisfies X clause Y` | `speckl:satisfies` property | Extension on element |
| `author: Name <email>` | `spdx:Relationship` (wasAttributedTo) | Agent element |
| `source: kind ref X` | `spdx:Relationship` (wasInformedBy) | Activity element |
| `provenance { regulation: X }` | `spdx:Relationship` + element | Regulation node |
| `review: manual` | `spdx:Annotation` (REVIEW) | Standard annotation |
| `review: auto` | No additional annotation | N/A |
| `review: hybrid` | `spdx:Annotation` (REVIEW) | `speckl:reviewType: hybrid` |
| Compilation artifacts (Z3, DST, WASM) | `spdx:SoftwareArtifact` elements | With hashes |
| Verification results (SAT/UNSAT) | `speckl:verificationResult` | Extension property |
| Reproducibility status | `speckl:reproducible` | Extension property |
#### 4.5.4 Two-Layer Architecture
Speckl produces **three complementary outputs**:
| Layer | Format | Concern | Standard |
|---|---|---|---|
| **Intent provenance** | JSON-LD / PROV-O | Who, why, what drove this specification | W3C PROV-O |
| **Composition BOM (CycloneDX)** | CycloneDX v1.6 JSON | What this spec depends on, builds with, produces | OWASP CycloneDX (ECMA-424) |
| **Composition BOM (SPDX)** | SPDX 3.0.1 JSON-LD | Same composition data, ISO-normative format | ISO 5962:2023 |
These layers are orthogonal:
- The provenance graph answers *"Why does this constraint exist?"* (regulatory, design decision, conversation)
- The SpeckBOM answers *"What is this spec made of, and can I reproduce it?"* (dependencies, toolchain, artifacts)
Together they form the complete audit trail: **intent** (PROV-O) + **composition** (CycloneDX or SPDX) = **full accountability**.
---
@ -270,6 +537,23 @@ speck ETLTransform {
```
speck DrugDosageCalculator {
provenance {
regulation: "FDA 21 CFR 820.30"
regulation: "IEC 62304 Class C"
design_decision: "ADR-0017: Separate dose calculation from administration"
}
review: manual
author: "Scott Scoble" <"scott@scoble.me">
source: regulation ref "FDA 21 CFR 820.30"
bom {
compiler: "speckl-compile" version "0.2.0"
solver: "z3" version "4.12.5"
runtime: "wasm-runtime" version "1.0.0"
license: "MIT"
hash: "sha256:e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
}
input: {
patientWeight: Real,
drugConcentration: Real,
@ -317,12 +601,32 @@ speck SpeckValidator {
}
```
### 5.5 Composed: Multi-Speck System
### 5.5 Composed: Multi-Speck System with Import Pinning
```
speck PaymentService {
import "rate-limiter.speck" as limiter
version "1.0.0"
hash "sha256:abcdef1234567890abcdef1234567890abcdef1234567890abcdef1234567890"
import "retry-handler.speck" as retry
version "2.1.0"
hash "sha256:fedcba0987654321fedcba0987654321fedcba0987654321fedcba0987654321"
provenance {
regulation: "PCI DSS 4.0 Requirement 6"
design_decision: "ADR-0022: Payment isolation with rate limiting"
}
review: hybrid
author: "Scott Scoble" <"scott@scoble.me">
source: compliance_audit ref "PCI-DSS-AUDIT-2026-Q2"
bom {
compiler: "speckl-compile" version "0.2.0"
solver: "z3" version "4.12.5"
runtime: "wasm-runtime" version "1.0.0"
license: "MIT"
hash: "sha256:9876543210abcdef9876543210abcdef9876543210abcdef9876543210abcdef"
}
input: { payment: Payment, apiKey: String }
output: Result
@ -354,13 +658,23 @@ The reference compiler (`speckl-compile`) is a Node.js/TypeScript application th
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.
7. Emits provenance graph metadata (JSON-LD / PROV-O) at each stage.
8. Emits SpeckBOM (CycloneDX v1.6 and/or SPDX 3.0.1) per §4.5.
### CLI
```
speckl-compile <file.speck> --output-dir <dir> --bom-format <cdx|spdx|both>
```
- `--output-dir`: Directory for output artifacts (default: `./out`)
- `--bom-format`: BOM output format — `cdx` (CycloneDX), `spdx` (SPDX), or `both` (default: `both`)
### Planned Tooling
| Tool | Purpose | Status |
|------|---------|--------|
| `speckl-compile` | Reference compiler | Spec only |
| `speckl-compile` | Reference compiler | In progress |
| `speckl-lsp` | Language Server Protocol (IDE support) | Planned |
| `speckl-playground` | Browser-based spec editor + live verification | Planned |
| `speckl-fmt` | Formatter | Planned |
@ -386,4 +700,72 @@ The reference compiler (`speckl-compile`) is a Node.js/TypeScript application th
---
*This is a v0.1 specification. The language is evolving. Feedback and contributions are welcome via the [Speckl repository](https://os.scoble.me/forgejo/sscoble/speckl).*
## Appendix B: Provenance and BOM Reference Mappings
### B.1 PROV-O JSON-LD Reference
| SpeckDL Primitive | PROV-O Class/Property | JSON-LD Key |
|---|---|---|
| `provenance { regulation: X }` | `prov:wasInformedBy` → `prov:Entity` (type: Regulation) | `wasInformedBy` |
| `provenance { design_decision: X }` | `prov:wasDerivedFrom` → `prov:Entity` (type: DesignDecision) | `wasDerivedFrom` |
| `provenance { parent_spec: X }` | `prov:wasDerivedFrom` → `prov:Entity` (type: Speck) | `wasDerivedFrom` |
| `provenance { external_doc: X }` | `prov:wasInformedBy` → `prov:Entity` (type: Document) | `wasInformedBy` |
| `author: Name <email>` | `prov:wasAttributedTo` → `prov:Agent` | `wasAttributedTo` |
| `source: kind ref X` | `prov:wasInformedBy` → `prov:Activity` (type: kind) | `wasInformedBy` |
| `derives from X via Y` | `prov:wasDerivedFrom` + `rdfs:comment` | `wasDerivedFrom`, `comment` |
| `satisfies X clause Y` | `speckl:satisfies` → `prov:Entity` | `speckl:satisfies` |
| `review: manual` | `prov:Activity` (type: ManualReview) | `speckl:reviewType` |
| `review: auto` | *(no node)* | N/A |
| `review: hybrid` | `prov:Activity` (type: HybridReview) | `speckl:reviewType` |
### B.2 SpeckBOM — CycloneDX v1.6
| SpeckDL Primitive | CycloneDX Location | Field |
|---|---|---|
| `bom { compiler }`, `bom { solver }`, `bom { runtime }` | `metadata.tools[]` | Standard tool entries |
| `bom { license }` | `metadata.component.licenses[]` | SPDX expression |
| `bom { hash }` | `metadata.component.hashes[]` | SHA-256 |
| `import "X" as Y hash H version V` | `components[]` | Component entry with purl, hashes, properties |
| `derives from X` | `component.properties[]` | `speckl:derivesFrom` |
| `satisfies X clause Y` | `component.properties[]` | `speckl:satisfies` |
| `author: Name <email>` | `annotations[]` | `speckl:provenanceType: author` |
| `source: kind ref X` | `annotations[]` | `speckl:provenanceType: source` |
| `provenance { regulation: X }` | `annotations[]` | `speckl:provenanceType: regulation` |
| `review: manual` | `annotations[]` | `speckl:reviewType: manual` |
| `review: auto` | No additional annotation | N/A |
| `review: hybrid` | `annotations[]` | `speckl:reviewType: hybrid` |
| Compilation artifacts (Z3, DST, WASM) | `components[]` (nested) | Type + hash |
| Verification results (SAT/UNSAT) | `metadata.component.properties[]` | `speckl:verificationResult` |
| Reproducibility status | `metadata.component.properties[]` | `speckl:reproducible` |
### B.3 SpeckBOM — SPDX 3.0.1
| SpeckDL Primitive | SPDX Location | Field |
|---|---|---|
| `bom { compiler }`, `bom { solver }`, `bom { runtime }` | `spdx:Build` (in `builtBy`) | Tool name + version |
| `bom { license }` | `spdx:licenseConcluded` | SPDX expression (native) |
| `bom { hash }` | `spdx:hash` | SHA-256 |
| `import "X" hash H version V` | `spdx:Software` element | Package with version + hash |
| `derives from X` | `spdx:Relationship` (derivesFrom) | Standard SPDX relationship |
| `satisfies X clause Y` | `speckl:satisfies` property | Extension on element |
| `author: Name <email>` | `spdx:Relationship` (wasAttributedTo) | Agent element |
| `source: kind ref X` | `spdx:Relationship` (wasInformedBy) | Activity element |
| `provenance { regulation: X }` | `spdx:Relationship` + element | Regulation node |
| `review: manual` | `spdx:Annotation` (REVIEW) | Standard annotation |
| `review: auto` | No additional annotation | N/A |
| `review: hybrid` | `spdx:Annotation` (REVIEW) | `speckl:reviewType: hybrid` |
| Compilation artifacts (Z3, DST, WASM) | `spdx:SoftwareArtifact` elements | With hashes |
| Verification results (SAT/UNSAT) | `speckl:verificationResult` | Extension property |
| Reproducibility status | `speckl:reproducible` | Extension property |
### B.4 Two-Layer Architecture
| Layer | Format | Concern | Standard |
|---|---|---|---|
| **Intent provenance** | JSON-LD / PROV-O | Who, why, what drove this specification | W3C PROV-O |
| **Composition BOM (CycloneDX)** | CycloneDX v1.6 JSON | Dependencies, toolchain, artifacts | OWASP CycloneDX (ECMA-424) |
| **Composition BOM (SPDX)** | SPDX 3.0.1 JSON-LD | Same data, ISO-normative format | ISO 5962:2023 |
---
*This is a v0.2 specification. Dark Provenance and SpeckBOM primitives are optional but recommended for safety-critical and regulated systems. Feedback and contributions are welcome via the [Speckl repository](https://os.scoble.me/forgejo/sscoble/speckl).*