From 712ec9449575093affcb930b8dd951b57b8fa194 Mon Sep 17 00:00:00 2001 From: Scott Scoble Date: Wed, 29 Apr 2026 14:43:53 -0700 Subject: [PATCH] Add SpeckDL examples with Dark Provenance primitives --- examples/AccessControl.speck | 157 ++++++++++++++++++++++++++++ examples/DrugDosageCalculator.speck | 119 +++++++++++++++++++++ examples/PaymentService.speck | 143 +++++++++++++++++++++++++ examples/RetryHandler.speck | 91 ++++++++++++++++ examples/TemperatureMonitor.speck | 138 ++++++++++++++++++++++++ 5 files changed, 648 insertions(+) create mode 100644 examples/AccessControl.speck create mode 100644 examples/DrugDosageCalculator.speck create mode 100644 examples/PaymentService.speck create mode 100644 examples/RetryHandler.speck create mode 100644 examples/TemperatureMonitor.speck diff --git a/examples/AccessControl.speck b/examples/AccessControl.speck new file mode 100644 index 0000000..489306b --- /dev/null +++ b/examples/AccessControl.speck @@ -0,0 +1,157 @@ +// AccessControl.speck +// Derives/satisfies for regulatory traceability +// +// Provenance: Access control system requiring full regulatory +// compliance traceability. Every access decision must be traceable +// to its source requirements and regulatory clauses. +// +// SpeckBOM: Full BOM with regulatory traceability, audit +// logging requirements, and compliance verification. +// +// Author: Security Engineering Team +// Source: Security Architecture Review, SOC 2 Compliance Audit + +speck AccessControl { + // SpeckBOM - declare toolchain and compliance metadata + 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: AccessControl-base-v1" + } + + // Intent provenance - regulatory and security context + provenance { + regulation: "SOC 2 Type II" // Trust Services Criteria + regulation: "ISO 27001:2022" // Information security + regulation: "GDPR Article 32" // Security of processing + design_decision: "ADR-0012 Identity and Access Management" + parent_spec: "SecurityFoundation" + external_doc: "NIST SP 800-63B" at "https://pages.nist.gov/800-63-3/sp800-63b.html" + } + + // Traceability to security requirements and regulatory clauses + satisfies ACCESS-REQ-001 + satisfies ACCESS-REQ-002 clause "4.1.3" + satisfies ACCESS-REQ-003 clause "5.2.1" + satisfies SOC2-CC-6-1 clause "Logical access security" + satisfies SOC2-CC-7-1 clause "Security monitoring" + satisfies GDPR-ART-32 clause "Security of processing" + + // Authorship and origin + author: "Security Engineering" <"security@scoble.me"> + source: architecture_review ref "AR-2024-0108" + source: compliance_audit ref "AUDIT-2024-SOC2-001" + source: meeting ref "zoom://2024-01-15/security-architecture" + + // Verification boundary - manual review required for security changes + review: manual + + // Derives from security foundation, satisfies access control requirements + derives from SecurityFoundation via "access control policy enforcement" + satisfies SECURITY-REQ-001 + + // Input: access request and context + input: { + userId: String, + resourceId: String, + requestedAction: Action, + userRoles: [String], + userGroups: [String], + timestamp: Nat, + ipAddress: String, + deviceFingerprint: String, + sessionToken: String + } + + // Output: access decision and metadata + output: { + allowed: Bool, + reason: String, + policyId: String, + auditTrail: [String], + rateLimitRemaining: Nat, + sessionValid: Bool + } + + // Constraints - access control invariants + constraint: userId != "" + constraint: resourceId != "" + constraint: timestamp > 0 + constraint: count(userRoles) >= 0 + constraint: count(userGroups) >= 0 + constraint: sessionToken != "" + + // Policy constraints - must have valid policy + constraint: policyId != "" + constraint: implies(allowed, policyId != "") + constraint: implies(not allowed, reason != "") + + // Rate limiting constraint + constraint: rateLimitRemaining >= 0 + constraint: rateLimitRemaining <= 100 + + // Session validation constraint + constraint: implies(sessionValid, sessionToken != "") + + // Verification: access decisions are correct + verify: always(implies( + allowed, + hasPermission(userId, resourceId, requestedAction, userRoles, userGroups) + )) + + verify: always(implies( + not allowed, + not hasPermission(userId, resourceId, requestedAction, userRoles, userGroups) + )) + + verify: always(implies( + rateLimitRemaining == 0, + allowed == false + )) + + // Verification: audit trail is complete + verify: always(implies( + allowed or not allowed, + count(auditTrail) >= 1 + )) + + // Events for security audit trail + event AccessAttempt { + userId: String + resourceId: String + requestedAction: String + allowed: Bool + timestamp: Nat + } + + event AccessDenied { + userId: String + resourceId: String + requestedAction: String + reason: String + timestamp: Nat + } + + event PolicyEvaluated { + policyId: String + userId: String + resourceId: String + result: String + timestamp: Nat + } + + event RateLimited { + userId: String + requestCount: Nat + limit: Nat + timestamp: Nat + } + + event SessionInvalidated { + sessionToken: String + reason: String + timestamp: Nat + } +} diff --git a/examples/DrugDosageCalculator.speck b/examples/DrugDosageCalculator.speck new file mode 100644 index 0000000..cc7f73a --- /dev/null +++ b/examples/DrugDosageCalculator.speck @@ -0,0 +1,119 @@ +// DrugDosageCalculator.speck +// Medical device showing provenance + SpeckBOM annotations +// +// Provenance: This is a safety-critical medical device component. +// Every calculation must be traceable to regulatory requirements, +// design decisions, and clinical evidence. +// +// SpeckBOM: Full bill of materials including compiler, solver, +// runtime, and full provenance graph with regulatory traceability. +// +// Author: Dr. Sarah Chen +// Source: IEC 62304 Class C medical device standard + +speck DrugDosageCalculator { + // SpeckBOM - critical for medical device compliance + 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: DrugDosageCalculator-base-v1" + } + + // Intent provenance - regulatory and design context + provenance { + regulation: "FDA 21 CFR 820.30" // Quality system regulation + regulation: "IEC 62304 Class C" // Medical device software lifecycle + regulation: "ISO 14971" // Risk management + design_decision: "ADR-0023 Infusion Safety Architecture" + external_doc: "AAMI TIR32" at "https://www.aami.org/tir32" + parent_spec: "InfusionPumpBase" // Decomposition + } + + // Traceability to system requirements and regulatory clauses + satisfies SYS-REQ-042 + satisfies SYS-REQ-043 clause "5.2.1" + satisfies FDA-820-30 clause "d" + satisfies IEC-62304-Annex-3 + + // Authorship and origin + author: "Dr. Sarah Chen" <"s.chen@meddevice.example"> + source: architecture_review ref "AR-2024-0315" + source: meeting ref "zoom://2024-03-10/medical-device-wg" + + // Verification boundary - MANUAL REVIEW REQUIRED before deployment + review: manual + + // Parent spec relationship - decomposed from broader controller + derives from InfusionPumpController via "decomposition of dosing logic" + + // Input parameters for dosage calculation + input: { + patientWeight: Real, // Patient weight in kg + drugConcentration: Real, // Drug concentration (mg/mL) + prescribedDose: Real, // Prescribed dose (mg) + minDose: Real, // Minimum therapeutic dose (mg) + maxDose: Real, // Maximum safe dose (mg) + frequency: Nat, // Administration frequency (times/day) + vtbi: Real // Volume to be infused (mL) + } + + // Output: calculated dosage and safety flags + output: { + volume: Real, // Calculated volume (mL) + safe: Bool, // Safety flag + concentrationCheck: Bool, // Concentration within limits + weightBasedCheck: Bool, // Weight-based calculation validated + maxRateCheck: Bool // Rate within safe limits + } + + // Safety constraints - ALL must hold for valid dosage + constraint: patientWeight > 0 + constraint: patientWeight <= 200 // Max realistic patient weight + constraint: drugConcentration > 0 + constraint: drugConcentration <= 100 // Realistic concentration range + constraint: minDose > 0 + constraint: maxDose > minDose + constraint: frequency >= 1 + constraint: frequency <= 6 // Reasonable frequency limits + constraint: vtbi > 0 + constraint: vtbi <= 1000 // Typical IV bag sizes + + // Therapeutic constraints - dose must be clinically appropriate + constraint: implies(safe, volume >= minDose / drugConcentration) + constraint: implies(safe, volume <= maxDose / drugConcentration) + constraint: implies(not safe, volume == 0) // No dose if unsafe + + // Safety verification - critical properties that must be proven + verify: always(implies( + prescribedDose >= minDose and prescribedDose <= maxDose, + safe + )) + + verify: always(implies( + patientWeight <= 0 or drugConcentration <= 0, + not safe + )) + + verify: always(implies(not safe, volume == 0)) + + // Events for clinical traceability and audit + event DoseCalculated { + volume: Real + safe: Bool + timestamp: Nat + } + + event DoseRejected { + reason: String + timestamp: Nat + } + + event CriticalLimitExceeded { + parameter: String + value: Real + limit: Real + timestamp: Nat + } +} diff --git a/examples/PaymentService.speck b/examples/PaymentService.speck new file mode 100644 index 0000000..45d4c64 --- /dev/null +++ b/examples/PaymentService.speck @@ -0,0 +1,143 @@ +// PaymentService.speck +// Import pinning with hash verification +// +// Provenance: Payment processing system component requiring strict +// integrity verification of all dependencies. Import hashes ensure +// reproducibility and tamper detection. +// +// SpeckBOM: Full BOM with import pinning, compiler versions, and +// hash verification for all transitive dependencies. +// +// Author: Platform Engineering Team +// Source: Payment Systems Architecture Review, PCI-DSS Compliance Audit + +speck PaymentService { + // SpeckBOM - declare toolchain with version pinning + 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: PaymentService-base-v1" + } + + // Intent provenance - regulatory and architectural context + provenance { + regulation: "PCI-DSS v4.0 Requirement 6.1" // Secure coding standards + regulation: "PCI-DSS v4.0 Requirement 6.3" // Change management + regulation: "PCI-DSS v4.0 Requirement 10.1" // Audit logging + design_decision: "ADR-0035 Payment Gateway Strategy" + parent_spec: "TransactionProcessor" + external_doc: "OWASP Payment Handling Guidelines" at "https://owasp.org/payment" + } + + // Traceability to system requirements and compliance + satisfies PAYMENT-REQ-001 + satisfies PAYMENT-REQ-002 clause "4.2.1" + satisfies PCI-DSS-6-1 clause "Secure coding practices" + satisfies PCI-DSS-10-1 clause "Audit trails" + + // Authorship and origin + author: "Platform Engineering" <"platform@scoble.me"> + source: architecture_review ref "AR-2024-0410" + source: compliance_audit ref "AUDIT-2024-Q2-PAYMENT" + + // Verification boundary - automated with spot-check sampling + review: hybrid + + // Derives from payment processor base, satisfies transaction requirements + derives from TransactionProcessor via "specialization for payment operations" + satisfies TRANSACTION-REQ-001 + + // Import statements with version pinning and hash verification + // These imports must match exactly - hash checked at compile time + import "rate-limiter.speck" as limiter + hash: "sha256:f7a1b2c3d4e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3f4a5b6c7d8e9f0a1" + version: "2.1.0" + + import "retry-handler.speck" as retry + hash: "sha256:b3c9d4e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3f4a5b6c7d8e9f0a1b2c3" + version: "1.4.0" + + import "fraud-scanner.speck" as fraud + hash: "sha256:a1b2c3d4e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3f4a5b6c7d8e9f0a1b2c3" + version: "3.0.0" + + // Input parameters for payment processing + input: { + payment: Payment, + apiKey: String, + merchantId: String, + customerIp: String, + userAgent: String + } + + // Output: processing result and metadata + output: { + result: PaymentResult, + transactionId: String, + fraudScore: Real, + fraudFlags: [String], + rateLimitRemaining: Nat, + retryCount: Nat + } + + // Constraints - payment processing invariants + constraint: limiter.maxRequests == 100 + constraint: limiter.window == 60 + constraint: retry.maxRetries == 3 + constraint: fraud.fraudCheckEnabled == true + constraint: transactionId != "" + + // Rate limiting constraint + constraint: implies(not limiter.allowed, result == RateLimited) + + // Retry constraint - if rate limited, must retry with backoff + constraint: implies(result == RateLimited, retryCount > 0) + + // Fraud constraint - fraud score must be calculated + constraint: fraudScore >= 0 + constraint: fraudScore <= 100 + + // Verify: rate limiting works correctly + verify: always(implies( + limiter.remaining == 0, + result == RateLimited + )) + + verify: always(implies( + result == Success, + transactionId != "" + )) + + // Events for payment audit trail + event PaymentProcessed { + transactionId: String + amount: Real + currency: String + status: String + timestamp: Nat + } + + event RateLimited { + clientIp: String + requestCount: Nat + windowSeconds: Nat + timestamp: Nat + } + + event FraudDetected { + transactionId: String + fraudScore: Real + flags: [String] + action: String + timestamp: Nat + } + + event RetryAttempted { + transactionId: String + attemptNumber: Nat + delayMs: Nat + timestamp: Nat + } +} diff --git a/examples/RetryHandler.speck b/examples/RetryHandler.speck new file mode 100644 index 0000000..38248de --- /dev/null +++ b/examples/RetryHandler.speck @@ -0,0 +1,91 @@ +// RetryHandler.speck +// Simple retry with backoff constraints +// +// Provenance: This spec defines a standard retry mechanism used across +// multiple services. It's a foundational component for resilience patterns. +// +// BOM: This spec is version-pinned and hash-verified for reproducibility. +// +// Author: Scott Scoble +// Source: Architecture review ADR-0021 - Resilience Patterns + +speck RetryHandler { + // SpeckBOM - declare toolchain dependencies and integrity + 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: RetryHandler-base-v1" + } + + // Intent provenance - where did this spec come from? + provenance { + design_decision: "ADR-0021 Resilience Patterns" + external_doc: "AWS Retry Best Practices" at "https://aws.amazon.com/architecture/retry/" + } + + // Traceability - derives from base fault handler, satisfies resiliency requirements + derives from FaultHandler via "specialization for retry logic" + satisfies RESILIENCE-REQ-01 clause "3.1.2" + satisfies RESILIENCE-REQ-02 + + // Who wrote this and why + author: "Scott Scoble" <"scott@scoble.me"> + source: architecture_review ref "AR-2024-0215" + + // Verification boundary - this needs manual review + review: manual + + // Input: operation to retry, max retries allowed + input: { + operation: Operation, + maxRetries: Nat, + initialDelay: Real, + maxDelay: Real + } + + // Output: result of operation (success or final failure) + output: { + success: Bool, + finalResult: String, + attemptCount: Nat, + totalDelay: Real + } + + // Constraints - invariants that must hold + constraint: maxRetries <= 10 + constraint: maxRetries >= 0 + constraint: initialDelay > 0 + constraint: maxDelay >= initialDelay + constraint: totalDelay == sum(delays) + constraint: totalDelay <= 30s + + // Backoff constraint - delay grows exponentially + constraint: backoff(delay(n)) == delay(n-1) * 2 + constraint: delay(n) <= maxDelay + + // Verify: if retry attempt > 1, delay must be positive + verify: always(implies(attempt > 1, delay > 0)) + + // Verify: if all retries exhausted, operation must have failed + verify: always(implies(attemptCount == maxRetries + 1, not success)) + + // Events for observability and provenance tracking + event RetryAttempted { + attemptNumber: Nat + delay: Real + remainingRetries: Nat + } + + event OperationSucceeded { + attemptCount: Nat + totalDelay: Real + } + + event OperationFailed { + attemptCount: Nat + totalDelay: Real + finalError: String + } +} diff --git a/examples/TemperatureMonitor.speck b/examples/TemperatureMonitor.speck new file mode 100644 index 0000000..6dddb29 --- /dev/null +++ b/examples/TemperatureMonitor.speck @@ -0,0 +1,138 @@ +// TemperatureMonitor.speck +// IoT with constraint-based verification +// +// Provenance: IoT sensor monitoring system for industrial safety. +// All temperature readings must be verified against safety constraints +// before triggering alerts or actions. +// +// SpeckBOM: Full BOM including sensor firmware hashes and +// constraint verification results for compliance. +// +// Author: Industrial IoT Team +// Source: Safety Critical Systems Design Review, ISO 13849 Compliance + +speck TemperatureMonitor { + // SpeckBOM - declare toolchain and firmware hashes + 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: TemperatureMonitor-base-v1" + } + + // Intent provenance - safety and compliance context + provenance { + regulation: "ISO 13849" // Machinery safety + regulation: "IEC 62061" // Functional safety + design_decision: "ADR-0048 Industrial IoT Architecture" + external_doc: "ISO 13849-2:2015 Annex B" at "https://www.iso.org/standard/59384.html" + external_doc: "IEC 62061:2021" at "https://www.iec.ch/dynamic/publication/62061" + } + + // Traceability to safety requirements + satisfies SAFETY-REQ-001 + satisfies SAFETY-REQ-002 clause "5.3.1" + satisfies ISO-13849-5 clause "Performance Level requirements" + + // Authorship and origin + author: "Industrial IoT Team" <"iot@scoble.me"> + source: architecture_review ref "AR-2024-0520" + source: compliance_audit ref "AUDIT-2024-INDUSTRY-001" + + // Verification boundary - automatic verification for sensor data + review: auto + + // Derives from sensor base, satisfies safety requirements + derives from SensorMonitor via "temperature-specific monitoring logic" + satisfies SENSOR-REQ-001 + + // Input: sensor readings and configuration + input: { + currentTemp: Real, // Current temperature reading (°C) + ambientTemp: Real, // Ambient temperature (°C) + setPoint: Real, // Target temperature (°C) + maxTemp: Real, // Maximum safe temperature (°C) + minTemp: Real, // Minimum safe temperature (°C) + hysteresis: Real, // Hysteresis band (°C) + sensorId: String, // Sensor identifier + calibrationOffset: Real // Calibration offset (°C) + } + + // Output: monitoring result and actions + output: { + status: TempStatus, + alert: Bool, + action: TempAction, + safe: Bool, + deviation: Real, + timeInAlert: Real + } + + // Constraints - temperature safety invariants + constraint: maxTemp > setPoint + constraint: setPoint > minTemp + constraint: hysteresis > 0 + constraint: hysteresis < (maxTemp - minTemp) / 2 + constraint: calibrationOffset >= -10 + constraint: calibrationOffset <= 10 + + // Safety constraint - deviation must be within bounds + constraint: implies(safe, deviation <= hysteresis) + constraint: implies(not safe, deviation > hysteresis) + + // Temperature range constraints + constraint: currentTemp >= minTemp - 20 // Allow temporary excursions + constraint: currentTemp <= maxTemp + 20 + constraint: ambientTemp >= -40 + constraint: ambientTemp <= 85 + + // Verification: alert logic is correct + verify: always(implies( + currentTemp > maxTemp + hysteresis, + alert + )) + + verify: always(implies( + currentTemp < minTemp - hysteresis, + alert + )) + + verify: always(implies( + alert, + action in [EmergencyShutDown, Warning, Override] + )) + + verify: always(implies( + not alert, + action == NormalOperation + )) + + // Events for safety audit trail + event TemperatureReading { + sensorId: String + temperature: Real + timestamp: Nat + } + + event TemperatureAlert { + sensorId: String + temperature: Real + threshold: Real + alertType: String + timestamp: Nat + } + + event SafetyAction { + sensorId: String + action: String + timestamp: Nat + } + + event CalibrationWarning { + sensorId: String + offset: Real + reason: String + timestamp: Nat + } +}