Repository navigation
Releases: kofun-lang/kofun
Release list
v0.13.4-seed
v0.13.4-seed
This seed release changes no published claim. It closes two of the five
command-I/O gaps the Kofun digest command needs: a compiled program now
receives its operands and writes a standard-error line, and it can read a file
or standard input past the 65,536-byte ceiling in bounded chunks with an
observable failure. Each addition carries its own Stage 2 pair gate. Nothing in
release/claims.json moved, so the version is a PATCH. The tagged
artifacts/release-evidence/CLAIMS.md is still the authority for each supported
slice.
Published claim changes
None. release/claims.json and spec/release-claim.schema.json are
byte-identical between the previous tag v0.13.3-seed and the release commit
(git diff --stat v0.13.3-seed 10e52e3a8ef3973595dc86b5168997485d513060 -- release/claims.json spec/release-claim.schema.json is empty).
Other implementation changes
- A C11 Stage 2 program receives its operands and writes a line to standard
error
(#1666,
PR #1702).- Operands are
Textin order, byte-exact, at most 256 with 255 bytes each
andargv[0]observable; a program can write one line to standard error.
The emitted prelude capturesargvinmainand defines
stage2_command_operand_count,stage2_command_operand_textand
stage2_command_stderr, withR034..R037on the count, index,
operand-length and line-length bounds. Both halves gate on the same
raw-sourcestage2_command_spelling. - New gate
task command-operands;spec/c11-command-io-v1.mdis extended
from the #1665 decision to name the realized builtins.
- Operands are
- A C11 Stage 2 program reads a file or standard input past 65,536 bytes in
bounded chunks, and can observe a failed read
(#1667,
PR #1703).- The three builtin tables admit
stage2_bytes_stream_open,
stage2_bytes_stream_stdinandstage2_bytes_stream_read. The stream
family lowers throughemit_bytes_mutation_callwith the open and the
standard-input selection carrier-free, and the emitted prelude holds one
open stream and returns the chunk count,0at end of stream, or a
negativeIntstatus on a refused open, an unreadable stream, or a spent
allocator. - New gate
task bytes-read-stream;spec/bytes-bounded-v1.mdstates the
chunked operation beside the singleread_fileceiling.
- The three builtin tables admit
- The release evidence pack is refreshed for #1666.
Defects inherited from v0.13.3-seed, left open
- #1483 — self-compilation bound.
--compile-outcome bootstrap/stage2/compiler.kofunstill exits 1; the first diagnostic is
E2S35: binding `value_end` is outside its lexical scope at byte 741079; declaration at byte 685527. The same class was measured onv0.13.3-seed
(... at byte 736030; declaration at byte 680478). The offset moves only
because the source grew in this range, so this range did not create the
defect. - #1679 — value-position
else ifchain. The chain still differs in
scope-HIR binding visibility between the pair halves, because the C half
refuses a valueelse ifchain withE2S18and its scope-HIR then truncates
the binding's visibility. The Text-literal initializer and thevalue_if_end
abort were fixed inv0.13.3-seed; the chain is the remaining slice and is
deliberately not grown into this release.
Proof
- exact-main CI run https://github.com/kofun-lang/kofun/actions/runs/37099816838: all four required jobs green at
10e52e3a8ef3973595dc86b5168997485d513060. - exact-tag release workflow run https://github.com/kofun-lang/kofun/actions/runs/37104237904 at the same SHA.
task release-verify-publicationproves nine assets, both digest manifests
over the seven payloads, and that localHEAD, remotemain, the local tag
and the remote tag all resolve to the release commit.
v0.13.3-seed
v0.13.3-seed
This seed release changes no published claim. It puts the Owned-composite
ownership classification into production and closes two Stage 2 pair
divergences; it also records two decisions as specification and simplifies the
release procedure. Nothing in release/claims.json moved, so the version is a
PATCH. The tagged artifacts/release-evidence/CLAIMS.md is still the authority
for each supported slice.
Published claim changes
None. release/claims.json and spec/release-claim.schema.json are
byte-identical between the previous tag v0.13.2-seed
(8f708f0c0769413eaa33f541f9dcf5dfd2318dd6) and the release commit
(git diff --stat v0.13.2-seed a596d133 -- release/claims.json spec/release-claim.schema.json is empty).
Other implementation changes
- Owned composites are classified and their copies refused
(#1243,
PR #1693).- Each accepted nominal record and ADT is classified Owned or Managed under
RFC-0004 K-JOIN/K-ANY. A mode-less parameter head, aletcopy and==/!=
of an Owned composite refuseE353with the causal path and the 32-byte
remedy; positionaltaketwice isE2S123and aneditparameter is
E2S181. - A value read out of a
RootAuthorityfield keeps its own direct-authority
E353wording; a field read is not a whole-binding copy. - New gate
task authority-structural-kind.
- Each accepted nominal record and ADT is classified Owned or Managed under
- An over-bound Text in
stage2_bytes_assign_textis refused by name
(#1660,
PR #1688).- The bridge raises
R033and returns the limit status instead of returning a
private status a discarded statement then drops. Both halves emit the same
check;spec/bytes-bounded-v1.md§6.7 and §8 state the enforced bound.
- The bridge raises
- The Kofun half is aligned with C on Text literals and value
if
(#1679,
PR #1687).let a: Text = "x"no longer refusesE2S15;value_if_endno longer
indexes with-1on a bare Bool binding; four shadowingvalue_endlocals
no longer read before initialisation. Three pair-agreement fixtures join
tests/conformance/result-propagation.
- The release procedure is simplified without dropping a proof
(#1685,
PR #1686).- Steps 2-5 become
task release-prepare; step 4's publication checks become
task release-verify-publication. Each moved check keeps a self-test under
task release-procedure, andgate-reachabilityand the
forbidden-requirements census record both operator commands.
- Steps 2-5 become
- The C11 command-I/O decision is recorded
(#1665,
PR #1691). Operands are
Text(at most 256, 255 bytes each,argv[0]observable); standard input and
standard error are bounded host-boundary operations; a failed operation
reports anIntstatus. - The DecimalError and Fixed v1 source forms are recorded
(#1663,
PR #1692).
spec/decimal-error-v1.mdis normative under RFC-0015. - RFC-0017's identity framing is amended to the #303 frame and KIF v3
domains (#1689,
PR #1699). - The live backlog snapshot is reconciled after #1243 and #1665 closed
(PR #1700).
Defects inherited from v0.13.2-seed, left open
- #1483 — self-compilation bound.
--compile-outcome bootstrap/stage2/compiler.kofunstill stops atE2S10 unsupported Core builtin call find at byte 1213(exit 3). The same stopping point was measured
onv0.13.2-seed, so this range did not create it. - #1679 — value-position
else ifchain. The chain still differs in
scope-HIR binding visibility between the pair halves (C47vs Kofun74),
because the C half refuses a valueelse ifchain withE2S18and its
scope-HIR then truncates the binding's visibility. It is the remaining slice
of the issue whose Text-literal initializer andvalue_if_endclasses this
range fixed (above); it is recorded on the issue and deliberately not grown
into this release.
Proof
- exact-main CI
run 36421502892:
all four required jobs green at
a596d133f0b32745113581df5d7c2a669288c4e2. - exact-tag release workflow
run 36487199296
at the same SHA. task release-verify-publicationproves nine assets, both digest manifests
over the seven payloads, and that localHEAD, remotemain, the local tag
and the remote tag all resolve to the release commit.
v0.13.2-seed
v0.13.2-seed
This seed release changes no published claim. It puts the scoped-parallelism
ownership rules into production as an analysis entry with registered
diagnostics, and replaces three Stage 2 failure paths with refusals by name:
operator operands, authority field reads and postfix ?. Nothing in
release/claims.json moved, so the version is a PATCH. The tagged
artifacts/release-evidence/CLAIMS.md is still the authority for each supported
slice.
Published claim changes
None. release/claims.json and spec/release-claim.schema.json are
byte-identical between the previous tag v0.13.1-seed
(5d2699250ed3b62b7f4657e71248b97620fa2221) and the release commit.
Other implementation changes
- Scoped-parallel ownership is decided in production (#1162, PR #1669).
kofun-stage2 --check-scoped-ownership INPUT OUTPUT LOGICAL-PATH(Kofun
check_scoped_ownership_file) derives, for eachpar, the bounded input of
the accepted modelspec/concurrency/scoped-parallelism-v1/model.mjs. The
facts come only from checked lifecycle rows, the complete capture collector
and the expanded parent accesses. The input is then decided natively with
the contract's rules: sibling exclusivity over live intervals, §6 overlap, a
takethat a join never restores, parent conflicts, and handle escape.- Conservative derivation:
- only a plain-statement join ends a task's liveness;
- a taken place stays removed after the scope;
- a
parin a loop cannot take an outer binding (E2S123); - a handle or the scope token used inside any closure is an escape;
- a parent use of an impure callable (a parameter, a capturing closure, a
returned lambda) takes an explicit unknown place.
- The model gains one place form,
{"unknown": ID}. Its 20 fixtures and 214
assertions are unchanged. - The new gate
task concurrency-ownershipcovers 42 decisions, 5 refusals,
all 18 source-expressible model fixtures and the 256/257 parent-action
bound. It runs on O0, O2, ASan+UBSan and the canonical Kofun half, and
requires every production decision to equal the model's decision over the
same derived input. - It stays analysis-only: ordinary compilation still refuses
parwith
E2S154. No scheduler, runtime, backend or capability support is claimed.
The next child, #1164,
isneeds-detail.
- One registered code per scoped-ownership class (#1163, PR #1671).
E2S183capture conflict,E2S184overlap unknown,E2S185parent
conflict,E2S186use after take,E2S187handle escape,E2S188invalid
model. The mapping sits in the §8 table of the spec and in
tests/diagnostics/registry.tsv.- Messages name lexical task numbers, both modes, and a disclosure-safe place:
visible names, exact i64 slice bounds,_for a dynamic bound,<hidden>
for an inaccessible name. kofun checkreports a rejectedparby its class. An acceptedparkeeps
itsE2S154refusal, so no program changes from accepted to rejected.
- Operator operands the C11 lowering cannot declare are refused at
check(#1658, PR #1677).==,!=,<,<=,>,>=,+,-,*with a record, enum,
List[Int]orBytesoperand, and a Text/Int comparison, now giveE2S15
naming both operand types before any C is written. Previously they passed
checkand failed in the host C compiler.- Every Int/Int and Text/Text case emits byte-identical C.
- An authority-typed record field read has its own type everywhere it is used (#1659, PR #1676).
- Reading a
RootAuthority,EnvironmentAuthorityorEnvironmentKeyfield
no longer builds as anInt. Return, operator andprintsites refuse with
E2S15; copying an Owned authority out with aletrefuses withE353. - The field's base is resolved through the scope HIR, so a shadowing binding is
typed correctly in both directions.
- Reading a
- Postfix
?is parsed and refused by the result-propagation-v1 rules (#1662, PR #1678).- Every
?Stage 2 can see is a misuse until aResulttype exists. It now
getsE2S189(operand is not aResult),E2S190(optional operand;
suggestsok_or(error)?) orE2S191(?on a pipeline stage; suggests
parenthesising), with exit 1 and no Stage 1 fallback. An unknown callee keeps
E2S16. - The new gate is
task result-propagation.
- Every
- The ownership code no longer spells the
parkeyword as a name (#1483, PR #1683).paris a Stage 2 keyword. The #1162 ownership helpers (PR #1669) used it
for the lexical-index parameter and locals, and the file entry's row offset.
The C half and the canonical interpreter accept that, but the Stage 2
compiler does not, so the release sources could not self-compile as far as
the previous tag.- The names are now
par_indexandpar_row; only code tokens change, and the
C half mirrors the names. task concurrency-ownershipnow refuses anypartoken in
compiler.kofun's code, outside strings and comments. This is the second
keyword-as-name regression in the Kofun half (the earlier one is
9f87c2a2).
An independent read-only correctness review of all five #1162/#1163/#1658/
#1659/#1662 PRs, by a peer agent session, found three soundness defects before
merge, all fixed with regression cases:
- closures that let racy or use-after-take programs through the ownership
derivation (#1669); - a false
E353, and in the other direction a missedE353, under a shadowing
binding (#1676); - a
?after a valueif/matchthat still fell back to Stage 1 (#1678).
Merged since the previous tag, in order, each as a linear stack whose merge tree
equals the head that passed exact-head CI: PR #1669 at f810cc55, PR #1671 at
6d371891, PR #1677 at 7f3c7dec, PR #1676 at b0f9140d, PR #1678 at
baa7c48b, then the VERSION-only commit f574f6af and the evidence-binding
commit f81174f1. PR #1683 lands the par-name fix on top.
Inherited limits
Previous published release: v0.13.1-seed, commit
5d2699250ed3b62b7f4657e71248b97620fa2221.
- #1483 remains open: native
self-compilation is incomplete. Re-measured on the release commit8f708f0c
(treee14e6cc8, inputcompiler.kofundigest98ff4cc6…) with a fresh
strict C11-O2 -Wall -Wextra -Werror -pedanticbuild (GCC 16.2.1) under
nice,--compile-outcome bootstrap/stage2/compiler.kofunstops with
error[E2S10]: unsupported Core builtin call `find` at byte 1213: exit 3
after 881 s, a retained 76,212-byte IR and 4,701,331-byte token tape, no C
output and empty stderr. That is the same stopping point, byte for byte, as the
v0.13.1-seedmeasurement. Thev0.13.2-seedsources carried a regression
that this release fixes: on the untagged release commitf81174f1the same
command stopped earlier, at parse, witherror[E2S154]: scoped parallelism `par` expects `|scope|` at byte 1270705
(exit 1, 593 s, 4,701,262-byte token tape, recorded on PR #1683);
#1683 restores the previous tag's stopping point on the tagged commit. This is
a measured stopping point, not an exhaustive list of later lowering gaps. - #1679: the Kofun half of the
Stage 2 pair refuseslet a: Text = "x"withE2S15 initializer type mismatch,
while the C half compiles it. Reproduced identically onv0.13.1-seedand on
the release sources: C exit 0, Kofun half exit 1. It is a pair-agreement defect;
the shipped compiler is the C half. - #1681: value
if/match
extent disagrees between the halves. On
let c = if flag { 1 } else { 2 }with aBoolbinding, the C half refuses
withE2S32and the Kofun half stops with "compiler index out of bounds",
identically onv0.13.1-seedand on the release sources. - #1551,
#1577 and
#1578 remain selected
decision profiles with no production implementation claimed.
spec/native-cli-action-binding-v1,spec/live-https-get-adapter-v1and
spec/atomic-publish-if-absent-v1are byte-identical between the previous tag
and the release commit.
No new regression is accepted into this release merely because it has an issue
number.
Verification
Required local task verify passed on tree
e14e6cc868bc08a421568de7642049eb6240c407 before the tag. That is the tree of
the release commit 8f708f0c0769413eaa33f541f9dcf5dfd2318dd6. The run was at PR
#1683's exact head 85313f96 in an isolated detached worktree; after the merge,
8f708f0c^{tree} was rechecked equal to it. The run used CC=/usr/bin/cc and
VERIFY_JOBS=3, from 2026-09-25 22:53:34 to 23:46:43 UTC (3,189 seconds), and
exited 0 with 1,828 PASS lines and no failure marker. Start/end load averages
were 0.80/0.96/0.62 and 0.99/1.10/1.22. The tree hash was identical and the tree
clean at start and end. Remote main was re-read at 8f708f0c before the tag.
The release adds no VERSION or evidence commit on top of the verified tree:...
v0.13.1-seed
v0.13.1-seed
This seed release changes no published claim. It lands compiler capture facts as KSE2 transactions and typed sidecars, the runtime half of Fixed[S], and the fuzz lane's first recorded finding with its fix. Nothing in release/claims.json moved, so the version is a PATCH. The tagged artifacts/release-evidence/CLAIMS.md is still the authority for each supported slice.
Published claim changes
None. release/claims.json is byte-identical between the previous tag v0.13.0-seed (fe1142a7039a0862ac3558729ab2477bb7a604d6) and the release commit.
Other implementation changes
- Compiler capture facts reach KSE2 and the typed sidecar (#1225, PR #1672).
- A new producer (
bootstrap/stage2/capture_events_producer.c) runs the §14 complete-capture pipeline in-process against the maintained C half. It publishes the checked capture section as one KSE2 transaction and a typed-sidecar v2 file:checked/completeon success;failed/partialwith the compiler's own code and byte offset;cancelled/partialwith exactly the committed prefix. - KSE2 gains node kind 13,
analysis.expression. KSE1 still refuses it. - The composed gate
task concurrency-capture-eventsderives its expectations from the authored fixtures, the independent oracle and the accepted model, never from the producer. - This closes the scoped-capture derivation umbrella #1161.
- It stays analysis-only: ordinary compilation still refuses
E2S154. Conflict and liveness decisions are #1162, and no scheduler, runtime, backend or capability support is claimed.
- A new producer (
- The runtime half of
Fixed[S](#1661, PR #1670).bootstrap/stage2/decimal_v1.{h,c}gain RFC-0015's construct, clone, move and drop entry points over the canonical Decimal payload.- Construction is exactly
kofun_decimal_round, restricted toSin0..6144. - Every failure is a returned status rather than the value shim's fatal exit, and a failure leaves the output empty, the input unchanged and no temporary live.
- No compiler calls them yet; #1250 is the first caller, and no capability row moves.
- The new gate
task decimal-fixed-runtimeruns strict and under ASan/UBSan, and refuses allocations one at a time. It found two defects that were already in the Decimal runtime, both fixed:magnitude_divmodreturned failure with its quotient still allocated when the remainder's allocation was refused.kofun_decimal_divide_exact,kofun_decimal_divide_roundedandkofun_decimal_roundeach leaked one block on such a refusal.kofun_decimal_equalcalledmemcmp(NULL, NULL, 0)when comparing two zeros. That is undefined; at-O2GCC used the implied non-null pointer to drop later null checks.
- Decimal statuses, D001–D007 messages and every existing golden are unchanged.
- The scheduled fuzz lane's first recorded finding, fixed (#1656, PR #1657).
- The failure: on 2026-09-24 the rotating-seed lane (base seed 44) failed with
adapter timed out: c11-stage1. On an emptybuild/,semantic_differential.sh's first case timed a cold build of the 38,037-line Stage 2 compiler inside the runner's 10 s adapter bound, not a generated program. The same seed agrees on all 48 programs once the compiler exists. - The fix: the generator now prepares the compiler before its first timed case, in both generation and
--replaymode. - A regression test in
task fuzzholds that property independent of machine speed. - The finding is the first row of
tests/fuzz/FINDINGS.md, resolved as fixed. - Fuzz run 36039706257, dispatched on
main@57600b24withseed=44, passes every generator. This includessemantic_differentialseed 1310084867 on 48 programs.
- The failure: on 2026-09-24 the rotating-seed lane (base seed 44) failed with
Merged since the previous tag: PR #1657 at 57600b24, PR #1670 at af125c85, PR #1672 at efce9fdb. Each merged after its exact-head CI passed.
Inherited limits
Previous published release: v0.13.0-seed, commit fe1142a7039a0862ac3558729ab2477bb7a604d6.
- #1483 remains open: native self-compilation is incomplete. The canonical pair is byte-identical between the previous tag and the release commit:
compiler.cbf169aef…,compiler.kofunf105856d…,SHA256SUMS,trusted_seed_sha256. Onlydecimal_v1.c, whichcompiler.cincludes, gained the additive entry points above.- Re-measured on the release sources (
git archive efce9fdb) with a fresh strict-C11-O2 -Wall -Wextra -Werror -pedanticbuild (GCC 16.2.1).--compile-outcomeovercompiler.kofun(input rechecked atf105856d…) still stops witherror[E2S10]: unsupported Core builtin call `find` at byte 1213: exit 3 after 842 s undernice, a retained 69,950-byte IR and 4,259,638-byte token tape, no C output and empty stderr. That is the same stopping point, byte for byte, as the v0.13.0-seed measurement. This is a measured stopping point, not an exhaustive list of later lowering gaps.
- Re-measured on the release sources (
- #1551 remains the selected user-defined native CLI action-binding profile. A production action table is still blocked on its typed authority/result carriers.
- #1577 remains the selected capability-bearing HTTPS GET adapter profile. A production live adapter is not claimed.
- #1578 remains the selected atomic create-if-absent profile. A production publication primitive is not claimed.
The three decision-profile directories are byte-identical between the previous tag and the release commit: spec/native-cli-action-binding-v1, spec/live-https-get-adapter-v1 and spec/atomic-publish-if-absent-v1. Their introducing commit, 144280a58a8af42f921f2f78f5203cee15db6dd0, is an ancestor of the previous tag. No new regression is accepted into this release merely because it has an issue number.
Verification
Required local task verify passed on tree ef4d307390929b98cb004b0dfaf5098c55bc432d before VERSION changed. That is the tree of actual main efce9fdbae928f1e76b34fe75e59ca155219f587. The run was at PR #1672's exact head 61cdbd5c in an isolated detached worktree; after both merges, efce9fdb^{tree} was rechecked equal to it. The run used CC=/usr/bin/cc and VERIFY_JOBS=3, from 2026-09-24 18:21:20 to 19:26:03 UTC (3,883 seconds), and exited 0 with 1,753 PASS lines and no failure marker. Start/end load averages were 19.56/16.53/8.27 and 1.64/1.51/2.65. The tree hash was identical and the tree clean at start and end. Remote main was re-read at efce9fdb before the VERSION commit. The release adds only separate VERSION (4a792905) and regenerated-evidence (5d269925) commits to this verified source tree.
Exact-main CI passed all four required jobs at 5d2699250ed3b62b7f4657e71248b97620fa2221: Kofun verification, Backlog issue state, Native host evidence binding and Release evidence pack.
Exact-tag release workflow succeeded at 5d2699250ed3b62b7f4657e71248b97620fa2221, including its independent task verify, six native checkpoint builds, source archive creation and publication.
The published release is a nondraft seed prerelease. All nine expected assets were downloaded; bin/kofun-digest verified the seven payloads against their manifests. A fresh git archive compressed with gzip -n was byte-identical to the published source archive. The tag, main, local HEAD and successful workflow head all resolve to the exact release commit.
The assets are the reproducible source archive plus six native checkpoint images and two digest files. Linux checkpoints print 42; the Windows and macOS checkpoints return zero. They demonstrate the bounded native image claim. A multi-platform compiler install remains an M4 deliverable.
v0.13.0-seed
v0.13.0-seed
This seed release adds the bounded deterministic benchmark report pipeline and widens the existing Bytes checkpoint. The MINOR version follows those claim changes. The tagged artifacts/release-evidence/CLAIMS.md remains the authority for each supported slice.
Published claim changes
benchmark-report-v1— implemented on the C11 backend. The production Kofun model preserves all 49 report fields and 100 samples in two capacity-64 segments. A pure bounded Bytes codec encodes and decodes exact canonicalkofun.bench-report/v1data; deterministic comparison uses the caller's threshold. The composed gate checks canonical reports over 4 KiB, unavailable versus zero, non-normalized identity and neutral failures. Encoding prepares a private buffer and commits after successful destination reserve. This is a bounded model/codec/comparison claim; the existingbenchmark-harnessrow is unchanged.bounded-bytes— widened checkpoint. The existing Bytes[65536] carrier now has a whole-file read and a Text bridge. Oversize input, unreadable paths and allocation refusal preserve the carrier, with R027/R026/R028. Text crosses as exact bytes; checked ranges cross back with R029..R032 for range, Text bound, NUL and UTF-8 failures. One Text is bounded to 255 bytes. File reads take a bare path and do not establish attenuated filesystem authority.
Other implementation changes
- Scoped-capture analysis now has production lifecycle identities (#1220), checked field/slice places (#1221), direct read/edit/take sets (#1222) and bounded same-unit call summaries with deterministic SCC convergence (#1223). The complete entry is
--emit-complete-capture-hir-v2; §14 of the scoped-capture specification defines its source profile and refusal bounds. Whole expectations cover native O0/O2, ASan/UBSan and canonical Kofun, including deep projection and forwarded/free-environment slice-bound validation. This remains analysis-only: ordinary compilation retains E2S154, conflict/liveness decisions remain #1162, and scheduling/runtime/backend support is not claimed. - Complete synthetic KSE2 transaction validation and typed-sidecar v2 projection land in #1224. Real compiler event production remains #1225; these are separate completion boundaries.
- The canonical compiler pair now shares bounded private Unicode escaping and file-identity guards (#1642); semantic logical paths follow the anchored URI-scheme rule (#1644). Streaming digest compatibility now includes binary chunk boundaries and the complete compiler sources (#1643).
- Exactly one terminal comma is accepted in parameter and argument lists; empty/doubled members receive E2S182 (#1640). The WASI adapter gains independently gated private command-memory carriers, an allocator and checked UTF-8, while host operations remain unimplemented (#1639).
Direct captures merged via PR #1652 at b338ea1f; complete summaries merged via PR #1654 at dec03313. Both issues are closed after final-head CI and all six original acceptance criteria were verified.
Inherited limits
Previous published release: v0.12.2-seed, commit 6aef329f39b015399c54adf2dda75ff2f162ab62.
- #1483 remains open: native self-compilation is incomplete. A fresh strict-C11 O2 build from the previous tag refuses its own source with
error[E2S35]: lexical use limit is 256 per function at byte 30874(exit 1). The new lexical-budget slice removes that first limit, and its two-host coverage measurement is recorded, but does not complete the issue. A fresh strict-C11 O2 archived-source probe of the b944ebc compiler pair, rechecked byte-identical to the release pair, reaches E2S10 for thefindbuiltin at byte 1213 (actual exit 3, 729 seconds), retaining a 69,950-byte IR and 4,259,638-byte token tape with no C output and empty stderr; both input hashes were rechecked. The keyword-binding regressions found during this release audit were fixed before publication. This is a measured stopping point, not an exhaustive list of later lowering gaps. - #1551 remains the selected user-defined native CLI action-binding profile; a production action table is still blocked on its typed authority/result carriers.
- #1577 remains the selected capability-bearing HTTPS GET adapter profile; a production live adapter is not claimed.
- #1578 remains the selected atomic create-if-absent profile; a production publication primitive is not claimed.
The three decision profile files above are byte-identical between the previous tag and the release commit fe1142a7039a0862ac3558729ab2477bb7a604d6. Their introducing commit 144280a58a8af42f921f2f78f5203cee15db6dd0 is an ancestor of that published tag. The final release tree fe1142a7039a0862ac3558729ab2477bb7a604d6 was rechecked against the previous tag before publication. No new regression is accepted into this release merely because it has an issue number.
Verification
Required local task verify passed on actual main 176689866970773d1e77f485a0b007c17608872e before VERSION changed: CC=/usr/bin/cc, VERIFY_JOBS=3, 2026-09-23 18:48:59–19:39:04 UTC, 3,005 seconds, exit 0. Start/end load averages were 1.25/0.89/0.68 and 2.14/1.80/1.78. HEAD, clean tree and remote main were rechecked unchanged; the full log and compiler census are retained. Preflight receipt. The release adds only separate VERSION and regenerated-evidence commits to this verified source tree.
Exact-main CI passed all four required jobs at fe1142a7039a0862ac3558729ab2477bb7a604d6: Kofun verification, Backlog issue state, Native host evidence binding and Release evidence pack.
Exact-tag release workflow succeeded at fe1142a7039a0862ac3558729ab2477bb7a604d6, including its independent task verify, six native checkpoint builds, source archive creation and publication.
The published release is a nondraft seed prerelease. All nine expected assets were downloaded; bin/kofun-digest verified the seven payloads against their manifests. A fresh git archive compressed with gzip -n was byte-identical to the published source archive. The tag, main, local HEAD and successful workflow head all resolve to the exact release commit.
The assets are the reproducible source archive plus six native checkpoint images and two digest files. Linux checkpoints print 42; the Windows and macOS checkpoints return zero. They demonstrate the bounded native image claim. A multi-platform compiler install remains an M4 deliverable.
v0.12.2-seed
No published claim changed
release/claims.json and spec/release-claim.schema.json are byte-identical
to v0.12.1-seed. No capability rose, no bounded slice widened, no refusal
moved. Under docs/RELEASING.md that is a PATCH, and the version number says
only that. artifacts/release-evidence/CLAIMS.md is unchanged and remains the
authority for what each claim covers.
What is in the range
One backend fix, in the wasm32-wasi-command1 target and its gate.
| commit | PR | issue | what |
|---|---|---|---|
cb74d6a9 |
#1637 | #1296 | The command target refuses a host operation at the operation's span, refuses non-canonical manifest bytes as NonCanonicalManifest, and leaves no artifact on a late write failure. |
The defect this removes
bin/kofun build … --target wasm32-wasi-command1 -o DIR, with DIR a
directory, exited 0, printed the output path, and wrote nothing there —
mv of the temporary onto a directory does not fail, it moves the complete
module into the directory under its temporary name. A complete artifact where
nothing expects one, reported as success. The driver now refuses a directory
output by name before anything is written, and the emitter carries an announced
fault seam (KOFUN_WASM_CORE_FAULT=write) so a genuinely late, mid-write
failure can be forced and shown to leave neither module nor temporary.
The manifest fix matters for artifact identity: the manifest's SHA-256 binds
into the module, so two spellings of one set of grants were two artifact
identities. Only the model's own canonical() spelling is accepted now.
What #1296 closes, and what it deliberately leaves
All eight of #1296's acceptance criteria hold at this release. The import
projection for programs that reach a checked operation is not here and is
not claimed: #1293's binding constraint has build refuse the root/environment
carrier until #1242–#1246 exist, so every host operation is refused at its span,
and the adapters are #1297–#1301 once that carrier lands. The gate header says
so.
Inherited defects deliberately left for a later release
No regression created by this range is shipped. The -o <directory>
defect is present in v0.12.1-seed and every tag since #1437; this range
removes it. Unchanged from the v0.12.1-seed notes, and all under active work
by other sessions:
| issue | bounded effect |
|---|---|
| #1483 | Stage 2 cannot yet compile its own compiler; PR #1635 is green and held out of this range by its owner pending a ledger re-measurement |
| #1513 | both halves of the Stage 2 pair do not yet agree on non-ASCII identifiers; under implementation |
| #1499 | a compiled program cannot receive input; PR #1636 open with conflicts |
| #1581 | a Bytes-return failure guard discards the moved result carrier without releasing it |
| #1551, #1577, #1578 | the decision-only boundaries v0.11.3-seed recorded |
Proof chain
| gate | result |
|---|---|
local task verify at f988a790480383190f1a83b6e424ddbefb706d71 |
exit 0, 1994 PASS lines, no failure marker, in an isolated worktree with the box cleared by its other user; HEAD^{tree} stamped identical before and after (9d6b147c…) |
task release-evidence + task release-claims, before and after the VERSION change |
pack current; claims join |
task repository-check |
PASS; bin/kofun --version reports Kofun Stage 1 0.12.2-seed |
exact-main CI at f988a790 |
all four required jobs succeeded — Backlog job re-run after a tracker correction (#1297), recorded on #1638 |
exact-main CI at 6aef329f39b015399c54adf2dda75ff2f162ab62 |
all four required jobs succeeded |
exact-tag release.yml at 6aef329f39b015399c54adf2dda75ff2f162ab62 |
success: independent task verify at the tagged commit, source archive, six native images, publication |
| publication metadata | not a draft; marked as a pre-release; exactly nine assets with the expected versioned names |
| digest manifests | post-publication download verified with bin/kofun-digest -c: one source archive and six checkpoint images, all OK |
What this release includes, and what it does not
It includes a source archive and its SHA-256, plus the exact six SHA-256-pinned
native checkpoint images covered by the native-six-host-execution claim and
one Kofun-computed digest manifest. Linux prints 42; the Windows and macOS
images return zero with no output. They prove final-image encoding and
matching-host execution; they are not general compiler CLIs.
It does not include a multi-platform compiler install. That remains an M4
deliverable (docs/ROADMAP.md §M4).
v0.12.1-seed
No published claim changed
release/claims.json and spec/release-claim.schema.json are byte-identical
to v0.12.0-seed. No capability rose, no bounded slice widened, no refusal
moved. Under docs/RELEASING.md that is a PATCH, and the version number says
only that. artifacts/release-evidence/CLAIMS.md is unchanged and remains the
authority for what each claim covers.
What is in the range
One tooling change.
| commit | PR | issue | what |
|---|---|---|---|
ffa05008 |
#1633 | #1632 | task preflight reports the silent-assertion budget. Landing #1539, a new shell script passed all eight preflight obligations and was then refused by the Kofun verification lane for 1 silent assertions and no budget entry — one CI lane to learn a fact a 2.4-second gate already knew. Preflight now runs nine checks, seven of them the fast half of gates verify already runs. |
What moved on the tracker in this window's lead-up
None of it is in the range; each is recorded on its own issue.
- #1516 and #1540 — shipped in
v0.12.0-seedon 2026-09-06 and left open for
fifteen days with live claims and an un-thawed FREEZE. Closed with terminal
claims; the window's THAW is on #1631. - #1513 — was in a four-week mutual
Blocked bycycle with #1483. The edge
from #1483 is technical and stays; the edge from #1513 was a resource lock on
a claim that ended 2026-08-25. Broken, promoted, and now under active
implementation by another session. - #1499 — re-measured:
stage2_bytes_byte_atis statement-only by design
(E2S179) andsha256_of_messagetakesList[Int], so no byte can reach
the digest from source. Moved toneeds-decisionwith the three options and
a decision owner recorded.
Inherited defects deliberately left for a later release
No regression created by this range is shipped: the range is a preflight
check. Unchanged from the v0.12.0-seed notes:
| issue | bounded effect |
|---|---|
| #1513 | both halves of the Stage 2 pair do not yet agree on non-ASCII identifiers or refuse output aliases of the input; Option A is decided, implementation in progress |
| #1499 | a compiled program cannot receive input; blocked on a decision about the published bounded-bytes boundary |
| #1581 | a Bytes-return failure guard discards the moved result carrier without releasing it |
| #1551, #1577, #1578 | the decision-only boundaries v0.11.3-seed recorded |
Proof chain
| gate | result |
|---|---|
local task verify at e12237103a8b6ce7509b81172a7f417985d5a317 |
exit 0, 1994 PASS lines, no failure marker, in an isolated worktree; HEAD^{tree} stamped identical before and after (fcc1b8ce…) |
task release-evidence + task release-claims, before and after the VERSION change |
pack current; claims join |
task repository-check |
PASS; bin/kofun --version reports Kofun Stage 1 0.12.1-seed |
exact-main CI at e1223710 |
all four required jobs succeeded — the Backlog job re-run after a tracker correction, recorded on #1634 |
exact-main CI at 2fd6fadfa3832511eb7863483483a10f6e92b59e |
all four required jobs succeeded — same re-run, same reason |
exact-tag release.yml at 2fd6fadfa3832511eb7863483483a10f6e92b59e |
success: independent task verify at the tagged commit, source archive, six native images, publication |
| publication metadata | not a draft; marked as a pre-release; exactly nine assets with the expected versioned names |
| digest manifests | post-publication download verified with bin/kofun-digest -c: one source archive and six checkpoint images, all OK |
What this release includes, and what it does not
It includes a source archive and its SHA-256, plus the exact six SHA-256-pinned
native checkpoint images covered by the native-six-host-execution claim and
one Kofun-computed digest manifest. Linux prints 42; the Windows and macOS
images return zero with no output. They prove final-image encoding and
matching-host execution; they are not general compiler CLIs.
It does not include a multi-platform compiler install. That remains an M4
deliverable (docs/ROADMAP.md §M4).
v0.12.0-seed
One claim added, two widened
This is a MINOR release: release/claims.json gained a published claim and two
existing claims' bounded slices widened. artifacts/release-evidence/CLAIMS.md
is the authority for the wording below; the notes do not describe any
capability a second way.
New: positional-move-crossings — checkpoint, frontend
A bare owning
Bytesor Int/Bool-only nominal record passed to a resolved
direct current-file positionaltakeparameter is a source-order move. Later
use and second transfer of that BindingId are E2S123 with exact primary and
related spans; a fresh shadowing BindingId remains distinct. Trivial-record
readkeeps its by-value ABI andeditis refused as E2S181 at the mode token
before C publication.
Gate: task move-call-crossings, in verify, running the production compiler
at O0 and O2 under ASan/UBSan with mutation tests over mode, direct-resolution,
bare-binding, type/owner, straight-line and identity decisions.
What it is not. Authorities, resource-bearing composite records,
indirect/member calls, borrowed-to-owning escalation, conditional/loop
crossings, and general CFG/lifetime/cleanup analysis remain outside the
checkpoint. Component exclusion witnesses do not imply full backend admission.
No general ownership pass, new source syntax, record reference ABI, authority
guarantee or cross-release compatibility is promised.
Widened: bounded-bytes — checkpoint, c-backend
Two refusals moved from "known gap" to "refused by name":
- Temporary
Bytesarguments to direct declaredread/edit/take
parameters are refused as E2S177 before C or executable publication, with
argument position and missing-guard mutations pinned. This is #1516: the
previous release emitted&<rvalue>and sent the author to a byte offset in
generated C. - The whole-carrier
Bytesreturn checks failure before transferring
ownership; a two-allocation fixture and emitted-C fault injection prove
success transfer and failure cleanup. This is #1581.
Still not established: a natural source-level failure reproducer, complete
cleanup across every exit or result path, an owning-Bytes fixture for record
typed returns, or transactionality beyond the named direct mutation cases. It is
not a general buffer and has no Text bridge.
Widened: affine-resource-handle — checkpoint, frontend
Production consuming calls invalidate the predecessor without a manual
post-calltake; reintroducing that marker is refused as a second move.
The RFC-0010 fixture and the public ownership example stop using a standalone
take after each consuming transition as a transfer workaround: the accepted
call itself consumes the predecessor. The standalone evaluator remains a
reference for successful observations, not positional move validation.
What is in the range
| commit | what |
|---|---|
86908e4b |
compiler: check bounded positional ownership crossings — #1516, #1540, RFC-0010 migration, shared helper refactor, the new checkpoint claim |
1f0f2376 |
examples: consume affine handles at positional calls; exact prior output preserved |
6316f8ca |
compiler: bind E2S181 to its structured semantic-event diagnostic and prove missing-observer registration fails |
Inherited defects deliberately left for a later release
previous_tag=v0.11.6-seed. No regression created by this range is shipped.
The only open boundaries carried forward are the decision-only ones every
release since v0.11.3-seed has named: #1513, #1551, #1577, #1578. Their
decisions are recorded; their capabilities are not claimed, and no claim
wording implies otherwise.
The three emission defects v0.11.5-seed named as #1628 were fixed in
v0.11.6-seed and are not carried.
Proof chain
| gate | result |
|---|---|
local task verify at 6316f8ca (release owner, 2026-09-06) |
exit 0, 1120 s, CC=cc VERIFY_JOBS=3; recorded in the FREEZE on #1516 and #1540 |
local task verify at 41e7464d (2026-09-21) |
exit 0, 1994 PASS lines, 20m16s, in an isolated worktree with the tree hash stamped before and after (a87b251e, unchanged). A first attempt in the shared checkout was discarded because a second session switched that checkout mid-run; the record on #1631 has the timeline |
task emission-compiles at 6316f8ca |
exit 0: 1312 of 1329 sources build or refuse by name, 17 recorded exceptions, all eight checker proofs pass |
exact-main CI at 41e7464d5ad0edb8741b25aa948e531a02e75ef2 |
all four required jobs succeeded — Kofun verification, Backlog issue state, Native host evidence binding, Release evidence pack |
exact-tag release.yml at 41e7464d5ad0edb8741b25aa948e531a02e75ef2 |
success: independent task verify at the tagged commit, source archive, six native images, publication |
| publication metadata | not a draft; marked as a pre-release; exactly nine assets with the expected versioned names |
| digest manifests | re-downloaded 2026-09-21 and verified with bin/kofun-digest -c: one source archive and six checkpoint images, all OK |
These notes were written fifteen days after the tag. The release was
published on 2026-09-06 through step 7 of docs/RELEASING.md and stopped
before step 8; the publication record is
#1631, which says so rather
than backdating.
What this release includes, and what it does not
It includes a source archive and its SHA-256, plus the exact six SHA-256-pinned
native checkpoint images covered by the native-six-host-execution claim and
one Kofun-computed digest manifest. Linux prints 42; the Windows and macOS
images return zero with no output. They prove final-image encoding and
matching-host execution; they are not general compiler CLIs.
It does not include a multi-platform compiler install. That remains an M4
deliverable (docs/ROADMAP.md §M4).
v0.11.6-seed
Fixes and maintainability
- #1628: all three tracked emission failures now build and execute. Bare lifted-lambda values reference the lifted function; unused scalar and direct enum-constructor bindings retain their initializers and receive explicit C references. Strict C11 warning flags remain enabled. Restoring each defective emitted shape fails its regression check, and unused initializer effects and traps are covered.
- #1581: the whole-carrier Bytes return checks failure and releases live owners before the non-failing transfer. A two-allocation emitted-C probe covers success and injected failure at
-O0and-O2under ASan/UBSan with leak detection; restoring the old post-take guard fails the live-allocation witness. This is a compiler-template fault probe, not a newly discovered natural source-level failure reproducer. - Shared
unused_binding_discardandemit_bytes_returnhelpers isolate these policies in both Stage 2 halves. The paired-decision gate pins their call sites.docs/STAGE2_EMISSION.mdmaps common emission issues to implementation points and focused gates. - The full 1,320-file emission census now has 363 builds, 940 named refusals, and 17 other-driver/seed exceptions. All three
emission-defectrows and two native-fixture exceptions made obsolete by the same repair are retired. The classifier's own eight-case refusal proof remains green.
No claim is promoted and no source syntax, operation, target, or compatibility promise is added. The bounded-bytes claim's description records the corrected return behavior and its bounded proof. An obsolete #1556 limitation is removed from the specification and claim: its 71-owner regression already passed in the previous release. artifacts/release-evidence/CLAIMS.md remains the authority for all 54 claims.
Inherited limitations
The following adjacent defects remain outside this queue. Both were reproduced against a clean archive of v0.11.5-seed and the new implementation commit, 7990f13c0c5d4664d410e73035277c9ffdd65acd:
- #1516: a temporary Bytes value passed to a user function's
readparameter still reaches a host-C lvalue error. The separately claimed, uncommitted #1516 worktree is preserved. - #1540: an ordinary positional
takecall still permits a subsequent source use of the moved binding. The same probe prints7and then0on both versions instead of refusing that later use. Recordeditremains outside the fixed scope.
The release adds no regression demonstrated by these probes. Complete cleanup across every result path, general compiler self-hosting, and the other limitations recorded by the claims remain outside this patch release. The historical multi-hour branch-coverage ledger was not remeasured; the static pair gates, focused runtime proofs, full emission census, and full verification runs are the evidence for this change.
Verification and publication
- Final release commit:
41f7c3de06ff8a47f16c4844dfecfd58b592acd7. Remotemain, local and remoterefs/tags/v0.11.6-seed, and both workflow heads were checked against this exact SHA. - Local pre-flight:
CC=cc VERIFY_JOBS=3 task verifyexited 0 at implementation commit7990f13c0c5d4664d410e73035277c9ffdd65acd, 2026-09-06 08:53:05–09:14:20 UTC. Start/end load samples were3.46/4.52/3.39and2.15/2.75/3.54. The subsequent changes only setVERSIONand bind the regenerated evidence to it; release-evidence, release-claims, and repository-check passed afterwards. - All four exact-main CI jobs succeeded: Kofun verification, Backlog issue state, Native host evidence binding, and Release evidence pack.
- The exact-tag Release workflow succeeded. Its independent
task verifyran from 09:42:44 to 10:07:20 UTC; the release was published at 10:07:53 UTC. - Post-publication validation confirmed a non-draft pre-release, exactly nine expected versioned asset names, and matching Kofun SHA-256 manifests for all seven downloaded payloads. The source archive's SHA-256 is
3eb94462ab1d56d5fb91b14641d3005959698c8174090f885327d12b0be2bfcb.
The release is a pre-release and contains exactly nine assets: a source archive and its SHA-256 manifest, six native checkpoint images, and their SHA-256 manifest. Post-publication downloads matched both manifests. Linux checkpoint images print 42; Windows and macOS checkpoint images return zero. These bounded images demonstrate final-image encoding and matching-host execution; they are not general compiler executables or a multi-platform compiler installation.
v0.11.5-seed
No published claim changed
release/claims.json and spec/release-claim.schema.json are byte-identical
to v0.11.4-seed. All 54 published claims remain at the same state and the
same bounded slice; no capability rose, no slice widened, no refusal moved.
Under docs/RELEASING.md that is a PATCH, and the version number says only
that. artifacts/release-evidence/CLAIMS.md is unchanged and remains the
authority for what each claim covers.
What is in the range
Two static gates over the Stage 2 pair and the emitted-C corpus.
| commit | PR | issue | what |
|---|---|---|---|
a0666d0e |
#1627 | #1584 | Both halves of the pair are held to the decisions they spell separately — a type set, a table size, a seed constant, a declared arity. |
c9bb8994 |
#1629 | #1539 | Every program Stage 2 accepts is checked to emit C that compiles. |
6f0dd09b |
#1629 | #1539 | The new gate's silent-assertion count driven to zero rather than budgeted. |
The pair now has four class gates, not three
stage2-pair-calls resolves call targets and their arity, stage2-pair-bindings
resolves reads, stage2-pair-mirror says a counterpart exists. None of them
reads what the counterpart decides, and six defects in one week were exactly
that — five of the six literal values sitting in source in both files.
stage2-pair-decisions is the fourth member of that family: 7 paired decisions
across 14 sites, 86 ms, in verify.
The measurement corrected the issue's own proposal. The halves do not spell the
same token — validate_value_if is parse_value_if in C — so a rule of the
form "this token occurs the same number of times in both halves" is
unsatisfiable for real rows. Each row names its own token per half and the exact
occurrence count each must have.
A gate falsified its own issue's prediction
#1539 said checking the emitted-C property over the tracked corpus "finds
nothing new, because those files already build in some gate." Measured over all
1,320 tracked *.kofun: 358 built, 940 refused by name, 22 neither.
Nineteen are the wrong invocation rather than a defect — native, wasm and
selfhost-A1 fixtures whose owning gates supply their own translation units, plus
the Stage 1 seed. Three are ordinary programs the default driver owns, and
the sharpest emits error: 'k_b1' undeclared (first use in this function): the
emitter wrote a reference to a variable it never declared. Filed as #1628.
Inherited defects deliberately left for a later release
No regression created by this range is shipped. The three emission defects
are newly named, not newly broken — the range made them visible. Proved by
byte witness against the previous tag:
$ git show v0.11.4-seed:tests/conformance/inference/hm-levels/recursion.kofun \
| cmp - tests/conformance/inference/hm-levels/recursion.kofun
$ echo $?
0| issue | bounded effect |
|---|---|
| #1628 | Three tracked programs Stage 2 accepts emit C that does not compile; one is a reference to an undeclared variable. Recorded as emission-defect rows in tests/emission/exceptions.tsv, so the gate lands green without anyone pretending they are fixed. |
| #1516 | A Bytes temporary in an argument emits &<rvalue> instead of a refusal. Held under a live claim by another session; not admitted to this queue. |
| #1540 | Stage 2 positional take crossings do not record the move, and record edit does not fail closed. |
| #1581 | A Bytes-return failure guard discards the moved result carrier without releasing it. |
| #1513, #1551, #1577, #1578 | The decision-only boundaries v0.11.3-seed recorded. Unchanged. |
#1516, #1540 and #1581 are named gaps the bounded-bytes claim already carries
in release/claims.json. That wording is unchanged, so the release advertises no
capability it does not have.
Proof chain
| gate | result |
|---|---|
local task verify at b7598082e4447a7bb7ba70366f392b87988b68f5 |
exit 0, 1989 PASS lines, no failure marker; status read from the command, not from a pipeline's tail |
task emission-compiles at the merged head |
PASS: 1298 of 1320 ... 22 recorded; 8 of 8 cases behaved as required. Outside verify at 249 s, so no CI lane runs it — this local run is its evidence, stated rather than implied |
task release-evidence + task release-claims, before and after the VERSION change |
54 release claims join their published wording and evidence; 23 mutations refused |
task repository-check |
PASS; bin/kofun --version reports Kofun Stage 1 0.11.5-seed |
exact-main CI at b7598082 |
all four required jobs succeeded |
exact-main CI at 6c169db42d8179cd5fa4ea8a8908b5fecc268a50 |
all four required jobs succeeded |
exact-tag release.yml at 6c169db42d8179cd5fa4ea8a8908b5fecc268a50 |
success: independent task verify at the tagged commit, source archive, six native images, publication |
| publication metadata | not a draft; marked as a pre-release; exactly nine assets with the expected versioned names |
| digest manifests | post-publication download verified with bin/kofun-digest -c: one source archive and six checkpoint images, all OK |
What this release includes, and what it does not
It includes a source archive and its SHA-256, plus the exact six SHA-256-pinned
native checkpoint images covered by the native-six-host-execution claim and one
Kofun-computed digest manifest. Linux prints 42; the Windows and macOS images
return zero with no output. They prove final-image encoding and matching-host
execution; they are not general compiler CLIs.
It does not include a multi-platform compiler install. That remains an M4
deliverable (docs/ROADMAP.md §M4).