feat: add deterministic property-test generation v1

AGENTS.md

@@ -86,6 +86,9 @@ proof scaffolding, not a wired native-runtime claim.
   mainnet authority.
 - `src/repair.rs`: bounded read-only Diagnostic Repair v1 discovery and
   instantiation plus the independently replayed Patch-v3 identity-rebase gate.
+- `src/properties.rs`, `tests/property_tests_v1.rs`: read-only deterministic
+  Property-Test Generation v1 over verified single-file sources; no symbolic
+  execution, shrinking, test running, or target execution.
 - `src/review.rs`: bounded read-only Semantic Review v1 over complete Impact-v1
   or shared identity-rebase evidence.
 - `src/target_evidence.rs`: bounded read-only Graph, capability, native-C11,

CHANGELOG.md

@@ -1,5 +1,19 @@
 # Changelog
 
+- Added the locally evidenced Property-Test Generation v1 tranche. The new
+  read-only `semaprax properties <file>` command and `properties` library API
+  generate deterministic boundary-lattice plus seeded candidates from admitted
+  monomorphic scalar signatures, filter them through authored `requires`
+  clauses, evaluate bodies and interprocedural admitted callees with checked
+  arithmetic, lazy booleans, lexical bindings, and call-depth/step budgets,
+  and report the first exact `ensures` counterexample (clause index, canonical
+  text, full argument tuple, observed result) in canonical compact
+  `semaprax.property-tests.v1` JSON with fixed key order, domain-separated
+  source digest binding, closed deferral/runtime/truncation reason sets,
+  byte-budget prefix truncation, and fixed nonclaims. Unsupported shapes defer
+  fail-closed with stable reasons instead of approximating. No target is
+  executed, no symbolic or SMT discharge is claimed, and completion totals
+  remain 39 Partial/17 Missing.
 - Added the locally evidenced Public Project Native Publication v1 tranche.
   `semaprax build --target native` over a `semaprax.toml` project now publishes
   the linked entry closure as one create-new executable through the unchanged

docs/ARCHITECTURE.md

@@ -46,6 +46,8 @@ The public verifier compatibility facade and HIR analysis boundary share one sou
 
 The initial contract lane is progressive: contracts are type-checked at compile time, required to be effect-free, and guarded in generated native and Wasm code. Static proof is a later lane, and its absence is reported honestly in the project status.
 
+The read-only `semaprax properties` command adds the first bounded property-test generation tranche over verified sources: deterministic boundary-lattice and seeded candidates from admitted scalar signatures, `requires` domain filtering, checked-semantics body/callee evaluation under one step budget, and exact `ensures` counterexample reporting in canonical digest-bound JSON (`semaprax.property-tests.v1`). It performs no symbolic execution, shrinking, or target execution; see `docs/PROPERTY-TESTS-V1.md`.
+
 Generated arithmetic is checked for overflow, zero division, and the signed division edge case. Failures have stable process exit codes and explicit diagnostics rather than C undefined behavior.
 
 The locally evidenced floating-point tranche adds IEEE-754 `f32`/`f64` Copy

docs/COMPLETION-MATRIX.md

@@ -544,7 +544,7 @@ exactly 39 Partial and 17 Missing.
 | Restricted `unsafe` and raw memory | Missing | — | Unsafe boundaries are explicit graph nodes with capability, audit summary, lint, and platform conformance coverage |
 | Checked/wrapping/saturating arithmetic | Partial | Checked `i64` arithmetic in the C/Clang lane returns exact `semaprax.arithmetic.v1` statuses without internal process termination | Full numeric family, explicit alternative modes, SIMD behavior, and backend equivalence verified |
 | Effects and capabilities | Partial | Declared function effects, module permits, and call-edge propagation | Inference, parameterized capabilities, no ambient authority, handlers, dependency summaries, and platform manifests verified |
-| Contracts and progressive verification | Partial | Contract type checking and runtime guards | Static discharge, bounded symbolic/SMT checks, counterexamples, invariants/state machines, property tests, and proof obligations verified |
+| Contracts and progressive verification | Partial | Contract type checking and runtime guards. The additive read-only Property-Test Generation v1 tranche (`semaprax.properties`) now generates deterministic boundary-lattice plus seeded candidates from admitted scalar signatures, filters them through `requires`, evaluates bodies and interprocedural callees with checked semantics under one step budget, and reports exact `ensures` counterexamples in canonical digest-bound `semaprax.property-tests.v1` JSON; it performs no symbolic execution, static discharge, shrinking, or target execution and changes no status | Static discharge, bounded symbolic/SMT checks, counterexamples, invariants/state machines, property tests, and proof obligations verified |
 | Structured concurrency | Missing | — | Scoped tasks, cancellation, cleanup, `Sendable`/`Shareable`, deterministic scheduler, actors/reducers, and synchronization verified |
 | Typed hygienic generation | Missing | — | Deterministic sandboxed generation is graph-visible and cannot perform unrestricted textual rewriting |
 

docs/PROPERTY-TESTS-V1.md

@@ -0,0 +1,92 @@
+# Property-Test Generation v1
+
+`semaprax properties <file.spx>` is a deterministic, read-only analysis that
+generates bounded test inputs from admitted function signatures and evaluates
+the authored `requires`/`ensures` contracts against them. It is the first
+executable tranche of the roadmap item "Property tests generated from types
+and contracts". It runs no target, executes no generated backend, and changes
+no source.
+
+## Command
+
+```sh
+semaprax properties <file> [--max-cases N] [--max-functions N] [--max-bytes N] [--seed N]
+```
+
+- `--max-cases` (default 64, maximum 4096): candidate input tuples generated
+  per analyzed function.
+- `--max-functions` (default 64, maximum 1024): functions processed in
+  authored order before `function_budget` truncation.
+- `--max-bytes` (default 64 KiB, bounds follow the Agent Context byte limits):
+  whole-report output budget; overflow selects the longest fitting prefix and
+  reports `byte_budget`.
+- `--seed` (default 11400714819323198485 = `0x9e3779b97f4a7c15`): decimal seed
+  for the deterministic per-parameter sampling streams.
+
+## Admission and evaluation model
+
+A function is admitted only when it is monomorphic, declares no effects, has
+only by-value direct `i64`/`bool` parameters, and returns direct `i64`/`bool`.
+Every other function is reported as `deferred` with one closed reason:
+`generic_function`, `declared_effects`, `unsupported_parameter_mode`,
+`unsupported_parameter_type`, `unsupported_result_type`, or the first
+unsupported construct found by the pre-case scan (`float_literal`,
+`record_construction`, `variant_construction`, `record_update`,
+`record_projection`, `match_expression`, `try_expression`, `generic_call`,
+`unresolved_call`, `unresolved_variable`, `unsupported_callee`,
+`ill_typed_expression`) or `evaluation_step_budget_exhausted`.
+
+For each admitted function the generator produces deterministic candidates:
+the first cases use a fixed boundary lattice per parameter (`0`, `±1`, `±2`,
+`±3`, `i64::MIN`/`MAX`/`MIN+1`/`MAX-1` for `i64`; `true`, `false` for `bool`),
+and later cases draw full-range samples from independent xorshift64* streams
+seeded through splitmix64 mixing of `(base seed, authored function index,
+parameter position)`.
+
+Each candidate tuple is classified exactly once:
+
+1. `requires` clauses are evaluated left-to-right under the parameter
+   bindings. The first `false` clause *filters* the case — the input lies
+   outside the declared domain and is not a counterexample.
+2. The body is evaluated with checked arithmetic, short-circuit booleans,
+   lexical `let` bindings, `if/else`, and interprocedural calls to other
+   admitted local functions. Callee preconditions are re-checked at each call;
+   violations surface as the `callee_requires_violated` runtime reason. A
+   callee's postconditions are not evaluated. Runtime reasons are closed:
+   `arithmetic_overflow`, `division_by_zero`, `remainder_by_zero`,
+   `negation_overflow`, `call_depth_exceeded`, `callee_requires_violated`.
+3. With the result bound, every `ensures` clause is evaluated. The first
+   `false` clause is recorded as the counterexample (clause index, canonical
+   clause text, full argument tuple, observed result) and stops further cases
+   for that function. All-passing tuples count as discharged.
+
+Evaluation shares one invocation-wide step budget; exhaustion stops the run
+and reports `step_budget` truncation for unprocessed functions.
+
+## Output
+
+The report is canonical compact JSON with schema
+`semaprax.property-tests.v1` and fixed key order: `schema`, `source`
+(`path`, `revision`, `sha256` over the domain-separated exact source bytes),
+`seed`, `limits`, `budget` (`used_functions`, `used_cases`, `used_nodes`),
+`truncation` (`truncated`, closed `reasons`: `function_budget`, `step_budget`,
+`byte_budget`, plus `omitted_functions`), `summary`, `functions`, and
+`nonclaims`. Analyzed entries carry `stable_id`, `name`, `outcome`,
+`signature`, clause listings, per-outcome counters, sorted `runtime_reasons`,
+and either `counterexample` or `null`. Integer values are serialized as
+decimal strings to keep the report JSON-number safe.
+
+## Nonclaims
+
+Property-Test Generation v1 performs no symbolic execution or SMT solving,
+discharges no contract statically, minimizes no counterexamples, makes no
+statistical coverage guarantee, is not a test runner, and executes no target.
+Runtime failures are defined-language observations, not safety claims. The
+tranche does not move any completion-matrix status.
+
+## Evidence
+
+```sh
+cargo test --locked -p semaprax --lib properties::
+cargo test --locked -p semaprax --test property_tests_v1 -- --test-threads=1
+```

docs/ROADMAP.md

@@ -250,7 +250,13 @@ gates below are not.
 - Diagnostic repairs beyond the implemented bounded `SPX-S103`
   `assign-function-id` tranche: typed holes, other diagnostics/declaration
   kinds, ranking, composition, automatic application, and multi-file repair.
-- Property tests generated from types and contracts.
+- Property tests generated from types and contracts: the bounded read-only
+  [Property-Test Generation v1](PROPERTY-TESTS-V1.md) tranche now generates
+  deterministic lattice-plus-seeded candidates from admitted scalar
+  signatures, filters them through `requires`, evaluates bodies and interprocedural
+  callees with checked semantics, and reports exact `ensures` counterexamples
+  (`semaprax properties`). General type-directed generation, shrinking,
+  statistical coverage, and test-runner integration remain open.
 - A persistent graph daemon and JSON-RPC agent transport.
 - Complete ownership/lifetime/region analysis across control flow.
 

src/lib.rs

@@ -35,6 +35,7 @@ pub mod patch_evidence;
 #[allow(dead_code, reason = "path-included by the unpublished native builder")]
 mod private_capacity_contract;
 pub mod project;
+pub mod properties;
 pub mod quality_route;
 pub mod repair;
 pub mod review;

src/main.rs

@@ -4,7 +4,7 @@ use std::process::{Command, ExitCode};
 use semaprax::diagnostic::{Diagnostic, Severity};
 use semaprax::{
     agent_economics, codegen, format, graph, impact, parse, patch, patch_evidence, project,
-    quality_route, repair, review, semantic_workspace, semantic_workspace_change,
+    properties, quality_route, repair, review, semantic_workspace, semantic_workspace_change,
     semantic_workspace_operations, semantic_workspace_structural_change, target_evidence, verify,
     wasm, workspace, workspace_analysis, workspace_graph, workspace_patch_evidence,
 };
@@ -558,6 +558,14 @@ fn run(args: Vec<String>) -> Result<(), u8> {
             println!("{report}");
             Ok(())
         }
+        "properties" => {
+            let path = required_path(&args, 1)?;
+            let options = property_options(&args)?;
+            let report =
+                properties::generate(&path, &options).map_err(|errors| report(&errors, false))?;
+            println!("{report}");
+            Ok(())
+        }
         "target-evidence" => {
             if args.len() != 3 {
                 eprintln!("target-evidence requires exactly <file> <patch.spatch>");
@@ -872,6 +880,80 @@ fn impact_number(option: &str, value: &str) -> Result<usize, u8> {
     })
 }
 
+fn property_options(args: &[String]) -> Result<properties::PropertyTestOptions, u8> {
+    let mut max_cases = properties::PropertyTestOptions::default().max_cases;
+    let mut max_functions = properties::PropertyTestOptions::default().max_functions;
+    let mut max_bytes = properties::PropertyTestOptions::default().max_bytes;
+    let mut seed = properties::PropertyTestOptions::default().seed;
+    let mut seen = std::collections::BTreeSet::new();
+    let mut index = 2usize;
+    while index < args.len() {
+        let option = args[index].as_str();
+        if !matches!(
+            option,
+            "--max-cases" | "--max-functions" | "--max-bytes" | "--seed"
+        ) {
+            eprintln!("unknown properties option `{option}`");
+            return Err(2);
+        }
+        if !seen.insert(option.to_owned()) {
+            eprintln!("duplicate properties option `{option}`");
+            return Err(2);
+        }
+        let value = args.get(index + 1).ok_or_else(|| {
+            eprintln!("properties option `{option}` requires a value");
+            2
+        })?;
+        match option {
+            "--seed" => seed = property_seed(option, value)?,
+            _ => {
+                let number = property_number(option, value)?;
+                match option {
+                    "--max-cases" => max_cases = number,
+                    "--max-functions" => max_functions = number,
+                    "--max-bytes" => max_bytes = number,
+                    _ => unreachable!("closed properties option table"),
+                }
+            }
+        }
+        index += 2;
+    }
+    properties::PropertyTestOptions::new(max_cases, max_functions, max_bytes, seed).map_err(
+        |error| {
+            eprintln!("{error}");
+            2
+        },
+    )
+}
+
+fn property_number(option: &str, value: &str) -> Result<usize, u8> {
+    if value.is_empty()
+        || !value.bytes().all(|byte| byte.is_ascii_digit())
+        || (value.len() > 1 && value.starts_with('0'))
+    {
+        eprintln!("properties option `{option}` requires a canonical nonnegative integer");
+        return Err(2);
+    }
+    value.parse::<usize>().map_err(|_| {
+        eprintln!("properties option `{option}` requires a canonical nonnegative integer");
+        2
+    })
+}
+
+fn property_seed(option: &str, value: &str) -> Result<u64, u8> {
+    if value.is_empty()
+        || !value.bytes().all(|byte| byte.is_ascii_digit())
+        || (value.len() > 1 && value.starts_with('0'))
+    {
+        eprintln!("properties option `{option}` requires a canonical nonnegative integer");
+        return Err(2);
+    }
+    value.parse::<u64>().map_err(|_| {
+        eprintln!("properties option `{option}` requires a canonical nonnegative integer");
+        2
+    })
+}
+
 enum ParsedContextOptions {
     V1(graph::AgentContextOptions),
     V2(graph::AgentContextV2Options),
@@ -1305,6 +1387,7 @@ fn print_help() {
            semaprax verify-workspace-patch-evidence <root> <patch.wspatch> <evidence.json>\n\
            semaprax workspace-apply-with-evidence <root> <patch.wspatch> <evidence.json>\n\
            semaprax impact <file> <patch.spatch> [--depth N] [--max-bytes N] [--max-nodes N]\n\
+           semaprax properties <file> [--max-cases N] [--max-functions N] [--max-bytes N] [--seed N]\n\
            semaprax review <file> <patch.spatch>\n\
            semaprax target-evidence <file> <patch.spatch>\n\
            semaprax patch-evidence <file> <patch.spatch>\n\