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
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
12 changes: 0 additions & 12 deletions src/v2/test/claim/affected_set_disposition_both_axes_test.dag
Original file line number Diff line number Diff line change
@@ -1,17 +1,5 @@
module v2.test.claim.affected_set_disposition_both_axes

import v2.std.logic { Bool }
import v2.workflow.affected_set_floor_runner {
DiffPathsProduced,
FrontierProduced,
RunWitness,
SkipAssumedGreen,
Refused,
floor_kernel_would_skip,
floor_witness_run_disposition
}
import v2.std.node { Atom, Node, SyntheticOccurrence, TypeNode }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

Expand Down
16 changes: 0 additions & 16 deletions src/v2/test/claim/affected_set_universe_test.dag
Original file line number Diff line number Diff line change
@@ -1,21 +1,5 @@
module v2.test.claim.affected_set_universe

import v2.std.logic { Bool }
import v2.std.collection { List }
import v2.std.node { Symbol }
import v2.std.algebra { bag_eq, list_snoc_item }
import v2.lens.affected_set {
RepoProcess,
RepoProcessUniverse,
UniverseComplete,
UniverseIncomplete,
ci_gate_processes,
meta_processes,
repo_process_universe,
repo_process_universe_from
}
import gunbc.ci_spec { Gate, gunbc_ci_gates, gunbc_ci_regen_floor_gates }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

Expand Down
21 changes: 0 additions & 21 deletions src/v2/test/claim/affected_set_witness_a_prove_test.dag
Original file line number Diff line number Diff line change
@@ -1,26 +1,5 @@
module v2.test.claim.affected_set_witness_a_prove

import v2.lens.edit_locus { GitDiffNameOnly, RepoPath }
import v2.std.algebra { count_equal, length }
import v2.std.collection { List }
import v2.std.exact_structural_equality_zip_fold_predicate {
exact_structural_equality_zip_fold
}
import v2.std.logic { Bool }
import v2.std.node { Node }
import v2.std.witness { Holds, Violates }
import v2.test.lens_affected_set.node_precision { affected_set_mid }
import v2.test.lens_affected_set.provenance_producer {
provenance_producer_node_precision_provenance,
provenance_producer_path_mid,
provenance_producer_reading_from_provenance
}
import v2.workflow.affected_set_floor_runner {
FloorDiffLineTouch,
floor_rust_run_implies_dag_run,
floor_test_fn_declaration_edited
}
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

Expand Down
Original file line number Diff line number Diff line change
@@ -1,8 +1,5 @@
module v2.test.claim.algebra.freemonoid_first_skip_witness

import std.algebra { Cons, Empty, FreeMonoid }
import v2.std.algebra { HeadAbsent, HeadFound, list_head, skip }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

Expand Down
Original file line number Diff line number Diff line change
@@ -1,9 +1,5 @@
module v2.test.claim.algebra.generic_alias_coproduct_instantiation

import std.algebra { Cons, Empty, FreeMonoid }
import v2.std.algebra { length }
import v2.std.node { Symbol }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

Expand Down
10 changes: 0 additions & 10 deletions src/v2/test/claim/algebra/list_linear_combinators_test.dag
Original file line number Diff line number Diff line change
@@ -1,15 +1,5 @@
module v2.test.claim.algebra.list_linear_combinators

import std.algebra { Cons, Empty, FreeMonoid }
import v2.std.algebra {
filter,
list_flat_map,
list_map,
list_reverse
}
import v2.std.integer { Int }
import v2.std.logic { Bool }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

Expand Down
3 changes: 0 additions & 3 deletions src/v2/test/claim/auth_declared_but_unwired_witness_test.dag
Original file line number Diff line number Diff line change
@@ -1,8 +1,5 @@
module v2.test.claim.auth_declared_but_unwired_witness

import tools.auth_declared_but_unwired_witness_transport { run_auth_declared_but_unwired_witness }
import v2.std.logic { Bool }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

Expand Down
71 changes: 0 additions & 71 deletions src/v2/test/claim/bash_command_fold_test.dag
Original file line number Diff line number Diff line change
@@ -1,76 +1,5 @@
module v2.test.claim.bash_command_fold

import extdeps.languages.bash.program {
AndOr,
AndThen,
Assign,
Command,
EnvPrefixed,
Exit,
Heredoc,
If,
Lit,
Negation,
OrElse,
Pipe,
RedirToFile,
RawLine,
ShellStmt,
StderrToNull,
StdoutAndStderrToNull,
StdoutToStderr,
Subshell,
VarRef,
WithRedir,
}
import v2.compiler.emit { emit }
import v2.compiler.infer { InferredFacts, InferredTree }
import v2.compiler.translate { target_serialize_source_from_model }
import v2.extdeps.languages.bash {
bash_stmt_env_prefixed_emitted,
bash_stmt_heredoc_emitted,
bash_stmt_negation_emitted,
bash_stmt_with_redir_emitted,
bash_word_pass_emitted
}
import v2.extdeps.languages.bash_command_fold {
bash_fold_and_then_true_false_emitted,
bash_fold_assign_wrong_target_model_witness,
bash_fold_cmd_echo_hi_emitted,
bash_fold_cmd_true_emitted,
bash_fold_cmd_true_wrong_emitted,
bash_fold_cmd_true_wrong_target_model_witness,
bash_fold_cmd_var_x_emitted,
bash_fold_env_prefixed_wrong_target_model_witness,
bash_fold_exit_wrong_target_model_witness,
bash_fold_heredoc_wrong_target_model_witness,
bash_fold_negation_wrong_target_model_witness,
bash_fold_pipe_echo_hi_wc_emitted,
bash_fold_raw_line_wrong_target_model_witness,
bash_fold_relation_row_witness,
bash_fold_stmt_bundle_witness,
bash_fold_stmt_emitted_witness,
bash_fold_target_model_for_stmt_witness,
bash_fold_with_redir_wrong_target_model_witness
}
import v2.std.compilers.target_model { TargetModel }
import v2.workflow.bash_program_emit { bash_program_serialize_stmt }
import v2.std.collection { Map }
import v2.std.diagnostic {
Accepted,
Diagnostic,
ExternalContractUnknown,
None,
Outcome,
Rejected,
Some,
Unavailable,
node_locus
}
import v2.std.logic { Bool }
import v2.std.node { Conj, Node, SyntheticOccurrence, TypeNode }
import v2.std.witness { Holds, Violates, Witness }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

Expand Down
27 changes: 0 additions & 27 deletions src/v2/test/claim/bash_program_fold_test.dag
Original file line number Diff line number Diff line change
@@ -1,32 +1,5 @@
module v2.test.claim.bash_program_fold

import extdeps.languages.bash.program {
CmdSubst,
AndOr,
AndThen,
Command,
Exit,
If,
OrElse,
Subshell,
Concat,
Lit,
ShellProgram,
ShellStmt,
ShellWord,
StderrToNull,
VarRef,
WithRedir,
assign,
command,
lit,
var_ref,
test_not_executable
}
import tools.build_step { BuildArtifact, emit_verifications }
import v2.workflow.bash_program_emit { bash_program_serialize, bash_program_serialize_stmt }
import v2.std.diagnostic { Accepted, Outcome, Rejected }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

Expand Down
Original file line number Diff line number Diff line change
@@ -1,25 +1,5 @@
module v2.test.claim.body_lowering.wave1_gate1_a1_symbol_index_helpers

import v2.compiler.body_lowering_fold {
body_lower_arrow_domain_binding_symbols,
body_lower_arrow_domain_matches_frontend_symbol_index,
body_lower_arrow_domain_matches_ingest_param_bindings,
body_lower_find_captured,
body_lower_fn_decl_ident_from_captured,
body_lower_param_binding_symbols_from_fn_decl_module
}
import v2.compiler.normalize { normalize }
import v2.compiler.parse { parse_module }
import v2.compiler.tokenize { tokenize }
import v2.extdeps.languages.dag {
dag_language_model,
ParseSubtreeFound
}
import v2.std.algebra { length }
import v2.std.collection { Absent, Optional, Present }
import v2.std.diagnostic { Accepted, Rejected }
import v2.std.logic { Bool }
import v2.std.node { Arrow, Conj, Node, TypeNode }

data wave1_gate1_a1_add_module_source: String = "module add_probe\n\nfn add(x: Int, y: Int) -> Int { x + y }\n"

Expand Down
Original file line number Diff line number Diff line change
@@ -1,32 +1,5 @@
module v2.test.claim.body_lowering.wave1_gate1_b1_bare_call_helpers

import v2.compiler.name_resolve {
Admission,
ResolutionSubject,
resolve_with_admission
}
import v2.compiler.normalize { normalize }
import v2.compiler.parse { parse_module }
import v2.compiler.tokenize { tokenize }
import v2.extdeps.languages.dag {
dag_language_model,
qualified_name_from_module_node
}
import std.algebra { Cons, Empty }
import v2.std.collection { Absent, Optional, Present }
import v2.std.diagnostic { Accepted, Rejected }
import v2.std.compilers.lexing { symbol_lexeme }
import v2.std.logic { Bool }
import v2.std.node {
Arrow,
ComputationNode,
Conj,
Named,
Node,
Positional,
Transform,
TypeNode
}

data wave1_gate1_b1_bare_call_module_source: String = "module wave1_gate1_b1_bare_call\n\nfn helper(x: Int) -> Int { x + x }\n\nfn caller(x: Int) -> Int { helper(x) }\n"

Expand Down
Original file line number Diff line number Diff line change
@@ -1,22 +1,5 @@
module v2.test.claim.body_lowering.wave1_gate1_normalize_add_helpers

import v2.compiler.normalize { normalize }
import v2.compiler.parse { parse_module }
import v2.compiler.resolve { resolve }
import v2.compiler.tokenize { tokenize }
import v2.extdeps.languages.dag { dag_language_model }
import v2.std.collection { Absent, Optional, Present }
import v2.std.diagnostic { Accepted, Rejected }
import v2.std.logic { Bool }
import v2.std.node {
Arrow,
ComputationNode,
Node,
Transform,
TypeNode,
well_formed
}
import v2.std.node_query { find_arrow_body_child }

data wave1_gate1_add_module_source: String = "module add_probe\n\nfn add(x: Int, y: Int) -> Int { x + y }\n"

Expand Down
15 changes: 0 additions & 15 deletions src/v2/test/claim/body_lowering_well_formed_wall_test.dag
Original file line number Diff line number Diff line change
@@ -1,20 +1,5 @@
module v2.test.claim.body_lowering_well_formed_wall

import v2.std.node {
Arrow,
Atom,
ComputationNode,
Edge,
Named,
Node,
Positional,
Symbol,
TypeNode,
Value,
node_synthetic,
well_formed
}
import v2.std.logic { Bool }

data body_lowering_well_formed_wall_note: String = "Discriminating RED control for the body-lowering-is-TOTAL change (clever-hawk-862): body-lowering never hard-rejects — a well-formed body it cannot lower is wrapper-retained (counted), and normalize's well_formed gate (03_normalize.dag well_formed(normalized)) is the SOLE structural wall. This witness proves 'total' is NOT fail-open: a genuinely MALFORMED body-lowering output still gets REJECTED by well_formed. The malformed shape is an Arrow whose arrow_body_edge target is a bare Atom — NOT a valid arrow-body realization (well_formed's arrow_body_target_is_valid_realization admits only a ComputationNode or a record-construct Conj). This is exactly the shape body_lower_body_from_fn_captured must never fabricate (its no-core-substrate arm wrapper-retains instead of forcing an atom operand into the Arrow body). If well_formed were weakened to admit it, the negative witness goes red. Paired with the positive control (a Value-bodied Arrow passes), the pair discriminates the wall, by execution."

Expand Down
4 changes: 0 additions & 4 deletions src/v2/test/claim/body_lowering_wrapper_retained_test.dag
Original file line number Diff line number Diff line change
@@ -1,9 +1,5 @@
module v2.test.claim.body_lowering_wrapper_retained

import v2.compiler.body_lowering_fold { body_lower_wrapper_retained_shell }
import v2.std.diagnostic { Accepted, Rejected, Some }
import v2.std.logic { Bool }
import v2.std.node { Conj, TypeNode, node_synthetic }

data wrapper_retained_diagnostics_shape_note: String = "Discriminating witness for the 2026-07-11 s1_closure floor panic: body_lower_wrapper_retained_shell constructed Accepted whose diagnostics field held a RAW NonEmptyDiagnostics where the Diagnostics coproduct (None | Some) is declared - the first downstream match over Diagnostics (diagnostics_merge in the normalize child fold) then panicked non-exhaustive on every file with a wrapper-retained fn body. This witness pins the SHAPE: the wrapper-retained outcome's diagnostics must inhabit the Some arm of Diagnostics and carry the typed wrapper-retained reason. Pre-fix it returns false (the Some pattern cannot match a raw record); post-fix true. Reproduced red/green by execution on dag/std/error_primitives.dag via s1_file_parses."

Expand Down
3 changes: 0 additions & 3 deletions src/v2/test/claim/bootstrap_test.dag
Original file line number Diff line number Diff line change
@@ -1,8 +1,5 @@
module v2.test.claim.bootstrap

import tools.bootstrap_witness_transport { run_bootstrap_witness }
import v2.std.logic { Bool }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

Expand Down
18 changes: 0 additions & 18 deletions src/v2/test/claim/boundary/english_ingest_fail_closed.dag
Original file line number Diff line number Diff line change
@@ -1,23 +1,5 @@
module v2.test.boundary.english_ingest_fail_closed

import v2.std.diagnostic {
AmbiguousIntent,
Diagnostic,
Unavailable,
diagnostics_singleton,
node_locus
}
import v2.std.node { Edge, Named, Node, Symbol, TypeNode, Atom, Conj, SyntheticOccurrence }
import v2.std.verification {
CompilesClaim,
DiagnosticClaim,
ManualAnchorAbsent,
TestClaim,
TestClassification,
Tier3,
Boundary,
manual_claim_anchor
}
fn atom_node(s: Symbol) -> Node {
Node { kind: TypeNode { connective: Atom { identity: s } }, children: [],
occurrence_id: SyntheticOccurrence
Expand Down
17 changes: 0 additions & 17 deletions src/v2/test/claim/branch_dispatch/rung_0_to_2_three_targets.dag
Original file line number Diff line number Diff line change
@@ -1,22 +1,5 @@
module v2.test.branch_dispatch.rung_0_to_2_three_targets

import v2.std.collection { List }
import v2.std.node { Atom, Node, Symbol, TypeNode, SyntheticOccurrence }
import v2.std.verification {
ManualAnchorAbsent,
TestClaim,
TestClassification,
Tier1,
Integration,
CompilesClaim,
manual_claim_anchor
}
import v2.test.computation_shapes.branch_dispatch {
branch_dispatch_subject,
claim_branch_dispatch_content_hash_stable,
claim_branch_dispatch_equals_refl,
claim_branch_dispatch_well_formed
}
data phase4_branch_dispatch_rung_subject: Node = Node {
kind: TypeNode { connective: Atom { identity: ^phase4_branch_dispatch_rung_subject_symbol } },
children: [],
Expand Down
Loading
Loading