Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
42 commits
Select commit Hold shift + click to select a range
be1a001
WIP: compiler correctness
Jul 31, 2026
40d615c
Bind the guarantee-recovery analysis into the doc graph
Jul 31, 2026
f71fee9
WIP: compiler correctness
Jul 31, 2026
9ca8d00
Reconcile the gap analysis against the independent review — three cor…
Jul 31, 2026
6a80656
Status header: two audit passes complete, open items typed
Jul 31, 2026
dd7e585
Align the bind's dissolution trigger with the doc's own authority mod…
Jul 31, 2026
a78e4bf
Address review 45305 (merge same-slug binds, fix stale block) + land …
Jul 31, 2026
5130f7a
WIP: compiler correctness
Jul 31, 2026
2687e32
WIP: compiler correctness
Jul 31, 2026
d2d7ed5
Integrate main (squash-merge of #7486)
Jul 31, 2026
0532d3e
Ladder follow-up: adopt the post-merge verdict (8 corrections) + the …
Jul 31, 2026
aa06080
Give works its executing consumers (review 45336): nonempty wall, sym…
Jul 31, 2026
9ac8bd5
Merge remote-tracking branch 'origin/main' into session/cool-badger-514
Jul 31, 2026
d256baf
De-inflate the three climb-node headlines (review 45349): work nodes …
Jul 31, 2026
93b95d2
WIP: compiler correctness
Jul 31, 2026
be77111
Merge 93b95d29a5011c610e9d265edcf96d0d51e329b4 into e156812de5c5e7d1e…
gunbai-bot[bot] Jul 31, 2026
dceeb89
chore: regenerate drifted generated artifacts (ci auto-heal)
Jul 31, 2026
2d836ed
Ladder nodes join the declared roadmap graph; binds nonempty by const…
Jul 31, 2026
df2c1a8
Merge remote-tracking branch 'origin/main' into session/cool-badger-514
Jul 31, 2026
754f187
WIP: compiler correctness
Jul 31, 2026
5bd52c4
Trim the three over-budget ladder briefs to the operator's 100-word t…
Jul 31, 2026
c0ac6e8
WIP: compiler correctness
Jul 31, 2026
cd3d4bb
Containment predicates consume doc_all_nodes, the one canonical walke…
Jul 31, 2026
a524d9e
Merge remote-tracking branch 'origin/main' into session/cool-badger-514
Jul 31, 2026
62c4700
Merge remote-tracking branch 'origin/main' into session/cool-badger-514
Jul 31, 2026
646078e
Merge remote-tracking branch 'origin/main' into session/cool-badger-514
Jul 31, 2026
26e803e
Post-merge verdict follow-up: open-candidate honesty, anchored baseli…
Jul 31, 2026
1c33799
WIP: compiler correctness
Jul 31, 2026
819e8f1
chore: regenerate drifted generated artifacts (ci auto-heal)
Jul 31, 2026
71b3a02
Route the ambiguity wall and cardinality seam through the closure doo…
Jul 31, 2026
d92594b
Merge branch 'session/cool-badger-514' of https://github.com/gunb-ai/…
Jul 31, 2026
ec15d71
Reconcile the sec-7b behavior-count passage to past tense (review 45558)
Jul 31, 2026
c23ac37
WIP: compiler correctness
Jul 31, 2026
64b757f
Remove probe demo scaffolding (net-zero vs main: files added by autoc…
Jul 31, 2026
3f5db40
Merge remote-tracking branch 'origin/main' into session/cool-badger-514
Jul 31, 2026
37cd00d
WIP: compiler correctness
Jul 31, 2026
ab0b5f9
Call-shape wall: refuse unknown argument labels and surplus positiona…
Jul 31, 2026
87026e7
Merge remote-tracking branch 'origin/main' into session/cool-badger-514
Jul 31, 2026
c31945d
chore: regenerate drifted generated artifacts (ci auto-heal)
Jul 31, 2026
d7eb539
Roster the call-shape witness blob in the scaffold index (review 45655)
Jul 31, 2026
c7bc814
Merge branch 'session/cool-badger-514' of https://github.com/gunb-ai/…
Jul 31, 2026
a1889e2
Merge remote-tracking branch 'origin/main' into session/cool-badger-514
Jul 31, 2026
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 ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ The graph has eleven lanes: SCM compatibility · namespace · P-derive · observ
- [ ] **Baseline prevalence: the whole-corpus floor rerun bucketed by ladder position, before any wall lands** — Re-run the whole-corpus floor and bucket every failure — statically-decidable-should-have-refused, runtime-value-dependent, external-boundary, resource-budget, capability-not-grounded, interpreter-defect — keyed to the carrier's class ids: the honest BEFORE picture. Replaces the carried-but-unverified historical figures (1454/149 and the 66/40/6 histogram) with current receipts. Anchored: anchor_commit 6c6e2dcb8587d73350ac252f5b07a6b50d684485 (the gunbc#7489 merge — pre-P0-implementation main), so the measurement is content-addressed and reproducible after in-flight branches merge; walls sequence after it without racing a live tree (post-merge verdict). Why: Denominates the climbs in displaced cost (DESIGN 6) instead of elegance; the honest number for how many programs the gap admits today. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) — requires all: ladder-probe-corpus, ladder-claims-carrier
- [ ] **Method existence: an unresolved method refuses at compile on every applicable path** — An unresolved method refuses at compile with name, receiver type, and locus: delete the method_pipe_map_keys_values_fallback else-arm and the resolve_builtin_call_type Absent-to-unit_type arm. Main today: compile-time method existence unenforced outside existing paths. Open candidate gunbc#7484 carries narrow R2 coverage for established receiver surfaces plus a typed, countable MethodExistenceUndecided frontier elsewhere — candidate evidence on an open branch, never main's rung (post-merge verdict). Zero-resolution is decided over the union of current admissible sources — enumeration suffices for absence — so the identity join gates only the more-than-one half, not this node. First: receiver normalization, then zero-resolution refusal. Why: The gunbc#7479 class (typechecked filter_map, HTTP 500 at dispatch) becomes unwritable-to-ship; the compile gate stops being quieter than the interpreter. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **Method ambiguity refuses: more than one resolution is a located error once primitive identity defines sameness** — The method-existence wall closes cardinality zero; this closes more-than-one — two distinct primitive identities (or a primitive and a user fn) resolving for one receiver/method pair refuse with both candidates named. Gated on primitive-identity-join because ambiguity is decidable only when sameness is: the length/count/size dispatch aliases make one method look like three today (the gunbc#7484 measured fork), so an ambiguity check before the join would refuse legitimate corpus or silently pick. Why: The silent-first-hit dispatch class: today arm order decides which of two candidates runs — an unstated tiebreak the census cannot even measure until sameness is defined. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) — requires all: floor-method-existence-wall, primitive-identity-join
- [ ] **Call shape: the silent positional label bind gets loud, then exact bijection** — Two moves in order. Floor first: a named argument matching no formal must diagnose — today direct_call_arg_mismatch_diags falls back to positional binding, so a misspelled label silently computes the wrong thing. Then the wall: argument population in exact bijection with non-default formals (missing, extra, duplicate, mislabeled each a typed located refusal). Invocation arity is a new judgment — ArityMismatch is type-constructor grain and stays so. Why: A misspelled label silently computing the wrong thing is the harm shape DESIGN 5 prices at interest, paid by the end user; the floor move alone retires it. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **Call shape: the silent positional label bind gets loud, then exact bijection** — Floor LANDED (cool-badger-514): unknown label and surplus positional refuse at the direct-call seam, blocking, exemption-free — the two classes the interpreter's call_function_inner already refuses, mirrored so the authorities agree. Census refused 28 live rename fossils, all fixed. Remaining wall: duplicate and missing land as an interpreter-first parity pair; method-pipe seam with the method wall. ArityMismatch stays type-constructor grain. Why: A misspelled label silently computing the wrong thing is the harm shape DESIGN 5 prices at interest, paid by the end user; the landed floor retires it at the direct-call seam. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **Delete module_skips_direct_call_arg_check: the compiler stops authoring itself under weaker checks** — Run the call-shape and inhabitance probes over v2.* and v1.compiler.*, classify every failure fresh (the historical 104 TypeMismatch figure has no locatable receipt and is neither blocker nor promise), repair the compatibility relation or the source, then delete the exemption. Its deletion is the terminal Tier-1 acceptance named by the doc-graph bind on this lane's analysis. Why: The dimension contract's one named escape hatch (enforced universally — no escape hatch, no wrapper functions); v1 currently admits unsound v2 source that v2 then self-certifies, and v1 deletion would not retroactively prove it. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) — requires all: floor-call-shape-wall, floor-inhabitance-wall
- [ ] **Declared types constrain produced values: return, data, and generic instantiation refuse non-inhabiting producers** — fn f() -> Int returning a string refuses at compile; data x: Int = "x" refuses; a generic record instantiation whose interior does not inhabit the substituted parameter refuses. The judgment is actual-inhabits-declared at the three unchecked positions gunbc#7481 probed, reusing the argument-position machinery that already refuses correctly. Why: The keystone gap: the recovered thesis's distinctness requirement — without it every declared type is part contract, part documentation, and WalkPlan-class defects surface at first field access. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **ExhaustivenessUnknown refuses: the PatternLookupBlocked silent arm closes** — lookup_variant_in_type and lookup_field_in_variant answer PatternLookupBlocked with diagnostics: [] — exhaustiveness-not-established passing as success-adjacent. Split the verdict three ways (Exhaustive | NonExhaustive | ExhaustivenessUnknown) and refuse Unknown into any accepted executable artifact. Why: Closes the fallback-arm shape the census names for blocked lookups — exhaustiveness-not-established passing as success-adjacent; the measured disposition lives in the carrier, not this ticket. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
Expand Down
6 changes: 6 additions & 0 deletions dag/gunbc/language_source_scaffold_index.dag
Original file line number Diff line number Diff line change
Expand Up @@ -347,6 +347,11 @@ data ct_row_ct_caret_parse_smoke_native_witness_tests: LanguageSourceScaffoldRow
disposition: compiler_tests_rust_hand_assertion_scaffold_trigger
}

data ct_row_ct_call_shape_wall_witness_test: LanguageSourceScaffoldRow = LanguageSourceScaffoldRow {
carrier_module: "v1.compiler.compiler_tests_rust", blob_decl: "ct_call_shape_wall_witness_test",
disposition: compiler_tests_rust_hand_assertion_scaffold_trigger
}

data ct_row_ct_profile_self_compile_test: LanguageSourceScaffoldRow = LanguageSourceScaffoldRow {
carrier_module: "v1.compiler.compiler_tests_rust", blob_decl: "ct_profile_self_compile_test",
disposition: compiler_tests_profile_trigger
Expand Down Expand Up @@ -401,6 +406,7 @@ data language_source_scaffold_roster: List<LanguageSourceScaffoldRow> = [
ct_row_ct_sole_constructor_fieldless_witness_test,
ct_row_ct_contracts_sidecar_witness_test,
ct_row_ct_caret_parse_smoke_native_witness_tests,
ct_row_ct_call_shape_wall_witness_test,
ct_row_ct_profile_self_compile_test,
ct_row_ct_profile_full_pipeline_test,
ct_row_ct_profile_reconcile_test,
Expand Down
12 changes: 6 additions & 6 deletions dag/gunbc/roadmap_authority.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1926,12 +1926,12 @@ fn guarantee_ladder_nodes() -> List<RoadmapNode> {
volume: VolumeMedium,
t: fields(
headline: "Call shape: the silent positional label bind gets loud, then exact bijection",
boundary: "Two moves in order. Floor first: a named argument matching no formal must diagnose — today direct_call_arg_mismatch_diags falls back to positional binding, so a misspelled label silently computes the wrong thing. Then the wall: argument population in exact bijection with non-default formals (missing, extra, duplicate, mislabeled each a typed located refusal). Invocation arity is a new judgment — ArityMismatch is type-constructor grain and stays so.",
displaced_cost: "A misspelled label silently computing the wrong thing is the harm shape DESIGN 5 prices at interest, paid by the end user; the floor move alone retires it.",
first_slice: "The floor diagnostic (any label matching no formal refuses), probe-paired.",
red_control: "Probe: misspelled label with a type-compatible positional slot — must refuse naming the unknown label; control: every legitimate labeled and positional form in corpus compiles.",
out_of_scope: "The v2.*/v1.compiler.* exemption (its own node); default-parameter semantics changes.",
handback: "The judgment's module path, refusal variants added, probe flip receipt."
boundary: "Floor LANDED (cool-badger-514): unknown label and surplus positional refuse at the direct-call seam, blocking, exemption-free — the two classes the interpreter's call_function_inner already refuses, mirrored so the authorities agree. Census refused 28 live rename fossils, all fixed. Remaining wall: duplicate and missing land as an interpreter-first parity pair; method-pipe seam with the method wall. ArityMismatch stays type-constructor grain.",
displaced_cost: "A misspelled label silently computing the wrong thing is the harm shape DESIGN 5 prices at interest, paid by the end user; the landed floor retires it at the direct-call seam.",
first_slice: "DONE — direct_call_shape_diags, probe-paired (pre 0 diagnostics, post two located refusals), census-adjudicated.",
red_control: "Landed: ct_call_shape_wall_witness_test — mislabel and surplus REDs, zero-diagnostic controls incl. the underscore idiom; every legitimate corpus form compiles (census dry).",
out_of_scope: "The v2.*/v1.compiler.* exemption (its own node); default-parameter semantics changes; the sig-unresolved fallthrough (closes with resolution coverage).",
handback: "v1.compiler.infer direct_call_shape_diags; CallArgumentNameUnknown + CallPositionalSurplus; receipts in direct_call_shape_wall_note."
)
),
active_sized(identity: "rn_6W5ACS5ZE3ZMTA7BFCQLY76VW4", id: "floor-inhabitance-wall",
Expand Down
34 changes: 17 additions & 17 deletions dag/gunbc/stage0_rust_source_lifecycle_scaffold.dag
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ fn observed_cargo_paths_subset_of_tracked(
) -> Bool {
fold_list(
xs: cargo_bin_repo_paths,
init: true,
empty: true,
cons: fn(ok, cargo_path) { ok && path_in_list(path: cargo_path, paths: tracked_paths) }
)
}
Expand All @@ -94,7 +94,7 @@ fn first_untracked_cargo_path(
) -> String {
fold_list(
xs: cargo_bin_repo_paths,
init: "",
empty: "",
cons: fn(first, cargo_path) {
if first != "" {
first
Expand All @@ -110,7 +110,7 @@ fn first_untracked_cargo_path(
fn count_tracked_unclassified(tracked_paths: List<String>, classified_paths: List<String>) -> Int {
fold_list(
xs: tracked_paths,
init: 0,
empty: 0,
cons: fn(count, path) {
if path_in_list(path: path, paths: classified_paths) {
count
Expand All @@ -128,7 +128,7 @@ fn count_newly_unclassified_tracked(
) -> Int {
fold_list(
xs: tracked_paths,
init: 0,
empty: 0,
cons: fn(count, path) {
let is_new = !path_in_list(path: path, paths: prior_tracked_paths)
let is_classified = path_in_list(path: path, paths: classified_paths)
Expand All @@ -144,7 +144,7 @@ fn count_newly_unclassified_tracked(
fn count_stale_lifecycle_rows(tracked_paths: List<String>, lifecycle_paths: List<String>) -> Int {
fold_list(
xs: lifecycle_paths,
init: 0,
empty: 0,
cons: fn(count, path) {
if path_in_list(path: path, paths: tracked_paths) {
count
Expand All @@ -158,7 +158,7 @@ fn count_stale_lifecycle_rows(tracked_paths: List<String>, lifecycle_paths: List
fn count_hand_maintained_in_tracked(tracked_paths: List<String>) -> Int {
fold_list(
xs: derived_hand_maintained_stage0_repo_paths(),
init: 0,
empty: 0,
cons: fn(count, hand_path) {
if path_in_list(path: hand_path, paths: tracked_paths) {
count + 1
Expand All @@ -172,7 +172,7 @@ fn count_hand_maintained_in_tracked(tracked_paths: List<String>) -> Int {
fn count_hand_maintained_in_prior_tracked(prior_tracked_paths: List<String>) -> Int {
fold_list(
xs: derived_hand_maintained_stage0_repo_paths(),
init: 0,
empty: 0,
cons: fn(count, hand_path) {
if path_in_list(path: hand_path, paths: prior_tracked_paths) {
count + 1
Expand All @@ -186,7 +186,7 @@ fn count_hand_maintained_in_prior_tracked(prior_tracked_paths: List<String>) ->
fn path_occurrence_count(paths: List<String>, needle: String) -> Int {
fold_list(
xs: paths,
init: 0,
empty: 0,
cons: fn(count, path) {
if path == needle {
count + 1
Expand All @@ -200,7 +200,7 @@ fn path_occurrence_count(paths: List<String>, needle: String) -> Int {
fn count_duplicate_path_excess(paths: List<String>) -> Int {
fold_list(
xs: paths,
init: 0,
empty: 0,
cons: fn(excess, path) {
let occurrences = path_occurrence_count(paths: paths, needle: path)
if occurrences > 1 {
Expand All @@ -219,7 +219,7 @@ fn count_observed_manifest_duplicate_excess(
) -> Int {
fold_list(
xs: [tracked_paths, prior_tracked_paths, cargo_bin_repo_paths],
init: 0,
empty: 0,
cons: fn(sum, paths) { sum + count_duplicate_path_excess(paths: paths) }
)
}
Expand Down Expand Up @@ -366,7 +366,7 @@ fn derived_partition_crate_lib_repo_paths() -> List<String> {
fn list_concat_unique(acc: List<String>, items: List<String>) -> List<String> {
fold_list(
xs: items,
init: acc,
empty: acc,
cons: fn(acc_paths, path) {
if any(xs: acc_paths, predicate: fn(p) { p == path }) {
acc_paths
Expand Down Expand Up @@ -539,7 +539,7 @@ fn witness_honest_minimal_observation_ok() -> RustManifestObserved {
fn first_classified_repo_path(classified: List<String>) -> String {
fold_list(
xs: classified,
init: "",
empty: "",
cons: fn(first, path) {
if first == "" {
path
Expand Down Expand Up @@ -599,7 +599,7 @@ fn lifecycle_row_well_formed(row: RustSourceLifecycleRow) -> Bool {
&& length(xs: row.obligations) > 0
&& fold_list(
xs: row.obligations,
init: true,
empty: true,
cons: fn(ok, obligation) {
ok && rust_source_lifecycle_obligation_well_formed(obligation: obligation)
}
Expand All @@ -609,15 +609,15 @@ fn lifecycle_row_well_formed(row: RustSourceLifecycleRow) -> Bool {
fn rust_source_lifecycle_residue_rows_well_formed() -> Bool {
fold_list(
xs: rust_source_lifecycle_residue_rows,
init: true,
empty: true,
cons: fn(ok, row) { ok && lifecycle_row_well_formed(row: row) }
)
}

fn list_paths_all_unique(paths: List<String>) -> Bool {
fold_list(
xs: paths,
init: true,
empty: true,
cons: fn(ok, path) { ok && path_occurrence_count(paths: paths, needle: path) == 1 }
)
}
Expand All @@ -633,7 +633,7 @@ fn duplicate_exact_paths_zero_holds() -> Bool {
fn generated_repo_paths_cover_authority_holds() -> Bool {
fold_list(
xs: generated_stage0_files,
init: true,
empty: true,
cons: fn(ok, basename) {
ok && any(
xs: derived_generated_stage0_repo_paths(),
Expand All @@ -646,7 +646,7 @@ fn generated_repo_paths_cover_authority_holds() -> Bool {
fn generated_authority_subset_of_derived_holds() -> Bool {
fold_list(
xs: derived_generated_stage0_repo_paths(),
init: true,
empty: true,
cons: fn(ok, path) {
let basename = replace(path, stage0_src_repo_prefix, "")
ok && is_generated_stage0_file(basename: basename)
Expand Down
Loading
Loading