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