Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
77f4781
WIP: Lane E: self-host frontier 27-row exact-head closeout, totality …
Aug 2, 2026
3d81253
WIP: Lane E: self-host frontier 27-row exact-head closeout, totality …
Aug 2, 2026
e6cb6db
WIP audit: push interim exact-head frontier probe census (17/27 at HE…
Aug 3, 2026
adb8072
WIP audit: hand-authored 17 frontier rows from survey; add compare or…
Aug 3, 2026
a1df25e
Fix CI: doc-graph bind for probe audit md; reorder sweep for rank mon…
Aug 3, 2026
19850a4
Align per-module survey scaffold order with frontier sweep_order.
Aug 3, 2026
51c8f45
WIP: Lane E: self-host frontier 27-row exact-head closeout, totality …
Aug 3, 2026
f725599
Fix invalid enum accessor impl after stage0 regen.
Aug 3, 2026
54ff631
Name offline consumer for frontier per-module probe witness.
Aug 3, 2026
f1b9867
Document survey stale-head drift and spot-check at current main.
Aug 3, 2026
76ef121
P2: selection degradation receipts (selected/total + reason) (#7722)
briansrls Aug 3, 2026
d16e173
Discharge namespace occurrence identity receipts (#7559)
briansrls Aug 3, 2026
b12027c
Root-cause disk-tier repeat-resolve memory growth (>8GiB OOM on secon…
briansrls Aug 3, 2026
0b6b993
Coordinator replay: wet witness per-row outcomes visible in CI job lo…
briansrls Aug 3, 2026
faa95d2
WIP: falsifier is flakey on budget - please investigate (#7738)
gunbai-bot[bot] Aug 3, 2026
4e089ef
P1 retention vs drain cohort receipt (authoritative) (#7725)
gunbai-bot[bot] Aug 3, 2026
7237024
Sole modeled publisher (model + shadow): policy-derived projection, p…
gunbai-bot[bot] Aug 3, 2026
44126ca
Lane A: R1 invert interpreter dispatch authority (roster becomes the …
briansrls Aug 3, 2026
3184d48
Fix audit scaffold fail-open and rename inflated closeout note.
Aug 3, 2026
79b0d4c
Merge 3184d48e20f23011c9071524934ce50e17c7da63 into 44126ca1de0fd8f6c…
briansrls Aug 3, 2026
8cd8c06
chore: regenerate drifted generated artifacts (ci auto-heal)
Aug 3, 2026
8cba865
Align probe note and survey md with interim audit framing.
Aug 3, 2026
c3f20a7
WIP: Lane E: self-host frontier 27-row exact-head closeout, totality …
Aug 3, 2026
4744b09
Regen stage0 lib.rs for regen_verify gate.
Aug 3, 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: 2 additions & 0 deletions .gitattributes
Original file line number Diff line number Diff line change
Expand Up @@ -184,12 +184,14 @@ src/v1/stage0/src/v1_compiler_trace.rs merge=generated-artifact
src/v1/stage0/src/v1_compiler_trait_derive_emit.rs merge=generated-artifact
src/v1/stage0/src/v1_compiler_workspace_members.rs merge=generated-artifact
src/v1/stage0/src/v1_gunbc_occurrence_binding_parser_walk.rs merge=generated-artifact
src/v1/stage0/src/v1_interpreter_dispatch_generated.rs merge=generated-artifact
src/v1/stage0/src/v1_probe_emit_interp.rs merge=generated-artifact
src/v1/stage0/src/v1_rt.rs merge=generated-artifact
src/v1/stage0/src/v1_std_core.rs merge=generated-artifact
src/v1/stage0/src/v1_test_non_ascii_perf_fixture.rs merge=generated-artifact
src/v1/stage0/src/v1_tests_claim_caret_parse_smoke_test.rs merge=generated-artifact
src/v1/stage0/src/v1_tests_claim_occurrence_binding_parser_walk_witness_test.rs merge=generated-artifact
src/v1/stage0/src/v1_tests_claim_occurrence_identity_debt_receipt_test.rs merge=generated-artifact
src/v1/stage0/src/v1_tests_claim_pattern_binder_declaration_node_test.rs merge=generated-artifact
src/v1/stage0/src/v1_tests_claim_required_expr_newline_continuation_test.rs merge=generated-artifact
src/v1/stage0/src/wt_a.rs merge=generated-artifact
Expand Down
3 changes: 2 additions & 1 deletion .github/workflows/ci.yml

Large diffs are not rendered by default.

3 changes: 1 addition & 2 deletions ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -37,11 +37,10 @@ The graph has eleven lanes: SCM compatibility · namespace · P-derive · observ
- [ ] **Keep an honest list of what still depends on the old compiler** — Every module is either generated by the new compiler or explicitly kept on the old one with a reason and a plan to move. Two separate questions, kept separate: whether the list found every module, and whether every module it found has been decided. A complete list of undecided modules and a decided list that missed modules are different failures and are reported differently. Why: Turns a vague sense of 'mostly done' into a finite, countable list someone can work through. [authority](dag/gunbc/v1_deletion_plan.dag)
- [ ] **Work through the remaining hand-written files the products need** — Move the hand-written files the shipping tools still depend on. Anything that genuinely has to stay gets an explicit reason. Why: The main command-line tool is itself one of these files, so 'the products still build' is not something we can honestly claim until this is done. [authority](dag/gunbc/v1_deletion_plan.dag)
- [ ] **Make sure deleting the old tests loses no coverage** — Every old test file removed has equivalent coverage that would actually catch the bug it was written for. Why: A guard that stays quiet is not the same as coverage; without this, deletion silently drops real protection. [authority](dag/gunbc/v1_deletion_plan.dag)
- [ ] **Let the model, not the Rust, decide what primitives exist** — Invert the roster. Today the Rust dispatch is the authority and the roster is derived from it; here the roster becomes the authority and the interpreter's local arm identity and spelling/form lookup are GENERATED from it, leaving hand Rust to supply only the handler bodies behind an exhaustive match. The semantic question of which primitive an arm realizes stays a separate join and does not move here. Why: While the denominator lives in Rust, 'which primitives does the interpreter provide' can only be answered by reading Rust, and a new dispatch site added there is invisible to every consumer that asks. That keeps interpreter deletion a judgment call instead of a derived population, and it leaves the primitive-identity join reading a surface that can grow behind its back. [authority](dag/gunbc/v1_interpreter_primitive_surface.dag)
- [ ] **Write the closing check for: Make exact prior results reusable across invocations** — One executable check states when this is done, transcribed from the node's own bar: Wrong content, a missing entry, and a full store each refuse rather than quietly falling back to recomputing. Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](docs/plans/witness-realization-plan.md)
- [ ] **Make exact prior results reusable across invocations** — Iteration-speed and runtime infrastructure: exact input identity selects a bounded materialized result that can be served after restart without compiling. The v1 exit is one consumer of this kernel, not the kernel's parent purpose. Why: Repeated invocations currently rebuild results that an exact identity could safely serve; product iteration, tests, and the v1 exit all pay that recomputation independently. [authority](docs/plans/witness-realization-plan.md)
- [ ] **Prove old and new agree, by running them, not by waiting** — Run the whole test suite cold on both, compare compile results, check the self-rebuild, and record each family's outcome. Why: Confidence that comes from 'it has been fine for a while' is not evidence; this replaces it with runs someone chose to do. [authority](dag/gunbc/v1_deletion_plan.dag) — requires all: v1-materialization-kernel, v1-emitter-fixed-point
- [ ] **Write the closing check for: Let the model, not the Rust, decide what primitives exist** — One executable check states when this is done, transcribed from the node's own bar: A roster row with no Rust handler must fail COMPILATION, not a test. A Rust handler that is not reachable through a generated arm identity must not be addable as another string-dispatch path. Editing alias order or an authored spelling must not change an arm identity. One spelling under two different forms must stay representable. An accepted shape or arity is either modeled on the roster or typed as unknown -- never guessed. And no Rust-only spelling denominator may remain anywhere: if one does, this node is not done. Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](dag/gunbc/v1_interpreter_primitive_surface.dag)
- [ ] **Let the model, not the Rust, decide what primitives exist** — Invert the roster. Today the Rust dispatch is the authority and the roster is derived from it; here the roster becomes the authority and the interpreter's local arm identity and spelling/form lookup are GENERATED from it, leaving hand Rust to supply only the handler bodies behind an exhaustive match. The semantic question of which primitive an arm realizes stays a separate join and does not move here. Why: While the denominator lives in Rust, 'which primitives does the interpreter provide' can only be answered by reading Rust, and a new dispatch site added there is invisible to every consumer that asks. That keeps interpreter deletion a judgment call instead of a derived population, and it leaves the primitive-identity join reading a surface that can grow behind its back. [authority](dag/gunbc/v1_interpreter_primitive_surface.dag)
- [ ] **Write the closing check for: The expecting-red probe corpus: the floor gap becomes a counted, continuously-measured number** — One executable check states when this is done, transcribed from the node's own bar: A probe that stops expecting red without its class's wall having landed is itself a red (greening is counted); the corpus reds if any probe pair loses its executing consumer. Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **The expecting-red probe corpus: the floor gap becomes a counted, continuously-measured number** — One probe pair per floor class (deliberately-bad input expected to refuse; legitimate control expected to accept), enrolled as expecting-red rows via the known-red quarantine mechanism so today's fail-open state is measured, not asserted. Every currently-legitimate map/fold/filter/flat_map/service invocation form appears as a positive control so a future wall cannot green by refusing the language. Why: Replaces anecdote (gunbc#7479's 500) with a counted deficit per class; each wall that lands flips its probes to regression controls loudly. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **The guarantee claims carrier: rung state becomes DERIVED from execution receipts, never stored** — Four carriers, measurement separated from claim: GuaranteeRequirement (class identity, domain, harm, ceiling with typed reason, next_rung_trigger); GuaranteePath (subject_grain, acceptance_boundary, realization_target per gunbc.guarantee_measurement; one row per in-scope path, population derived from the census or completeness-witnessed); GuaranteeMeasurement (executed receipts naming their consumer); and GuaranteeDisposition DERIVED per path — Unmeasured | BelowFloor | FrontierAccepted | OnLadder | OutsideModeledGuarantee — folded by below-floor dominance, then frontier, then unmeasured, then MINIMUM rung across paths. No stored current_rung field exists, so a transcribed rung is unrepresentable; the five recovered vocabularies stay orthogonal, joined by class identity. Full shape: gap analysis sec 12 Stage 1b. Why: Ends the per-conversation re-derivation of what the compiler guarantees (the operator performed the missing meta-lens by hand three times this month); grounds the enforcement-intent StandingIntent thread instead of minting beside it. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
Expand Down
102 changes: 102 additions & 0 deletions dag/extdeps/git/publication_transport.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,102 @@
module extdeps.git.publication_transport

import std.types { Bool, CommitSha, GitRef, Int, List, NonEmptyStr, String }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
import extdeps.uri { Uri, Https }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "git-scm.com/docs/git-push"
}
}

data git_commit_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "git-scm.com/docs/git-commit"
}
}

data extdeps_model_scope: ExternalModelScope = ExternalModelScope {
subject: ExternalSubjectRef {
declaration: DeclarationRef {
module_path: "extdeps.git.publication_transport",
decl_name: "PublicationTransport",
field: WholeDeclaration
}
},
first_citation: extdeps_external_authority_anchor,
further_citations: [git_commit_external_authority_anchor]
}

data git_publication_transport_note: String = "Modeled upstream publication write operations de-fused from git.Core. GitPushRequest and GitCommitRequest are the interface shapes; shell argv lives only in git.PublicationTransport service transport rows — no parallel free-fn argv surface. Slice 1 is model + shadow only — consumers route through tools.publication_publisher before binding a transport handler in the live slice."

type GitRefUpdateSpec {
local_ref: GitRef
remote_ref: GitRef
}

type GitPushRequest {
remote: NonEmptyStr
ref_updates: List<GitRefUpdateSpec>
}

type GitCommitRequest {
message: NonEmptyStr
allow_empty: Bool
}

data git_commit_allow_empty_dispatch_note: String = "GitCommitRequest.allow_empty selects RecordEmptyCommit vs RecordCommit at transport bind — two operations, because shell argv templates cannot branch on Bool."

service git.PublicationTransport {
operation PushRefUpdate {
input {
remote: NonEmptyStr
refspec: NonEmptyStr
}
output {
exit_code: Int from "exit_code"
stderr: String from "stderr"
success: Bool from "exit_success"
}
transport shell { argv: ["git", "push", "{remote}", "{refspec}"] }
exit {
0 => Unit
nonzero => String "Push failed"
}
}

operation RecordCommit {
input {
message: NonEmptyStr
}
output {
sha: CommitSha from "stdout"
success: Bool from "exit_success"
stderr: String from "stderr"
}
transport shell { argv: ["git", "commit", "-m", "{message}"] }
exit {
0 => Unit
nonzero => String "Commit failed"
}
}

operation RecordEmptyCommit {
input {
message: NonEmptyStr
}
output {
sha: CommitSha from "stdout"
success: Bool from "exit_success"
stderr: String from "stderr"
}
transport shell { argv: ["git", "commit", "--allow-empty", "-m", "{message}"] }
exit {
0 => Unit
nonzero => String "Commit failed"
}
}
}
Loading
Loading