diff --git a/AGENTS.md b/AGENTS.md index dc4c4dd..6ee1d28 100644 --- a/AGENTS.md +++ b/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, diff --git a/CHANGELOG.md b/CHANGELOG.md index 4fd461f..4f1e365 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,19 @@ # Changelog +- Added the locally evidenced Property-Test Generation v1 tranche. The new + read-only `semaprax properties ` 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 diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 599843f..12d453c 100644 --- a/docs/ARCHITECTURE.md +++ b/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 diff --git a/docs/COMPLETION-MATRIX.md b/docs/COMPLETION-MATRIX.md index 629b0ef..35d38e0 100644 --- a/docs/COMPLETION-MATRIX.md +++ b/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 | diff --git a/docs/PROPERTY-TESTS-V1.md b/docs/PROPERTY-TESTS-V1.md new file mode 100644 index 0000000..4165fab --- /dev/null +++ b/docs/PROPERTY-TESTS-V1.md @@ -0,0 +1,92 @@ +# Property-Test Generation v1 + +`semaprax properties ` 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 [--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 +``` diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index be69793..6127aa0 100644 --- a/docs/ROADMAP.md +++ b/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. diff --git a/src/lib.rs b/src/lib.rs index d68b08e..a73ed44 100644 --- a/src/lib.rs +++ b/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; diff --git a/src/main.rs b/src/main.rs index b1a4675..0e5adea 100644 --- a/src/main.rs +++ b/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) -> 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 "); @@ -872,6 +880,80 @@ fn impact_number(option: &str, value: &str) -> Result { }) } +fn property_options(args: &[String]) -> Result { + 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 { + 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::().map_err(|_| { + eprintln!("properties option `{option}` requires a canonical nonnegative integer"); + 2 + }) +} + +fn property_seed(option: &str, value: &str) -> Result { + 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::().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 \n\ semaprax workspace-apply-with-evidence \n\ semaprax impact [--depth N] [--max-bytes N] [--max-nodes N]\n\ + semaprax properties [--max-cases N] [--max-functions N] [--max-bytes N] [--seed N]\n\ semaprax review \n\ semaprax target-evidence \n\ semaprax patch-evidence \n\ diff --git a/src/properties.rs b/src/properties.rs new file mode 100644 index 0000000..e930f54 --- /dev/null +++ b/src/properties.rs @@ -0,0 +1,1152 @@ +//! Deterministic, read-only Property-Test Generation v1. + +use std::collections::{BTreeMap, BTreeSet}; +use std::path::Path; + +use sha2::{Digest as _, Sha256}; + +use crate::ast::{ + BinaryOp, Expr, ExprKind, Function, ParamMode, Program, Statement, Type, UnaryOp, +}; +use crate::bounded_output::{with_limit, BudgetedJoin as _}; +use crate::diagnostic::{quote_json, Diagnostic}; +use crate::{format, graph, parse, patch, verify}; + +macro_rules! bformat { + ($($argument:tt)*) => { + crate::bounded_output::budgeted_format(format_args!($($argument)*)) + }; +} + +pub const SCHEMA: &str = "semaprax.property-tests.v1"; + +const DEFAULT_MAX_CASES: usize = 64; +const DEFAULT_MAX_FUNCTIONS: usize = 64; +const DEFAULT_MAX_BYTES: usize = 64 * 1024; +pub const DEFAULT_SEED: u64 = 0x9e37_79b9_7f4a_7c15; + +pub const MAX_CASES_LIMIT: usize = 4096; +pub const MAX_FUNCTIONS_LIMIT: usize = 1024; +const MAX_TOTAL_STEPS: usize = 1_000_000; +const MAX_CALL_DEPTH: usize = 16; + +const REASON_GENERIC_FUNCTION: &str = "generic_function"; +const REASON_DECLARED_EFFECTS: &str = "declared_effects"; +const REASON_UNSUPPORTED_PARAMETER_MODE: &str = "unsupported_parameter_mode"; +const REASON_UNSUPPORTED_PARAMETER_TYPE: &str = "unsupported_parameter_type"; +const REASON_UNSUPPORTED_RESULT_TYPE: &str = "unsupported_result_type"; +const REASON_EVALUATION_STEP_BUDGET_EXHAUSTED: &str = "evaluation_step_budget_exhausted"; +const REASON_FLOAT_LITERAL: &str = "float_literal"; +const REASON_RECORD_CONSTRUCTION: &str = "record_construction"; +const REASON_VARIANT_CONSTRUCTION: &str = "variant_construction"; +const REASON_RECORD_UPDATE: &str = "record_update"; +const REASON_RECORD_PROJECTION: &str = "record_projection"; +const REASON_MATCH_EXPRESSION: &str = "match_expression"; +const REASON_TRY_EXPRESSION: &str = "try_expression"; +const REASON_GENERIC_CALL: &str = "generic_call"; +const REASON_UNRESOLVED_CALL: &str = "unresolved_call"; +const REASON_UNRESOLVED_VARIABLE: &str = "unresolved_variable"; +const REASON_UNSUPPORTED_CALLEE: &str = "unsupported_callee"; +const REASON_ILL_TYPED_EXPRESSION: &str = "ill_typed_expression"; + +const RUNTIME_ARITHMETIC_OVERFLOW: &str = "arithmetic_overflow"; +const RUNTIME_DIVISION_BY_ZERO: &str = "division_by_zero"; +const RUNTIME_REMAINDER_BY_ZERO: &str = "remainder_by_zero"; +const RUNTIME_NEGATION_OVERFLOW: &str = "negation_overflow"; +const RUNTIME_CALL_DEPTH_EXCEEDED: &str = "call_depth_exceeded"; +const RUNTIME_CALLEE_REQUIRES_VIOLATED: &str = "callee_requires_violated"; + +const TRUNCATION_BYTE_BUDGET: &str = "byte_budget"; +const TRUNCATION_FUNCTION_BUDGET: &str = "function_budget"; +const TRUNCATION_STEP_BUDGET: &str = "step_budget"; + +const NONCLAIMS_JSON: &str = "\"no_symbolic_execution_or_smt\",\ +\"no_static_contract_discharge\",\ +\"no_counterexample_minimization\",\ +\"no_statistical_coverage_guarantee\",\ +\"not_a_test_runner\",\ +\"no_target_execution\""; + +const I64_LATTICE: [i64; 11] = [ + 0, + 1, + -1, + 2, + -2, + 3, + -3, + i64::MIN, + i64::MAX, + i64::MIN + 1, + i64::MAX - 1, +]; + +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +pub struct PropertyTestOptions { + pub max_cases: usize, + pub max_functions: usize, + pub max_bytes: usize, + pub seed: u64, +} + +impl PropertyTestOptions { + pub fn new( + max_cases: usize, + max_functions: usize, + max_bytes: usize, + seed: u64, + ) -> Result { + if max_cases == 0 || max_cases > MAX_CASES_LIMIT { + return Err(option_error(format!( + "property test max_cases must be between 1 and {MAX_CASES_LIMIT}" + ))); + } + if max_functions == 0 || max_functions > MAX_FUNCTIONS_LIMIT { + return Err(option_error(format!( + "property test max_functions must be between 1 and {MAX_FUNCTIONS_LIMIT}" + ))); + } + if !(graph::MIN_AGENT_CONTEXT_BYTES..=graph::MAX_AGENT_CONTEXT_BYTES).contains(&max_bytes) { + return Err(option_error(format!( + "property test max_bytes must be between {} and {}", + graph::MIN_AGENT_CONTEXT_BYTES, + graph::MAX_AGENT_CONTEXT_BYTES + ))); + } + Ok(Self { + max_cases, + max_functions, + max_bytes, + seed, + }) + } +} + +impl Default for PropertyTestOptions { + fn default() -> Self { + Self { + max_cases: DEFAULT_MAX_CASES, + max_functions: DEFAULT_MAX_FUNCTIONS, + max_bytes: DEFAULT_MAX_BYTES, + seed: DEFAULT_SEED, + } + } +} + +fn option_error(message: String) -> Diagnostic { + Diagnostic::io("SPX-P101", message) +} + +pub fn generate( + source_path: &Path, + options: &PropertyTestOptions, +) -> Result> { + generate_with_hook(source_path, options, &mut |_, _| Ok(())) +} + +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +enum HookPhase { + AfterParse, + BeforeFinalCheck, +} + +fn generate_with_hook( + source_path: &Path, + options: &PropertyTestOptions, + hook: &mut dyn FnMut(HookPhase, &Path) -> std::io::Result<()>, +) -> Result> { + let canonical_source_path = patch::canonical_source_path(source_path)?; + let snapshot = patch::read_source_snapshot(&canonical_source_path)?; + let program = parse(snapshot.source(), source_path).map_err(|error| vec![error])?; + let diagnostics = verify::verify(&program); + if diagnostics.iter().any(|item| item.severity.is_error()) { + return Err(diagnostics); + } + hook(HookPhase::AfterParse, &canonical_source_path).map_err(|error| { + vec![Diagnostic::io( + "SPX-I207", + format!("property test hook failed: {error}"), + )] + })?; + let revision = graph::revision(&program); + let report = build_report(snapshot.source(), source_path, &program, options); + hook(HookPhase::BeforeFinalCheck, &canonical_source_path).map_err(|error| { + vec![Diagnostic::io( + "SPX-I207", + format!("property test final-check hook failed: {error}"), + )] + })?; + patch::validate_source_unchanged(&canonical_source_path, source_path, &snapshot, &revision)?; + Ok(report) +} + +#[derive(Default)] +struct Summary { + functions_total: usize, + functions_analyzed: usize, + functions_deferred: usize, + functions_with_counterexamples: usize, + cases_attempted: usize, + filtered_cases: usize, + discharged_cases: usize, + runtime_failure_cases: usize, +} + +fn build_report( + source: &str, + source_path: &Path, + program: &Program, + options: &PropertyTestOptions, +) -> String { + let mut analyzer = Analyzer::new(program); + let mut entries: Vec = Vec::new(); + let mut summary = Summary::default(); + let mut used_cases = 0usize; + let mut step_stop = false; + + for (index, function) in program.functions.iter().enumerate() { + if step_stop || entries.len() >= options.max_functions { + break; + } + match analyzer.analyze_function(index, function, options) { + FunctionOutcome::Deferred(reason) => { + summary.functions_deferred += 1; + entries.push(deferred_entry_json(function, reason)); + } + FunctionOutcome::Analyzed(entry) => { + summary.functions_analyzed += 1; + summary.functions_with_counterexamples += usize::from(entry.counterexample); + summary.cases_attempted += entry.cases_attempted; + summary.filtered_cases += entry.filtered_cases; + summary.discharged_cases += entry.discharged_cases; + summary.runtime_failure_cases += entry.runtime_failure_cases; + used_cases += entry.cases_attempted; + entries.push(entry.json); + } + FunctionOutcome::Exhausted => { + step_stop = true; + } + } + } + + summary.functions_total = program.functions.len(); + let omitted_functions = program.functions.len() - entries.len(); + let mut reasons: Vec<&'static str> = Vec::new(); + if omitted_functions > 0 { + reasons.push(if step_stop { + TRUNCATION_STEP_BUDGET + } else { + TRUNCATION_FUNCTION_BUDGET + }); + } + + let path_json = quote_json(&source_path.display().to_string()); + let revision_json = quote_json(&graph::revision(program)); + let digest_json = quote_json(&source_digest(source)); + + let render = + |count: usize, dropped: usize, render_reasons: &[&'static str]| -> (String, bool) { + with_limit(options.max_bytes, || { + render_report( + &path_json, + &revision_json, + &digest_json, + options, + count, + dropped, + omitted_functions, + render_reasons, + &summary, + analyzer.steps, + used_cases, + &entries, + ) + }) + }; + + let total_entries = entries.len(); + let (output, overflowed) = render(total_entries, 0, &reasons); + if !overflowed { + return output; + } + reasons.push(TRUNCATION_BYTE_BUDGET); + let mut low = 0usize; + let mut high = total_entries; + let mut best: Option<(String, usize)> = None; + while low <= high { + let middle = (low + high) / 2; + let dropped = total_entries - middle; + let (candidate, still_over) = render(middle, dropped, &reasons); + if still_over { + if middle == 0 { + break; + } + high = middle - 1; + } else { + best = Some((candidate, middle)); + if middle == total_entries { + break; + } + low = middle + 1; + } + } + let (count, dropped) = best.map_or((0, total_entries), |(_, count)| { + (count, total_entries - count) + }); + render(count, dropped, &reasons).0 +} + +#[allow(clippy::too_many_arguments)] +fn render_report( + path_json: &str, + revision_json: &str, + digest_json: &str, + options: &PropertyTestOptions, + count: usize, + byte_dropped: usize, + omitted_functions: usize, + reasons: &[&'static str], + summary: &Summary, + used_nodes: usize, + used_cases: usize, + entries: &[String], +) -> String { + let truncated = !reasons.is_empty() || byte_dropped > 0; + let total_omitted = omitted_functions + byte_dropped; + let reasons_json = reasons + .iter() + .map(|reason| bformat!("\"{reason}\"")) + .collect::>(); + let functions_json = entries[..count].budgeted_join(","); + bformat!( + "{{\"schema\":\"{}\",\"source\":{{\"path\":{},\"revision\":{},\"sha256\":{}}},\ +\"seed\":\"{}\",\"limits\":{{\"max_cases\":{},\"max_functions\":{},\"max_bytes\":{}}},\ +\"budget\":{{\"used_functions\":{},\"used_cases\":{},\"used_nodes\":{}}},\ +\"truncation\":{{\"truncated\":{},\"reasons\":[{}],\"omitted_functions\":{}}},\ +\"summary\":{{\"functions_total\":{},\"functions_analyzed\":{},\"functions_deferred\":{},\ +\"functions_with_counterexamples\":{},\"cases_attempted\":{},\"filtered_cases\":{},\ +\"discharged_cases\":{},\"runtime_failure_cases\":{}}},\ +\"functions\":[{}],\"nonclaims\":[{}]}}", + SCHEMA, + path_json, + revision_json, + digest_json, + options.seed, + options.max_cases, + options.max_functions, + options.max_bytes, + entries.len(), + used_cases, + used_nodes, + truncated, + reasons_json.budgeted_join(","), + total_omitted, + summary.functions_total, + summary.functions_analyzed, + summary.functions_deferred, + summary.functions_with_counterexamples, + summary.cases_attempted, + summary.filtered_cases, + summary.discharged_cases, + summary.runtime_failure_cases, + functions_json, + NONCLAIMS_JSON, + ) +} + +fn source_digest(source: &str) -> String { + let mut hasher = Sha256::new(); + hasher.update(b"semaprax.property-tests.source.v1\0"); + hasher.update((source.len() as u64).to_le_bytes()); + hasher.update(source.as_bytes()); + format!( + "sha256:{:x}", + crate::digest_hex::LowerHex(hasher.finalize()) + ) +} + +fn deferred_entry_json(function: &Function, reason: &str) -> String { + bformat!( + "{{\"stable_id\":{},\"name\":{},\"outcome\":\"deferred\",\"reason\":\"{}\"}}", + quote_json(&function.stable_id), + quote_json(&function.name), + reason, + ) +} + +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +enum Value { + Int(i64), + Bool(bool), +} + +impl Value { + fn render(self) -> String { + match self { + Value::Int(value) => value.to_string(), + Value::Bool(value) => value.to_string(), + } + } +} + +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +enum RuntimeReason { + ArithmeticOverflow, + DivisionByZero, + RemainderByZero, + NegationOverflow, + CallDepthExceeded, + CalleeRequiresViolated, +} + +impl RuntimeReason { + fn text(self) -> &'static str { + match self { + RuntimeReason::ArithmeticOverflow => RUNTIME_ARITHMETIC_OVERFLOW, + RuntimeReason::DivisionByZero => RUNTIME_DIVISION_BY_ZERO, + RuntimeReason::RemainderByZero => RUNTIME_REMAINDER_BY_ZERO, + RuntimeReason::NegationOverflow => RUNTIME_NEGATION_OVERFLOW, + RuntimeReason::CallDepthExceeded => RUNTIME_CALL_DEPTH_EXCEEDED, + RuntimeReason::CalleeRequiresViolated => RUNTIME_CALLEE_REQUIRES_VIOLATED, + } + } +} + +enum Outcome { + Value(Value), + Runtime(RuntimeReason), + Unsupported(&'static str), + Exhausted, +} + +struct AnalyzedEntry { + json: String, + cases_attempted: usize, + filtered_cases: usize, + runtime_failure_cases: usize, + discharged_cases: usize, + counterexample: bool, +} + +enum FunctionOutcome { + Analyzed(AnalyzedEntry), + Deferred(&'static str), + Exhausted, +} + +type Environment = Vec<(String, Value)>; + +fn lookup(environment: &Environment, name: &str) -> Option { + environment + .iter() + .rev() + .find(|(key, _)| key == name) + .map(|(_, value)| *value) +} + +struct Analyzer<'a> { + admitted: BTreeMap<&'a str, &'a Function>, + names: BTreeSet<&'a str>, + steps: usize, +} + +impl<'a> Analyzer<'a> { + fn new(program: &'a Program) -> Self { + let mut admitted = BTreeMap::new(); + let mut names = BTreeSet::new(); + for function in &program.functions { + names.insert(function.name.as_str()); + admitted.entry(function.name.as_str()).or_insert(function); + } + Self { + admitted, + names, + steps: 0, + } + } + + fn admission(function: &Function) -> Option<&'static str> { + if !function.type_parameters.is_empty() { + return Some(REASON_GENERIC_FUNCTION); + } + if !function.effects.is_empty() { + return Some(REASON_DECLARED_EFFECTS); + } + for param in &function.params { + if param.mode != ParamMode::Value { + return Some(REASON_UNSUPPORTED_PARAMETER_MODE); + } + if !matches!(param.ty, Type::I64 | Type::Bool) { + return Some(REASON_UNSUPPORTED_PARAMETER_TYPE); + } + } + if !matches!(function.return_type, Type::I64 | Type::Bool) { + return Some(REASON_UNSUPPORTED_RESULT_TYPE); + } + None + } + + fn scan(&mut self, expression: &Expr) -> Option<&'static str> { + self.steps += 1; + if self.steps >= MAX_TOTAL_STEPS { + return Some(REASON_EVALUATION_STEP_BUDGET_EXHAUSTED); + } + match &expression.kind { + ExprKind::Int(_) | ExprKind::Bool(_) | ExprKind::Var(_) => None, + ExprKind::Float32(_) | ExprKind::Float64(_) => Some(REASON_FLOAT_LITERAL), + ExprKind::Call { + name, + type_arguments, + args, + } => { + if !type_arguments.is_empty() { + return Some(REASON_GENERIC_CALL); + } + if !self.names.contains(name.as_str()) { + return Some(REASON_UNRESOLVED_CALL); + } + if !self.admitted.contains_key(name.as_str()) { + return Some(REASON_UNSUPPORTED_CALLEE); + } + args.iter().find_map(|argument| self.scan(argument)) + } + ExprKind::Unary { value, .. } => self.scan(value), + ExprKind::Binary { left, right, .. } => self.scan(left).or_else(|| self.scan(right)), + ExprKind::Block { statements, tail } => statements + .iter() + .find_map(|statement| match statement { + Statement::Let { value, .. } => self.scan(value), + }) + .or_else(|| self.scan(tail)), + ExprKind::If { + condition, + then_branch, + else_branch, + } => self + .scan(condition) + .or_else(|| self.scan(then_branch)) + .or_else(|| self.scan(else_branch)), + ExprKind::ConstructRecord { .. } => Some(REASON_RECORD_CONSTRUCTION), + ExprKind::ConstructVariant { .. } => Some(REASON_VARIANT_CONSTRUCTION), + ExprKind::UpdateRecord { .. } => Some(REASON_RECORD_UPDATE), + ExprKind::Project { .. } => Some(REASON_RECORD_PROJECTION), + ExprKind::Match { .. } => Some(REASON_MATCH_EXPRESSION), + ExprKind::Try { .. } => Some(REASON_TRY_EXPRESSION), + } + } + + fn scan_function_contracts_and_body(&mut self, function: &'a Function) -> Option<&'static str> { + for clause in function.requires.iter().chain(function.ensures.iter()) { + if let Some(reason) = self.scan(clause) { + return Some(reason); + } + } + self.scan(&function.body) + } + + fn evaluate( + &mut self, + expression: &Expr, + environment: &mut Environment, + depth: usize, + ) -> Outcome { + self.steps += 1; + if self.steps >= MAX_TOTAL_STEPS { + return Outcome::Exhausted; + } + match &expression.kind { + ExprKind::Int(value) => Outcome::Value(Value::Int(*value)), + ExprKind::Float32(_) | ExprKind::Float64(_) => { + Outcome::Unsupported(REASON_FLOAT_LITERAL) + } + ExprKind::Bool(value) => Outcome::Value(Value::Bool(*value)), + ExprKind::Var(name) => lookup(environment, name).map_or_else( + || Outcome::Unsupported(REASON_UNRESOLVED_VARIABLE), + Outcome::Value, + ), + ExprKind::Unary { op, value } => match self.evaluate(value, environment, depth) { + Outcome::Value(Value::Bool(inner)) => match op { + UnaryOp::Not => Outcome::Value(Value::Bool(!inner)), + UnaryOp::Neg => Outcome::Unsupported(REASON_ILL_TYPED_EXPRESSION), + }, + Outcome::Value(Value::Int(inner)) => match op { + UnaryOp::Neg => inner.checked_neg().map_or( + Outcome::Runtime(RuntimeReason::NegationOverflow), + |result| Outcome::Value(Value::Int(result)), + ), + UnaryOp::Not => Outcome::Unsupported(REASON_ILL_TYPED_EXPRESSION), + }, + other => other, + }, + ExprKind::Binary { op, left, right } => match op { + BinaryOp::And => match self.evaluate(left, environment, depth) { + Outcome::Value(Value::Bool(false)) => Outcome::Value(Value::Bool(false)), + Outcome::Value(Value::Bool(true)) => self.evaluate(right, environment, depth), + other => other, + }, + BinaryOp::Or => match self.evaluate(left, environment, depth) { + Outcome::Value(Value::Bool(true)) => Outcome::Value(Value::Bool(true)), + Outcome::Value(Value::Bool(false)) => self.evaluate(right, environment, depth), + other => other, + }, + _ => { + let evaluated_left = self.evaluate(left, environment, depth); + let Outcome::Value(left_value) = evaluated_left else { + return evaluated_left; + }; + let evaluated_right = self.evaluate(right, environment, depth); + let Outcome::Value(right_value) = evaluated_right else { + return evaluated_right; + }; + combine_binary(*op, left_value, right_value) + } + }, + ExprKind::Call { + name, + type_arguments, + args, + } => { + if !type_arguments.is_empty() { + return Outcome::Unsupported(REASON_GENERIC_CALL); + } + let Some(callee) = self.admitted.get(name.as_str()).copied() else { + return if self.names.contains(name.as_str()) { + Outcome::Unsupported(REASON_UNSUPPORTED_CALLEE) + } else { + Outcome::Unsupported(REASON_UNRESOLVED_CALL) + }; + }; + if depth >= MAX_CALL_DEPTH { + return Outcome::Runtime(RuntimeReason::CallDepthExceeded); + } + let mut arguments = Vec::with_capacity(args.len()); + for argument in args { + match self.evaluate(argument, environment, depth) { + Outcome::Value(value) => arguments.push(value), + other => return other, + } + } + if arguments.len() != callee.params.len() { + return Outcome::Unsupported(REASON_ILL_TYPED_EXPRESSION); + } + let mut frame: Environment = callee + .params + .iter() + .zip(arguments) + .map(|(param, value)| (param.name.clone(), value)) + .collect(); + for clause in &callee.requires { + match self.evaluate(clause, &mut frame, depth + 1) { + Outcome::Value(Value::Bool(true)) => {} + Outcome::Value(Value::Bool(false)) => { + return Outcome::Runtime(RuntimeReason::CalleeRequiresViolated); + } + other => return other, + } + } + self.evaluate(&callee.body, &mut frame, depth + 1) + } + ExprKind::Block { statements, tail } => { + let base = environment.len(); + let mut interrupted = None; + for statement in statements { + let Statement::Let { name, value, .. } = statement; + match self.evaluate(value, environment, depth) { + Outcome::Value(value) => environment.push((name.clone(), value)), + other => { + interrupted = Some(other); + break; + } + } + } + let outcome = + interrupted.unwrap_or_else(|| self.evaluate(tail, environment, depth)); + environment.truncate(base); + outcome + } + ExprKind::If { + condition, + then_branch, + else_branch, + } => match self.evaluate(condition, environment, depth) { + Outcome::Value(Value::Bool(true)) => self.evaluate(then_branch, environment, depth), + Outcome::Value(Value::Bool(false)) => { + self.evaluate(else_branch, environment, depth) + } + other => other, + }, + ExprKind::ConstructRecord { .. } => Outcome::Unsupported(REASON_RECORD_CONSTRUCTION), + ExprKind::ConstructVariant { .. } => Outcome::Unsupported(REASON_VARIANT_CONSTRUCTION), + ExprKind::UpdateRecord { .. } => Outcome::Unsupported(REASON_RECORD_UPDATE), + ExprKind::Project { .. } => Outcome::Unsupported(REASON_RECORD_PROJECTION), + ExprKind::Match { .. } => Outcome::Unsupported(REASON_MATCH_EXPRESSION), + ExprKind::Try { .. } => Outcome::Unsupported(REASON_TRY_EXPRESSION), + } + } + + fn analyze_function( + &mut self, + index: usize, + function: &'a Function, + options: &PropertyTestOptions, + ) -> FunctionOutcome { + if let Some(reason) = Self::admission(function) { + return FunctionOutcome::Deferred(reason); + } + if let Some(reason) = self.scan_function_contracts_and_body(function) { + return FunctionOutcome::Deferred(reason); + } + let parameter_kinds: Vec = function + .params + .iter() + .map(|param| ScalarKind::of(¶m.ty)) + .collect(); + let mut streams: Vec = function + .params + .iter() + .enumerate() + .map(|(position, _)| parameter_stream_seed(options.seed, index, position)) + .collect(); + let requires_json: Vec = function + .requires + .iter() + .enumerate() + .map(|(index, clause)| { + bformat!( + "{{\"index\":{},\"text\":{}}}", + index, + quote_json(&format::expr(clause, 0)) + ) + }) + .collect(); + let ensures_json: Vec = function + .ensures + .iter() + .enumerate() + .map(|(index, clause)| { + bformat!( + "{{\"index\":{},\"text\":{}}}", + index, + quote_json(&format::expr(clause, 0)) + ) + }) + .collect(); + + let mut cases_attempted = 0usize; + let mut filtered_cases = 0usize; + let mut runtime_failure_cases = 0usize; + let mut discharged_cases = 0usize; + let mut runtime_reasons: BTreeSet<&'static str> = BTreeSet::new(); + let mut counterexample: Option = None; + + for case_index in 0..options.max_cases { + if self.steps >= MAX_TOTAL_STEPS { + return FunctionOutcome::Exhausted; + } + cases_attempted += 1; + let mut arguments = Vec::with_capacity(parameter_kinds.len()); + let mut environment: Environment = Vec::with_capacity(function.params.len()); + for (position, kind) in parameter_kinds.iter().enumerate() { + let value = scalar_value(*kind, &mut streams[position], case_index); + arguments.push((function.params[position].name.clone(), value)); + environment.push((function.params[position].name.clone(), value)); + } + let arguments_json = arguments + .iter() + .map(|(name, value)| { + bformat!( + "{{\"name\":{},\"value\":\"{}\"}}", + quote_json(name), + value.render() + ) + }) + .collect::>() + .budgeted_join(","); + + let mut case_classified = false; + for clause in function.requires.iter() { + match self.evaluate(clause, &mut environment, 0) { + Outcome::Value(Value::Bool(true)) => {} + Outcome::Value(Value::Bool(false)) => { + filtered_cases += 1; + case_classified = true; + break; + } + Outcome::Value(Value::Int(_)) => { + return FunctionOutcome::Deferred(REASON_ILL_TYPED_EXPRESSION) + } + Outcome::Runtime(reason) => { + runtime_failure_cases += 1; + runtime_reasons.insert(reason.text()); + case_classified = true; + break; + } + Outcome::Unsupported(reason) => return FunctionOutcome::Deferred(reason), + Outcome::Exhausted => return FunctionOutcome::Exhausted, + } + } + if case_classified { + continue; + } + match self.evaluate(&function.body, &mut environment, 0) { + Outcome::Value(result_value) => { + environment.push(("result".to_owned(), result_value)); + let mut ensured = true; + let mut found_counterexample = false; + for (clause_index, clause) in function.ensures.iter().enumerate() { + match self.evaluate(clause, &mut environment, 0) { + Outcome::Value(Value::Bool(true)) => {} + Outcome::Value(Value::Bool(false)) => { + counterexample = Some(bformat!( + "{{\"index\":{},\"text\":{},\"arguments\":[{}],\"result\":\"{}\"}}", + clause_index, + quote_json(&format::expr(clause, 0)), + arguments_json, + result_value.render() + )); + ensured = false; + found_counterexample = true; + break; + } + Outcome::Value(Value::Int(_)) => { + return FunctionOutcome::Deferred(REASON_ILL_TYPED_EXPRESSION) + } + Outcome::Runtime(reason) => { + runtime_failure_cases += 1; + runtime_reasons.insert(reason.text()); + ensured = false; + break; + } + Outcome::Unsupported(reason) => { + return FunctionOutcome::Deferred(reason) + } + Outcome::Exhausted => return FunctionOutcome::Exhausted, + } + } + environment.pop(); + if found_counterexample { + break; + } + if ensured { + discharged_cases += 1; + } + } + Outcome::Runtime(reason) => { + runtime_failure_cases += 1; + runtime_reasons.insert(reason.text()); + } + Outcome::Unsupported(reason) => return FunctionOutcome::Deferred(reason), + Outcome::Exhausted => return FunctionOutcome::Exhausted, + } + } + + let runtime_reasons_json = runtime_reasons + .iter() + .map(|reason| bformat!("\"{reason}\"")) + .collect::>(); + let found_counterexample = counterexample.is_some(); + let counterexample_json = counterexample.unwrap_or_else(|| "null".to_owned()); + let json = bformat!( + "{{\"stable_id\":{},\"name\":{},\"outcome\":\"analyzed\",\ +\"signature\":{{\"params\":[{}],\"result\":\"{}\"}},\ +\"requires\":[{}],\"ensures\":[{}],\ +\"cases_attempted\":{},\"filtered_cases\":{},\"runtime_failures\":{},\ +\"runtime_reasons\":[{}],\"discharged_cases\":{},\"counterexample\":{}}}", + quote_json(&function.stable_id), + quote_json(&function.name), + function + .params + .iter() + .map(|param| { + bformat!( + "{{\"name\":{},\"type\":\"{}\"}}", + quote_json(¶m.name), + scalar_type_text(¶m.ty) + ) + }) + .collect::>() + .budgeted_join(","), + scalar_type_text(&function.return_type), + requires_json.budgeted_join(","), + ensures_json.budgeted_join(","), + cases_attempted, + filtered_cases, + runtime_failure_cases, + runtime_reasons_json.budgeted_join(","), + discharged_cases, + counterexample_json, + ); + FunctionOutcome::Analyzed(AnalyzedEntry { + json, + cases_attempted, + filtered_cases, + runtime_failure_cases, + discharged_cases, + counterexample: found_counterexample, + }) + } +} + +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +enum ScalarKind { + Int, + Bool, +} + +impl ScalarKind { + fn of(ty: &Type) -> Self { + match ty { + Type::I64 => ScalarKind::Int, + Type::Bool => ScalarKind::Bool, + _ => ScalarKind::Int, + } + } +} + +fn scalar_type_text(ty: &Type) -> &'static str { + match ty { + Type::I64 => "i64", + Type::Bool => "bool", + _ => "i64", + } +} + +fn scalar_value(kind: ScalarKind, state: &mut u64, case_index: usize) -> Value { + match kind { + ScalarKind::Int => { + if case_index < I64_LATTICE.len() { + Value::Int(I64_LATTICE[case_index]) + } else { + Value::Int(next_sample(state) as i64) + } + } + ScalarKind::Bool => { + if case_index < 2 { + Value::Bool(case_index == 0) + } else { + Value::Bool(next_sample(state) & 1 == 1) + } + } + } +} + +fn next_sample(state: &mut u64) -> u64 { + let mut x = *state; + x ^= x >> 12; + x ^= x >> 25; + x ^= x >> 27; + *state = x; + x.wrapping_mul(0x2545_F491_4F6C_DD1D) +} + +fn splitmix64(state: &mut u64) -> u64 { + *state = state.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = *state; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) +} + +fn parameter_stream_seed(base: u64, function_index: usize, parameter_index: usize) -> u64 { + let mut state = base + ^ ((function_index as u64).wrapping_mul(0xA24B_AED4_963E_E407)) + ^ ((parameter_index as u64).wrapping_mul(0x9FB2_1C65_1E98_DF25)); + splitmix64(&mut state) +} + +fn combine_binary(op: BinaryOp, left: Value, right: Value) -> Outcome { + match (left, right) { + (Value::Int(left), Value::Int(right)) => match op { + BinaryOp::Add => checked_int(left.checked_add(right)), + BinaryOp::Sub => checked_int(left.checked_sub(right)), + BinaryOp::Mul => checked_int(left.checked_mul(right)), + BinaryOp::Div => { + if right == 0 { + Outcome::Runtime(RuntimeReason::DivisionByZero) + } else { + checked_int(left.checked_div(right)) + } + } + BinaryOp::Rem => { + if right == 0 { + Outcome::Runtime(RuntimeReason::RemainderByZero) + } else { + checked_int(left.checked_rem(right)) + } + } + BinaryOp::Eq => Outcome::Value(Value::Bool(left == right)), + BinaryOp::Ne => Outcome::Value(Value::Bool(left != right)), + BinaryOp::Lt => Outcome::Value(Value::Bool(left < right)), + BinaryOp::Le => Outcome::Value(Value::Bool(left <= right)), + BinaryOp::Gt => Outcome::Value(Value::Bool(left > right)), + BinaryOp::Ge => Outcome::Value(Value::Bool(left >= right)), + BinaryOp::And | BinaryOp::Or => Outcome::Unsupported(REASON_ILL_TYPED_EXPRESSION), + }, + (Value::Bool(left), Value::Bool(right)) => match op { + BinaryOp::Eq => Outcome::Value(Value::Bool(left == right)), + BinaryOp::Ne => Outcome::Value(Value::Bool(left != right)), + _ => Outcome::Unsupported(REASON_ILL_TYPED_EXPRESSION), + }, + _ => Outcome::Unsupported(REASON_ILL_TYPED_EXPRESSION), + } +} + +fn checked_int(value: Option) -> Outcome { + match value { + Some(value) => Outcome::Value(Value::Int(value)), + None => Outcome::Runtime(RuntimeReason::ArithmeticOverflow), + } +} + +#[cfg(test)] +mod tests { + use super::*; + use std::path::PathBuf; + use std::sync::atomic::{AtomicUsize, Ordering}; + + static COUNTER: AtomicUsize = AtomicUsize::new(0); + + fn write_temp(source: &str) -> PathBuf { + let path = std::env::temp_dir().join(format!( + "semaprax-property-tests-{}-{}.spx", + std::process::id(), + COUNTER.fetch_add(1, Ordering::SeqCst) + )); + std::fs::write(&path, source).unwrap(); + path + } + + #[allow(dead_code)] + fn cleanup(path: &Path) { + let _ = std::fs::remove_file(path); + } + + const VALID_SOURCE: &str = r#" +module test.probe; + +@id("probe.ok") +fn ok(value: i64) -> bool + ensures result == true +{ + true +} + +@id("app.main") +fn main() -> i64 + ensures result == 1 +{ + if ok(3) { 1 } else { 0 } +} +"#; + + #[test] + fn options_reject_out_of_bounds_values() { + assert!(PropertyTestOptions::new(0, 8, DEFAULT_MAX_BYTES, 1).is_err()); + assert!(PropertyTestOptions::new(MAX_CASES_LIMIT + 1, 8, DEFAULT_MAX_BYTES, 1).is_err()); + assert!(PropertyTestOptions::new(8, 0, DEFAULT_MAX_BYTES, 1).is_err()); + assert!( + PropertyTestOptions::new(8, MAX_FUNCTIONS_LIMIT + 1, DEFAULT_MAX_BYTES, 1).is_err() + ); + assert!(PropertyTestOptions::new(8, 8, 512, 1).is_err()); + assert!(PropertyTestOptions::new(8, 8, graph::MAX_AGENT_CONTEXT_BYTES + 1, 1).is_err()); + assert!(PropertyTestOptions::new(1, 1, graph::MIN_AGENT_CONTEXT_BYTES, u64::MAX).is_ok()); + } + + #[test] + fn defaults_are_stable() { + let options = PropertyTestOptions::default(); + assert_eq!(options.max_cases, 64); + assert_eq!(options.max_functions, 64); + assert_eq!(options.max_bytes, 64 * 1024); + assert_eq!(options.seed, DEFAULT_SEED); + } + + #[test] + fn stream_seeds_are_stable_and_distinct() { + assert_eq!( + parameter_stream_seed(7, 3, 1), + parameter_stream_seed(7, 3, 1) + ); + assert_ne!( + parameter_stream_seed(7, 3, 1), + parameter_stream_seed(7, 3, 2) + ); + assert_ne!( + parameter_stream_seed(7, 1, 1), + parameter_stream_seed(7, 2, 1) + ); + let mut first = parameter_stream_seed(DEFAULT_SEED, 0, 0); + let a = next_sample(&mut first); + let mut second = parameter_stream_seed(DEFAULT_SEED, 0, 0); + let b = next_sample(&mut second); + assert_eq!(a, b); + } + + #[test] + fn lattice_covers_boundaries_before_sampling() { + let mut state = parameter_stream_seed(DEFAULT_SEED, 0, 0); + assert_eq!(scalar_value(ScalarKind::Int, &mut state, 0), Value::Int(0)); + assert_eq!( + scalar_value(ScalarKind::Int, &mut state, 7), + Value::Int(i64::MIN) + ); + assert_eq!( + scalar_value(ScalarKind::Bool, &mut state, 0), + Value::Bool(true) + ); + assert_eq!( + scalar_value(ScalarKind::Bool, &mut state, 1), + Value::Bool(false) + ); + } + + #[test] + fn parse_errors_surface_as_diagnostics() { + let path = write_temp("this is not semaprax"); + let outcome = generate(&path, &PropertyTestOptions::default()); + assert!(outcome.is_err()); + cleanup(&path); + } + + #[test] + fn verification_errors_fail_closed() { + let source = r#" +module test.probe; + +@id("probe.bad") +fn bad(value: i64) -> i64 + ensures result == missing +{ + value +} +"#; + let path = write_temp(source); + let outcome = generate(&path, &PropertyTestOptions::default()); + let errors = outcome.expect_err("verification errors must fail closed"); + assert!(errors.iter().any(|item| item.severity.is_error())); + cleanup(&path); + } + + #[test] + fn drift_after_parse_fails_closed() { + let path = write_temp(VALID_SOURCE); + let mut mutate = |_phase: HookPhase, canonical: &Path| { + let mut current = std::fs::read_to_string(canonical)?; + current.push('\n'); + std::fs::write(canonical, current) + }; + let outcome = generate_with_hook(&path, &PropertyTestOptions::default(), &mut mutate); + assert!(outcome.is_err(), "drift after parse must reject the report"); + cleanup(&path); + } + + #[test] + fn clean_hooks_preserve_success() { + let path = write_temp(VALID_SOURCE); + let mut noop = |_phase, _canonical: &Path| Ok(()); + let outcome = generate_with_hook(&path, &PropertyTestOptions::default(), &mut noop); + let report = outcome.expect("clean hooks must not interfere"); + assert!(report.contains(SCHEMA)); + cleanup(&path); + } +} diff --git a/tests/property_tests_v1.rs b/tests/property_tests_v1.rs new file mode 100644 index 0000000..0892bf1 --- /dev/null +++ b/tests/property_tests_v1.rs @@ -0,0 +1,429 @@ +use std::path::{Path, PathBuf}; +use std::process::Command; +use std::sync::atomic::{AtomicUsize, Ordering}; + +use semaprax::properties::{self, PropertyTestOptions}; +use serde_json::Value; +use sha2::{Digest as _, Sha256}; + +static COUNTER: AtomicUsize = AtomicUsize::new(0); + +fn write_source(name: &str, source: &str) -> PathBuf { + let path = std::env::temp_dir().join(format!( + "semaprax-property-tests-v1-{}-{}-{name}.spx", + std::process::id(), + COUNTER.fetch_add(1, Ordering::SeqCst) + )); + std::fs::write(&path, source).unwrap(); + path +} + +fn generate_value(source_path: &Path, options: &PropertyTestOptions) -> Value { + let report = properties::generate(source_path, options).unwrap(); + serde_json::from_str(&report).unwrap() +} + +fn function_entry<'a>(report: &'a Value, name: &str) -> &'a Value { + report["functions"] + .as_array() + .unwrap() + .iter() + .find(|entry| entry["name"] == name) + .unwrap_or_else(|| panic!("missing function entry {name}")) +} + +#[test] +fn meaning_example_is_deterministic_and_discharges() { + let source_path = Path::new(env!("CARGO_MANIFEST_DIR")).join("examples/meaning.spx"); + let options = PropertyTestOptions::default(); + let first = properties::generate(&source_path, &options).unwrap(); + let second = properties::generate(&source_path, &options).unwrap(); + assert_eq!(first, second, "repeated generation must be byte-identical"); + + let report: Value = serde_json::from_str(&first).unwrap(); + assert_eq!(report["schema"], "semaprax.property-tests.v1"); + assert_eq!( + report["seed"], + properties::DEFAULT_SEED.to_string(), + "the default seed must be serialized as a decimal string" + ); + + let source_bytes = std::fs::read(&source_path).unwrap(); + let mut hasher = Sha256::new(); + hasher.update(b"semaprax.property-tests.source.v1\0"); + hasher.update((source_bytes.len() as u64).to_le_bytes()); + hasher.update(&source_bytes); + let expected_digest = format!( + "sha256:{:x}", + semaprax::digest_hex::LowerHex(hasher.finalize()) + ); + assert_eq!(report["source"]["sha256"], expected_digest.as_str()); + assert!( + report["source"]["revision"] + .as_str() + .unwrap() + .starts_with("sha256:"), + "the bound graph revision must be a digest string" + ); + assert_eq!(report["limits"]["max_cases"], 64); + assert_eq!(report["limits"]["max_functions"], 64); + assert_eq!(report["limits"]["max_bytes"], 65536); + assert_eq!(report["truncation"]["truncated"], false); + assert_eq!(report["truncation"]["reasons"], serde_json::json!([])); + assert_eq!( + report["nonclaims"], + serde_json::json!([ + "no_symbolic_execution_or_smt", + "no_static_contract_discharge", + "no_counterexample_minimization", + "no_statistical_coverage_guarantee", + "not_a_test_runner", + "no_target_execution", + ]) + ); + + let summary = &report["summary"]; + let analyzed = summary["functions_analyzed"].as_u64().unwrap(); + let deferred = summary["functions_deferred"].as_u64().unwrap(); + assert_eq!(summary["functions_total"], analyzed + deferred); + assert_eq!( + report["budget"]["used_functions"], + report["functions"].as_array().unwrap().len() + ); + assert!(analyzed >= 2, "add and main must both be analyzed"); + + let add = function_entry(&report, "add"); + assert_eq!(add["outcome"], "analyzed"); + assert_eq!( + add["signature"], + serde_json::json!({ + "params": [ + {"name": "left", "type": "i64"}, + {"name": "right", "type": "i64"}, + ], + "result": "i64", + }) + ); + assert_eq!( + add["requires"], + serde_json::json!([ + {"index": 0, "text": "left >= 0"}, + {"index": 1, "text": "right >= 0"}, + ]) + ); + assert_eq!( + add["ensures"], + serde_json::json!([ + {"index": 0, "text": "result == left + right"}, + ]) + ); + assert!(add["filtered_cases"].as_u64().unwrap() > 0); + assert!(add["discharged_cases"].as_u64().unwrap() > 0); + assert_eq!(add["counterexample"], Value::Null); + + let main = function_entry(&report, "main"); + assert_eq!(main["outcome"], "analyzed"); + assert_eq!( + main["discharged_cases"], main["cases_attempted"], + "main must discharge every generated case" + ); +} + +#[test] +fn ensures_violation_reports_exact_counterexample_and_stops() { + let source = r#" +module test.probe; + +@id("probe.bad") +fn bad(x: i64) -> i64 + ensures result == x + 1 +{ x } + +@id("app.main") +fn main() -> i64 { 0 } +"#; + let path = write_source("counterexample.spx", source); + let report = generate_value(&path, &PropertyTestOptions::default()); + assert_eq!(report["summary"]["functions_with_counterexamples"], 1); + let bad = function_entry(&report, "bad"); + assert_eq!(bad["cases_attempted"], 1); + assert_eq!( + bad["counterexample"], + serde_json::json!({ + "index": 0, + "text": "result == x + 1", + "arguments": [{"name": "x", "value": "0"}], + "result": "0", + }) + ); +} + +#[test] +fn runtime_failures_report_closed_reasons() { + let source = r#" +module test.probe; + +@id("probe.divide") +fn divide(left: i64, right: i64) -> i64 { left / right } + +@id("probe.remainder") +fn remainder(left: i64, right: i64) -> i64 { left % right } + +@id("probe.negate") +fn negate(value: i64) -> i64 { -value } + +@id("app.main") +fn main() -> i64 { 0 } +"#; + let path = write_source("runtime.spx", source); + let report = generate_value(&path, &PropertyTestOptions::default()); + for name in ["divide", "remainder", "negate"] { + let entry = function_entry(&report, name); + assert!( + entry["runtime_failures"].as_u64().unwrap() > 0, + "{name} must observe at least one runtime failure" + ); + assert_eq!(entry["counterexample"], Value::Null); + } + assert!(function_entry(&report, "divide")["runtime_reasons"] + .as_array() + .unwrap() + .iter() + .any(|reason| reason == "division_by_zero")); + assert!(function_entry(&report, "remainder")["runtime_reasons"] + .as_array() + .unwrap() + .iter() + .any(|reason| reason == "remainder_by_zero")); + assert!(function_entry(&report, "negate")["runtime_reasons"] + .as_array() + .unwrap() + .iter() + .any(|reason| reason == "negation_overflow")); +} + +#[test] +fn unsupported_shapes_defer_with_closed_reasons() { + let source = r#" +module test.probe; + +permit { clock.read } + +record Pair { + left: i64, + right: bool, +} + +variant Choice { + None, + Number { value: i64, }, +} + +@id("probe.generic") +fn generic(value: T) -> T { value } + +@id("probe.effectful") +fn effectful(value: i64) -> i64 + uses { clock.read } +{ value + 1 } + +@id("probe.floaty") +fn floaty(value: f32) -> f32 { value } + +@id("probe.constructs") +fn constructs(value: i64) -> i64 { + let pair = Pair { left: value, right: true }; + pair.left +} + +@id("probe.maybe") +fn maybe(flag: bool) -> Result { + if flag { + Result::Ok { value: 7 } + } else { + Result::Err { error: false } + } +} + +@id("probe.branching") +fn branching(value: i64, flag: bool) -> i64 { + let choice = if flag { + Choice::None {} + } else { + Choice::Number { value: value } + }; + match choice { + Choice::None {} => 0, + Choice::Number { value: number } => number, + } +} + +@id("app.main") +fn main() -> i64 { 0 } +"#; + let path = write_source("deferred.spx", source); + let report = generate_value(&path, &PropertyTestOptions::default()); + let expected: &[(&str, &str)] = &[ + ("generic", "generic_function"), + ("effectful", "declared_effects"), + ("floaty", "unsupported_parameter_type"), + ("constructs", "record_construction"), + ("maybe", "unsupported_result_type"), + ("branching", "variant_construction"), + ]; + for (name, reason) in expected { + let entry = function_entry(&report, name); + assert_eq!(entry["outcome"], "deferred", "{name}"); + assert_eq!(entry["reason"], *reason, "{name}"); + } + assert_eq!( + report["summary"]["functions_deferred"], + expected.len(), + "every unsupported shape must defer" + ); +} + +#[test] +fn function_budget_truncates_with_stable_order() { + let source = r#" +module test.probe; + +@id("probe.first") +fn first(value: i64) -> i64 { value } + +@id("probe.second") +fn second(value: i64) -> i64 { value } + +@id("probe.third") +fn third(value: i64) -> i64 { value } + +@id("app.main") +fn main() -> i64 { 0 } +"#; + let path = write_source("caps.spx", source); + let options = PropertyTestOptions::new(4, 2, 64 * 1024, 7).unwrap(); + let report = generate_value(&path, &options); + assert_eq!(options.max_cases, 4); + assert_eq!(report["budget"]["used_functions"], 2); + assert_eq!(report["truncation"]["omitted_functions"], 2); + assert_eq!(report["truncation"]["truncated"], true); + assert_eq!( + report["truncation"]["reasons"], + serde_json::json!(["function_budget"]) + ); + let names: Vec<&str> = report["functions"] + .as_array() + .unwrap() + .iter() + .map(|entry| entry["name"].as_str().unwrap()) + .collect(); + assert_eq!(names, vec!["first", "second"]); + + let limited_cases = generate_value( + &path, + &PropertyTestOptions::new(1, 64, 64 * 1024, 7).unwrap(), + ); + for entry in limited_cases["functions"].as_array().unwrap() { + if entry["outcome"] == "analyzed" { + assert_eq!(entry["cases_attempted"], 1); + } + } +} + +#[test] +fn byte_budget_truncates_prefix_without_invalid_json() { + let source = r#" +module test.probe; + +@id("probe.first") +fn first(value: i64) -> i64 + requires value >= 0 +{ value } + +@id("probe.second") +fn second(value: i64) -> i64 + requires value >= 0 +{ value } + +@id("probe.third") +fn third(value: i64) -> i64 + requires value >= 0 +{ value } + +@id("app.main") +fn main() -> i64 { 0 } +"#; + let path = write_source("bytes.spx", source); + let options = PropertyTestOptions::new(8, 16, 1024, 11).unwrap(); + let report_text = properties::generate(&path, &options).unwrap(); + let report: Value = serde_json::from_str(&report_text) + .unwrap_or_else(|error| panic!("truncated output must stay valid JSON: {error}")); + assert_eq!(report["truncation"]["truncated"], true); + let reasons = report["truncation"]["reasons"].as_array().unwrap(); + assert!( + reasons.iter().any(|reason| reason == "byte_budget"), + "byte budget exhaustion must be reported" + ); + assert_eq!( + report["truncation"]["omitted_functions"], + 4 - report["functions"].as_array().unwrap().len() + ); +} + +#[test] +fn seeds_change_sampled_cases_deterministically() { + let source = r#" +module test.probe; + +@id("probe.positive") +fn positive(value: i64) -> i64 + requires value > 0 +{ value } + +@id("app.main") +fn main() -> i64 { 0 } +"#; + let path = write_source("seeds.spx", source); + let baseline = properties::generate( + &path, + &PropertyTestOptions::new(64, 8, 64 * 1024, 1000).unwrap(), + ) + .unwrap(); + let repeat = properties::generate( + &path, + &PropertyTestOptions::new(64, 8, 64 * 1024, 1000).unwrap(), + ) + .unwrap(); + assert_eq!(baseline, repeat, "same seed must reproduce exact bytes"); + let other = properties::generate( + &path, + &PropertyTestOptions::new(64, 8, 64 * 1024, 1001).unwrap(), + ) + .unwrap(); + assert_ne!(baseline, other, "different seeds must sample differently"); +} + +#[test] +fn cli_rejects_unknown_options_and_missing_paths() { + let cli = |arguments: &[&str]| { + Command::new(env!("CARGO_BIN_EXE_semaprax")) + .args(arguments) + .output() + .unwrap() + }; + let missing = cli(&["properties"]); + assert_eq!(missing.status.code(), Some(2)); + let unknown = cli(&["properties", "examples/meaning.spx", "--wat", "1"]); + assert_eq!(unknown.status.code(), Some(2)); + let duplicate = cli(&[ + "properties", + "examples/meaning.spx", + "--max-cases", + "2", + "--max-cases", + "3", + ]); + assert_eq!(duplicate.status.code(), Some(2)); + let noncanonical = cli(&["properties", "examples/meaning.spx", "--max-cases", "02"]); + assert_eq!(noncanonical.status.code(), Some(2)); +}