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.

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.