Scope
Axiom.jl contains tracked Rust source (crypto/src/lib.rs). Under the current estate language policy, Rust must be paired with Creusot verification.
Deferred work
This issue records the required Rust/Creusot reconciliation only. Do not perform a conversion or broad source correction while the open-PR backlog campaign is in progress.
After the backlog is cleared:
- inventory the Rust component and existing proof/contract coverage;
- add or reconcile Creusot contracts and verification tooling;
- preserve the estate's Zig FFI/API and Idris2 ABI boundaries;
- update CI and documentation with executable verification evidence;
- close or supersede any older Rust-policy issues discovered during implementation.
Discovery context
Found while repairing the existing invisible-character CI PR. The CI repair itself is independent and must not be expanded into a Rust conversion.
Scope
Axiom.jlcontains tracked Rust source (crypto/src/lib.rs). Under the current estate language policy, Rust must be paired with Creusot verification.Deferred work
This issue records the required Rust/Creusot reconciliation only. Do not perform a conversion or broad source correction while the open-PR backlog campaign is in progress.
After the backlog is cleared:
Discovery context
Found while repairing the existing invisible-character CI PR. The CI repair itself is independent and must not be expanded into a Rust conversion.