# Clone Gate (Idris 2) A type-level license gate written in Idris 2. Code can reach the clone payload only by holding a `LicenseProof Valid`, and the only function that can produce one is `decideLicense`. ## How it works | Piece | Role | |---|---| | `LicenseStatus` (`Trial`, `Expired`, `Valid`) | Status carried by a `LicenseToken` with a 16-byte fingerprint | | `LicenseProof : LicenseStatus -> Type` | One constructor, `ValidProof : LicenseProof Valid`. Exported abstractly, so modules outside `CloneGate` cannot construct it | | `decideLicense` | Returns `Just ValidProof` only when the token status is `Valid` and `verifyCrypto` matches the decrypted challenge against the token fingerprint | | `CloneGate : GateState -> Type` | Gate indexed by `Locked`, `Unlocked`, `Spent`; constructors are private | | `unlockGate` | Takes the proof at multiplicity 0 (erased at runtime) and consumes a `Locked` gate linearly (multiplicity 1) | | `cloneGate` | Consumes the `Unlocked` gate linearly and returns the payload with a `Spent` gate | | `discardGate` | Consumes the `Spent` gate linearly, closing the protocol | | `gateFlow` | End-to-end flow: decide, unlock, clone, discard | The challenge cipher in this module (`sbox`, `subBytes`, `addRoundKey`, `aesRound`, `decryptChallenge`) is the small AES-shaped cipher described in the source comments (`sbox b = b + 1`, XOR round key). The gate logic does not depend on which cipher `verifyCrypto` uses, so a full AES implementation can replace it without changing the types. ## Build and test Tested with Idris 2 v0.7.0. ```bash idris2 --install clonegate.ipkg # type-checks under %default total and installs the package cd tests idris2 --build smoke.ipkg && ./build/exec/smoke # Just [0, 0, 0, 0] # Nothing # clone gate smoke test: OK idris2 --check -p clonegate Forge.idr # must FAIL: "Name CloneGate.ValidProof is private." ``` `tests/Forge.idr` is a negative test: it tries to build `ValidProof` from outside the module, and the compiler rejects it. ## License Sovereign Leviathan Covenant (`LicenseRef-Sovereign-Leviathan-SL-AGPL3-001`), the same as the repository it ships in. See the repository `LICENSE`. Copyright (c) 2026 Ahmad Ali Parr