// ============================================================================
// SECRET ROTATION — a revoked credential never logs in again
// ============================================================================
//
// In 2016, attackers found Uber's AWS keys sitting in a private GitHub
// repo. The keys were long-lived — never rotated — and unlocked data on
// 57 million riders and drivers. The pattern repeats everywhere: a
// credential leaks, someone "disables" it in a dashboard, and months
// later a recovery script or a confused admin re-enables it.
//
// Here the credential lifecycle is a machine where `revoked` and
// `retired` are TERMINAL — `soma verify` proves no handler, script, or
// 3 a.m. admin can resurrect a dead key. Authentication consults the
// machine, so a revoked key fails closed. Key age sits behind a memory
// invariant: a credential older than the 90-day rotation policy cannot
// even be recorded, which makes "we forgot to rotate" a write error.
// ============================================================================

cell SecretVault {
    face {
        signal mint(key: String) -> Map
        signal begin_rotation(key: String) -> Map
        signal retire(key: String) -> Map
        signal revoke(key: String) -> Map
        signal authenticate(key: String) -> Map
        signal record_age(key: String, days: Int) -> Map
    }

    memory {
        age_days: Map<String, Int> [persistent, consistent]
        invariant age_days >= 0 && age_days <= 90
    }

    // `revoked` (compromise) and `retired` (rotated out) have no exit.
    // An active key may rotate or be revoked; nothing comes back.
    state credential {
        initial: minted
        minted -> active
        active -> rotating
        rotating -> retired
        active -> revoked
        rotating -> revoked
    }

    on mint(key: String) {
        let r = try { transition(key, "active") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        age_days.set(key, 0)
        return map("ok", true, "state", "active")
    }

    on begin_rotation(key: String) {
        let r = try { transition(key, "rotating") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", "rotating")
    }

    on retire(key: String) {
        let r = try { transition(key, "retired") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", "retired")
    }

    on revoke(key: String) {
        let r = try { transition(key, "revoked") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", "revoked")
    }

    // fails closed: only `active` and `rotating` (overlap window) serve
    on authenticate(key: String) {
        let s = get_status(key)
        if s == "active" || s == "rotating" {
            return map("ok", true, "state", s)
        }
        return map("ok", false, "reason", "credential is {s}")
    }

    on record_age(key: String, days: Int) {
        let w = try { age_days.set(key, days) }
        if w.error != () {
            return map("ok", false, "reason", "rotation policy: {w.error}")
        }
        return map("ok", true, "age", days)
    }
}

cell test VaultTests {
    rules {
        // a leaked key is revoked...
        assert mint("AKIA-uber-prod").ok == true
        assert authenticate("AKIA-uber-prod").ok == true
        assert revoke("AKIA-uber-prod").ok == true
        assert authenticate("AKIA-uber-prod").ok == false

        // ...and THE RESURRECTION does not exist as an edge
        assert_fails transition("AKIA-uber-prod", "active")
        assert_fails transition("AKIA-uber-prod", "rotating")
        assert_fails transition("AKIA-uber-prod", "minted")

        // healthy rotation: overlap window authenticates, retired never
        assert mint("AKIA-v2").ok == true
        assert begin_rotation("AKIA-v2").ok == true
        assert authenticate("AKIA-v2").ok == true
        assert retire("AKIA-v2").ok == true
        assert authenticate("AKIA-v2").ok == false
        assert_fails transition("AKIA-v2", "active")

        // the 90-day policy is a wall, not a wiki page
        assert record_age("AKIA-v3", 89).ok == true
        assert_fails age_days.set("AKIA-v3", 91)
        assert_fails age_days.set("AKIA-v3", -1)
    }
}