Run generated properties through the compiled backend

[onatozmenn]

What this changes

deed test --compiled stopped after written test blocks, while the interpreted command also ran seven properties generated from contracts. The corpus therefore reported 111 compiled passes against 138 interpreted results.

The compiled path now runs those generated properties too. The corpus reports 118 compiled passes, and the existing six backend skip records remain named separately.

Why this way

The generator, precondition filtering and contract evaluation stay in deed-interp; there is still one implementation of ensures. Each accepted generated value is encoded into the compiled module's own memory from its MIR layout, the export is called, and the answer is decoded and compared structurally with the interpreter's answer.

This covers numbers, booleans, unit, text, lists, records, choices and Result, including nested values. The codegen oracle exposes one prepared-call boundary rather than duplicating the module's layout or allocator in the CLI.

What it still does not do

This does not add postcondition checks to ordinary compiled calls. It runs contract-generated tests through the compiled backend while keeping the interpreter as the contract oracle. It also does not make the backend lower the six existing skip records.

Checks

• cargo fmt --all -- --check
• cargo clippy --workspace --all-targets -- -D warnings
• cargo nextest run --workspace --profile ci --no-fail-fast (2486 passed)
• cargo test --doc --workspace
• cargo run -q -p deed-lang -- test --compiled examples (118 passed, 6 named skips)
• Property codec and compiled runner mutations: 54 tested, 49 caught, 5 unviable
• Integer shrinker mutations: 11 tested, 11 caught
• Prepared-call mutations: 12 tested, 6 caught, 6 unviable
• Property callback mutations: 18 tested, 15 caught, 3 unviable
• All four mutation sets: 0 missed, 0 timeout
• Tests cover wrong contracts, scalar and boxed runtime disagreements, every generated input shape, corrupt memory lengths, property-only files, written-only files, exact rejection counts, and both sides of assert refuses classification.

AI assistance: GitHub Copilot implemented and verified this change.