| <!-- SPDX-License-Identifier: LicenseRef-Sovereign-Leviathan-SL-AGPL3-001 --> |
| # 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 |
|
|
