Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
6cb783e
docs(r1): mark R1C-C closed
briansrls Apr 26, 2026
a12d0d1
Merge remote-tracking branch 'origin/main' into session/zesty-hawk-239
briansrls Apr 26, 2026
e5d3f4c
Merge remote-tracking branch 'origin/main' into session/zesty-hawk-239
briansrls Apr 26, 2026
4944303
Merge remote-tracking branch 'origin/main' into session/zesty-hawk-239
briansrls Apr 26, 2026
4021274
Merge remote-tracking branch 'origin/main' into session/zesty-hawk-239
briansrls Apr 26, 2026
7ac5afe
Merge remote-tracking branch 'origin/main' into session/zesty-hawk-239
briansrls Apr 26, 2026
085732a
Merge remote-tracking branch 'origin/main' into session/zesty-hawk-239
briansrls Apr 26, 2026
5554138
Merge remote-tracking branch 'origin/main' into session/zesty-hawk-239
briansrls Apr 26, 2026
fa142e1
Merge remote-tracking branch 'origin/main' into session/zesty-hawk-239
briansrls Apr 26, 2026
1e7a00a
Merge remote-tracking branch 'origin/main' into session/zesty-hawk-239
briansrls Apr 26, 2026
6cfda63
Merge remote-tracking branch 'origin/main' into session/zesty-hawk-239
briansrls Apr 27, 2026
0b5e816
WIP: zesty-hawk-239
briansrls Apr 27, 2026
b8776ea
regen(v3): refresh verification predicate snapshots
briansrls Apr 27, 2026
9c21a7a
Merge remote-tracking branch 'origin/main' into session/zesty-hawk-239
briansrls Apr 27, 2026
3b025ec
test(v3): update verification predicate ratchets
briansrls Apr 27, 2026
7b56924
WIP: zesty-hawk-239
briansrls Apr 27, 2026
8453083
chore: apply cargo fmt
briansrls Apr 27, 2026
28a6195
WIP: zesty-hawk-239
briansrls Apr 27, 2026
a18159a
WIP: zesty-hawk-239
briansrls Apr 27, 2026
22b1cff
WIP: zesty-hawk-239
briansrls Apr 27, 2026
126119b
test(v3): refresh verification parse manifest
briansrls Apr 27, 2026
30eb5ef
WIP: zesty-hawk-239
briansrls Apr 27, 2026
8b4fa4e
WIP: zesty-hawk-239
briansrls Apr 27, 2026
03493ce
feat(v3): wire PB census TestPredicate shapes
briansrls Apr 27, 2026
1dccd3c
fix(v3): refresh PB census bootstrap artifacts
briansrls Apr 27, 2026
dfe9ac8
Merge remote-tracking branch 'origin/session/zesty-hawk-239' into ses…
briansrls Apr 27, 2026
f960827
fix(v3): avoid diagnostic bootstrap payload collision
briansrls Apr 27, 2026
c670f85
fix(v3): refresh compiler diagnostic bootstrap mirror
briansrls Apr 27, 2026
976531c
fix(v3): type PB census fixture constants
briansrls Apr 27, 2026
8c89a07
fix(v3): refresh PB census parse manifest
briansrls Apr 27, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2,557 changes: 1,286 additions & 1,271 deletions src/v3/compiler/src/bootstrap_generated.rs

Large diffs are not rendered by default.

2,405 changes: 1,210 additions & 1,195 deletions src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs

Large diffs are not rendered by default.

194 changes: 194 additions & 0 deletions src/v3/compiler/src/test_runner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1434,6 +1434,13 @@ impl<'a> TestRunner<'a> {
"DifferentialEquals" => self.eval_differential_equals(claim, &payload),
"AlgebraicLaw" => self.eval_algebraic_law(claim, &payload),
"ExecuteCommand" => self.eval_execute_command(claim, &payload),
"CensusBoundCheck" => self.eval_census_bound_check_shape(claim, &payload),
"CensusSubsetCount" => self.eval_census_subset_count_shape(claim, &payload),
"FixedPointConverges" => {
self.eval_fixed_point_converges_shape(claim, &payload)
}
"RatchetZero" => self.eval_ratchet_zero_shape(claim, &payload),
"GeneratedFromDag" => self.eval_generated_from_dag_shape(claim, &payload),
"MockBackedInvariant" => {
if !claim.requires.is_empty() {
if let Err(reason) = self.validate_resource_requirements(claim) {
Expand Down Expand Up @@ -2202,6 +2209,193 @@ impl<'a> TestRunner<'a> {
}
}

fn eval_census_bound_check_shape(
&self,
claim: &TestClaimValue,
payload: &[FieldValue],
) -> ClaimResult {
let [authority, list_constant, FieldValue::Literal(LiteralBits::Int(_bound))] = payload
else {
return ClaimResult::Fail(
"CensusBoundCheck payload should be (DeclarationRef, CensusListConstant, Int)"
.to_string(),
);
};
if let Err(reason) = self.resolve_census_authority_ref(authority, "authority") {
return ClaimResult::Fail(reason);
}
let list_constant_name = match self.resolve_census_list_constant_ref(list_constant) {
Ok(name) => name,
Err(reason) => return ClaimResult::Fail(reason),
};
self.nyi_external_pb_predicate(&claim.claim_name, "CensusBoundCheck", &list_constant_name)
}

fn eval_census_subset_count_shape(
&self,
claim: &TestClaimValue,
payload: &[FieldValue],
) -> ClaimResult {
let [authority, list_constant, subset_predicate] = payload else {
return ClaimResult::Fail(
"CensusSubsetCount payload should be (DeclarationRef, CensusListConstant, DeclarationRef)".to_string(),
);
};
if let Err(reason) = self.resolve_census_authority_ref(authority, "authority") {
return ClaimResult::Fail(reason);
}
let list_constant_name = match self.resolve_census_list_constant_ref(list_constant) {
Ok(name) => name,
Err(reason) => return ClaimResult::Fail(reason),
};
if let Err(reason) = self.resolve_pb_marker_ref(
subset_predicate,
"subset_predicate",
"lens_producer_files_subset_predicate",
"LensProducerFilesSubsetPredicate",
) {
return ClaimResult::Fail(reason);
}
self.nyi_external_pb_predicate(&claim.claim_name, "CensusSubsetCount", &list_constant_name)
}

fn eval_fixed_point_converges_shape(
&self,
claim: &TestClaimValue,
payload: &[FieldValue],
) -> ClaimResult {
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)
}

fn eval_ratchet_zero_shape(
&self,
claim: &TestClaimValue,
payload: &[FieldValue],
) -> ClaimResult {
let [authority, ratchet_kind] = payload else {
return ClaimResult::Fail(
"RatchetZero payload should be (DeclarationRef, DeclarationRef)".to_string(),
);
};
if let Err(reason) = self.resolve_census_authority_ref(authority, "authority") {
return ClaimResult::Fail(reason);
}
if let Err(reason) = self.resolve_pb_marker_ref(
ratchet_kind,
"ratchet_kind",
"compiler_std_positive_set_ratchet",
"CompilerStdPositiveSetRatchet",
) {
return ClaimResult::Fail(reason);
}
self.nyi_external_pb_predicate(
&claim.claim_name,
"RatchetZero",
"compiler_std_positive_set_ratchet",
)
}

fn eval_generated_from_dag_shape(
&self,
claim: &TestClaimValue,
payload: &[FieldValue],
) -> ClaimResult {
let [authority, FieldValue::List(generated_paths)] = payload else {
return ClaimResult::Fail(
"GeneratedFromDag payload should be (DeclarationRef, List<Path>)".to_string(),
);
};
if let Err(reason) = self.resolve_census_authority_ref(authority, "authority") {
return ClaimResult::Fail(reason);
}
if let Some(other) = generated_paths
.iter()
.find(|value| !matches!(value, FieldValue::Literal(LiteralBits::String(_))))
{
return ClaimResult::Fail(format!(
"GeneratedFromDag generated_paths must contain only Path/String values, got {other:?}"
));
}
self.nyi_external_pb_predicate(&claim.claim_name, "GeneratedFromDag", "generated_paths")
}

fn resolve_census_authority_ref(
&self,
value: &FieldValue,
field_label: &str,
) -> Result<DeclarationId, String> {
match value {
FieldValue::Reference(id) => Ok(*id),
other => Err(format!(
"PB census predicate `{field_label}` should be a DeclarationRef edge, got {other:?}"
)),
}
}

fn resolve_pb_marker_ref(
&self,
value: &FieldValue,
field_label: &str,
expected_decl_name: &str,
expected_marker_type: &str,
) -> Result<DeclarationId, String> {
let FieldValue::Reference(id) = value else {
return Err(format!(
"PB census predicate `{field_label}` should be a DeclarationRef edge to `{expected_decl_name}`, got {value:?}"
));
};
let decl = self.dag.declaration(*id);
let actual_name = decl_display_name(*id, decl);
if decl.name.as_deref() != Some(expected_decl_name) {
return Err(format!(
"PB census predicate `{field_label}` expected `{expected_decl_name}`, got `{actual_name}`"
));
}
match self.decl_inhabits_named_role(decl, expected_marker_type) {
Ok(true) => Ok(*id),
Ok(false) => Err(format!(
"PB census predicate `{field_label}` declaration `{actual_name}` must inhabit `{expected_marker_type}`"
)),
Err(reason) => Err(reason),
}
}

fn resolve_census_list_constant_ref(&self, value: &FieldValue) -> Result<String, String> {
let FieldValue::Reference(id) = value else {
return Err(format!(
"PB census predicate `list_constant` should be a CensusListConstant edge, got {value:?}"
));
};
let decl = self.dag.declaration(*id);
let actual_name = decl_display_name(*id, decl);
match self.decl_inhabits_named_role(decl, "CensusListConstant") {
Ok(true) => Ok(actual_name),
Ok(false) => Err(format!(
"PB census predicate `list_constant` declaration `{actual_name}` must inhabit `CensusListConstant`"
)),
Err(reason) => Err(reason),
}
}

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"
))
}

/// 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
Expand Down
28 changes: 28 additions & 0 deletions src/v3/compiler/tests/integration/m1_5_verification_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -188,6 +188,34 @@ fn bootstrap_loads_verification_authority_types() {
String::from("AlgebraicLaw"),
vec![String::from("law"), String::from("lens_ref")],
),
(
String::from("CensusBoundCheck"),
vec![
String::from("authority"),
String::from("list_constant"),
String::from("bound"),
],
),
(
String::from("CensusSubsetCount"),
vec![
String::from("authority"),
String::from("list_constant"),
String::from("subset_predicate"),
],
),
(
String::from("FixedPointConverges"),
vec![String::from("compile_target"), String::from("expected")],
),
(
String::from("RatchetZero"),
vec![String::from("authority"), String::from("ratchet_kind")],
),
(
String::from("GeneratedFromDag"),
vec![String::from("authority"), String::from("generated_paths")],
),
]
);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -39,5 +39,5 @@ src/v3/std/substrate.dag 54 116421 438b971e40f25a6b
src/v3/std/substrate_minimal.dag 8 5372 feeb314c735f4672
src/v3/std/termination.dag 18 36478 d010232f0373dc99
src/v3/std/tokenize.dag 8 38819 2e158a74f33c18cc
src/v3/std/verification.dag 19 43253 8bc2b1db7983ebbc
src/v3/std/verification.dag 29 58941 d96f3dd31d258ce3
src/v3/std/workflows.dag 4 3135 bb6f9b042a02e8d6
81 changes: 81 additions & 0 deletions src/v3/compiler/tests/integration/test_runner_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -460,6 +460,87 @@ data suite: TestSuite = {
));
}

#[test]
fn test_runner_dispatches_pb_census_predicate_shapes() {
let source = r#"
import std.verification {
compiler_std_positive_set_ratchet,
expected_hand_authored_non_test,
lens_producer_files_subset_predicate
}

data census_authority: Int = 0

data census_bound_claim: TestClaim = {
name: "pb_hand_rust_at_shim_floor",
source: "let x: Int = 1",
file_name: "pb_hand_rust_at_shim_floor.v3",
predicate: CensusBoundCheck(census_authority, expected_hand_authored_non_test, 0),
requires: []
}

data census_subset_claim: TestClaim = {
name: "lens_producer_files_remaining",
source: "let x: Int = 1",
file_name: "lens_producer_files_remaining.v3",
predicate: CensusSubsetCount {
authority: census_authority,
list_constant: expected_hand_authored_non_test,
subset_predicate: lens_producer_files_subset_predicate
},
requires: []
}

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"),
requires: []
}

data ratchet_zero_claim: TestClaim = {
name: "pb_compiler_std_ratchet_zero",
source: "let x: Int = 1",
file_name: "pb_compiler_std_ratchet_zero.v3",
predicate: RatchetZero {
authority: census_authority,
ratchet_kind: compiler_std_positive_set_ratchet
},
requires: []
}

data generated_from_dag_claim: TestClaim = {
name: "pb_test_file_generated_from_dag",
source: "let x: Int = 1",
file_name: "pb_test_file_generated_from_dag.v3",
predicate: GeneratedFromDag(census_authority, ["src/v3/compiler/tests/integration.rs"]),
requires: []
}

data suite: TestSuite = {
name: "pb_census_predicate_shapes",
claims: [
census_bound_claim,
census_subset_claim,
fixed_point_claim,
ratchet_zero_claim,
generated_from_dag_claim
]
}
"#;
let dag = compile_clean(source, "pb_census_predicate_shapes.dag");
let results = TestRunner::new(&dag).run_suite("suite");

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:?}"
);
}

#[test]
fn mock_backed_invariant_predicate_accepts_declaration_ref_like_lens_output_equals() {
let source = r#"
Expand Down
Loading
Loading