Idris2 as source-of-truth for the cartridge interface. Today the cartridge ABI is dual-encoded: the Idris2 contract (e.g. SafeK9iser.canTransition/exposureSatisfied) and the Zig FFI mirror are written by hand and only cross-checked by tests. The estate ideal (interface-safety policy) is the Zig interface generated from / proven against the Idris2 ABI. Affects ssg-mcp, k9iser-mcp (boj-server#73), and every future cartridge. Pre-existing pattern, not introduced by the pilot.
Idris2 as source-of-truth for the cartridge interface. Today the cartridge ABI is dual-encoded: the Idris2 contract (e.g.
SafeK9iser.canTransition/exposureSatisfied) and the Zig FFI mirror are written by hand and only cross-checked by tests. The estate ideal (interface-safety policy) is the Zig interface generated from / proven against the Idris2 ABI. Affects ssg-mcp, k9iser-mcp (boj-server#73), and every future cartridge. Pre-existing pattern, not introduced by the pilot.