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
2 changes: 1 addition & 1 deletion dsl/gunbc/ci_spec.dag
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,7 @@ fn ci_rust_gate_test_command() -> String {
// known-green subset. The `--` is required: `cargo test` accepts a single
// positional TESTNAME, so a second bare filter errors ("unexpected argument");
// multiple substring filters must follow `--` to reach the test binary.
"cargo test -p v1-compiler-tests -- interp_recorded_fixture resolve_expr_types_retraversal"
"cargo test -p v1-compiler-tests -- interp_recorded_fixture wet_hermetic resolve_expr_types_retraversal"
}

fn claim_executor_bin_shell() -> String {
Expand Down
31 changes: 19 additions & 12 deletions dsl/std/realization_width.dag
Original file line number Diff line number Diff line change
Expand Up @@ -23,9 +23,12 @@ module std.realization_width
import std.types { Int, List }
import std.measure {
HardwareThreadCount,
NanosecondDuration,
Nano,
hardware_thread_count,
hardware_thread_count_value,
}
import std.verification {
NanosecondDuration,
nanosecond_duration,
}
import std.pareto { AxisGoal, LowerIsBetter }
Expand All @@ -36,9 +39,13 @@ import std.realization_schedule {
CostAccount,
CostBasis,
schedule_eq,
cost_account_measured,
cost_account_predicted_zero,
cost_account_time_nanos,
cost_account_time_count,
}
import std.realization_measurement { cost_account_measured_from_time }

fn cost_account_predicted_zero_nano() -> CostAccount<Nano> {
cost_account_predicted_zero()
}

fn int_min(a: Int, b: Int) -> Int {
Expand Down Expand Up @@ -72,13 +79,13 @@ fn width_fold_objective_goals() -> List<AxisGoal> {
}

type WidthBoundedRealization {
plan: RealizationPlan
plan: RealizationPlan<Nano>
spawn_width: HardwareThreadCount
}

// Width is peripheral: the schedule topology is unchanged (§3 invariant).
fn width_bounded_realization(
plan: RealizationPlan,
plan: RealizationPlan<Nano>,
shard_count: Int,
hardware_threads: HardwareThreadCount
) -> WidthBoundedRealization {
Expand All @@ -89,7 +96,7 @@ fn width_bounded_realization(
}

fn witness_width_fold_preserves_schedule_topology(
plan: RealizationPlan,
plan: RealizationPlan<Nano>,
shard_count: Int,
hardware_threads: HardwareThreadCount
) -> Bool {
Expand Down Expand Up @@ -123,18 +130,18 @@ fn witness_budget_ignoring_fold_fails(
}

// Measured shard-balance scaffold: assignment must read CostAccount.basis=Measured.
fn shard_balance_slot_for_cost(cost: CostAccount, baseline: CostAccount) -> Int {
fn shard_balance_slot_for_cost(cost: CostAccount<Nano>, baseline: CostAccount<Nano>) -> Int {
match cost.basis {
Measured => cost_account_time_nanos(account: cost)
Predicted => cost_account_time_nanos(account: baseline)
Measured => cost_account_time_count(account: cost)
Predicted => cost_account_time_count(account: baseline)
}
}

// RED guard (b): asymmetric measured costs must yield different slot assignments.
fn witness_measured_cost_affects_shard_balance() -> Bool {
let high = cost_account_measured(time: nanosecond_duration(count: 100))
let low = cost_account_measured(time: nanosecond_duration(count: 10))
let baseline = cost_account_predicted_zero()
let high = cost_account_measured_from_time(time: nanosecond_duration(count: 100))
let low = cost_account_measured_from_time(time: nanosecond_duration(count: 10))
let baseline = cost_account_predicted_zero_nano()
let left = shard_balance_slot_for_cost(cost: high, baseline: baseline)
let right = shard_balance_slot_for_cost(cost: low, baseline: baseline)
left != right
Expand Down
11 changes: 8 additions & 3 deletions dsl/test/claim/realization_width_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,13 @@

module test.claim.realization_width_witness

import std.measure { HardwareThreadCount, hardware_thread_count, hardware_thread_count_value }
import std.measure { HardwareThreadCount, Nano, hardware_thread_count, hardware_thread_count_value }
import std.realization_schedule {
RealizationPlan,
RealizationObjective,
Runnable,
RunnableSingleClaim,
CostAccount,
cost_account_predicted_zero,
}
import std.realization {
Expand All @@ -34,7 +35,11 @@ fn witness_threads_4() -> HardwareThreadCount {
hardware_thread_count(4)
}

fn synthetic_plan() -> RealizationPlan {
fn synthetic_plan_total() -> CostAccount<Nano> {
cost_account_predicted_zero()
}

fn synthetic_plan() -> RealizationPlan<Nano> {
RealizationPlan {
target: "width-witness-target"
objective: RealizationObjective { goals: [] }
Expand All @@ -44,7 +49,7 @@ fn synthetic_plan() -> RealizationPlan {
RunnableSingleClaim { entry: gate_entry, function: "rust_monolith_gate_passes" }
]
]
total: cost_account_predicted_zero()
total: synthetic_plan_total()
}
}

Expand Down
24 changes: 24 additions & 0 deletions dsl/test/claim/wet_hermetic_equivalence_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
// dsl/test/claim/wet_hermetic_equivalence_witness_test.dag
//
// 🟡 SCAFFOLD (§6) — P3c wet/hermetic equivalence roster pin + comparator wiring.
// Dissolution-on-arrival: gains real teeth when the first live-transport +
// published-mock witness lands (wet = live call, hermetic = published mock);
// until then the lens_mock_totality roster contains no eval_service_call
// dispatcher and the by-execution roster check is vacuous-by-construction.
//
// Enrolled Rust consumers (CI via gunbc.ci_spec.ci_rust_gate_test_command):
// * wet_hermetic_comparator_* — comparator unit teeth (Pass vs Fail divergence)
// * wet_hermetic_scaffold_roster_filter_uses_dag_prefix_authority — prefix drift RED
// * wet_hermetic_scaffold_roster_outcomes_agree — roster run (structural green only)

module test.claim.wet_hermetic_equivalence_witness

// Single authority (§3): Rust `wet_hermetic_scaffold_roster_entry_prefix` reads this
// data binding; do not duplicate the path in hand-Rust substring filters.
// Pin: one `test fn` per extdeps published-mock layer (18 witnesses today).
data wet_hermetic_equivalence_representative_prefix: String = "src/v2/test/lens_mock_totality/"

test fn wet_hermetic_equivalence_roster_authority_is_pinned() -> Bool {
wet_hermetic_equivalence_representative_prefix.starts_with("src/v2/test/")
&& wet_hermetic_equivalence_representative_prefix.ends_with("lens_mock_totality/")
}
11 changes: 5 additions & 6 deletions src/v1/stage0/src/bin/claim_batch.rs
Original file line number Diff line number Diff line change
Expand Up @@ -221,9 +221,8 @@ struct ParsedArgs {
source_roots: Vec<String>,
entry_groups: Vec<EntryGroup>,
discovery: Option<DiscoveryConfig>,
/// Witness execution mode. Phase 1 default: Wet (CI unchanged).
/// `--hermetic` replays recorded fixtures when `--fixture-store` is set, else
/// modeled `mock_response`; `--record` is wet capture into the fixture store.
/// Witness execution mode. Phase 2 default: Hermetic (CI floor). `--wet` opts into
/// live dispatch for real-I/O witnesses; `--hermetic` is explicit parity with default.
execution_mode: ExecutionMode,
/// Directory for recorded fixture JSON files (`--fixture-store <path>`).
fixture_store: Option<PathBuf>,
Expand All @@ -241,9 +240,9 @@ fn parse_args(args: &[String]) -> Result<ParsedArgs, ExitCode> {
let mut roster_from_discovery = false;
let mut scan_dirs: Vec<String> = Vec::new();
let mut notice_title = "v2 CI claim gate".to_string();
// Phase 1: default Wet so CI behavior is unchanged. Phase 2 flips default
// to Hermetic; `--wet` then opts into live dispatch for real-I/O witnesses.
let mut execution_mode = ExecutionMode::Wet;
// Phase 2: default Hermetic for CI floor (P3c equivalence gate green). `--wet` opts
// into live dispatch for real-I/O witnesses.
let mut execution_mode = ExecutionMode::Hermetic;
let mut fixture_store: Option<PathBuf> = None;

let mut i = 1;
Expand Down
7 changes: 6 additions & 1 deletion src/v1/stage0/src/bin/claim_executor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -294,6 +294,7 @@ fn run_single_claim(source_roots: &[String], entry: String, function: String) ->
}
};
// Context scoped to this claim's graph: its `data` cache drops with it.
// Effectful gate transports (shell.Exec, Filesystem.*) require Wet dispatch.
let ctx = make_eval_context(&graph, source_indices, ExecutionMode::Wet);
match run_claim(&ctx, &function) {
ClaimOutcome::Pass => ClaimResult {
Expand Down Expand Up @@ -334,6 +335,10 @@ fn run_discovery_batch_node(
explicit_entries.len(),
spawn_width.max(1),
);
// CI floor discovery still dispatches Wet: many roster witnesses (e.g.
// dsl_compile_clean_witnesses) shell out via shell.Exec.Run and need live
// transport shape. claim_batch CLI default is Hermetic (P3c); executor flip
// waits on full-corpus wet==hermetic equivalence, not just mock_totality.
match run_discovery_corpus(
&source_roots,
&scan_dirs,
Expand Down Expand Up @@ -383,7 +388,7 @@ fn eval_plan(
) -> Result<Vec<Vec<Runnable>>, String> {
let (plan_graph, plan_indices) = resolve_entry_graph(source_roots, plan_entry)
.map_err(|msg| format!("resolve failed for plan {}:\n{}", plan_entry, msg))?;
let plan_ctx = make_eval_context(&plan_graph, plan_indices, ExecutionMode::Wet);
let plan_ctx = make_eval_context(&plan_graph, plan_indices, ExecutionMode::Hermetic);
let plan_value = run_value(&plan_ctx, plan_function).map_err(|msg| {
format!(
"plan eval failed ({}::{}): {}",
Expand Down
Loading
Loading