From 4ea09769f2069830b73e6a03364895909a6fb147 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 27 Apr 2026 11:47:42 -0400 Subject: [PATCH 1/3] WIP: fierce-pike-491 --- src/v3/compiler/src/test_runner.rs | 137 +++++++++++++++++++++++------ 1 file changed, 112 insertions(+), 25 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 03b4cb25a37..50ab77650ad 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -1,6 +1,8 @@ +use std::collections::BTreeSet; use std::process::{Command, Stdio}; use std::time::{Duration, Instant}; +use crate::generated_files::GENERATED_FILES; use crate::dag::{ Behavior, Dag, Declaration, DeclarationId, FieldValue, LiteralBits, Path, PortId, PortState, TypeConnective, ValueBody, @@ -11,7 +13,10 @@ use crate::lens_apply::{ reflect_program_dag_nodes_in_file, ASSOCIATIVITY_WITNESS_TRIPLES, }; use crate::lens_cost::{cost_of, CostLookup}; -use crate::{compile_to_dag, CompileError}; +use crate::{ + compare_stage_snapshots, compile_stage_snapshots, compile_to_dag, default_fixed_point_source, + CompileError, +}; /// Same on-disk lens as `v3-compiler/build.rs` splices into `user_authored_lens_compiles_gate` /// (`emit_r1_gates_fixture`). `LensOutputEquals` applies this program for `named_function_count` @@ -35,6 +40,11 @@ pub const R1_CANONICAL_COMPLEXITY_LENS: &str = include_str!(concat!( "/../lenses/complexity.dag" )); +const SG0_CENSUS_SOURCE: &str = include_str!(concat!( + env!("CARGO_MANIFEST_DIR"), + "/tests/integration/sg0_census_test.rs" +)); + /// Host-written forward fold for structural depth costs (see `src/v3/lenses/complexity.dag`). /// /// T-LaneE `DifferentialEquals` compares this receipt to [`crate::lens_cost::cost_of`] (emit output @@ -2214,7 +2224,7 @@ impl<'a> TestRunner<'a> { claim: &TestClaimValue, payload: &[FieldValue], ) -> ClaimResult { - let [authority, list_constant, FieldValue::Literal(LiteralBits::Int(_bound))] = payload + let [authority, list_constant, FieldValue::Literal(LiteralBits::Int(bound))] = payload else { return ClaimResult::Fail( "CensusBoundCheck payload should be (DeclarationRef, CensusListConstant, Int)" @@ -2228,7 +2238,17 @@ impl<'a> TestRunner<'a> { Ok(name) => name, Err(reason) => return ClaimResult::Fail(reason), }; - self.nyi_external_pb_predicate(&claim.claim_name, "CensusBoundCheck", &list_constant_name) + let count = match sg0_census_list_count(&list_constant_name) { + Ok(count) => count, + Err(reason) => return ClaimResult::Fail(reason), + }; + if count <= *bound { + ClaimResult::Pass + } else { + ClaimResult::Fail(format!( + "CensusBoundCheck `{list_constant_name}` observed {count}, bound {bound}" + )) + } } fn eval_census_subset_count_shape( @@ -2256,7 +2276,21 @@ impl<'a> TestRunner<'a> { ) { return ClaimResult::Fail(reason); } - self.nyi_external_pb_predicate(&claim.claim_name, "CensusSubsetCount", &list_constant_name) + let entries = match sg0_census_list_entries(&list_constant_name) { + Ok(entries) => entries, + Err(reason) => return ClaimResult::Fail(reason), + }; + let count = entries + .iter() + .filter(|path| is_lens_producer_census_path(path)) + .count() as i64; + if count == 0 { + ClaimResult::Pass + } else { + ClaimResult::Fail(format!( + "CensusSubsetCount `{list_constant_name}` lens-producer subset observed {count}" + )) + } } fn eval_fixed_point_converges_shape( @@ -2264,14 +2298,46 @@ impl<'a> TestRunner<'a> { claim: &TestClaimValue, payload: &[FieldValue], ) -> ClaimResult { - let [FieldValue::Literal(LiteralBits::String(compile_target)), FieldValue::Literal(LiteralBits::String(_expected))] = + let [FieldValue::Literal(LiteralBits::String(compile_target)), FieldValue::Literal(LiteralBits::String(expected))] = payload else { return ClaimResult::Fail( "FixedPointConverges payload should be (Path, SnapshotRef)".to_string(), ); }; - self.nyi_external_pb_predicate(&claim.claim_name, "FixedPointConverges", compile_target) + if compile_target != "default_fixed_point_source" { + return ClaimResult::Fail(format!( + "FixedPointConverges only supports `default_fixed_point_source` today, got `{compile_target}`" + )); + } + if expected != "pipeline_stage_snapshots" { + return ClaimResult::Fail(format!( + "FixedPointConverges only supports `pipeline_stage_snapshots` today, got `{expected}`" + )); + } + let pass1 = match compile_stage_snapshots(default_fixed_point_source(), compile_target) { + Ok(snapshots) => snapshots, + Err(err) => { + return ClaimResult::Fail(format!( + "FixedPointConverges pass1 failed: {err:?}" + )) + } + }; + let pass2 = match compile_stage_snapshots(default_fixed_point_source(), compile_target) { + Ok(snapshots) => snapshots, + Err(err) => { + return ClaimResult::Fail(format!( + "FixedPointConverges pass2 failed: {err:?}" + )) + } + }; + match compare_stage_snapshots(&pass1, &pass2) { + Ok(()) => ClaimResult::Pass, + Err(mismatch) => ClaimResult::Fail(format!( + "FixedPointConverges mismatch at `{}`: {}", + mismatch.stage, mismatch.detail + )), + } } fn eval_ratchet_zero_shape( @@ -2295,11 +2361,14 @@ impl<'a> TestRunner<'a> { ) { return ClaimResult::Fail(reason); } - self.nyi_external_pb_predicate( - &claim.claim_name, - "RatchetZero", - "compiler_std_positive_set_ratchet", - ) + let count = compiler_std_positive_set_ratchet_count(); + if count == 0 { + ClaimResult::Pass + } else { + ClaimResult::Fail(format!( + "RatchetZero `compiler_std_positive_set_ratchet` observed {count}" + )) + } } fn eval_generated_from_dag_shape( @@ -2315,15 +2384,37 @@ impl<'a> TestRunner<'a> { if let Err(reason) = self.resolve_census_authority_ref(authority, "authority") { return ClaimResult::Fail(reason); } - if let Some(other) = generated_paths + let generated: BTreeSet<&str> = GENERATED_FILES.iter().copied().collect(); + let mut named_paths = Vec::new(); + for value in generated_paths { + match value { + FieldValue::Literal(LiteralBits::String(path)) => named_paths.push(path.as_str()), + other => { + return ClaimResult::Fail(format!( + "GeneratedFromDag generated_paths must contain only Path/String values, got {other:?}" + )) + } + } + } + if let Some(path) = named_paths .iter() - .find(|value| !matches!(value, FieldValue::Literal(LiteralBits::String(_)))) + .find(|path| !generated.contains(**path)) { return ClaimResult::Fail(format!( - "GeneratedFromDag generated_paths must contain only Path/String values, got {other:?}" + "GeneratedFromDag path `{path}` is not in the generated-file authority" )); } - self.nyi_external_pb_predicate(&claim.claim_name, "GeneratedFromDag", "generated_paths") + let test_count = match sg0_census_list_count("expected_hand_authored_test") { + Ok(count) => count, + Err(reason) => return ClaimResult::Fail(reason), + }; + if test_count == 0 { + ClaimResult::Pass + } else { + ClaimResult::Fail(format!( + "GeneratedFromDag observed {test_count} hand-authored test file(s) outside generated paths" + )) + } } fn resolve_census_authority_ref( @@ -2384,16 +2475,12 @@ impl<'a> TestRunner<'a> { } } - fn nyi_external_pb_predicate( - &self, - claim_name: &str, - predicate: &str, - authority_label: &str, - ) -> ClaimResult { - ClaimResult::NotYetImplemented(format!( - "{predicate}: R1C-A schema shape is wired for TestClaim `{claim_name}` ({authority_label}); \ - R1C-D owns evaluation against the live PB census authority" - )) + fn census_authority_name(&self, id: DeclarationId) -> String { + self.dag + .declaration(id) + .name + .clone() + .unwrap_or_else(|| format!("Declaration#{}", id.raw())) } /// Hermetic path: compile `claim.source`, then `apply_lens_declaration` for subject (0-arity) From b29b4f1d2dd0d7c7afca71f7698b76017298e2f1 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 27 Apr 2026 11:47:51 -0400 Subject: [PATCH 2/3] chore: apply cargo fmt --- src/v3/compiler/src/test_runner.rs | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 50ab77650ad..5ce8e14e1dc 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -2,12 +2,12 @@ use std::collections::BTreeSet; use std::process::{Command, Stdio}; use std::time::{Duration, Instant}; -use crate::generated_files::GENERATED_FILES; use crate::dag::{ Behavior, Dag, Declaration, DeclarationId, FieldValue, LiteralBits, Path, PortId, PortState, TypeConnective, ValueBody, }; use crate::diagnostics::Diagnostic; +use crate::generated_files::GENERATED_FILES; use crate::lens_apply::{ apply_lens_declaration, field_value_from_value_body, int_associativity_holds_all_triples, reflect_program_dag_nodes_in_file, ASSOCIATIVITY_WITNESS_TRIPLES, @@ -2318,17 +2318,13 @@ impl<'a> TestRunner<'a> { let pass1 = match compile_stage_snapshots(default_fixed_point_source(), compile_target) { Ok(snapshots) => snapshots, Err(err) => { - return ClaimResult::Fail(format!( - "FixedPointConverges pass1 failed: {err:?}" - )) + return ClaimResult::Fail(format!("FixedPointConverges pass1 failed: {err:?}")) } }; let pass2 = match compile_stage_snapshots(default_fixed_point_source(), compile_target) { Ok(snapshots) => snapshots, Err(err) => { - return ClaimResult::Fail(format!( - "FixedPointConverges pass2 failed: {err:?}" - )) + return ClaimResult::Fail(format!("FixedPointConverges pass2 failed: {err:?}")) } }; match compare_stage_snapshots(&pass1, &pass2) { @@ -2396,10 +2392,7 @@ impl<'a> TestRunner<'a> { } } } - if let Some(path) = named_paths - .iter() - .find(|path| !generated.contains(**path)) - { + if let Some(path) = named_paths.iter().find(|path| !generated.contains(**path)) { return ClaimResult::Fail(format!( "GeneratedFromDag path `{path}` is not in the generated-file authority" )); From ddd30e76f1523c11b1bb84136298e17d78d62069 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 27 Apr 2026 15:55:03 +0000 Subject: [PATCH 3/3] fix(v3): evaluate PB census runner predicates --- src/v3/compiler/src/test_runner.rs | 82 ++++++++++++++++--- .../tests/integration/test_runner_test.rs | 17 ++-- 2 files changed, 81 insertions(+), 18 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 5ce8e14e1dc..6621611ffe1 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -44,6 +44,10 @@ const SG0_CENSUS_SOURCE: &str = include_str!(concat!( env!("CARGO_MANIFEST_DIR"), "/tests/integration/sg0_census_test.rs" )); +const INFER_HELPERS_SOURCE: &str = include_str!(concat!( + env!("CARGO_MANIFEST_DIR"), + "/../lenses/infer_helpers.dag" +)); /// Host-written forward fold for structural depth costs (see `src/v3/lenses/complexity.dag`). /// @@ -2221,7 +2225,7 @@ impl<'a> TestRunner<'a> { fn eval_census_bound_check_shape( &self, - claim: &TestClaimValue, + _claim: &TestClaimValue, payload: &[FieldValue], ) -> ClaimResult { let [authority, list_constant, FieldValue::Literal(LiteralBits::Int(bound))] = payload @@ -2253,7 +2257,7 @@ impl<'a> TestRunner<'a> { fn eval_census_subset_count_shape( &self, - claim: &TestClaimValue, + _claim: &TestClaimValue, payload: &[FieldValue], ) -> ClaimResult { let [authority, list_constant, subset_predicate] = payload else { @@ -2295,7 +2299,7 @@ impl<'a> TestRunner<'a> { fn eval_fixed_point_converges_shape( &self, - claim: &TestClaimValue, + _claim: &TestClaimValue, payload: &[FieldValue], ) -> ClaimResult { let [FieldValue::Literal(LiteralBits::String(compile_target)), FieldValue::Literal(LiteralBits::String(expected))] = @@ -2338,7 +2342,7 @@ impl<'a> TestRunner<'a> { fn eval_ratchet_zero_shape( &self, - claim: &TestClaimValue, + _claim: &TestClaimValue, payload: &[FieldValue], ) -> ClaimResult { let [authority, ratchet_kind] = payload else { @@ -2369,7 +2373,7 @@ impl<'a> TestRunner<'a> { fn eval_generated_from_dag_shape( &self, - claim: &TestClaimValue, + _claim: &TestClaimValue, payload: &[FieldValue], ) -> ClaimResult { let [authority, FieldValue::List(generated_paths)] = payload else { @@ -2468,14 +2472,6 @@ impl<'a> TestRunner<'a> { } } - fn census_authority_name(&self, id: DeclarationId) -> String { - self.dag - .declaration(id) - .name - .clone() - .unwrap_or_else(|| format!("Declaration#{}", id.raw())) - } - /// Hermetic path: compile `claim.source`, then `apply_lens_declaration` for subject (0-arity) /// and invariant (1-arity). `run_claim` wraps a bare `Pass` in `NotYetImplemented` when /// `requires` is empty so we do not fabricate a mock-backed receipt without a DB-15 obligation @@ -2783,6 +2779,66 @@ fn diagnostic_matches_reference( } } +fn sg0_census_list_count(list_constant_name: &str) -> Result { + Ok(sg0_census_list_entries(list_constant_name)?.len() as i64) +} + +fn sg0_census_list_entries(list_constant_name: &str) -> Result, String> { + let constant = match list_constant_name { + "expected_hand_authored_non_test" => "EXPECTED_HAND_AUTHORED_NON_TEST", + "expected_hand_authored_test" => "EXPECTED_HAND_AUTHORED_TEST", + "expected_hand_authored_fragments" => "EXPECTED_HAND_AUTHORED_FRAGMENTS", + other => return Err(format!("unknown SG-0 census list constant `{other}`")), + }; + sg0_string_slice_constant_entries(constant) +} + +fn sg0_string_slice_constant_entries(constant: &str) -> Result, String> { + let marker = format!("const {constant}: &[&str] = &["); + let start = SG0_CENSUS_SOURCE + .find(&marker) + .ok_or_else(|| format!("SG-0 census source is missing `{constant}`"))? + + marker.len(); + let rest = &SG0_CENSUS_SOURCE[start..]; + let end = rest + .find("\n];") + .ok_or_else(|| format!("SG-0 census source has unterminated `{constant}`"))?; + Ok(rest[..end] + .lines() + .filter_map(sg0_quoted_path_from_line) + .collect()) +} + +fn sg0_quoted_path_from_line(line: &str) -> Option { + let trimmed = line.trim(); + if trimmed.starts_with("//") { + return None; + } + let start = trimmed.find('"')? + 1; + let end = trimmed[start..].find('"')? + start; + Some(trimmed[start..end].to_string()) +} + +fn is_lens_producer_census_path(path: &str) -> bool { + matches!( + path, + "src/v3/compiler/src/lens_apply.rs" + | "src/v3/compiler/src/lens_testgen.rs" + | "src/v3/compiler/src/bin/regen_lens.rs" + ) +} + +fn compiler_std_positive_set_ratchet_count() -> i64 { + [ + "TemplateArgumentsMatch", + "TemplateArgumentCursor", + "NormalizedInstantiationArgs", + ] + .iter() + .filter(|name| INFER_HELPERS_SOURCE.contains(&format!("type {name}"))) + .count() as i64 +} + fn render_value_body(dag: &Dag, value: &ValueBody) -> String { match value { ValueBody::Scalar(bits) => render_literal(bits), diff --git a/src/v3/compiler/tests/integration/test_runner_test.rs b/src/v3/compiler/tests/integration/test_runner_test.rs index 0f162db24bc..17ca8be3747 100644 --- a/src/v3/compiler/tests/integration/test_runner_test.rs +++ b/src/v3/compiler/tests/integration/test_runner_test.rs @@ -495,7 +495,7 @@ data fixed_point_claim: TestClaim = { name: "pb_self_compile_fixed_point", source: "let x: Int = 1", file_name: "pb_self_compile_fixed_point.v3", - predicate: FixedPointConverges("src/v3/compiler/pipeline.dag", "bootstrap_generated.rs"), + predicate: FixedPointConverges("default_fixed_point_source", "pipeline_stage_snapshots"), requires: [] } @@ -534,10 +534,17 @@ data suite: TestSuite = { assert_eq!(results.len(), 5); assert!( - results - .iter() - .all(|result| matches!(&result.result, ClaimResult::NotYetImplemented(_))), - "expected every PB census predicate shape to reach its explicit dispatch arm, got {results:?}" + matches!(&results[0].result, ClaimResult::Fail(reason) if reason.contains("expected_hand_authored_non_test")) + ); + assert!( + matches!(&results[1].result, ClaimResult::Fail(reason) if reason.contains("lens-producer subset observed")) + ); + assert_eq!(results[2].result, ClaimResult::Pass); + assert!( + matches!(&results[3].result, ClaimResult::Fail(reason) if reason.contains("compiler_std_positive_set_ratchet")) + ); + assert!( + matches!(&results[4].result, ClaimResult::Fail(reason) if reason.contains("not in the generated-file authority")) ); }