policy: implement Idris2 ABI, Zig FFI, and Hexadeca conformance

[hyperpolymath]

Policy outcome required

Bring IDApTIK's external interface boundary into estate policy:

• ABI contracts and proofs are Idris2.
• FFI implementation/adaptation is Zig.
• Public APIs conform to the canonical Zig unified Hexadeca API.
• Any eligible BEAM native work uses SNIF rather than an application-owned NIF.

This issue is separate from #102, which tracks the priority tests and benchmarks derived from Proven-Tests doctrine.

Verified current state (2026-08-29)

Observation horizon: the complete tracked working tree excluding target/ and the vendored Burble source under vendor/.

• There are zero Idris2 source/package files in IDApTIK.
• There are zero Zig source files in IDApTIK.
• crates/idaptik-ffi implements the exported C ABI directly in Rust and generates include/idaptik.h with cbindgen.
• Its Rust tests provide valuable in-process-vs-ABI parity for the Ghost Lobby run and snapshot, but this is not an Idris proof or Zig adapter conformance test.
• README, ADR-0001, META/STATE/ECOSYSTEM metadata, and Rust module documentation describe Zig and Idris2 as if implemented; those are currently design intent, not repository reality.
• No IDApTIK-owned BEAM NIF loader was found. SNIF conversion is therefore not presently applicable inside this repository. The external Burble relay has its own SNIF/native-dependency ledger in policy: complete Idris2/Zig/SNIF boundary and native-dependency migration burble#207.
• The project assurance profile already records DIRECT_FFI_NO_HEXADECA and UNVERIFIED_RUST; that warning is correct.

Required implementation

Idris2 ABI

• Model every exported handle/function in crates/idaptik-ffi/include/idaptik.h.
• Prove ownership/lifetime transitions: allocated handle is freed once; freed/null handles cannot be treated as live.
• Prove string ownership and idap_string_free pairing.
• Model JSON success/error shape distinction and valid UTF-8/NUL constraints.
• Model deterministic one-tick transition and snapshot format/version invariants.
• Add a package build and CI gate; scan for postulate, believe_me, assert_total, and partial with reviewed exceptions only.

Zig FFI/API adapter

• Add the actual Zig adapter over the core boundary; declarations and tests must correspond one-for-one with the Idris model.
• Add clean/firing conformance fixtures comparing Rust in-process truth, the C export, the Zig adapter, and Idris-derived vectors.
• Generate or validate headers through an authoritative pipeline; fail on drift.
• Keep unsafe pointer ownership in the smallest auditable boundary and fuzz null, invalid UTF-8, malformed JSON, double-free prevention strategy, panic containment, and snapshot round trips.

Hexadeca conformance blocker

A complete hyperpolymath repository-name enumeration (limit 1000) and bounded local searches found conflicting historical names but did not locate a canonical Zig unified Hexadeca API repository/specification. Conformance cannot honestly be implemented or asserted until that authority is located or published.

• Locate/publish the canonical authority, pin its version/digest, then add adapter conformance tests.
• Do not substitute an invented local approximation and call it canonical.

Documentation and metadata gate

• Until implementation lands, change all current-state claims to explicit design intent / gap language.
• Once implemented, derive machine-readable status from passing gates so it cannot claim ffi-language=zig and abi-model-language=idris2 merely from policy intent.

Definition of done

The Idris2 package compiles without unreviewed proof escapes; every external ABI operation is represented; the executable Zig adapter agrees with Rust truth and Idris-derived fixtures including a planted failing fixture; the API conforms to a located and pinned Hexadeca authority; and CI rejects boundary drift.

[linear-code]

HYPER-11

[hyperpolymath]

Rust + Creusot amendment (verified 2026-08-29)

Estate policy clarification: Rust means Rust with Creusot.

Observation horizon: IDApTIK main at 116bae1, all tracked Rust/TOML/workflow/documentation files; vendor/bevy_winit is counted separately.

• 120 first-party Rust files: idaptik-core 72, idaptik-bevy 18, idaptik-tui 16, idaptik-net 13, idaptik-ffi 1.
• 10 additional vendored bevy_winit Rust files are upstream and are not a first-party proof target.
• No Creusot dependency, contract annotation, cargo-creusot command, verifier workflow, or verifier result exists.
• crates/idaptik-ffi exports eight C ABI functions directly from Rust. These remain the concrete Idris2 ABI / Zig FFI migration surface already described above.
• No Creusot executable is currently installed in the canonical developer tools area, so no Creusot proof has been run or claimed.

Additional acceptance conditions:

• Classify first-party Rust modules by safety criticality and write explicit Creusot obligations for the state transition core, snapshot round trips, command folding, pointer ownership/lifetimes, JSON error shape, panic containment, and deterministic tick behaviour.
• Install and pin the authoritative Creusot toolchain under developer/tools and in CI.
• Run Creusot on the selected first-party targets, retain verifier evidence, and add a planted contract violation proving the gate can fail.
• Record unmodelled Rust modules as proof debt; compilation, tests, or annotations alone must not be reported as proof.
• Exclude vendored code explicitly by path and record the upstream trust boundary rather than silently counting it as verified.