Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
10,290 changes: 5,189 additions & 5,101 deletions src/v3/compiler/src/bootstrap_generated.rs

Large diffs are not rendered by default.

7,716 changes: 3,902 additions & 3,814 deletions src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs

Large diffs are not rendered by default.

107 changes: 107 additions & 0 deletions src/v3/compiler/src/test_runner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2571,6 +2571,9 @@
}
"RatchetZero" => self.eval_ratchet_zero_shape(claim, &payload),
"BridgeLedgerZero" => self.eval_bridge_ledger_zero(claim, &payload),
"TestCostDimensionDeclared" => {
self.eval_test_cost_dimension_declared(claim, &payload)
}
"GeneratedFromDag" => self.eval_generated_from_dag_shape(claim, &payload),
"ReleaseDeferredClaim" => {
self.eval_release_deferred_claim_shape(claim, &payload)
Expand Down Expand Up @@ -4854,6 +4857,110 @@
}
}

/// `TestPredicate::TestCostDimensionDeclared { node_ref: DeclarationRef }`.
fn eval_test_cost_dimension_declared(
&self,
_claim: &TestClaimValue,
payload: &[FieldValue],
) -> ClaimResult {
let [node_fv] = payload else {
return ClaimResult::Fail(format!(
"TestCostDimensionDeclared payload should be exactly one DeclarationRef field \
(node_ref); got {} payload slot(s)",
payload.len()
));
};
let node_id = match self.resolve_declaration_ref_id(node_fv, "node_ref") {
Ok(id) => id,
Err(msg) => return ClaimResult::Fail(msg),
};
let node_decl = self.dag.declaration(node_id);
let node_name = decl_display_name(node_id, node_decl);
match self.decl_inhabits_named_role(node_decl, "TestNode") {
Ok(true) => {}
Ok(false) => {
return ClaimResult::Fail(format!(
"TestCostDimensionDeclared: node_ref `{node_name}` must inhabit TestNode"
));
}
Err(msg) => return ClaimResult::Fail(format!("TestCostDimensionDeclared: {msg}")),
}
let Some(fields) = structural_fields(node_decl) else {
return ClaimResult::Fail(format!(
"TestCostDimensionDeclared: node_ref `{node_name}` is not structural"
));
};
let Some(FieldValue::Reference(_)) = field(fields, "claim") else {
return ClaimResult::Fail(format!(
"TestCostDimensionDeclared: node_ref `{node_name}` must carry a `claim: TestClaim` reference"
));
};
let Some(cost) = field(fields, "cost") else {
return ClaimResult::Fail(format!(
"TestCostDimensionDeclared: node_ref `{node_name}` is missing `cost`"
));
};
let cost_fields = match cost {
FieldValue::Reference(cost_id) => {
let cost_decl = self.dag.declaration(*cost_id);
let Some(fields) = structural_fields(cost_decl) else {
return ClaimResult::Fail(format!(
"TestCostDimensionDeclared: node_ref `{node_name}` cost reference `{}` must resolve to a Dimension<TestCost, Int> record",
decl_display_name(*cost_id, cost_decl)
));
};
fields
}
other => {
let Some(fields) = record_fields(other) else {
return ClaimResult::Fail(format!(
"TestCostDimensionDeclared: node_ref `{node_name}` cost must resolve to a Dimension<TestCost, Int> record"
));
};
fields
}
};
let Some(FieldValue::Literal(LiteralBits::Int(value_s))) = field(cost_fields, "value")
else {
return ClaimResult::Fail(format!(
"TestCostDimensionDeclared: node_ref `{node_name}` cost must carry an Int `value`"
));
};
if let FieldValue::Reference(cost_id) = cost {
let cost_decl = self.dag.declaration(*cost_id);
match &cost_decl.connective {

Check failure on line 4931 in src/v3/compiler/src/test_runner.rs

View workflow job for this annotation

GitHub Actions / v3

you seem to be trying to use `match` for destructuring a single pattern. Consider using `if let`
TypeConnective::Instantiation {
template,
arguments,
} => {
let template_name = self.dag.declaration(*template).name.clone();
let args_match = matches!(
arguments.as_slice(),
[unit, carrier]
if self.type_ref_normalizes_to_named(unit.value, "TestCost")
&& self.type_ref_normalizes_to_named(carrier.value, "Int")
);
if template_name.as_deref() != Some("Dimension") || !args_match {
return ClaimResult::Fail(format!(
"TestCostDimensionDeclared: cost reference `{}` must be typed Dimension<TestCost, Int>",
decl_display_name(*cost_id, cost_decl)
));
}
}
_ => {}
}
}
match value_s.parse::<i64>() {
Ok(value) if value >= 0 => ClaimResult::Pass,
Ok(value) => ClaimResult::Fail(format!(
"TestCostDimensionDeclared: node_ref `{node_name}` cost must be nonnegative, got {value}"
)),
Err(_) => ClaimResult::Fail(format!(
"TestCostDimensionDeclared: node_ref `{node_name}` cost value `{value_s}` is not a valid i64"
)),
}
}

fn eval_generated_from_dag_shape(
&self,
_claim: &TestClaimValue,
Expand Down
36 changes: 36 additions & 0 deletions src/v3/compiler/tests/dag/t_wad_test_cost_dimension_landed.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
// T-WAD FULL R3 gate #101 — cost dimension on test nodes.

module v3.compiler.tests.t_wad.test_cost_dimension_landed

import v3.std.dimensions { Dimension }
import std.verification { TestClaim, TestCost, TestNode, TestSuite }

data modeled_test_claim: TestClaim = {
name: "modeled test claim compiles",
source: "let answer: Int = 1 + 1",
file_name: "t_wad_modeled_test_claim.v3",
predicate: Compiles,
requires: []
}

data modeled_test_cost: Dimension<TestCost, Int> = {
value: 2
}

data modeled_test_node: TestNode = {
claim: modeled_test_claim,
cost: modeled_test_cost
}

data test_cost_dimension_landed: TestClaim = {
name: "test_cost_dimension_landed",
source: "let receipt: Int = 1",
file_name: "t_wad_test_cost_dimension_landed.v3",
predicate: TestCostDimensionDeclared { node_ref: modeled_test_node },
requires: []
}

data suite_t_wad_test_cost_dimension_landed: TestSuite = {
name: "t-wad/test_cost_dimension_landed",
claims: [Enumerated(test_cost_dimension_landed)]
}
13 changes: 13 additions & 0 deletions src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -169,6 +169,19 @@ fn t_pb_b_1_contract_port_cost_suite_passes_through_runner() {
run_suite_all_pass(&dag, "suite_contract_port_and_cost");
}

#[test]
fn t_wad_test_cost_dimension_landed_suite_passes_through_runner() {
let dag = lower(
include_str!("../dag/t_wad_test_cost_dimension_landed.dag"),
"src/v3/compiler/tests/dag/t_wad_test_cost_dimension_landed.dag",
);
run_suite_all_pass_with_expected_claim_names(
&dag,
"suite_t_wad_test_cost_dimension_landed",
&["test_cost_dimension_landed"],
);
}

#[test]
fn r3_fieldproject_dual_authority_dissolution_suite_passes_through_runner() {
let dag = lower(
Expand Down
20 changes: 20 additions & 0 deletions src/v3/std/verification.dag
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ module std.verification
import std.list { List, map }
import std.types { FilePath, NonEmptyStr }
import v3.std.substrate { ComparisonOp }
import v3.std.dimensions { Dimension }
import v3.spec.v3_l1 { DeclarationRef }
import v3.std.resources { ResourceReference }
import v3.std.bridge_ledger { BridgeLedgerRef }
Expand Down Expand Up @@ -132,6 +133,17 @@ type ProgramShape
file_name: String
}

// T-WAD FULL R3 gate #101 (`test_cost_dimension_landed`): test nodes carry
// their own `Cost` dimension so the slow-test ratchet can consume structural
// data instead of a side file. This is distinct from the compiler's
// `SymbolicCost` lens over target programs.
type TestCost

type TestNode {
claim: TestClaim
cost: Dimension<TestCost, Int>
}

type TestPredicate
= Compiles
| FailsWithDiagnostic(DiagnosticReference)
Expand Down Expand Up @@ -348,6 +360,14 @@ type TestPredicate
| BridgeLedgerZero {
ledger: BridgeLedgerRef
}
// 🟢 TERMINAL at T-WAD Slice 8 substrate-shape scope. The referenced
// declaration must be a `TestNode` with a declared `cost:
// Dimension<TestCost, Int>` value. The runner validates shape only; policy
// over high-cost / slow-test thresholds belongs to sibling gate
// `slow_test_exemptions_dissolved`.
| TestCostDimensionDeclared {
node_ref: DeclarationRef
}

// Structural runner input role for predicates whose input is the compiled
// `TestClaim.source` program.
Expand Down
Loading