policy: enforce Rust = Rust + Creusot without proof theatre

[hyperpolymath]

Policy decision

Estate policy is explicit: any first-party Rust means Rust with Creusot.

This extends #124 and complements #92. It must not turn the existence of annotations or a workflow into a proof claim.

Verified baseline (2026-08-29)

Observation horizon: PR #691 head 5a8cf26 and every tracked Rust, TOML, workflow, and documentation file in standards.

• 41 Rust files are tracked: 20 in RSR satellites, 17 in RSR examples, and 4 in estate tools.
• No Creusot dependency, contract annotation, cargo-creusot command, verifier workflow, or retained verifier result exists.
• The central language-policy gate does not enforce the Rust-plus-Creusot rule.
• why3 exists on the development machine; Creusot itself is not installed in the canonical developer/tools area. No Creusot proof was run or claimed.

Required central policy

• Define first-party, vendored, generated, example, and executable Rust scopes precisely.
• Require each first-party Rust repository to enumerate Creusot targets, obligations, exclusions, and proof debt.
• Pin Creusot and its Rust toolchain under developer/tools and in reusable CI.
• Require verifier execution and retain machine-readable results.
• Require a planted failing contract as a positive control.
• Fail claims that label configuration, annotations, compilation, tests, or unexecuted proof scaffolding as proved.
• Add template guidance for unsafe boundaries and for the estate Idris2 ABI / Zig FFI / unified Hexadeca API policy.
• Add SNIF classification guidance: pure eligible BEAM compute goes through SNIF; host I/O is isolated out of process rather than falsely described as SNIF-compatible.

Rollout targets from this audit

• policy: implement Idris2 ABI, Zig FFI, and Hexadeca conformance metadatastician/IDApTIK#103: 120 first-party Rust files, including eight direct Rust C ABI exports.
• policy: complete Idris2/Zig/SNIF boundary and native-dependency migration metadatastician/burble#207: 57 Rust files.
• hyperpolymath/oikos: 30 Rust files.
• proven-tests-and-benches: zero tracked Rust files, therefore not applicable.

Definition of done

The authoritative policy and reusable gate are merged; planted controls prove gate reach; target repositories report verified coverage and explicit debt; and no scaffold-only result is reported as a proof.