363 linker envelope numeric - #426
Merged
Merged
Conversation
…363) Real toolchain output uses integer width conversions and sign-extension pervasively; both families were refused at every layer of the pipeline on the premise that the wasm-verifier proof contract modelled neither. That premise no longer holds: the contract gained interpreted `T_unop`/`T_cvtop` terms with semantic rules discharged inside its soundness theorem, so the eight operators now have real lowerings and are admitted in lockstep across the four places that refused them. Sign-extension is not a conversion. The proof contract spells `i32.extend8_s` and its four siblings as `BI_unop t (Unop_extend n)`, beside `clz`/`ctz`/`popcnt`; only `i32.wrap_i64` and `i64.extend_i32_s/u` are `BI_cvtop`. The WASM mnemonics group them misleadingly, which is why they were retracted alongside the conversion block in the first place. `Unop_extend`'s argument is the source width in bits, not bytes. The contract's typing side condition ignores the argument entirely while its denotation divides by eight, so a byte count elaborates, satisfies the side condition, and denotes the constant zero for every input. `coqc` cannot see that class of error at all — measured, not assumed: a planted `Unop_extend 1%N` type-checks clean. Two byte-comparison tests are the whole guard, and each names the other so neither is removable as redundant. The four layers, all required together to keep the allow-list contract ("an allow-listed operator is one the translator can render") true at the Rocq level rather than only at the Rust one: - the vendored stub gains `Unop_extend`, a `cvtop` inductive, and `BI_cvtop`. `cvtop` declares only `CVO_wrap`/`CVO_extend`, since the remaining six each need a float number type the stub deliberately omits; a stub narrower than the backend keeps an accidental emission an unbound-constructor error instead of a silently type-checking term; - `wasm-to-v` lowers all eight and scopes its rejection to conversions that name a float, with a message that says why; - the linker allow-list admits all eight as pure numeric operators; - `SUPPORTED_WASM_FEATURES` gains `SIGN_EXTENSION`, which the validator refused before any body was scanned. `SATURATING_FLOAT_TO_INT` stays out: its operands are floats, so admitting it would recreate the allow-listed-but-unlowerable divergence this gate exists to close. Verified against the real backend rather than the stub alone: under Coq 8.20 with WasmCert-Coq v2.2.0, the emitted module elaborates and the upstream reflective checker accepts the emitted body, confirming cvtop argument order, arity, and the bit-width literal against the real model. Inference codegen emits none of the eight, so every committed `.wasm` and `.v` golden is byte-identical; only an external `.wasm` that previously failed to link is affected.
Tier B's admission is easy to read as a bounds guarantee — "the closure
loads or stores through addresses the caller supplies" — and it is not
one. The analysis proves every address *flows from* a caller parameter;
it says nothing about the address staying inside the region the caller
meant to grant, and it cannot, because it carries no sizes. Its lattice
has three tags and no numeric component, so "how far from p" is not
representable.
Admitted by design, and all verified linking today:
store at p + 1048576 a constant displacement
store at p + q two parameters, no constant
store at p + p (= 2p) nowhere near p
ptr = p; loop { store ptr; ptr += 4 } off the end of any buffer
`Param + Param` is a deliberate test-pinned admission: the caller supplied
both operands, so under the derivation property their sum is the caller's
business. That is also why bounding the constant displacement buys nothing
— the cheapest way to address arbitrarily far from p uses no constant at
all, so a cap would be a bound on the one form that is not the problem.
What limits the damage today is not this analysis but the main module's
fixed single page: an out-of-region address is usually out of bounds and
traps. That is an accidental backstop rather than a guarantee, and it
weakens as the declared memory grows past what the program uses — which is
what makes it worth writing down now, ahead of configurable linear memory.
Documentation only; no behavior change and no code line touched.
#363) Every artifact a real toolchain produces carries an lld-synthesized `__stack_pointer` mutable global, and a `std` build also carries an empty `(table 1 1 funcref)`. A leaf integer function reads neither. Tier C rejected both on the mere presence of the declaration, so essentially no real external could be classified at all — while the effect flags that describe what the closure actually does were already computed, and already false. Globals and tables now gate on `effects.uses_*`. Data deliberately does not: an active data segment initializes the shared memory at instantiation whether or not any instruction names it, so dropping an unused one changes program semantics. A passive segment would be inert, but the parser keeps only `data_count` and discards segment kinds, so the two cannot be told apart and both stay rejected. This is safe because effects are closure-scoped — accumulated over exactly the function set the merge later walks — so an admitted closure contains no global or table operator at all, and no stale index can survive into the output. The property is load-bearing for globals, where a leaked `global.get` would rebind to the main module's own global and pass post-merge validation with a wrong value and no diagnostic. For tables it is only fail-safe: no table section is emitted, so a leaked table operator fails validation as an unknown table. Two tests carry that argument, and each catches what the other cannot. A biconditional beside `check_operator` pins that every admitted operator naming a global or table sets the corresponding flag. A closure-level scan pins that the merged function set and the scanned function set agree — verified by neutralization: making `local_func_indices` over-approximate while leaving `effects` correct fails it with the offending operator named, and left the whole suite green before the fixture that reaches a sibling body outside the closure. The reason strings are split so each names what actually fired; they previously conflated defining a global with reading one, and a table operator with an element segment, neither of which implies the other. This relaxes the global and table gate only. A stock `wasm32-unknown-unknown` artifact still fails memory reconciliation against the compiler's fixed one-page maximum, and against a memoryless main it widens the output memory to the external's declared size even when the closure never touches memory. Both are pinned by fixtures as current behavior, not endorsed, and are the subject of the configurable-memory work.
…#363) Every merged external's memory section was folded into reconciliation unconditionally, so a module's declared page count became a fact about the merged output even when no merged body could observe it. Both consequences were wrong in the same way. Against a memoryless main, a leaf `i32.add` over a 17-page `wasm32-unknown-unknown` artifact produced a merged module declaring 17 pages — written into the `.wasm` and restated in the paired `.v` as the machine the proof is about, introduced by a pure function. Against the compiler's own `(memory 1 1)`, that same pure function was rejected outright over pages nothing would have touched. Dropping the declaration is unobservable because `uses_memory` is closure-scoped: when it is false, no body in the merged closure holds a load, a store, `memory.copy`/`fill`/`init`, or `memory.size`/`memory.grow`. The last two are worth naming — they yield or extend a page count rather than addressing a byte, so they read as unrelated to a memory's limits when they are in fact the operators that observe them most directly. Both count as use. Two guards deliberately stay outside the new gate. An unsupported memory shape — memory64, shared, a custom page size — is still rejected for every declared external memory, adopted or not, so that rejection stays absolute rather than becoming conditional on an effect flag. And a closure that uses memory when no module declares one is still rejected unchanged. This partly supersedes the tier-gate change: a stock lld artifact clears the tier gate and then fails reconciliation only when its closure actually uses memory. A pure leaf now links against a stock compiler main with main's single page kept as-is. The reconciler's refusal to relax a main module's pinned maximum is untouched, so a memory-using external over a multi-page module still fails; configurable linear memory is separate. The two fixtures that pinned the old outcomes as behavior recorded rather than endorsed are updated to the new ones, which is what they were written for.
The compiler's memory shape lived in two constants: `STACK_SIZE` in
`core/wasm-codegen/src/memory.rs` and a `STACK_BUDGET_BYTES` in
`core/analysis/src/rules/stack_depth.rs` whose own doc comment recorded
that the two "must stay in sync" and were duplicated deliberately,
because the crates share no dependency that could hold the value. That
arrangement is safe only while the number never changes; a configurable
stack turns a stale A036 budget into a rule policing a shadow stack the
artifact does not have — rejecting programs a larger stack accommodates
or, in the dangerous direction, accepting programs that overflow a
smaller one.
`MemoryLayout { pages, stack_size }` on `CodegenOptions` is now the
single source for the memory section, the `__stack_pointer` initializer,
and the per-frame size assertion, and `AnalysisOptions` carries the
budget to every rule through `Rule::check`. Neither crate gained a
dependency: each keeps its own representation, as `EmitFeatures` already
does for the feature vocabulary, and the equality of the two defaults is
asserted from the test crate that depends on both — the guard the old
comment asked for in prose and had no way to state.
`validate` rejects a layout that cannot describe a real memory. Beyond
the obvious bounds it enforces that the memory and the stack together
span no more than the 32-bit address space, because a stack overflow
wraps to an address at least 2^32 minus the stack size, and that address
must stay past the end of memory for the overflow to trap rather than
write into it. That headroom is what a one-page memory supplied
implicitly and a larger one does not.
No user-facing knob yet: the manifest table and compiler flags are
separate work. Every emitted artifact is byte-identical under the
default layout, which all 212 golden `.wasm` files confirm.
`MemoryLayout` was defined in `core/wasm-codegen`, which is the wrong crate for it once `pages` and `stack-size` become things a user writes. `Inference.toml` must be validated when it is loaded, by `apps/infs`, which cannot reach into code generation to learn what a legal layout is; the alternative is a second copy of the invariants, and a second copy is exactly the arrangement the previous commit removed. `core/compiler-interface` already holds the user-facing vocabulary for the same reason — `WasmFeatureName` and its diagnostics live there so that a manifest entry and a command-line flag are rejected in the same words — and both `apps/infs` and `core/cli` already depend on it. The type moves there together with `PAGE_SIZE` and `FRAME_ALIGNMENT`, which `validate` reads: the grid a rejected stack size is measured against must be the grid code generation rounds frames to, or the error names a constraint the emitter does not have. Unlike `WasmFeatureName`, this type is not mirrored on the codegen side. There, the user's request and code generation's emission permissions are genuinely different things, and the mapping between them carries a decision. Here they are the same two numbers, so a mirror would buy nothing and give the invariants somewhere to drift apart. `core/wasm-codegen` re-exports it, so `inference_wasm_codegen::MemoryLayout` and `CodegenOptions.layout` are unchanged and all seventeen references outside these two crates resolve unedited. No behavior change: same 51 targets, same 2906 tests, every golden byte-identical.
`b58075f` removed one hand-synced constant from this rule and left its neighbour. `FRAME_ALIGNMENT` carried the same "mirroring core/wasm-codegen" caveat and the same failure mode one step smaller: A036 rounds every per-function frame estimate to this grid precisely so the estimate cannot fall below the frame code generation really allocates. A coarser grid on the codegen side would void that guarantee silently, and the rule would then admit a call chain that overflows the shadow stack — the direction that matters, since the rule exists to reject exactly those. That commit argued for adding no dependency, and this one adds one. What changed is `afdcbe6`: the constant now lives in `core/compiler-interface` beside `MemoryLayout`, a leaf crate whose purpose is to be depended on by both sides of this kind of agreement. The coupling `b58075f` declined was a dependency on code generation itself, taken to reach a constant private to it; that is still declined here. The relation the constant protects turns out not to rest on the two numbers agreeing at all: `a036_estimate_is_sound_upper_bound_of_codegen_frame` already asserts `estimate >= real` per function across a corpus, reading codegen's own layout through `CodegenOutput::frame_sizes()`. A doc comment in that file claimed the opposite — that per-function parity was validated by construction because the field "is not exposed across crates" — which has not been true since that accessor existed, and is corrected here.
An `[memory]` table in `Inference.toml` with `pages` and `stack-size`, the `infc --memory-pages` / `--stack-size` flags it forwards, and ABI minor 2 to 3 so `infs` can refuse rather than forward a request an older compiler cannot honour. A project that declares no `[memory]` table forwards nothing and still builds against a minor-2 `infc`. The load-bearing part is not the flag; it is that one resolved layout feeds two consumers. `--stack-size` sets the `__stack_pointer` initializer *and* A036's budget from the same value. Wiring only code generation is not a partial feature but an unsound one, and the neutralization run shows both of its faces: with the analysis half reverted, `infc --stack-size 8192` on a twelve-kilobyte call chain exits 0 and writes the module, and a single sixteen-kilobyte frame panics out of frame layout with exit 101 instead of reporting anything. Wired, the same program exits 1 with an A036 diagnostic naming the configured stack. The test asserts that text and the absence of a panic, so a regression cannot pass as a mere failure. `MemoryLayout`'s fields are now private with `resolve` as the only checked constructor, per the type-invariant rule in CONTRIBUTING. A layout that cannot be emitted now has no representation outside `core/compiler-interface`, which is why `codegen`'s validate-then-emit refusal is deleted rather than moved: with the invariant held by the type, that check guards nothing a caller could reach, and keeping it would force `validate` to stay public purely to serve it — re-advertising an obligation the encapsulation exists to retire. Either key may be given alone, and the pair is checked jointly *after* filling, which is what lets a value legal on its own still be refused: `stack-size = 131072` with no `pages` is a 128 KiB stack in a 64 KiB memory. Each layer's tests pin that rejection beside the `pages = 4` case that makes the same stack size legal, so the diagnostic is about the combination rather than the number. Defaults are unchanged, so every emitted artifact is byte-identical; all 212 golden `.wasm` files confirm it.
…#363, #420) Tier B admits an external whose every memory access provably derives from a parameter of the call. It does not show the access stays inside the buffer that parameter points into, and it cannot: the analysis carries no sizes. `p + q` and `2p` reach arbitrarily far with no constant at all, and both are deliberate, test-pinned accepts. A single fixed page was an accidental backstop for that gap. A reach past the caller's buffer left the memory and trapped, so the missing containment proof cost nothing observable. Configurable memory removes the backstop: above one page the same reach lands in valid memory, possibly a region another merged module owns. Nothing about the merge became less sound, but a guarantee readers could previously rely on by accident is gone, and that is worth saying out loud. The condition is the *reconciled* memory size, not a raised `[memory] pages`. The backstop is gone whichever module enlarged the memory — a main configured to two pages and a memoryless main adopting a seventeen-page external memory are equally exposed — and a manifest-only check would stay silent on the second. The message names the externals, states the derives-from/stays-within distinction plainly, and says it reports the limit of what the merge proves rather than a fault found in the merged code. `link` keeps its signature, so the 109-site test suite and every other caller are untouched; `link_with_warnings` carries `LinkOutput` and `infc` prints each warning to stderr. The byte-identical fast path returns `Vec::new()` for a stated reason: it runs only when there is no external to warn about. Two documentation corrections this branch owes. `4b00a7f` changed the Tier-C gate but left two doc comments describing it as "own static data, mutable globals" — wrong twice over, since globals and tables now gate on use rather than mutation and tables and elements were missing entirely. `974480f` made the linker README's claim that a pure leaf still contributes its module's memory false, and left it standing.
The warning added in `2120f65` had five tests inside `core/wasm-linker`, every one of them calling the library. The three lines in `infc` that actually print it had none: deleting the loop left the whole suite green, so nothing established that a user ever sees the message. That is the same shape as a guard whose condition has been replaced by `true` — covered everywhere except at the point where it does its work. Two tests through the real binary. One build triggers the warning and asserts it reaches stderr, the process still exits successfully, and the `.wasm` is written — a driver that printed the message and then aborted would satisfy a stderr-only assertion while breaking every such build. The other builds the same project without `--memory-pages` and asserts the message is absent, so a warning that fired unconditionally could not pass. Both assert `Linked 1 external module(s)`, which is what makes the negative case attributable: an external that silently failed to bind would also produce no warning, for a reason having nothing to do with the page count. The text is matched on the claim the warning exists to make, not on its punctuation. Two constraints shaped the fixture, and both are worth knowing before writing another test in this area. A Tier-B external cannot be written in Inference at all — a compound parameter is copied into the callee's frame on entry, so no Inference function addresses memory through a caller's pointer — which is why the external is assembled from WAT and `wat` joins the dev-dependencies. And the program's array is load-bearing rather than illustrative: code generation emits a memory section only for a module that needs a frame, so without it the main module declares no memory, the merge adopts the external's single page, and `--memory-pages` has nothing to enlarge. The positive test would then pass while exercising nothing.
Every optimizing toolchain emits `base + index * elem_size` or its shift form, and the linker rejected all of it: the four scaling operators produced `NotParam` unconditionally. Admitting them meant reasoning about what arithmetic can do to a parameter, and that turned up two ways a fixed absolute address was already passing as parameter-derived. Neither needed the feature being added. `t = p; 32x (t = t + t)` leaves `t == 2^32 * p == 0`, so a store at `t + 4096` writes address 4096 for every caller — no call, no recursion, `i32.add` only. It was admitted, and the module doc named `2p` as an accept *by design*, which is the framing error underneath: doubling is not "reaching further from the pointer", it is one step of walking the value to zero. The second is the same trick across a call boundary — a root re-entered as `r(a, -a)`, with `-a` built from additions. The lattice now tracks affine forms by coefficient parity. A value is parameter-derived when some coefficient is odd, because an odd coefficient is a unit modulo 2^N: the value is a bijection in that parameter and no further arithmetic flattens it to a constant. All-even coefficients are `Scaled` — never an address alone, but `odd + even = odd` is precisely the idiom this phase exists to admit. `Param + Param` now requires disjoint odd supports, which is what kills both gadgets while keeping the genuinely independent case. The correlation rule applies to the odd support rather than the whole mask. Scoping it to the full support would have rejected `base + (index << 2)` inside every called helper, which is where real toolchain output puts the idiom — the phase would have bought nothing. A third defect surfaced on the way: exceeding a loop's fixpoint round cap was an over-acceptance, not a rejection. The analysis broke out and kept the state from before the unfinished descent. It now yields no verdict, and the cap is derived from the lattice height instead of assumed, clamped separately by what termination cost allows. Verified by execution, not only by argument: a differential harness runs each fixture under wasmtime with disjoint arguments and requires an accepted module's written byte-sets to be disjoint, and a declared fabricator's to intersect — so a rejection fixture cannot quietly become vacuous. It caught both gadgets when their guards were neutralized.
Reading or writing a module global was a Tier-C signal, so any closure that touched one was refused. Merging them is mostly bookkeeping — an output global list, a per-external remap, main's globals first — but it sits on top of one operator-rewriting hazard that decides whether the change is correct or silently wrong. `global.get` and `global.set` fell into the rewriter's verbatim catch-all. Merging globals without adding remapping arms in front of it rebinds every external `global.get 0` onto the main module's global 0, which is `__stack_pointer`. Neutralizing the arm shows exactly how quiet that failure is: the link still succeeds, the output still validates, and the global count, the section's presence and the operator's presence are all unchanged. Only the operand tells the two apart, so that is what the test asserts. Globals are not deduplicated the way signatures are. Two externals whose globals match in type and initializer hold distinct state, and collapsing them aliases two modules' variables. An external contributes its globals only when its closure uses one, which keeps an inert declaration dropped and every pre-existing merge byte-identical. The global remap is fallible, like the type remap rather than the function remap. That is what makes the dropped space fail-safe: a closure touching no global gets an empty remap, so a leaked `global.get` fails its lookup instead of silently rebinding. Two limits are recorded in `tier.rs` rather than smoothed over. A merged mutable global's initializer is a claim on a region of linear memory that no section the linker parses describes — which is the real reason a later data-placement pass cannot prove disjointness on top of this, and it holds whatever provenance tags a global read. And an external that *returns* a global-derived value its caller then dereferences is Tier A, never provenance-analyzed; that hole is not opened here, and the same shape links identically with a bare address constant and no global at all.
The linker envelope exists so real toolchain code can be reasoned about, not merely folded in. This is the minimal end-to-end path: one linked external, one main-side `spec` naming it, one obligation, proved. Adopting an external's own shipped specs and write-set contracts stay with #362. A call to an `external fn` inside an assertion was `P005`. It now resolves, keyed on the declaration's `DefId` rather than its name. The distinction is not pedantic: `collect_top_level_extern_decls` never descends into spec bodies, so a spec-inner `external fn` is never bound, and a name-keyed lookup would hand it the top-level declaration's origin and emit an obligation naming a merged body the call does not reach. A024 rejects such a call first, which makes the keying defense in depth everywhere except an analysis-skipping pipeline — and the proof-mode gates are exactly that. The obligation pass is therefore strictly more precise than code generation, which resolves provenance by `DefId` but probes its import table by bare name, program-wide. That divergence is real and reproducible — the two disagree about which function a call names, and the executable follows code generation — so it is recorded at the type rather than asserted away. It is #423, and it is not this change's to fix. Also here: an arity backstop on symbol resolution, because a wrong-arity application resolved, printed, and passed coqc — the gate cannot catch it, the term being well-formed Rocq either way. And the coqc gate grew a linked corpus, since it compiled one file and translated raw unlinked wasm, so a two-file fixture could not be registered at all. The obligation is discharged against the real verifier, not the vendored stub: `ValidModule` and `ValidSpec` both `Qed`, no `Admitted`, no `admit`, no `Abort`, and `Print Assumptions` within the verifier's own allowlist. The stub is deliberately narrower than the backend, so passing it proves the emitted shape is legal, never that the theorem holds. A companion lemma proves the empty interpretation cannot discharge the payload, so the `Qed` rests on the merged body being there rather than on the application being silent.
A committed `cargo build --release --target wasm32-unknown-unknown` artifact, its source, and the exact rustc version that produced it. CI never needs the target installed, and anyone can regenerate and diff it. The tests link it into an `infc` main, execute the result under wasmtime, translate it, and elaborate the translation under coqc. Before this branch that artifact was rejected three separate ways: the width-changing operators were outside the envelope, lld's synthesized `__stack_pointer` global forced Tier C on declaration alone, and its sixteen-page memory failed reconciliation against a fixed one-page main. Each of those is now a merge that produces a module which runs and computes the right answers. What the gate does **not** establish is that the fixture's obligations are true. `admit_open_proofs` rewrites `Qed.` to `Admitted.`, so elaboration proves well-typedness and nothing more; the executed points are the only evidence either obligation holds anywhere. The fixture says so rather than letting a green gate imply otherwise. One honest gap, recorded rather than papered over: no real toolchain body here witnesses the width conversions the envelope was opened for. Written as a saturating add over an i64 intermediate, LLVM recognizes the pattern at `-Oz` and lowers it to i32 compares and selects, so the conversions never reach the artifact. They survive only at `-O0`, which does not link for unrelated reasons. The operators are exercised by hand-written fixtures and validated against the real verifier; what is missing is a *toolchain-produced* witness. The needle that checks the artifact still lowers as expected was itself vacuous at first: matched module-wide, and the artifact carries two `select`s, so the exact drift it documents would have stayed green on the unrelated one. Needles are now scoped to the function that owns them, proven by a stand-in with a branchy clamp and a select-keeping `sum_n`.
The acceptance fixture did not exercise the operators this branch opened with. Written as a saturating add over an i64 intermediate, LLVM recognizes the pattern at `-Oz` and lowers it to i32 compares and two selects — the artifact contains no `i64.extend_i32_s` and no `i32.wrap_i64` at all. I had described that fixture as exercising them because the Rust source computes through an i64, which is a claim about the source rather than about the bytes, and it was wrong. `mulhi` fixes it by making the wide intermediate load-bearing: the high half of a full 64-bit product has no i32-only lowering, so the conversions survive every optimization level that links. Confirmed by decoding the body — two `i64.extend_i32_s`, `i64.mul`, `i64.shr_u`, `i32.wrap_i64` — and again in the emitted Rocq, where they appear as the `BI_cvtop` forms the translator is credited with and elaborate under coqc. The executed points include two negatives, and they are the interesting ones: `mulhi(-1, -1) == 0` and `mulhi(-1, 1) == -1` pin the *signedness* of the widening, which is what `(Some SX_S)` records. An unsigned widening agrees on every non-negative input and returns -2 and 0 at those two, so without them a wrong lowering passes silently. Neutralized by rebuilding the crate with a plain 32-bit multiply and swapping it in: the execution test fails at `mulhi(65536, 65536)` with `left: 0` — the "stayed in 32 bits" outcome its message predicts — and the Rocq needle fails naming the missing conversion. The whole coqc gate stayed green, which is the expected and instructive part: elaboration cannot tell the two apart. Every number in the fixture README was re-derived from the binary rather than patched, which caught a duplicated paragraph and a stale byte count. The optimization sweep was re-run against the three-export crate instead of assumed to carry: `-O0` still fails to link, every level that links keeps both conversions.
Nine sites across eight files, doc-only. Every changed line is a comment, and the suite is unmoved at 51 targets, 0 failures, 161 ignored. Four of these were introduced by this branch and four of those by me. Removing globals from the Tier-C gate left four docs still saying a global forces Tier C — including the crate's front door and the doc on the error variant itself, in two crates. That is not a wording slip: `tier.rs` argues that merging globals is sound only because provenance tags a global-derived address `NotParam`, and separately that merging globals is mutually exclusive with placing external data segments at their original addresses. A reader who believes global-touching closures are already excluded reads both safeguards as redundant, and two unsound changes then look like cleanups. The replacement is one paragraph, byte-identical at all four sites, saying what does happen to globals rather than merely dropping the false clause. The scaled-index work left two more. An extent operand does not carry the same requirement as an address — it is the same test minus the correlation clause — and `sub` is not unconditional, having three propagating arms, so it did not belong in a list asserting uniformity with `xor` and `and`. Both contradicted a passage later in their own module doc, which is the tell. The type checker's phase lists said imports resolve before collection when the code does the reverse. That one had concealed a live defect: extern signature types are validated during collection, hence before imports bind, so a qualified type on an `external fn` is rejected with a diagnostic naming an import the file already has. Anyone reasoning about ordering from those lists concludes the failure is impossible. Filed as #425; the code fix and the missing ordering constraint belong there, and the lists are corrected here because nothing in that fix would force anyone to notice them. Two claims are true today but rest on a fact nobody recorded: the fast path's empty warning list is a fact about the path only while `LinkWarning` has one variant concerning merged externals, and the two `link_with_warnings` entry points return different verdicts on identical bytes when there are no externals. Both are now stated where someone about to break them will look. Reviewed independently against the code rather than against the briefs that produced it — which caught, among other things, that a corrected paragraph had reintroduced the same concealment in milder form by implying all signature validation follows import resolution.
0xGeorgii
added
linker
Codecov Report❌ Patch coverage is 📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Confidence Score: 5/5
The PR appears safe to merge; no concrete changed-code defect remained after checking the memory-layout, linker-remapping, provenance, and proof-resolution paths.
The configurable layout is consistently shared and ABI-gated, newly merged global state is constrained and remapped, unsafe provenance cancellation paths fail closed, and linked proof applications are checked against the final module for ambiguity and arity.
Important Files Changed
Flowchart
%%{init: {'theme': 'neutral'}}%% flowchart LR Manifest[Inference.toml / CLI memory options] --> Infs[infs compatibility gate] Infs --> Infc[infc resolves MemoryLayout] Infc --> Analysis[A036 stack analysis] Infc --> Codegen[WASM codegen] Analysis --> Codegen Codegen --> Linker[Static linker] External[External integer-only WASM] --> Linker Linker --> Linked[Linked WASM with remapped globals and names] Linked --> Translator[wasm-to-v] Translator --> Rocq[Rocq module and obligations]Reviews (1): Last reviewed commit: "Correct documentation that asserts prope..." | Re-trigger Greptile
Context used (5)
hassert: The Verification-Obligation IR