Run generated properties through the compiled backend

CHANGELOG.md

@@ -40,12 +40,26 @@ release notes.
 
 ### Diagnostics
 
+- `deed test --compiled` runs the properties contracts generate, rather than
+  stopping after written test blocks. The corpus now reports 118 compiled
+  passes instead of 111: the same seven generated properties the interpreter
+  runs, alongside the blocks the backend can compile. The remaining difference
+  is written code the backend names in its six existing skip records.
+
+  Generated inputs use the same generator and precondition filtering as the
+  interpreter. Each accepted value is written into the compiled module's own
+  memory using the MIR layout, the export is called, and its answer is decoded
+  from that memory and compared structurally with the reference answer. The
+  interpreter remains the one implementation of contract evaluation, so this
+  does not create a second `ensures` evaluator that could drift from the first.
+  A wrong contract still fails the property, and a backend answer that differs
+  from the interpreter fails it independently.
+
 - `deed test --compiled` says what it did not compile. It ran a hundred and
-  eleven of the corpus's blocks where the interpreter ran a hundred and
-  thirty-eight, and reported `111 passed, 0 failed`, which is what a complete
-  run looks like. A file the backend refused outright said `no tests found in
-  the compiled backend` and exited zero, which is what a file with no tests in
-  it says.
+  eleven results where the interpreter reported a hundred and thirty-eight,
+  and printed `111 passed, 0 failed`, which is what a complete run looks like.
+  A file the backend refused outright said `no tests found in the compiled
+  backend` and exited zero, which is what a file with no tests in it says.
 
   Skipping is right — the backend compiles a subset of the language on purpose
   — and staying quiet about it was not. Every block that is dropped is now

crates/deed-cli/src/args.rs

@@ -42,8 +42,8 @@ Options:
                           than all of it.
   --check                 With `fmt` or `fix`, change nothing and report what
                           would have changed.
-  --compiled              With `test`, run test blocks through the compiled
-                          WebAssembly backend instead of the interpreter.
+    --compiled              With `test`, run test blocks and generated properties
+                                                    through the compiled WebAssembly backend.
   --component             With `build`, write a core module, the `.wit` world
                           its exports describe, and a component binary, instead
                           of a standalone program. The component is written
@@ -72,9 +72,9 @@ the directory and the module path, so it is lowercase letters, digits and `_`.
 It writes no manifest: a manifest here says where code outside your tree lives,
 and a new project has none.
 `deed test` refuses to run anything that does not check.
-`deed test --compiled` runs the same test blocks through the compiled backend.
-  Blocks the backend cannot compile are skipped, and the count of the ones that
-  ran has to match what the interpreter ran.
+`deed test --compiled` runs test blocks and the properties contracts generate
+through the compiled backend. Blocks the backend cannot compile are skipped and
+named, so the summary says both how much ran and what did not.
 `deed run` calls `main`, handing it the one `System` capability there is.
 Everything after `--` goes to the program, which reads it with `Io.args`.
 Standard input is read when, and only when, `main`'s row says `Io.line`. A