Activity

1. afflom

   added this to the LexLean v0.4 milestone on Oct 14, 2026
2. afflom

   added a parent issue on Oct 14, 2026

   • [v0.4] Author the production compiler itself in LexLean and verify the generated Lean implementation #27
3. github-project-automation

   added this to LexLeanon Oct 14, 2026
4. afflom

   changed the title [-][v0.4] #27 stage 5: the Rust runtime and package text generated, or declared as the minimal typed adapter[/-] [+][v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus[/+] on Oct 14, 2026
5. humuhumu33 commented on Oct 14, 2026

   

   humuhumu33

   on Oct 14, 2026

   Contributor

   More actions

   I'd like to take stage 1 (inventory and boundary) of this issue, unless someone already has it.

   It needs no library change, so it can proceed while #93 is in flight; stages 2 to 4 stay where the delivery order on #27 puts them. Stage 1 is also on #84's path: #84's new constructs (a borrowed local &T, fold_list over the defunctionalized Fn<n> by reference, Vec::with_capacity) should land in the AST this stage bounds.

   Plan, in the manner of the stage designs on #27 and #93:

   1. Post the inventory here as a design comment before any code: every construct runtime.rs (and the headers in ast.rs, the manifest and lint tables in package.rs) uses that RustSyntax lacks, and a proposed closed list of machine primitives, each with its meaning.
   2. On agreement, one PR: the §17.16 text for the boundary, its register rows, and a gate that refuses a runtime construct outside the list (with a plant).

   A draft of (1) is ready. Two points I'd like the maintainers' view on when it lands: whether the work counter is a machine primitive or a static in RustSyntax, and whether Same/Key stay as two closed traits.

   ---

   Generated by Claude Code
6. humuhumu33 commented on Oct 14, 2026

   

   humuhumu33

   on Oct 14, 2026

   Contributor

   More actions

   #91 stage 1: inventory and boundary of the Rust runtime

   Measured on main at d284b165 (after #81 / PR #88). Sources: crates/lexlean/src/calculus/rust/{runtime,ast,package}.rs, compiler/src/RustSyntax.lex.tex, compiler/src/RustSemantics.lex.tex, SPEC §17.16 and the Rust machine paragraph of §17.

   What exists today

   The runtime is two text constants: CORE (72 lines, both profiles) and STD (220 lines, rust-std only), each recorded by SHA-256 in language/semantics-1.2.toml.
   Generated code reaches it only through Item: 50 variants, 144 functions once each width is counted (36 width-free, 13 per width × 8 widths, plus 4 signed negations).
   RustSyntax (the formal AST) mirrors ast.rs without origins: 21 Expr constructors, 17 RustType constructors, 3 ItemDef constructors (enum, apply, function).
   RustSemantics evaluates every item as the calculus primitive it realizes (itemPrimitive), on erased values: an Rc or box is the value it holds.
   RustSemantics has no work counter: counted work is measured by the differential (TC-07, RB-06, RB-08), never proved.
   Outside the runtime, handwritten text also lives in ast.rs::print (crate headers #![no_std], #![forbid(unsafe_code)]) and package.rs (Cargo manifest template, ALLOWED_LINTS, provenance).

   Every construct the runtime text uses, against the AST

   Constructs the AST already has: literals, match with tuple/option/result/ordering patterns, if, let, calls, !, Ok/Some/None construction, Rc::new (as box), .clone(), i128::from (as widen), &T as a type.

   Constructs the AST lacks, by kind:

   Kind	Where in the runtime	Sites
   Item: use of fixed paths	core::cmp::Ordering, AtomicU64, Ordering as Memory	2
   Item: unit struct with derives	Overflow (Clone, Copy, PartialEq, Eq, Debug)	1
   Item: generic type alias	R<T>	1
   Item: static atomic	WORK, tick, work	1
   Item: tuple and named-field structs, generic	Str, Bytes, Node<T>, List<T>	4
   Item: generic enum with a struct variant	Repr<T>::Run { buffer, len }	1
   Item: traits and impls	Same, Key; impls for scalars, Ordering, (A, B), Str, Bytes; manual Clone; Drop	2 traits; 7 impls written, 18 from scalar!
   Item: inherent impl with &self / &mut self methods	Str, Bytes, List	3
   Item: pub mod	fixed_u8 … fixed_i64	8
   Item: macro_rules!	scalar!, fixed!, decimal!	3
   Item: generic functions with trait bounds	equal<T: Same>, compare<T: Key>, append_list, length_list, index_list, slice_list	6
   Expr: loops (while, while let, for, loop) with break/return	walk, onto, chars, Same/Key for Str, Drop, canonical_decimal	8
   Expr: mutable locals and assignment	walk, onto, items, chars, the counting and slicing items, join, canonical_decimal	many
   Expr: &mut borrows and std::mem::replace	List::take	1
   Expr: closures, &mut dyn FnMut	walk and its 5 callers	6
   Expr: field access and indexing, slicing	.0, .head, buffer[len - 1], &a.0[s..e]	many
   Expr: if let, match guards	cons, Same for Str	2
   Expr: as casts	as u64, as usize, as u128	several
   Type: usize, u128, i128, char, &str, &[u8], Vec<T>, Rc<str>, Rc<[u8]>	throughout STD	9 types
   Library calls	listed under the boundary below	see below

   Proposed boundary

   The rule: a library function is a machine primitive only if the runtime cannot state it in the AST without a loss of meaning or safety. Everything else becomes runtime source in the AST.

   Scalar primitives (per width u8…u64, i8…i64, plus usize, u128, i128 where the runtime needs them):

   1. checked_add, checked_sub, checked_mul, checked_div, checked_rem, checked_neg, checked_shl, checked_shr.
   2. &, |, ^, ! on integers; ==, <, <=, cmp.
   3. try_from between integer widths and from (widening).

   Derived in the AST from those (no longer primitives):

   Today	In the AST
   saturating_sub	checked_sub, else 0
   wrapping_rem (int_rem, b != 0)	checked_rem, else 0 (MIN % -1 is the only None, and wrapping gives 0)
   if amount < BITS { Some(wrapping_shl) } else { None }	checked_shl (it is None exactly when amount >= BITS; same for shr)
   ok_or, unwrap_or, map, map_err, and_then, copied	match on Option/Result
   &&, ||	if

   Memory primitives (rust-std): Rc::new, Rc::clone, Rc::get_mut (the unique-holder test), Rc::try_unwrap (iterative release), Vec::with_capacity, push, truncate, len, indexed read.

   Text primitives: core::str::from_utf8 (validation) and str::as_bytes, plus Rc<str>/Rc<[u8]> construction from a slice.
   Everything else on text is stated in the AST over bytes. Character count is the count of non-continuation bytes. Str equality and order are byte equality and byte order, which equal code-point order on valid UTF-8. split_exact, join, decimal parse and format become digit and byte loops over the checked primitives.
   These must reproduce today's tick counts exactly (#91 DoD: counted work unchanged). Same for Str ticks once per character pair plus once at the end, so the byte version ticks per non-continuation byte.

   Work counter: one primitive, tick(units) (and work()), meaning "add units to the run's counter". Its two-line implementation over a relaxed AtomicU64 is the trusted part, so the AST needs neither static nor atomics.

   Eliminated, not added:

   1. macro_rules!: the backend emits each width's instance.
   2. &mut dyn FnMut and closure literals: walk becomes a cursor loop in each list item.

   The closure by reference #84 needs is different: fold_list(&closure, …) borrows the defunctionalized Fn<n> enum and calls its apply. The AST already has &T as a type and apply as an expression; #84 needs &T on locals, not trait objects.

   Data, not text: the crate headers become a field of Profile. The manifest template and ALLOWED_LINTS become typed tables printed by the AST printer. This is #91 stage 4; it is listed here so the boundary is complete.

   What the AST gains under this boundary

   1. Items: struct (tuple, named, unit), enum variants with fields (generic over one type parameter), type alias, impl blocks, Clone and Drop impls, a closed derive set, a closed use list.
   2. Expressions: loop with break and return, mutable local and assignment, field read, indexed read, & and &mut borrow of a local, as casts between the integer types listed.
   3. Types: usize, u128, i128, Vec<T>, &[T], &str, type parameters.
   4. A rust::validate rule replacing the text test every_runtime_loop_ticks: every loop body calls tick, except a loop inside a Drop impl.
   5. Each constructor added to Expr changes its recursor, so every library theorem matching on Expr gains a case (afflom's note on [v0.4] perf(backend): borrowed projections, fold as a runtime item, and list views as borrows in the rust-std machine (follow-up to #81) #84). This is why stage 3 (memory model) waits on the core-module surface ([v0.4] #27 stage 3: the LexLean authoring surface: a human-writable .lex.tex syntax, an SDK API, and no other authoring path #93 stages 3c/3d) and stage 1 does not.

   Open questions for the maintainers

   1. Same/Key: keep two closed traits with generated impls (smaller change), or replace with per-type generated functions so the AST stays trait-free (larger change, no dispatch)? I recommend the closed traits, since Item::Equal/Compare already take no type.
   2. Work counter: a machine primitive (my recommendation, above) or the static atomic in RustSyntax as [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91's scope lists?
   3. pub mod fixed_<w>: keep the module paths (no change to any rendering's call sites) or flatten to fixed_<w>_<op>? I recommend keeping them.
   4. What stages 2 to 4 wait on. The [v0.4] #27 stage 3: the LexLean authoring surface: a human-writable .lex.tex syntax, an SDK API, and no other authoring path #93 status comment says [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 "depends only on semantic modules", which holds for RustSyntax and RustSemantics (compiler/src/*.lex.tex) once feat(surface): the language-1.2 authoring notation for semantic modules (#93, stage 3a of #27) #94 and feat(#93): every language-1.2 source is written in the authoring notation (AU-04), fmt migrates the data form #96 merge. But stage 2 already adds a constructor (a primitive callee, or the scalar items as AST functions), and the DoD asks for a kernel-checked refinement statement per item. Both touch the preservation library, which is core-module data and editable only after [v0.4] #27 stage 3: the LexLean authoring surface: a human-writable .lex.tex syntax, an SDK API, and no other authoring path #93 stages 3c/3d. Is the intent that the new statements are semantic-module theorems while the existing Expr cases are regenerated, or does stage 2 wait for 3c/3d?

   Not in this inventory

   1. Proof obligations per primitive: those are stage 3 (refinement statements).
   2. lower.rs, moves.rs, validate.rs changes beyond the loop rule.
   3. A measured differential: stage 2 is where the generated runtime first runs against the committed one.

   ---

   Generated by Claude Code
7. afflom commented on Oct 15, 2026

   

   afflom

   on Oct 15, 2026 – with Claude

   MemberAuthor

   More actions

   Answers for stage 1 (@humuhumu33), as a maintainer, so #102 can leave draft.

   1. Same/Key: keep two closed traits with generated impls.

   2. Work counter: a machine primitive, not a static in RustSyntax. Its meaning ("add units to the run's counter") is the whole of the trusted part.

   3. fixed_<w> modules: keep the paths.

   4. What stages 2 to 4 wait on. The binding constraint is not the notation. [v0.4] #27 stage 3: the LexLean authoring surface: a human-writable .lex.tex syntax, an SDK API, and no other authoring path #93 stage 3c (merged soon: feat(#93): the calculus and the Rust machine are sources; the authoring API; no writer owns a product source (AU-07, AU-08) #103, feat(#93): core modules in the authoring notation, with names (AU-09..AU-12); the language-1.2 libraries are written in it #104) makes the libraries readable and editable as text; it does not make an inductive type of the preservation library extensible. Adding a constructor to Expr (or Corr) changes Expr.rec, and every row that Lean derived from it (casesOn, below, brecOn, noConfusion, sizeOf) and every proof that Lean's equation compiler produced against it is exported data: a person can read it, but regenerating it means re-running Lean's elaborator on Lean source, which is exactly what we do not accept as a source, and no surface of ours reproduces those constructions. My scope for [v0.4] #27 stage 3: the LexLean authoring surface: a human-writable .lex.tex syntax, an SDK API, and no other authoring path #93 3d (named binders and labels for kernel terms, no inference; see the [v0.4] #27 stage 3: the LexLean authoring surface: a human-writable .lex.tex syntax, an SDK API, and no other authoring path #93 comment) lets a person write a new closed proof term; it does not rewrite brecOn towers. So please design stage 2 on this rule: no new constructor of Expr, Corr, or Item that a library row or proof matches on. Scalar items as AST functions over existing constructors and machine primitives satisfy it if the primitives are table data of itemPrimitive (a semantic module, so authorable and kernel-checked with the generated Lean), and new refinement statements are semantic-module theorems about the generated runtime.

      One thing I do not know and want measured before stage 2 is written down: does adding an Item constructor break a library row? Please spike it on a scratch branch: add one dummy constructor to Item in RustSyntax, regenerate, and run the library compile (conformance_sp_12 builds it) and check-calculus. If nothing in the library matches on Item, stage 2 proceeds as above. If something does, the options are (a) make the primitive set a table lookup rather than an inductive (the machine's primitive list is then data, not a type), or (b) decide that extending the library needs the full elaborator, which is its own issue with its own trust argument and I would rather not start it for this. Stage 3 (loops, locals, borrows, Rc, Vec) adds Expr constructors by definition, so it hits the same wall one level up; it waits for that answer and I will not pretend otherwise.

   Everything else in the boundary table is agreed. Merge #102 when its checks are green.

   ---

   Generated by Claude Code
8. humuhumu33

   added a commit that references this issue on Oct 15, 2026

   feat(rust): close the runtime's library boundary (RB-09, stage 1 of #91)

   ...

   76bc8e2
9. humuhumu33 commented on Oct 15, 2026

   

   humuhumu33

   on Oct 15, 2026

   Contributor

   More actions

   Spike: does a new Item constructor break the library? Yes. Measured on main at 514e95ad.

   What I ran. I appended one constructor, spike, to Item in compiler/src/RustSyntax.lex.tex, and added a spike arm, copied from the natAdd arm, to each of the seven exhaustive matches on Item in RustSemantics.lex.tex. Then I built the compiler project. The generated TargetSyntax and TargetSemantics were byte-identical to language/preservation-1.2/modules/, and RustSyntax differed by the | spike line alone. Last, I compiled the library's generated Lean against the four machine modules under Lean 4.32.1, up to RustCorr.

   Result.

   machine modules	RustCorr
   shipped (baseline)	builds
   with Item.spike	refused

   The first refusal:

   error: LexLeanPreservation/RustCorr.lean:611:0: native core declaration 'LexLeanPreservation.Rust.plainItem._sparseCasesOn_1':
     core declaration 'LexLeanPreservation.Rust.plainItem._sparseCasesOn_1' is not the sparse casesOn the elaborator makes
   

   The seven errors after it are unknown constant cascades (rebuildTail.match_14, directPat, uninh.match_1, Corr), declarations the module never reached. So the compile names the first break, not every break. check-calculus is not informative here: it can only report that the shipped modules differ from the regenerated ones, which is the edit itself.

   Every break, read from the native data. I walked each declaration's type and value in the 13 core modules (9,247 declarations) and counted the ones that eliminate each type directly, through its rec, casesOn, ctorIdx, noConfusion, below, brecOn or a match_ of its own:

   type	declarations that eliminate it	affected with their dependents
   RustSyntax.Item	9	31 (RustCorr 13, RustSound 10, RustLemmas 8)
   RustSyntax.Callee	1	101
   RustSyntax.Expr	64	295
   Rust.Corr	56	57
   RustSyntax.RustType	0	0

   The Item rows are plainItem's matcher, splitter and sparse cases, itemOperands_eq, takes_of_typed and sem_primWiden. This count is a lower bound. The library also applies matchers that Lean generates for RustSemantics definitions, such as runItem.match_1, runItem.match_3 and widened.match_1 (23 equations). Those matchers change shape when a matched type grows.

   What this means for the stages.

   1. Stage 2 cannot add Item constructors. Your option (a) is the way through: the primitive set becomes a table lookup that itemPrimitive reads, rather than an inductive. That needs one more change than the spike, because plainItem and runItem would have to stop matching on the individual primitives. I have not measured that change.
   2. New Rust types cost nothing. No library declaration eliminates RustType, so usize, u128, i128, Vec<T>, &[T] and &str add no library break.
   3. Stage 3 hits the wall. Loops, locals and borrows are Expr constructors, with 64 direct and 295 affected declarations, so it waits on the full-elaborator decision, as you said.

   The spike is on a local branch, not pushed. The analysis script reads lexlean/core-module/2 data and I can attach it.

   ---

   Generated by Claude Code
10. humuhumu33 commented on Oct 15, 2026

    

    humuhumu33

    on Oct 15, 2026

    Contributor

    More actions

    A third route for extending the machine: regenerate what Lean derives, author only the proofs. This follows the spike above, measured on main at 514e95ad.

    Why neither (a) nor (b) as stated.

    • (a) A table lookup in place of the Item inductive changes Item once, so it hits the same 31 declarations once. It also does not help stage 3, whose loops, locals and borrows are Expr constructors.
    • (b) The full elaborator brings in the trust argument you would rather not open.
    • Stage 2 cannot stay inside today's constructors either. A generated nat_add has to turn the None of checked_add into Err(Overflow), and the only source of failure in RustSemantics today is a fallible item called with ?. So even the scalar stage needs one new construct, a raise.

    The observation. The loader already trusts Lean's derivation generators without trusting Lean source. backend/core_v2.rs:187-213 rebuilds every stored sparse casesOn with Lean.Meta.mkSparseCasesOn and refuses the stored row unless its type and value are exactly what Lean makes. That is the spike's failure: the stored plainItem._sparseCasesOn_1 is no longer "the sparse casesOn the elaborator makes" for the new Item.

    Most of each break is derived. I split the declarations that eliminate each type by whether Lean derives them (matchers, splitters, sparse casesOn, their eq_N/else_eq, below/brecOn) or someone authored them:

    type grown	eliminate it directly	of which derived	of which authored
    Item	9	6	3: itemOperands_eq, takes_of_typed, sem_primWiden
    Lit	9	8	1
    Ctor	46	44	2
    Callee	1	0	1
    Pat	65	54	11
    Expr	64	49	15
    RustType, CaptureRead	0	0	0

    Proposal (c). Growing a machine type is one PR with three parts:

    1. Regenerate the derived rows with Lean's own generators, checked as today. Sparse casesOn already works this way. Matchers, splitters and their equations would get the same treatment: rebuilt from the stored matcher record over the grown type and compared, never taken from Lean source. This extends a trust the loader already places in Lean's meta code. It adds no elaboration of Lean source.
    2. Author the remaining proofs as closed terms in the [v0.4] #27 stage 3: the LexLean authoring surface: a human-writable .lex.tex syntax, an SDK API, and no other authoring path #93 3d surface. Most of these are one new minor premise per casesOn over the grown type.
    3. Recheck the dependents unchanged. When the matched type grows under a wildcard arm, a matcher's type does not change, only its body. So most dependents should check as they are. The upper bounds are 31 for Item and 295 for Expr. The real number is what step 1 leaves failing, and I would measure it before writing step 2.

    What it buys. For Item, three proofs. For stage 2's raise, one Lit or two Ctor proofs. For #84's borrowed projection or a loop, the 15 Expr proofs plus the Corr template work. That is bounded and known in advance, instead of re-elaborating the library.

    First step, if you agree: a prototype of part 1 for plainItem.match_1 alone, run against the spike's Item. It answers two things: whether a matcher can be rebuilt from its stored record, and how many of the 31 still fail afterwards. I would not start part 2 before that number is in, or before 3d can state a closed proof term.

    ---

    Generated by Claude Code
11. humuhumu33 commented on Oct 15, 2026

    

    humuhumu33

    on Oct 15, 2026

    Contributor

    More actions

    Route (c), measured: growing Item leaves two proofs to write. This is the prototype the proposal above offers, run on main at 514e95ad with the spike's Item.spike.

    What I ran. I used the spike's regenerated RustSyntax and RustSemantics, and the library's generated Lean for all 13 modules. In a scratch copy only, I changed the core-module decoder in three ways:

    1. A sparse casesOn that mkSparseCasesOn makes differently is accepted and logged, instead of refused.
    2. A declaration that fails is logged, and loading continues.
    3. A failure in the metadata steps is logged, not raised.

    The whole library then built under Lean 4.32.1 (all 13 modules, 135 s), so every failure is counted, not only the first.

    Result.

    what changed	count	how it gets regenerated
    sparse casesOn remade by Lean (plainItem._sparseCasesOn_1, plainItem.match_1.splitter._sparseCasesOn_2)	2	already by the decoder's own mkSparseCasesOn construction, which only has to keep what it makes
    equation lemmas and splitters derived from matchers: RustSemantics.itemPrimitive.match_1.eq_1..eq_50 and its splitter, plainItem.match_1.eq_2, plainItem._sparseCasesOn_1.else_eq	53	by Lean's equation generation for those matchers, realized the same way, still to be shown
    authored proofs: itemOperands_eq, takes_of_typed	2	each needs one new case in its Item.casesOn
    everything else	0	loads unchanged

    Three things the static count got wrong:

    1. The matchers themselves (plainItem.match_1, itemPrimitive.match_1) load unchanged against the grown Item. So do their splitter abbreviations once the sparse casesOn under them is remade.
    2. sem_primWiden uses Item.ctorIdx but still checks.
    3. The dependents of the two failing proofs (accepts_of_typed, runItem_eq) load, because the proofs' statements do not change. So the 31 affected declarations come down to 2 proofs plus derived rows.

    What this means for the route.

    • One new Item constructor costs: the decoder keeping what Lean's derivation makes, for sparse casesOn (done in this prototype) and for matcher equations (next), plus two one-case proofs in the 3d surface.
    • Matchers do not need rebuilding when the new constructor falls under an existing wildcard. That held for both Item matchers here.
    • I have not measured Expr yet. Its static estimate was 15 authored declarations; by the same mechanism the real number is likely smaller. I can run the same measurement with a dummy Expr constructor next.

    Caveats.

    • The spike's RustSemantics arms copy natAdd, so a real constructor's arms and proofs differ in content, not in kind.
    • The 53 equation rows are still to be regenerated, not just listed.

    ---

    Generated by Claude Code
12. humuhumu33 commented on Oct 15, 2026

    

    humuhumu33

    on Oct 15, 2026

    Contributor

    More actions

    Route (c), measured for Expr: 11 proofs to write. This is the same prototype as the Item comment above, run with one dummy Expr constructor, spike, whose eval arm returns stuck. Measured on main at 514e95ad; the whole library built under Lean 4.32.1 in 80 s.

    	Item	Expr
    sparse casesOn the decoder remakes	2	16
    derived rows that fail: equation lemmas, splitters, eq_def, else_eq	53	39
    matchers that fail	0	1 (rc_litValue.match_1)
    authored declarations that fail	2	11

    The 11 Expr declarations:

    • RustBase: stable
    • RustLemmas: rc_negate, rc_negate_halt, rc_read, rcb_flat, foldStep_spec
    • RustMatches: ctorOf_eq, loadOf_spec, rc_partRead, rebuildArg_rc, rebuild_value

    Ten are theorems whose proof fails at one Expr.casesOn, so each needs one new case. Their statements do not change, so their dependents load. The eleventh, stable, is a structurally recursive definition: its value is built on Expr.brecOn, so the new case goes into its recursion, not only into a case split.

    Two things the Item run did not show:

    • One matcher needs rebuilding, not just keeping. rc_litValue.match_1 has no wildcard covering the new constructor. So part 1 of route (c) has to rebuild a matcher from its stored record, as well as keep the remade sparse casesOn and equation rows.
    • This is the constructor stage 3 needs. A loop, a mutable local or a borrow is an Expr constructor. So is production: the collection and iteration primitives are realized by self-recursive functions but registered recursion = false; a root overflows the stack at about 40k iterations #105's step 2, the template tail call realized as a loop.

    Since #104, part 2 can be written. The core-module notation of §17.21.8 (AU-09..AU-12) states a closed proof term with named binders, as authored_eq_symm shows. So the 2 + 11 new cases are writable in the surface today. The open work is part 1: the decoder keeping what Lean's own generators make (sparse casesOn, matcher equations and splitters, and the one matcher).

    The decision this needs from the maintainers: is route (c) accepted for #91 stages 2 and 3, and for #105 step 2? If yes, I will start with part 1 as its own PR, with a register row, scenario, failing test and plants: the decoder admits a derived row only when it equals what Lean's construction makes for the current inductive, and refuses any other change. Then one PR per new construct, with its cases written in the notation.

    ---

    Generated by Claude Code
13. afflom

    added a commit that references this issue on Oct 15, 2026

    Merge pull request #102: close the runtime's library boundary (RB-09,…

    ...

    70de63d
14. afflom commented on Oct 15, 2026

    

    afflom

    on Oct 15, 2026 – with Claude

    MemberAuthor

    More actions

    Stage 1 is merged (#102, merge commit 70de63d); stages 2 to 4 stay open on this issue.

    Stage 1 as this issue scoped it ("inventory and boundary: a closed list of what the runtime may take from Rust's library, and which of it are machine primitives"): calculus::rust_library lists the 21 machine primitives, each with its meaning, and the 79 library names the runtime text takes, each with one of three roles; RB-09 (conformance_rb_09) refuses a name the table lacks, a row the text does not use, a row citing a non-primitive, and a primitive no row cites, with the plants recorded in VERIFICATION.md. It changes no rendered byte, package, golden or semantic ID (rb_07 confirms). just vv, all four host legs, repro and honesty are green on the merged head, and the register is at 380 IDs.

    What remains of the DoD, unchanged: the primitives' meanings stated in RustSemantics (stages 2 and 3, where the scalar items and the memory model use them), the runtime generated from the calculus with no handwritten Rust text (stage 4), and the refinement statements kernel-checked. Stage 2 waits on the spike #102 names: whether adding an Item constructor breaks a library row. #105 step 2 (template self tail calls as loops) waits on stage 3's loop construct.

    ---

    Generated by Claude Code
15. humuhumu33 commented on Oct 15, 2026

    

    humuhumu33

    on Oct 15, 2026

    Contributor

    More actions

    On stage 2 waiting for the #102 spike: the spike is answered. Adding an Item constructor leaves the matchers loading unchanged. Lean remakes 2 sparse casesOn and 53 derived equation rows, and only 2 authored proofs need a new case (itemOperands_eq, takes_of_typed); for Expr it is 11 (issuecomment-6190972859, issuecomment-6198533402).

    I have since measured whether the decoder can take the derived rows from Lean instead of from the source. I realized every row whose name Lean reserves (matcher equations and splitters, eq_N, eq_def, else_eq) through Lean's own reserved-name action. That reproduces 7,065 of the library's 7,071 derived rows exactly, once the decoder installs each row's metadata as it adds the row. The last 6 share one known cause: a sparse casesOn not yet visible to Lean when the next row is realized.

    Unless you object, I am taking stage 2 on route (c), in this order:

    1. The decoder change: derived rows realized by Lean and refused when they differ, with a register row, a gate and plants.
    2. The scalar items, with the meanings of the 21 machine primitives stated in RustSemantics.
    3. The 2 Item proofs, written in the core notation.

    If stage 2 changes whether the Bytes primitives reduce in the kernel, the PR will say so.
16. 1 remaining item

    Load more
17. humuhumu33

    added a commit that references this issue on Oct 16, 2026

    fix(#91): the harness compiles shipped modules with their source root

    ...

    71354a3
18. afflom commented on Oct 16, 2026

    

    afflom

    on Oct 16, 2026 – with Claude

    MemberAuthor

    More actions

    @humuhumu33, a scheduling question, not a design objection. #91 stages 2 to 4 are now the longest serial chain to v0.4: #92's boundary waits on stage 4, #105 steps 2 and 3b on stage 3's loop, and everything after is CI-bound (about two hours a landing). Most of the other v0.4 lanes now have a second contributor session (#89 stage 3 certificate A, the #92 pilot). Could #91 have one too?

    Which slices could run in parallel with yours without colliding on RustSyntax/RustSemantics, as I read the DoD and your order (decoder, scalar items, the two Item proofs, then stage 3, then stage 4):

    1. Package scaffolding as generated output (a slice of stage 4, independent of 2 and 3). The DoD says "the printed headers and the manifest/lint tables become generated or data": calculus/rust/package.rs (manifest template, lint allow-list, provenance) and the file headers calculus/rust/ast.rs prints. This touches neither Item nor Expr. The open question is what "data" means when .lex.tex is the only authoring surface: I would read it as a language-1.2 module (a typed record of the manifest and the lint set), rendered by the Rust backend like any other, but that is a decision for you and me before anyone builds.
    2. The runtime items authored in .lex.tex (stage 4 proper) cannot start before stage 3's constructs exist, so it stays behind you.
    3. Stage 3's Expr constructors (loop, mutable local, borrow) and the memory model collide with the scalar items in the same inductives. I would not split those.

    So the proposal is slice 1 only, as a contributor session on a branch of its own, draft, stacked on main; nothing from it is on your path. If you would rather do all of #91 yourself, say so and I will not start it. If you agree, tell me whether the "data" reading in 1 is right, and anything about the headers or the provenance I have not seen. Also welcome: your estimate of the number of PRs and landings left in stages 2 to 4, so the plan on #15 has real numbers.

    ---

    Generated by Claude Code
19. humuhumu33

    added 7 commits that reference this issue on Oct 17, 2026

    fix(#91): a certificate rendered outside the module system leaves the…

    ...

    ac11e6c

    fix(#91): certificates-total-limit records the longer decoder's bytes

    ...

    1e4ce71

    fix(#91): a row private to another module is data

    ...

    bed743f

    Revert "fix(#91): a row private to another module is data"

    ...

    9f41fc5

    fix(#91): the text library's private names name the module it compile…

    ...

    060a46b

    chore(#91): regenerate the records the text library's private names move

    ...

    39f3b04

    chore(#91): regenerate the records #160 brings under the old language…

    ...

    ed51aad
20. humuhumu33 commented on Oct 17, 2026

    

    humuhumu33

    on Oct 17, 2026

    Contributor

    More actions

    Yes to slice 1 as a parallel session. It touches no inductive of mine. What it does share with my lane is the language-1.2 identity. Answers to your three points follow, measured on main at 243f0c73.

    (a) Slice 1: agreed, with one coupling to plan for

    The two lanes share no inductive, but they do share the ID. rust_renderer hashes all seven files of calculus/rust/, including ast.rs and package.rs. schemas/rust-provenance.schema.json is embedded. So every slice-1 landing moves the language-1.2 ID, and so does every PR on my chain. Whichever lands second merges main and regenerates every lock, golden and package. #155 has merged main five times since it was marked ready, most of them with a regeneration, and a sixth is in progress now. This does not argue against the split. It argues for three things:

    1. Slice 1 lands as one PR, so it costs my chain one regeneration rather than several.
    2. Its boundary: package.rs, the header lines of ast::print, the provenance schema, and the new module. Not runtime.rs, lower.rs, RustSyntax or RustSemantics. print keeps splicing runtime::CORE/STD until stage 4. My stage 2 will edit ast.rs and lower.rs outside print, so the textual merges should be clean.
    3. It can carry production: the collection and iteration primitives are realized by self-recursive functions but registered recursion = false; a root overflows the stack at about 40k iterations #105 3b. On production: the collection and iteration primitives are realized by self-recursive functions but registered recursion = false; a root overflows the stack at about 40k iterations #105 we agreed (issuecomment-6203599898) that the rust-provenance record of a root's effects goes with the next change that moves the ID anyway. That was to be production: the collection and iteration primitives are realized by self-recursive functions but registered recursion = false; a root overflows the stack at about 40k iterations #105 step 2, which now sits behind my stage 3. Slice 1 already edits the provenance writer and its schema, and it lands well before stage 3. The other half of 3b should go with it: the production-1.2.toml sentence that says recursion "stops the realization with an explicit failure", when in fact the process aborts. I am glad to hand 3b to that session if you agree.

    (b) "Data" as a language-1.2 module: yes, with four refinements

    A language-1.2 module is the right reading. Decision 1 on #27 makes .lex.tex the only authoring surface, so a Rust const table (today's ALLOWED_LINTS) is a second surface. A typed record also lets a property be stated as data and checked, rather than restated in prose. Four things I would settle before building:

    1. The module is read, not rendered into lib.rs. The Rust backend renders programs to Rust source. Cargo.toml is TOML. So package.rs keeps a canonical TOML printer over the record. That leaves a printer, like ast::print, but no text constant holding manifest content, which is what the DoD and its planted-constant gate are about. Nothing in crates/lexlean/src reads values out of a compiler/src module today, so how the renderer obtains the record is new and needs design. The two options are evaluating the module, or decoding its semantic data. This is the first design point for that session.
    2. Where it lives decides whether the ID covers it. The embedded digest covers language/ and schemas/, not compiler/src/. Today a lint change moves the ID because rust_renderer hashes package.rs. After the move, the module's committed data must sit under language/ (as the generated machine modules do under language/preservation-1.2/modules/), or its hash must be recorded in semantics-1.2.toml beside rust_runtime_core. Otherwise a changed lint set would not change LexLean's identity.
    3. The headers need no new field. #![no_std] is exactly allocation = false on the target row of language/production-1.2.toml. The header should be derived from that row, so the fact lives in one place. This corrects my stage-1 inventory, which proposed a new field of Profile. Also, #![forbid(unsafe_code)] in lib.rs restates unsafe_code = "forbid" in Cargo.toml's [lints.rust]. I would keep both in the output (a lib.rs built outside Cargo still forbids unsafe code), but generate both from that one lint row. One caveat: deriving from production-1.2.toml keeps a TOML source in the chain. Whether the target table itself becomes a module is a separate question that slice 1 should not take on.
    4. The lint record should carry the Clippy group. SPEC §17.16 gives each allowed lint a Clippy group and says "No allowed lint is in Clippy's correctness group." ALLOWED_LINTS has no group field, and as far as I can find, no gate binds the SPEC table to the code. A record of {lint, group, reason}, with group ≠ correctness checked, makes that claim checked rather than prose. The ten load-bearing plants recorded in VERIFICATION.md then become "drop a row from the module".

    Provenance needs nothing beyond 3b. It is already computed values under a schema (lexlean/rust-provenance/1), with no handwritten content other than the key set the schema fixes. Its runtime hash stays as it is until stage 4.

    (c) PRs left in stages 2 to 4

    This is a count with its uncertainty, not a schedule. It counts PRs after #155, which is in flight. The low end groups constructs into fewer PRs; the high end is one PR per construct, as I proposed on route (c).

    Stage	PRs	What
    2	1 to 2	the scalar items over the 21 machine primitives with their meanings in RustSemantics, and the two Item proofs (itemOperands_eq, takes_of_typed) in the same PR, since a PR that grows Item without them fails the library compile; the raise construct (one Lit or two Ctor proof cases) with them or on its own
    3	4 to 8	route (c) part 1 extended to rebuild a matcher (rc_litValue.match_1); the Expr constructs (loop with break/return, mutable local and assignment, borrows, field and indexed read, casts) at about 11 proof cases each by the dummy measurement; the item kinds (structs, enums with fields, impl, Clone/Drop, Same/Key); the memory-model refinement statements for List, Str, Bytes
    4	2 to 3 on my chain, plus slice 1	the runtime authored in .lex.tex with the old text moved to tests/ as the oracle (core and std together or apart); then removing the oracle and adding the planted-text gate

    So 7 to 13 serial landings on the #91 chain, plus slice 1 in parallel. Every one of them moves the language-1.2 ID, so each also costs every other open ID-moving PR a main merge and a regeneration.

    Where the range comes from, from most to least uncertain:

    1. Memory-model proofs: never measured. The refinement statements (a run is a prefix of its buffer, no write to a shared buffer, constant-work cons/uncons, iterative release) are new theorems. They are not cases added to existing ones.
    2. Item kinds: the structs, impls and traits are ItemDef constructors, and I have not spiked ItemDef against the library. I will run the same dummy-constructor measurement before stage 3, as I did for Item and Expr.
    3. The 11 cases per Expr constructor came from a dummy whose eval arm is stuck. A real constructor's proofs differ in content, and may need more cases than the dummy did.

    I will post the ItemDef number here when I have it, so the plan on #15 can take the stage 3 range down.

    ---

    Generated by Claude Code
21. afflom

    added a commit that references this issue on Oct 17, 2026

    chore(#91): regenerate on the combined language-1.2 identity (main 24…

    ...

    5a04afd
22. afflom commented on Oct 17, 2026

    

    afflom

    on Oct 17, 2026 – with Claude

    MemberAuthor

    More actions

    Slice 1 (package scaffolding as data): first design point, how the renderer obtains the record. Contributor session, branch train/package-scaffold; I take hh's four refinements as written and #105 step 3b with them.

    Decision: decode the module's semantic data; do not evaluate it.

    • The record is one language-1.2 semanticmodule, RustPackage, written in the notation at language/package-1.2/RustPackage.lex.tex. It declares a LintRow {lint, group, reason} with a closed ClippyGroup inductive, the rustc gate rows (unsafe_code forbid, warnings deny), the Clippy base gate, the [package]/[lib] values (edition, publish, library path), and the allowed lints as a list of records.
    • package.rs reads it from the embedded tree: the notation is read to its canonical data (surface::module, as identity::data_form already does for the ID), and a small decoder walks the definition bodies, which are closed (record, cons, nil, ctor, string and boolean literals). Anything else in a body is refused, so the decoder cannot silently read less than the module says. The module is read, never rendered into lib.rs, and package.rs keeps only a canonical TOML printer over the record.
    • Because the file sits under language/, the ID covers it with no registry row: identity_bytes already contributes the data form of a .lex.tex there. A gate shows it: one lint row changed in a scratch copy of the embedded tree changes the language-1.2 ID, and a comment-only edit of the notation does not.
    • The headers are derived, not stored: #[no_std] iff the target row of language/production-1.2.toml has allocation = false; #[forbid(unsafe_code)] is printed for every rustc gate row at level forbid, the same row that prints unsafe_code = "forbid" in Cargo.toml.
    • group != correctness is checked twice: by the decoder, which refuses a row in that group (a registered failure), and by a theorem in the module itself over the same list. SPEC §17.16's lint table is compared with the rows by a gate.

    Alternative rejected: evaluate the module. The shipped crate has no evaluator of semantic terms. The meaning of those terms is decided by the generated Lean and its kernel, so a second interpreter in lexlean would be an unverified reading of the language it ships, to learn what a closed list of strings is. Decoding costs a reader of constructor, list and literal shapes, and refuses every other shape. The two cannot disagree on data that shape.

    Alternative rejected: keep the module in compiler/src and commit a generated copy under language/. It adds a regeneration path and a comparison gate for a file that is already the data; the hand-written source under language/ is itself what the ID hashes.

    #105 3b rides in the same PR as agreed on #105 (comment 6203599898): lexlean/rust-provenance/1 gains effects (the root's declared effects on that target, ascending; same set as PX-13), and the recursion sentence of language/production-1.2.toml states the abort. Nothing else of #105 moves.

    Hand-written work only goes to the branch; every generated tree is left to the train's one regeneration.

    ---

    Generated by Claude Code
23. afflom

    added 3 commits that reference this issue on Oct 17, 2026

    Merge pull request #155 from UOR-Foundation/claude/issue-91-derived-rows

    ...

    97a3df7

    train: regenerate every record the combined tree moves

    ...

    e24a7ff

    fix(rust): address review of the package scaffold (#91 slice 1)

    ...

    dd8691b