speckl/speckdl/SPEC.md

SpeckDL Language Specification v0.1

The specification-first language for auditable software. Part of the 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, and event.

2.2 EBNF Grammar

file           = { speck_def | import_stmt }

speck_def      = "speck" IDENT "{" { member } "}"

member         = input_def | output_def | constraint_def
               | verify_def | interface_def | event_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 [","] } "}"

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:

(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:

(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.

---

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

At each compilation stage, the pipeline records derivation 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: {
        author: "scott",
        timestamp: "2026-04-28T09:00:00Z",
        tool: "speckl-compiler v0.1",
        z3_version: "4.12.5"
      }

The provenance graph is serialized as JSON-LD and stored alongside the compiled artifacts.

---

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
  ))
}

---

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))

---

This is a v0.1 specification. The language is evolving. Feedback and contributions are welcome via the Speckl repository.