speckl/examples/PaymentService.speck

143 lines
4.1 KiB
Text

// 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 <platform@scoble.me>
// 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
}
}