Skip to content
Merged
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
29 changes: 29 additions & 0 deletions dsl/std/verification.dag
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,8 @@

module std.verification

import std.types { Milliseconds }

// The predicate form of an assertion.
// Each variant corresponds to a standard verification predicate
// that every test framework supports.
Expand All @@ -38,10 +40,37 @@ type TestClaim {
label: String
}

// R3 T-Workflow-As-Data gate #101 (`test_cost_dimension_landed`).
//
// Test execution cost is a first-class structural fact attached to a
// modeled test node. This deliberately does not reuse compiler-internal
// `SymbolicCost`: the slow-test ratchet needs observed/budgeted wall-clock
// cost for the test node itself, so #102 can derive exemption status from
// substrate instead of `scripts/slow-test-exemptions.txt`.
//
// Legacy dsl projection note: this tree does not carry T-WAD's v3
// `TimingBudget` / `TimingMeasurement` / `Nanoseconds` substrate yet.
// The bootstrap-local v3 authority (`src/v3/std/verification.dag`) is the
// convergence shape. These `_ms` fields use the existing branded
// non-negative `Milliseconds` carrier as the older dsl projection of that
// same timing fact, not a parallel cost algebra.
// Retirement trigger: #102 (`slow_test_exemptions_dissolved`) consumes the v3
// `Nanoseconds` timing authority for the slow-test ratchet, then deletes or
// rewires this dsl projection instead of extending it.

// A named test case — a conjunction of claims.
// All claims must hold for the test to pass.
type TestCase {
name: String
claims: List<TestClaim>
ignored: Bool
}

type TestNodeRef
= TestCaseNode(TestCase)

type TestNodeCostDimension {
node: TestNodeRef
budget_ms: Milliseconds
measured_ms: Milliseconds
}
Loading
Loading