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
12 changes: 0 additions & 12 deletions dag/test/claim/fleet/fleet_printer_access_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -231,15 +231,3 @@ test fn a_404_over_an_existing_receipt_is_not_read_as_never_provisioned() -> Boo
PrinterCredentialLocusConflicted { printer: _, matches: _ } => false
}
}

test fn fleet_printer_access_witnesses_hold() -> Bool {
printer_access_code_locus_roster_is_the_exact_declared_population()
&& each_printer_locus_names_the_secret_its_canonical_constructor_produces()
&& an_unknown_printer_refuses_instead_of_fabricating_a_secret_locus()
&& duplicate_printer_loci_refuse_instead_of_taking_the_last_row()
&& both_human_retrieval_loci_name_the_observed_auth_gated_drive_resources()
&& a_404_is_read_as_the_container_being_absent()
&& a_status_that_is_not_404_never_becomes_absence()
&& a_present_container_with_no_receipt_is_not_reported_as_absent()
&& a_404_over_an_existing_receipt_is_not_read_as_never_provisioned()
}
Original file line number Diff line number Diff line change
Expand Up @@ -279,18 +279,3 @@ test fn transport_requires_clean_worktree_before_publication() -> Bool {
_ => false
}
}

test fn all_floor_discovery_exact_subject_controls_hold() -> Bool {
exact_subject_binds()
&& wrong_commit_refuses_at_commit_coordinate()
&& wrong_tree_refuses_at_tree_coordinate()
&& source_root_order_is_part_of_the_subject()
&& request_preserves_subject_refusal()
&& wrong_scope_refuses_without_widening()
&& wrong_execution_mode_refuses()
&& exact_request_binds()
&& commit_and_tree_each_move_request_identity()
&& canonical_request_identity_matches_bootstrap_golden()
&& transport_preserves_exact_subject_and_refuses_dirty_worktree()
&& transport_requires_clean_worktree_before_publication()
}
11 changes: 0 additions & 11 deletions dag/test/claim/floor/floor_preparation_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -264,14 +264,3 @@ test fn changed_closure_changes_prepared_artifact_set_identity() -> Bool {
)
canonical.artifact_set_identity.digest != changed.artifact_set_identity.digest
}

test fn all_floor_preparation_controls_hold() -> Bool {
exact_prepared_artifact_set_serves()
&& missing_prepared_identity_refuses()
&& absent_artifact_is_typed_miss_without_cold_fallback()
&& wrong_artifact_key_refuses()
&& duplicate_selected_identity_refuses()
&& duplicate_probe_identity_refuses()
&& unexpected_probe_identity_refuses()
&& changed_closure_changes_prepared_artifact_set_identity()
}
Original file line number Diff line number Diff line change
Expand Up @@ -216,14 +216,3 @@ test fn pcie_refusals_survive_the_candidate_join() -> Bool {
_ => false
}
}

fn main() -> Bool {
real_candidates_reach_typed_verdicts()
&& an_unobserved_ocp_standing_survives_into_the_generation_only_receipt()
&& matching_generation_does_not_establish_physical_variant()
&& unknown_unit_never_borrows_mtcollins1_observation()
&& absent_ocp_bay_cannot_admit_a_matching_card()
&& changed_bay_generation_does_not_relabel_the_candidate()
&& other_ocp2_physical_variants_still_refuse_wrong_generation()
&& pcie_refusals_survive_the_candidate_join()
}
18 changes: 0 additions & 18 deletions dag/test/claim/model/model_population_narrowing_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -256,24 +256,6 @@ test fn w_a_narrowed_stage_refuses_completeness_about_the_open_weight_universe()
question: CompleteForPublisher { publisher: "deepseek-ai" as NonEmptyStr }))
}

// AGGREGATE, so the whole carrier is established in ONE corpus resolve rather than eight. It is a
// conjunction of the individual claims and adds no coverage; it exists because each separate entry
// point re-resolves the corpus, and eight resolves exceed a remote dispatch budget that one fits
// inside. Every conjunct remains independently runnable, so a failure is still located.
test fn w_all_population_claims_hold() -> Bool {
w_ollama_local_absence_does_not_remove_from_the_open_weight_population()
&& w_ollama_cloud_presence_does_not_imply_local_weights_are_unavailable()
&& w_an_empty_narrowing_does_not_remove_from_the_open_weight_population()
&& w_narrowing_cannot_introduce_a_member_the_parent_lacked()
&& w_a_closed_weight_release_is_excluded_from_the_open_weight_population()
&& w_completeness_refuses_when_every_source_is_a_single_distributor()
&& w_completeness_answers_for_the_publisher_whose_catalog_is_held()
&& w_one_publishers_catalog_does_not_answer_for_another_publisher()
&& w_universe_completeness_is_never_answerable()
&& w_a_backward_or_same_stage_transition_refuses()
&& w_a_narrowed_stage_refuses_completeness_about_the_open_weight_universe()
}

// THE DISCRIMINATING CONTROL, kept enrolled. `population_holds` must not be constantly true, or
// every claim above is a conjunction of things that hold by vacuity rather than by the structural
// separation. It asserts both directions in one row: a release the root population does not carry
Expand Down
15 changes: 0 additions & 15 deletions dag/test/claim/model/release_relative_selection_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -218,18 +218,3 @@ test fn w_the_comparator_itself_has_no_cross_release_answer() -> Bool {
Present { value: _ } => false
}
}

test fn w_all_release_relative_selection_claims_hold() -> Bool {
w_no_alternatives_is_its_own_arm()
&& w_a_single_alternative_returns_the_exact_payload_supplied()
&& w_the_higher_rank_wins_in_both_roster_orders()
&& w_negative_ranks_order_without_a_nonnegative_assumption()
&& w_the_comparator_is_total_at_the_bounds_of_int()
&& w_two_releases_have_no_common_scale_in_both_orders()
&& w_the_release_count_counts_releases_and_not_rows()
&& w_a_repeated_release_is_counted_once_when_its_rows_are_not_adjacent()
&& w_an_equal_top_rank_refuses_in_both_orders()
&& w_a_tie_beneath_a_unique_maximum_does_not_refuse()
&& w_a_duplicated_top_alternative_is_not_silently_deduplicated()
&& w_the_comparator_itself_has_no_cross_release_answer()
}
11 changes: 0 additions & 11 deletions dag/test/claim/mt_collins_dimm_physical_identity_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -180,14 +180,3 @@ test fn w_mirror_comparison_rejects_different_unread_and_wrong_subject_receipts(
&& specification_citation_read_byte_standing(publisher: unread, mirror: mt_collins_2u_mirror_citation_read_receipt) == ReadBytesNotComparable
&& specification_citation_read_byte_standing(publisher: mt_collins_2u_publisher_citation_read_receipt, mirror: wrong_subject) == ReadBytesNotComparable
}

fn main() -> Bool {
w_missing_and_duplicate_identities_refuse()
&& w_socket_disagreement_and_role_deficit_refuse()
&& w_duplicate_within_a_row_refuses()
&& w_every_figure_connector_resolves()
&& w_sixteen_dimm_join_keeps_orientation_and_physical_gaps()
&& w_bad_population_never_returns_partial_slots()
&& w_operator_colour_report_is_unit_scoped_and_preserves_documentary_gaps()
&& w_mirror_comparison_rejects_different_unread_and_wrong_subject_receipts()
}
42 changes: 0 additions & 42 deletions dag/test/claim/public_workload_census_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ module test.claim.public_workload_census_witness

import std.types { Bool, List, String, NonEmptyStr }
import std.measure { hardware_thread_count }
import std.process { ProcessExit, ExitSuccess, ExitFailure }
import extdeps.time.rfc3339 { Rfc3339Timestamp }
import extdeps.toolchain.types { X86_64 }
import extdeps.github.workflow_runs {
Expand Down Expand Up @@ -1194,44 +1193,3 @@ test fn witness_mixed_catalog_arm_and_not_arm_alternatives_are_unresolved() -> B
DeclaredNotArm { via, architecture } => false
}
}

fn all_claims_hold() -> Bool {
witness_x64_catalog_label_is_never_arm_evidence()
&& witness_an_unresolved_label_is_not_reported_as_x64()
&& witness_selected_population_is_three_complementary_jobs()
&& witness_rejected_and_unresolved_remain_visible()
&& witness_every_row_is_job_scoped_and_versioned()
&& witness_biome_baseline_is_admitted_and_openobserve_is_not()
&& witness_pdns_declared_architecture_stays_unresolved_while_observed_is_arm()
&& witness_declared_and_observed_providers_are_separate_readings()
&& witness_openobserve_amd64_is_catalog_x64_and_rejected()
&& witness_observed_labels_and_attempt_are_read_from_the_job_resource()
&& witness_unobserved_cache_is_never_warm()
&& witness_effect_disposition_is_derived_from_kind()
&& witness_admitted_same_revision_and_blob_equivalent_hold()
&& witness_blob_mismatch_is_refused_even_when_tests_ran()
&& witness_matrix_selector_mismatch_is_refused_when_display_name_matches()
&& witness_axis_name_mismatch_is_refused_when_values_and_display_name_match()
&& witness_swapped_axis_names_are_refused_when_value_order_matches_the_observed_name()
&& witness_job_key_mismatch_is_refused_when_display_name_and_matrix_match()
&& witness_uninspected_yaml_job_name_is_not_defaulted_to_job_key()
&& witness_multiple_labels_are_not_resolved_from_the_first()
&& witness_a_green_job_without_tests_is_not_a_baseline()
&& witness_empty_labels_are_not_an_architecture_reading()
&& witness_absent_conclusion_is_not_a_baseline()
&& witness_run_attempt_zero_is_not_attempt_one()
&& witness_empty_matrix_axes_do_not_bind_as_empty_parenthetical()
&& witness_plural_yaml_job_name_rows_are_uninspected()
&& witness_unread_job_run_is_unresolved_identity()
&& witness_empty_declared_alternatives_are_unresolved()
&& witness_empty_declared_label_is_unresolved()
&& witness_mixed_catalog_arm_and_not_arm_alternatives_are_unresolved()
}

fn public_workload_census_witness_main() -> ProcessExit {
if all_claims_hold() {
ExitSuccess
} else {
ExitFailure { code: 1, reason: "one or more public workload census claims did not hold" }
}
}
18 changes: 0 additions & 18 deletions dag/test/claim/ray_threshold_memory_monitor_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -187,21 +187,3 @@ fn min_free_is(m: RayMinMemoryFree, wanted: NonEmptyStr) -> Bool {
MinMemoryFreeFloor { bytes: _ } => wanted == ("floor" as NonEmptyStr)
}
}

test fn w_all_ray_threshold_monitor_claims_hold() -> Bool {
w_the_env_spelling_is_the_config_name_with_a_ray_prefix()
&& w_the_config_field_names_are_distinct()
&& w_disabling_the_monitor_is_a_zero_refresh_on_the_derived_spelling()
&& w_the_defaults_are_the_ones_read_at_the_pinned_revision()
&& w_the_swap_counting_knob_is_recorded_as_absent_at_this_revision()
&& w_the_absent_field_is_not_enumerated_as_a_config()
&& w_the_uncapturable_line_does_not_report_a_measurement()
&& w_the_node_and_user_slice_lines_are_distinguishable()
&& w_a_zero_interval_with_isolation_on_still_enforces()
&& w_a_zero_interval_with_isolation_off_enforces_nothing()
&& w_the_default_interval_builds_an_enforcing_threshold_monitor()
&& w_only_the_noop_monitor_does_not_enforce()
&& w_the_lines_that_explain_an_absent_alarm_are_exactly_the_non_measurements()
&& w_the_user_slice_snapshot_failure_is_not_a_measurement()
&& w_the_min_memory_free_default_is_the_disabled_sentinel()
}
13 changes: 0 additions & 13 deletions dag/test/claim/runner/runner_canary_receipt_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -425,16 +425,3 @@ test fn stale_or_wrong_teardown_subjects_refuse() -> Bool {
}
})
}

fn main() -> Bool {
vmm_cannot_observe_its_own_teardown() && changing_observation_instrument_refuses() &&
cross_boot_processes_refuse() && evidence_frontier_is_well_formed() &&
fractional_minutes_preserve_meter_and_exclude_staging() &&
missing_meter_and_initiator_refuse() &&
different_tenant_or_attempt_cannot_supply_usage_or_initiator() &&
invalid_interval_and_cross_clock_refuse() && cpu_clock_meter_refuses() &&
zero_cpu_or_unrecorded_resolution_refuse() &&
independent_present_then_absent_is_accepted() && destroyer_cannot_attest_its_own_teardown() &&
an_always_absent_instrument_refuses() && every_residue_and_unreadable_resource_refuses() &&
missing_observer_receipt_is_detectable() && stale_or_wrong_teardown_subjects_refuse()
}
33 changes: 0 additions & 33 deletions dag/test/claim/runner_label_resolution_witness_test.dag
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
module test.claim.runner_label_resolution_witness_test

import std.types { Bool, List, NonEmptyStr, String }
import std.process { ProcessExit, ExitSuccess, ExitFailure }
import std.decl_ref { DeclarationRef, declaration_ref_eq }
import extdeps.toolchain.types { Aarch64, X86_64 }
import extdeps.ci_runner.types { CatalogSnapshot, RunnerLabelRow }
Expand Down Expand Up @@ -603,35 +602,3 @@ test fn witness_a_lowercase_separator_is_refused_rather_than_misordered() -> Boo
}
lowercase_t && canonical_still_orders
}

fn all_claims_hold() -> Bool {
witness_the_seam_refuses_a_row_from_another_surface()
&& witness_a_lowercase_separator_is_refused_rather_than_misordered()
&&
witness_two_catalogs_sharing_a_provider_still_read_as_two_catalogs()
&& witness_one_catalog_listing_a_label_twice_names_that_catalog()
&& witness_the_untrusted_partition_is_readable_from_the_value()
&&
witness_an_unorderable_snapshot_is_not_reported_as_an_old_one()
&&
witness_every_surveyed_runs_on_label_resolves()
&& witness_another_ci_systems_label_namespace_is_not_consulted()
&& witness_two_catalogs_carrying_one_label_refuse_rather_than_race()
&& witness_no_surveyed_label_is_carried_by_two_catalogs()
&& witness_biome_selected_label_resolves_arm_from_depots_catalog()
&& witness_the_unsuffixed_depot_label_derives_x64()
&& witness_each_surveyed_providers_arm_and_x64_labels_resolve()
&& witness_a_label_outside_every_catalog_yields_no_architecture()
&& witness_an_unresolved_label_carries_both_readings_unresolved()
&& witness_hosted_label_architecture_does_not_vary_with_repository_visibility()
&& witness_a_miss_against_an_older_snapshot_is_our_coverage_obligation()
&& witness_a_miss_against_snapshots_that_all_postdate_it_is_a_finding()
&& witness_every_snapshot_the_stale_arm_reports_predates_the_observation()
&& witness_rfc3339_comparison_orders_utc_values_of_equal_precision()
&& witness_rfc3339_comparison_refuses_mixed_precision_and_offsets()
&& witness_a_resolved_label_carries_its_snapshot_provenance()
}

fn runner_label_resolution_witness_main() -> ProcessExit {
if all_claims_hold() { ExitSuccess } else { ExitFailure { code: 1, reason: "one or more runner-label resolution claims did not hold" } }
}
Original file line number Diff line number Diff line change
Expand Up @@ -100,12 +100,3 @@ test fn w_the_ucx_name_carries_a_port_and_the_nccl_name_does_not() -> Bool {
&& all(hca, e => e.value == (fx_rdma_device as String))
&& all(ucx, e => e.value == join([fx_rdma_device as String, ":1"], ""))
}

test fn w_all_collective_transport_plan_claims_hold() -> Bool {
w_a_socket_plan_projects_no_device_no_capability_no_lock()
&& w_a_roce_plan_projects_the_device_the_capability_and_the_lock()
&& w_both_arms_project_the_interface_env()
&& w_the_roce_arm_projects_more_env_than_the_socket_arm()
&& w_only_the_roce_arm_projects_the_endpoint_env()
&& w_the_ucx_name_carries_a_port_and_the_nccl_name_does_not()
}
9 changes: 0 additions & 9 deletions dag/test/claim/spark/prefill_batch_sweep_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -83,12 +83,3 @@ test fn only_direct_measurement_reports_as_measured() -> Bool {
&& !reading_is_measured(b: DerivedAtCommonWorkload { normalised_tokens: token_count(count: 16400), from_samples: 20 })
&& !reading_is_measured(b: PredictedOutsideMeasuredArm { requested_budget: 1024, measured_budgets: "2048, 8192, 16384" as NonEmptyStr })
}

test fn w_all_prefill_batch_sweep_claims_hold() -> Bool {
the_derived_law_reproduces_the_independent_fit()
&& a_single_budget_population_refuses_rather_than_splitting_the_terms()
&& the_real_population_spans_budgets_and_the_planted_one_does_not()
&& too_few_probes_refuse_before_any_arithmetic()
&& the_predicted_step_duration_matches_the_measured_co_tenant_stall()
&& only_direct_measurement_reports_as_measured()
}
18 changes: 0 additions & 18 deletions dag/test/claim/spark/serving_engine_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -308,21 +308,3 @@ test fn w_ray_on_a_discrete_host_is_outside_the_counting_rule() -> Bool {
test fn w_the_verified_negatives_carry_upstream_error_text() -> Bool {
length(vllm_verified_negatives) > 0
}

test fn w_all_serving_engine_claims_hold() -> Bool {
w_a_second_engine_on_a_unified_pool_refuses_and_names_both()
&& w_an_empty_unified_pool_admits()
&& w_discrete_memory_hosts_are_outside_this_refusal()
&& w_no_declared_enforcer_refuses()
&& w_two_enforcers_refuse_rather_than_layering()
&& w_a_live_ray_monitor_on_a_unified_pool_refuses()
&& w_a_declared_ray_monitor_refuses_although_ray_started_none()
&& w_a_declared_guard_beside_rays_implied_monitor_is_two_enforcers()
&& w_a_zero_refresh_with_isolation_on_is_still_a_live_ray_monitor()
&& w_the_accounting_partition_over_every_enforcer_kind()
&& w_an_isolated_threshold_monitor_has_unestablished_accounting()
&& w_a_declared_guard_admits_when_the_factory_yields_only_noop()
&& w_a_non_ray_backend_is_outside_the_monitor_rule()
&& w_ray_on_a_discrete_host_is_outside_the_counting_rule()
&& w_the_verified_negatives_carry_upstream_error_text()
}
36 changes: 0 additions & 36 deletions dag/test/claim/spark/serving_performance_subject_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -680,39 +680,3 @@ test fn w_a_one_axis_difference_over_unread_axes_is_not_a_clean_cut() -> Bool {
AxisDeltaUndecidable { because: _ } => false
}
}

test fn w_all_serving_performance_subject_claims_hold() -> Bool {
w_a_deepseek_measurement_does_not_read_for_a_glm_decision()
&& w_the_refusal_does_not_name_axes_that_agree()
&& w_a_subject_reads_for_itself()
&& w_moving_the_topology_alone_is_detected_and_named()
&& w_moving_the_batch_budget_alone_is_detected_and_named()
&& w_moving_the_kv_dtype_alone_is_detected_and_named()
&& w_socket_and_rdma_are_different_subjects()
&& w_an_unread_transport_is_incomparable_and_never_equal()
&& w_a_partial_standing_names_its_gap_and_the_remedy()
&& w_a_one_axis_difference_over_fully_read_subjects_names_that_axis()
&& w_a_one_axis_difference_over_unread_axes_is_not_a_clean_cut()
&& w_a_multi_axis_pair_is_uncontrolled_rather_than_attributed()
&& w_two_identical_subjects_are_a_repeat_and_not_a_cut()
&& w_the_axis_roster_is_not_degenerate()
&& w_a_repinned_runtime_image_is_a_different_subject()
&& w_a_different_checkpoint_revision_is_a_different_subject()
&& w_a_different_max_num_seqs_is_a_different_subject()
&& w_turning_speculation_on_is_a_different_subject()
&& w_a_different_rank_population_is_a_different_subject()
&& w_a_known_checkpoint_difference_survives_an_unread_transport()
&& w_an_unread_axis_decides_only_when_nothing_known_differs()
&& w_the_transport_wire_is_derived_from_the_variant()
&& w_a_subject_with_an_absent_axis_cannot_become_established()
&& w_a_fully_read_subject_becomes_established()
&& w_a_partial_standing_still_carries_its_subject()
&& w_every_modelled_topology_round_trips_through_its_rank_count()
&& w_an_unmodelled_rank_count_refuses_rather_than_choosing_the_nearest()
&& w_a_zero_rank_count_refuses_too()
&& w_every_batch_arm_carries_its_own_partial_subject()
&& w_the_depth_law_does_not_read_for_the_batch_arms()
&& w_a_live_batch_arm_refuses_a_glm_decision_by_naming_the_checkpoint()
&& w_the_depth_law_does_not_even_read_for_itself_while_its_transport_is_unread()
&& w_the_topology_cut_moves_two_axes_rather_than_isolating_the_degree()
}
4 changes: 0 additions & 4 deletions dag/test/claim/srv3/srv3_host_effect_apply_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -276,10 +276,6 @@ test fn witness_srv3_nbd_proxy_on_bmc_refuses_typed() -> Bool {
}
}

test fn srv3_typed_receipt_emit_realizes_in_process_not_shell() -> Bool {
witness_srv3_receipt_emit_apply_converges_in_process()
}

test fn srv3_typed_receipt_carrier_holds_lines() -> Bool {
let receipt = srv3_typed_receipt_from_lines(lines: ["a", "b"])
srv3_typed_receipt(receipt: receipt).lines.length() == 2
Expand Down
11 changes: 0 additions & 11 deletions dag/test/claim/vllm_kv_pool_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -149,14 +149,3 @@ test fn w_a_cap_pool_pair_carries_its_utilization_and_its_source_line() -> Bool
}
}
}

test fn w_all_vllm_kv_pool_claims_hold() -> Bool {
w_block_arithmetic_is_not_the_pool()
&& w_the_utilization_product_is_a_budget_not_a_pool()
&& w_an_unobserved_format_is_not_an_observation()
&& w_the_three_startup_prefixes_are_distinct()
&& w_the_pool_is_read_from_the_kv_cache_size_line()
&& w_the_concurrency_line_refuses_rather_than_becoming_a_pool()
&& w_the_resolved_format_line_refuses_rather_than_becoming_a_pool()
&& w_a_cap_pool_pair_carries_its_utilization_and_its_source_line()
}
10 changes: 0 additions & 10 deletions dag/test/claim/yaml_ingest_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -89,16 +89,6 @@ test fn witness_comment_only_document_is_rejected() -> Bool {
!yaml_source_parses(src: "# no document node follows\n")
}

test fn witness_yaml_comment_boundary_controls_hold() -> Bool {
witness_column_zero_full_line_comment_is_lexically_ignored()
&& witness_indented_full_line_comment_is_lexically_ignored()
&& witness_inline_trailing_comment_refuses_instead_of_becoming_scalar_content()
&& witness_tab_separated_inline_comment_refuses_instead_of_becoming_scalar_content()
&& witness_hash_inside_double_quoted_scalar_is_content()
&& witness_shell_issue_reference_inside_block_literal_is_content()
&& witness_comment_only_document_is_rejected()
}

test fn witness_malformed_scalar_line_rejected() -> Bool {
yaml_source_parses(src: "just a bare word\n") == false
}
Expand Down
Loading