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
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
2 changes: 1 addition & 1 deletion DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -169,4 +169,4 @@ still a violation) · internal review finds missing tests, external review finds

- `cargo test --workspace` · `cargo clippy --all-targets -- -D warnings` · `cargo fmt --all --check`
- one-time: `git config core.hooksPath .githooks` (pre-push runs `cargo fmt`)
- CI floor is one binary: `cargo run -p ci_claim_gate --release -- --source-root src/v2 --roster-from-discovery --scan-dir src/v2/test`
- CI floor is one binary: `cargo run -p ci_claim_gate --release -- --source-root src/v2 --roster-from-discovery --scan-dir src/v2/test` — also enforces v2 `.dag` filename hygiene (no `__` in basenames; use subdirectories)
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// src/v2/test/claim/lens_affected_set/edit_locus_resolver.dag
// src/v2/lens/affected_set/edit_locus_resolver_test.dag
// Scope: git diff → edit_locus Node resolver receipts (path-regex bindings).
// Status: T-21 wire claim; host git projection lands with BinaryShim runner.

Expand Down Expand Up @@ -46,7 +46,7 @@ import v2.std.verification {
UnifiedTestClaim
}
data edit_locus_path_src_v4_affected_set: RepoPath = "src/v2/lens/affected_set.dag"
data edit_locus_path_source_producer_fixture: RepoPath = "src/v2/test/claim/lens_affected_set/source_producer_fixture.dag"
data edit_locus_path_source_producer_fixture: RepoPath = "src/v2/lens/affected_set/source_producer_fixture.dag"
data edit_locus_source_producer_fixture_compilation_unit: Symbol = ^edit_locus_source_producer_fixture_compilation_unit
data edit_locus_path_unknown: RepoPath = "src/v2/lens/unknown_path.dag"
data edit_locus_pattern_v4_lens: PathRegex = edit_locus_pattern_v4_lens
Expand Down Expand Up @@ -279,7 +279,7 @@ data edit_locus_narrow_resolution_holds_symbol: Symbol = edit_locus_narrow_resol
// Co-located with `edit_locus_narrow_resolution_holds` so glob discovery finds the witness without the central roster.
data unified_claim_edit_locus_narrow: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/lens_affected_set/edit_locus_resolver.dag",
entry: "src/v2/lens/affected_set/edit_locus_resolver_test.dag",
function: edit_locus_narrow_resolution_holds
}
}
Expand All @@ -288,7 +288,7 @@ data unified_claim_edit_locus_narrow: UnifiedTestClaim = BoolWitnessClaim {
// Co-located with `edit_locus_fail_closed_holds` so glob discovery finds the witness without the central roster.
data unified_claim_edit_locus_fail_closed: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/lens_affected_set/edit_locus_resolver.dag",
entry: "src/v2/lens/affected_set/edit_locus_resolver_test.dag",
function: edit_locus_fail_closed_holds
}
}
Expand All @@ -297,7 +297,7 @@ data unified_claim_edit_locus_fail_closed: UnifiedTestClaim = BoolWitnessClaim {
// Co-located with `edit_locus_source_provenance_producer_holds` so glob discovery finds the witness without the central roster.
data unified_claim_edit_locus_source_provenance_producer: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/lens_affected_set/edit_locus_resolver.dag",
entry: "src/v2/lens/affected_set/edit_locus_resolver_test.dag",
function: edit_locus_source_provenance_producer_holds
}
}
Expand All @@ -306,7 +306,7 @@ data unified_claim_edit_locus_source_provenance_producer: UnifiedTestClaim = Boo
// Co-located with `edit_locus_source_provenance_affected_set_wire_holds` so glob discovery finds the witness without the central roster.
data unified_claim_edit_locus_source_provenance_affected_set_wire: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/lens_affected_set/edit_locus_resolver.dag",
entry: "src/v2/lens/affected_set/edit_locus_resolver_test.dag",
function: edit_locus_source_provenance_affected_set_wire_holds
}
}
Expand All @@ -315,7 +315,7 @@ data unified_claim_edit_locus_source_provenance_affected_set_wire: UnifiedTestCl
// Co-located with `edit_locus_source_provenance_producer_rejects_malformed_source_holds` so glob discovery finds the witness without the central roster.
data unified_claim_edit_locus_source_provenance_producer_rejects_malformed_source: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/lens_affected_set/edit_locus_resolver.dag",
entry: "src/v2/lens/affected_set/edit_locus_resolver_test.dag",
function: edit_locus_source_provenance_producer_rejects_malformed_source_holds
}
}
2 changes: 1 addition & 1 deletion scripts/v2-spice-ngspice-rc-oracle.sh
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ else
exit 77
fi

claim_entry="$root/src/v2/test/claim/formats/spice_rc_ngspice_oracle.dag"
claim_entry="$root/src/v2/extdeps/formats/spice_rc_ngspice_oracle_test.dag"

# Step 1: emit correctness — exit code is the sole authority.
# --claim-run exits 0 when the witness Bool is true, 1 when false.
Expand Down
2 changes: 1 addition & 1 deletion src/v1/stage0/src/bin/claim_executor.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
//! Batch claim executor: the host transport for the v2.workflow.executor .dag.
//!
//! The `.dag` is the batching AUTHORITY. A plan function (default
//! `bre_claim_batches` in `src/v2/test/claim/workflow/batch_runner.dag`) folds
//! `bre_claim_batches` in `src/v2/workflow/batch_runner.dag`) folds
//! the dependency frontier through `v2.workflow.executor` and returns
//! `List<List<ClaimRef>>` — the outer list is batches in execution order, the
//! inner list is the claims runnable in parallel within that batch. This binary
Expand Down
2 changes: 1 addition & 1 deletion src/v1/tests/src/coproduct_reflection_conformance_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use v1_compiler::v1_interpreter::{self, Value};

use crate::helpers::{resolve_imports_transitively_with_source_roots, workspace_root};

const CONFORMANCE_ENTRY: &str = "src/v2/test/claim/manual/coproduct_reflection_conformance.dag";
const CONFORMANCE_ENTRY: &str = "src/v2/compiler/manual/coproduct_reflection_conformance.dag";
const WITNESS_FN: &str = "coproduct_reflection_conformance_holds";

fn v2_source_roots() -> Vec<std::path::PathBuf> {
Expand Down
2 changes: 1 addition & 1 deletion src/v1/tests/src/fold_list_generic_instantiation_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ use v1_compiler::v1_interpreter::{self, Value};

use crate::helpers::{resolve_imports_transitively_with_source_roots, workspace_root};

const CERT_ENTRY: &str = "src/v2/test/claim/manual/fold_list_generic_instantiation.dag";
const CERT_ENTRY: &str = "src/v2/compiler/manual/fold_list_generic_instantiation.dag";
const WITNESS_FN: &str = "fold_list_generic_instantiation_holds";

fn v2_source_roots() -> Vec<std::path::PathBuf> {
Expand Down
2 changes: 1 addition & 1 deletion src/v1/tests/src/interpreted_parse_termination_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ use v1_compiler::v1_interpreter::{self, Value};

use crate::helpers::{resolve_imports_transitively_with_source_roots, workspace_root};

const BISECT_ENTRY: &str = "src/v2/test/claim/manual/validate_ingest_staging_stage_bisect.dag";
const BISECT_ENTRY: &str = "src/v2/compiler/manual/validate_ingest_staging_stage_bisect.dag";

fn v2_source_roots() -> Vec<std::path::PathBuf> {
vec![workspace_root().join("src/v2")]
Expand Down
2 changes: 1 addition & 1 deletion src/v1/tests/src/map_lookup_dual_dispatch_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ fn probe() -> Int {

// NB: the native-map-miss -> `Witness` `Violates` bridge (runtime completeness for the
// `Map.lookup: fn(K) -> Witness<V>` contract) is regression-tested at the v2 layer in
// src/v2/test/claim/manual/map_lookup_miss_witness_violates.dag — the bootstrap
// src/v2/compiler/manual/map_lookup_miss_witness_violates_test.dag — the bootstrap
// typechecker projects a raw `.lookup` result as Option (Some/None) unless it flows
// through a `-> Witness` annotated wrapper, which the std `Map` contract provides but a
// bare v2-harness fixture (no v2.std) cannot.
4 changes: 2 additions & 2 deletions src/v1/tests/src/nodefold_generic_instantiation_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ use v1_compiler::v1_interpreter::{self, Value};

use crate::helpers::{resolve_imports_transitively_with_source_roots, workspace_root};

const NODEFOLD_CERT: &str = "src/v2/test/claim/manual/nodefold_topdown_inline_algebra.dag";
const CHAINED_CERT: &str = "src/v2/test/claim/manual/chained_generic_field_access.dag";
const NODEFOLD_CERT: &str = "src/v2/compiler/manual/nodefold_topdown_inline_algebra.dag";
const CHAINED_CERT: &str = "src/v2/compiler/manual/chained_generic_field_access.dag";

fn v2_source_roots() -> Vec<std::path::PathBuf> {
vec![workspace_root().join("src/v2")]
Expand Down
2 changes: 1 addition & 1 deletion src/v1/tests/src/r2_emit_add_named_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ use v1_compiler::v1_interpreter::{self, Value};

use crate::helpers::{resolve_imports_transitively_with_source_roots, workspace_root};

const CERT_ENTRY: &str = "src/v2/test/claim/manual/mvp1_rust_add_translate.dag";
const CERT_ENTRY: &str = "src/v2/compiler/manual/mvp1_rust_add_translate_test.dag";
const WITNESS_FN: &str = "mvp1_rust_emit_add_fn_accepts_holds";

/// The exact canonical Rust source the R2 keystone pins (rust.dag:rust_mvp1_source_text).
Expand Down
2 changes: 1 addition & 1 deletion src/v1/tests/src/target_model_runtime_import_repro.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ use v1_compiler::v1_compiler_compile::{compile_to_resolved, SourceFile};
use crate::helpers::{resolve_imports_transitively_with_source_roots, workspace_root};

const TARGET_MODEL: &str = "src/v2/std/compilers/target_model.dag";
const CLAIM_ENTRY: &str = "src/v2/test/claim/manual/mvp1_rust_add_translate.dag";
const CLAIM_ENTRY: &str = "src/v2/compiler/manual/mvp1_rust_add_translate_test.dag";

#[derive(Clone, Copy, PartialEq, Eq)]
enum TargetModelPatch {
Expand Down
4 changes: 2 additions & 2 deletions src/v1/tests/src/typescript_effect_io_receipt_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
//! (`target_value_expression_effect_apply` → `target_value_expression_to_concrete_tokens`'s
//! `TargetValueExprEffectApply` arm → `serialize_concrete_syntax_tokens_to_source`). It drives
//! the real v2 compile+interpret pipeline over
//! `src/v2/test/claim/manual/typescript_effect_io_emit.dag` to obtain the COMPILER-EMITTED
//! `src/v2/compiler/manual/typescript_effect_io_emit.dag` to obtain the COMPILER-EMITTED
//! TypeScript call expressions for an applied `WriteResource` and an applied `ReadResource`,
//! then assembles a node-runnable program in which the two host-shim callees
//! (`__gunbc_effect_write` / `__gunbc_effect_read`) are bound to `fs.writeFileSync` /
Expand All @@ -26,7 +26,7 @@ use v1_compiler::v1_interpreter::{self, InterpContext, Value};

use crate::helpers::{resolve_imports_transitively_with_source_roots, workspace_root};

const WITNESS_ENTRY: &str = "src/v2/test/claim/manual/typescript_effect_io_emit.dag";
const WITNESS_ENTRY: &str = "src/v2/compiler/manual/typescript_effect_io_emit.dag";
const WRITE_FN: &str = "ts_effect_write_call_source";
const READ_FN: &str = "ts_effect_read_call_source";

Expand Down
2 changes: 1 addition & 1 deletion src/v1/tests/src/value_carrier_swap_test.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
//! ctrl#1533 phase 2 — persistent-carrier swap probes.
//!
//! The v2.std.value_carrier sharing/identity laws have executable witnesses
//! in src/v2/test/claim/std_grounding/value_carrier_laws.dag; those run at
//! in src/v2/std/grounding/value_carrier_laws_test.dag; those run at
//! small n. These probes cover what the witnesses cannot: collection sizes
//! past the carriers' inline-chunk thresholds (so HAMT/RRB tree nodes are
//! actually exercised), prior-version validity after derived updates (the
Expand Down
2 changes: 1 addition & 1 deletion src/v1/tests/src/witness_option_bridge_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -222,7 +222,7 @@ fn rejects_custom_lookup_failure() -> Bool {

#[test]
fn mark_excluded_no_longer_pattern_match_fails() {
let entry = "src/v2/test/claim/lens_affected_set/excluded_propagation_proof.dag";
let entry = "src/v2/lens/affected_set/excluded_propagation_proof.dag";
let content = std::fs::read_to_string(workspace_root().join(entry))
.unwrap_or_else(|e| panic!("read {entry}: {e}"));
// Returns Bool (true or false) — the pre-fix crash was PatternMatchFailure on Holds.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -49,31 +49,31 @@ data perturb_row_std_prefix: LayeringImportsScannerPerturbReceiptRow = LayeringI
label: "src/v2/std × v2.compiler.* prefix",
layer_root: layer_root_src_v2_std,
forbidden_form: form_v2_compiler_prefix,
scanner_entry: "src/v2/compiler/layering_imports__scanner__std_v4_prefix.dag",
scanner_entry: "src/v2/compiler/layering_imports/scanner/std_v4_prefix.dag",
scanner_function: "scanner_std_v4_prefix_detects_holds"
}

data perturb_row_extdeps_prefix: LayeringImportsScannerPerturbReceiptRow = LayeringImportsScannerPerturbReceiptRow {
label: "src/v2/extdeps × v2.compiler.* prefix",
layer_root: layer_root_src_v2_extdeps,
forbidden_form: form_v2_compiler_prefix,
scanner_entry: "src/v2/compiler/layering_imports__scanner__extdeps_v4_prefix.dag",
scanner_entry: "src/v2/compiler/layering_imports/scanner/extdeps_v4_prefix.dag",
scanner_function: "scanner_extdeps_v4_prefix_detects_holds"
}

data perturb_row_dsl_extdeps_exact: LayeringImportsScannerPerturbReceiptRow = LayeringImportsScannerPerturbReceiptRow {
label: "dsl/extdeps × v2.compiler exact",
layer_root: layer_root_dsl_extdeps,
forbidden_form: form_v2_compiler_exact,
scanner_entry: "src/v2/compiler/layering_imports__scanner__dsl_extdeps_v4_exact.dag",
scanner_entry: "src/v2/compiler/layering_imports/scanner/dsl_extdeps_v4_exact.dag",
scanner_function: "scanner_dsl_extdeps_v4_exact_detects_holds"
}

data perturb_row_parse_level_pre_resolve: LayeringImportsScannerPerturbReceiptRow = LayeringImportsScannerPerturbReceiptRow {
label: "src/v2/std parse-level pre-resolve text scan",
layer_root: layer_root_src_v2_std,
forbidden_form: form_v2_compiler_prefix,
scanner_entry: "src/v2/compiler/layering_imports__scanner__parse_level_pre_resolve.dag",
scanner_entry: "src/v2/compiler/layering_imports/scanner/parse_level_pre_resolve.dag",
scanner_function: "scanner_parse_level_pre_resolve_detects_holds"
}

Expand Down
File renamed without changes.
Original file line number Diff line number Diff line change
Expand Up @@ -448,126 +448,126 @@ data witness_integer_interval_bound_compare_orders_pointer_width_bounds: Bool =

data unified_claim_project_to_core_accepts_sibling: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_project_to_core_real_dispatch_accepts_sibling
}
}

data unified_claim_project_to_core_rejects_wrong_core: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_project_to_core_real_dispatch_rejects_wrong_core
}
}

data unified_claim_project_to_core_rejects_empty_core: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_project_to_core_rejects_surface_only_empty_core
}
}

data unified_claim_project_to_core_rejects_surface_wrapped_core: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_project_to_core_rejects_core_only_under_surface
}
}

data unified_claim_project_to_core_preserves_ambiguity: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_project_to_core_derives_preserves_ambiguity
}
}

data unified_claim_project_to_core_drops_nested_surface: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_project_to_core_drops_nested_surface
}
}

data unified_claim_project_to_core_rejects_nested_core_difference: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_project_to_core_rejects_nested_core_difference
}
}

data unified_claim_project_to_core_rejects_different_connective_same_core_children: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_project_to_core_rejects_different_connective_same_core_children
}
}

data unified_claim_integer_value_set_accepts_subset: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_integer_value_set_accepts_i32_subset_python_int
}
}

data unified_claim_integer_value_set_accepts_proper_subrange: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_integer_value_set_accepts_i16_subset_i32
}
}

data unified_claim_integer_value_set_accepts_cross_signed_subrange: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_integer_value_set_accepts_u8_subset_i16
}
}

data unified_claim_integer_value_set_rejects_malformed_interval: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_integer_value_set_rejects_malformed_interval_payload
}
}

data unified_claim_integer_value_set_interval_rejects_malformed_interval: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_integer_value_set_interval_containment_rejects_malformed_payload
}
}

data unified_claim_integer_value_set_reverse_strict: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_integer_value_set_reverse_is_strict_coarsening
}
}

data unified_claim_integer_value_set_refuses_incompatible: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_integer_value_set_refuses_incompatible_unknown
}
}

data unified_claim_refinement_widening_refuses_semantically_equal_value_sets: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_refinement_widening_refuses_semantically_equal_value_sets
}
}

data unified_claim_integer_interval_bound_compare_orders_pointer_width_bounds: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_integer_interval_bound_compare_orders_pointer_width_bounds
}
}

data unified_claim_integer_value_set_rejects_unbounded_with_extra_field: UnifiedTestClaim = BoolWitnessClaim {
witness: BoolWitness {
entry: "src/v2/test/claim/manual/find_witness_project_to_core_controls.dag",
entry: "src/v2/compiler/manual/find_witness_project_to_core_controls.dag",
function: witness_integer_value_set_rejects_unbounded_with_extra_field
}
}
Loading