Main.hs

{-# LANGUAGE GADTs, DataKinds, KindSignatures, StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies, FlexibleInstances, ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}

-- Main.hs - Airlock Kernel v6.0 (Certified Core)
-- Zero Runtime Exceptions. Pure Domain Logic. Multi-Sig Enforcement.
-- Compiler used: https://play.haskell.org/

module Main where

import Data.Char (ord)
import Data.List (intercalate, nub)

-- ==================== 1. TYPE-LEVEL SAFETY & IMPACT ====================

data ImpactLevel = Safe | Critical | Existential
    deriving (Show, Eq, Ord)

-- Intent is separate from Impact. 
-- Intent = Why? Impact = What?
data Intent = Benevolent | Neutral | Malicious 
    deriving (Show, Eq)

data Target = System | Human 
    deriving (Show, Eq)

data Priority = Standard | Supreme 
    deriving (Show, Eq)

-- ==================== 2. THE COMMAND GADT (EXHAUSTIVE) ====================

data Command (impact :: ImpactLevel) where
    -- Safe
    QueryStatus    :: Command 'Safe
    DispenseCoffee :: Command 'Safe
    
    -- Critical (Requires Rollback Plan)
    RestartService :: String -> Command 'Critical
    UpdateConfig   :: String -> String -> Command 'Critical

    -- Existential (Requires Multi-Sig)
    FormatDisk     :: Command 'Existential
    DeployAirbag   :: Command 'Existential

deriving instance Show (Command i)

-- Forensic Hashing (Deterministic)
class Fingerprint a where
    fingerprint :: a -> String

instance Fingerprint (Command i) where
    fingerprint cmd = case cmd of
        QueryStatus        -> "CMD_001_QUERY"
        DispenseCoffee     -> "CMD_002_COFFEE"
        RestartService s   -> "CMD_101_RST:" ++ s
        UpdateConfig k v   -> "CMD_102_CFG:" ++ k ++ "=" ++ v
        FormatDisk         -> "CMD_999_WIPE"
        DeployAirbag       -> "CMD_998_BAG"

-- ==================== 3. CONTEXT & QUORUM ====================

newtype Timestamp = Timestamp Int deriving (Show, Eq)

data User = User { uid :: String, role :: String } 
    deriving (Show, Eq)

-- Multi-Sig Support: A list of unique approvals
newtype Quorum = Quorum [User] 
    deriving Show

data KernelEnv = KernelEnv {
    envTime :: Timestamp,
    envRequester :: User,
    envApprovals :: Quorum
} deriving Show

-- ==================== 4. PURE EFFECTS & PLANS (NO IO HERE) ====================

-- Description of Atomic Effects (Data, not Functions)
data Atom
    = DB_Read String
    | DB_Write String
    | Hardware_GPIO Int Bool
    | Sys_ProcessControl String String
    | Disk_RawWrite Int
    | Log_Entry String
    deriving Show

-- The Execution Plan: Forward action + Compensation logic
data TransactionPlan 
    = AtomicPlan { 
        forward :: Atom, 
        backward :: Maybe Atom, -- Pure description of rollback
        risk :: ImpactLevel 
    }
    | MultiStepPlan [TransactionPlan]
    deriving Show

-- ==================== 5. THE PURE INTERPRETER ====================

-- Transforms Domain Command -> Execution Plan (Purely)
interpret :: Command i -> TransactionPlan
interpret cmd = case cmd of
    -- SAFE: No rollback needed
    QueryStatus -> AtomicPlan 
        (DB_Read "SELECT status") Nothing Safe
    
    DispenseCoffee -> AtomicPlan 
        (Hardware_GPIO 13 True) Nothing Safe

    -- CRITICAL: Explicit Rollback defined as Data
    RestartService s -> AtomicPlan 
        (Sys_ProcessControl "restart" s) 
        (Just (Sys_ProcessControl "stop" s)) -- The undo data
        Critical
    
    UpdateConfig k v -> AtomicPlan 
        (DB_Write ("SET " ++ k ++ "=" ++ v))
        (Just (DB_Write ("REVERT " ++ k))) 
        Critical

    -- EXISTENTIAL: Irreversible (Backward is Nothing)
    FormatDisk -> AtomicPlan 
        (Disk_RawWrite 0) Nothing Existential
    
    DeployAirbag -> AtomicPlan 
        (Hardware_GPIO 99 True) Nothing Existential

-- ==================== 6. THE CONSTITUTION (EXHAUSTIVE RULES) ====================

data Violation = Violation { code :: String, reason :: String } deriving Show

data Verdict (i :: ImpactLevel)
    = Blocked Violation
    | Authorized (Command i) String -- String is the Audit Hash

-- Helper to safely extract runtime impact level without partial functions
getImpact :: Command i -> ImpactLevel
getImpact cmd = case cmd of
    QueryStatus      -> Safe
    DispenseCoffee   -> Safe
    RestartService _ -> Critical
    UpdateConfig _ _ -> Critical
    FormatDisk       -> Existential
    DeployAirbag     -> Existential

-- The Rules
type Rule = KernelEnv -> Intent -> Target -> Priority -> ImpactLevel -> Maybe Violation

-- Rule 1: Human Safety (Asimov's 1st Law)
ruleHumanSafety :: Rule
ruleHumanSafety _ intent target _ _ 
    | target == Human && intent == Malicious = Just $ Violation "R1" "Malicious vs Human"
    | otherwise = Nothing

-- Rule 2: Sabotage (Malicious Intent + High Impact)
ruleSabotage :: Rule
ruleSabotage _ intent target _ impact
    | target == System && intent == Malicious && impact /= Safe = 
        Just $ Violation "R2" "Sabotage Attempt (Malicious + Impactful)"
    | otherwise = Nothing

-- Rule 3: Two-Man Rule (Quorum Check)
ruleMultiSig :: Rule
ruleMultiSig env _ _ _ impact
    | impact == Existential = 
        let (Quorum approvers) = envApprovals env
        in if length (nub $ map uid approvers) >= 2 
           then Nothing 
           else Just $ Violation "R3" "Existential Action requires Quorum (Min 2 Approvals)"
    | otherwise = Nothing

-- The Auditor
audit :: KernelEnv -> Intent -> Target -> Priority -> Command i -> Verdict i
audit env intent target priority cmd = 
    let 
        impact = getImpact cmd
        rules = [ruleHumanSafety, ruleSabotage, ruleMultiSig]
        
        -- Run all rules. Order independent. First failure blocks.
        failures = [ v | r <- rules, Just v <- [r env intent target priority impact] ]
        
        -- Forensic Hashes
        cmdHash = fingerprint cmd -- "CMD_WIPE" (Global)
        txHash  = "TX_" ++ show (envTime env) ++ "_" ++ uid (envRequester env) -- "TX_100_USER" (Local)
        
    in case failures of
        (v:_) -> Blocked v
        []    -> Authorized cmd (cmdHash ++ "|" ++ txHash)

-- ==================== 7. RUNTIME (THE ONLY IO) ====================

-- Executes the pure Atom
execAtom :: Atom -> IO ()
execAtom a = putStrLn $ "      [HW] Executing: " ++ show a

-- Executes the pure Plan
runPlan :: TransactionPlan -> IO ()
runPlan (AtomicPlan fwd bwd risk) = do
    putStrLn $ "   [EXEC] Running Plan (Risk: " ++ show risk ++ ")"
    execAtom fwd
    -- Here a real runtime would log the 'bwd' (undo) atom to a journal
    -- for recovery if the crash happens immediately after.
    case bwd of
        Just undo -> putStrLn $ "      [JOURNAL] Undo Step Saved: " ++ show undo
        Nothing   -> putStrLn "      [JOURNAL] Atomic / Irreversible"

runKernel :: KernelEnv -> Intent -> Target -> Priority -> Command i -> IO ()
runKernel env i t p cmd = do
    putStrLn $ "\n--- REQUEST: " ++ fingerprint cmd ++ " ---"
    
    case audit env i t p cmd of
        Blocked v -> do
            putStrLn $ "❌ BLOCKED: [" ++ code v ++ "] " ++ reason v
            putStrLn $ "   [FORENSIC] " ++ fingerprint cmd
        
        Authorized c sig -> do
            putStrLn "✅ AUTHORIZED"
            putStrLn $ "   [SIG] " ++ sig
            let plan = interpret c
            runPlan plan

-- ==================== 8. CERTIFICATION SUITE ====================

main :: IO ()
main = do
    putStrLn "🛡️  AIRLOCK KERNEL V6.0 (CERTIFIED CORE)"
    putStrLn "========================================"

    let time = Timestamp 16788
    let alice = User "alice" "admin"
    let bob   = User "bob"   "admin"
    let eve   = User "eve"   "hacker"

    -- Scenario 1: Malicious Sabotage (Critical Impact)
    -- Should be BLOCKED by R2 (Sabotage), regardless of Quorum.
    runKernel (KernelEnv time eve (Quorum [eve, bob])) 
              Malicious System Standard (RestartService "Firewall")

    -- Scenario 2: Existential Threat (Single User)
    -- Should be BLOCKED by R3 (Quorum). Alice is alone.
    runKernel (KernelEnv time alice (Quorum [alice])) 
              Neutral System Standard FormatDisk

    -- Scenario 3: Existential Operation (Two-Man Rule)
    -- Should be AUTHORIZED. Alice and Bob both approved.
    runKernel (KernelEnv time alice (Quorum [alice, bob])) 
              Neutral System Standard FormatDisk

    -- Scenario 4: Rollback Data Verification
    -- Shows that 'undo' logic is pure data available before execution.
    runKernel (KernelEnv time alice (Quorum [alice])) 
              Benevolent System Standard (UpdateConfig "MAX_TEMP" "80")

    putStrLn "\n========================================"