Prove that Divider divides by mark-christiaens · Pull Request #65 · Verilean/sparkle

mark-christiaens · 2026-06-25T18:52:22Z

No description provided.

junjihashimoto · 2026-06-26T08:29:30Z

@mark-christiaens Thx!
This PR specifies a .so file in the lakefile, but I'm not sure if it will work on macOS. I wanted to see how the CI would handle it, but since it attempts to check out the specific commit hash of the PR, the CI isn't actually running.
The contents of the PR look good. I wonder if the "co-authored by" commit attribution is necessary? I don't think there's any need to explicitly attribute copyright to Claude.

`/work/.sparkle-kernel-prefix` ends up as the `env_name` that `jupyter lite build --XeusAddon.prefix=…` writes into `site/xeus/kernels.json` and uses as the parent directory of `kernel.json` (`site/xeus/.sparkle-kernel-prefix/xlean/kernel.json`). The GitHub Pages deploy step then filters dotfiles Jekyll-style, so the entire `site/xeus/.sparkle-kernel-prefix/` tree disappears from the upload — except for one straggler JSON that the path-filter happens to pass through. The deployed site ends up listing `kernels.json = []`, so JupyterLite's Launcher renders no Lean 4 notebook card, even though every other piece of the lab is healthy. Renaming `/work/.sparkle-kernel-prefix` → `/work/sparkle-kernel-prefix` gives jupyterlite-xeus a Jekyll-safe env_name, the kernel.json tree ships intact, and the browser sees a populated kernelspec list. Verified locally with the browser-mcp Chromium driver: * `verilean.github.io/xeus-lean/xeus/kernels.json` (works) → `[{"kernel":"xlean","env_name":"wasm-host"}]` * `verilean.github.io/sparkle/xeus/kernels.json` (this PR target) → `[]` before fix, expected `[{...,"env_name":"sparkle-kernel-prefix"}]` after fix.

The interpreter/LSP force-loads an IP lib's monolithic `libsparkle_IP_*.so` (via `--load-dynlib`) at startup, before Sparkle's per-module dynlibs are loaded by olean imports. Once `Signal.map` began routing through the `@[extern "sparkle_cache_get"]` LICM barrier, that monolithic failed to load with a confusing undefined-symbol error on a Signal closure even though the `.olean` built fine. Fix it on two fronts: - Force the `sparkle_barrier` / `sparkle_jit` extern archives whole-into the precompiled `libsparkle_Sparkle.so` so it is self-contained regardless of load order or dlopen scope (`--whole-archive` on GNU ld, `-force_load` on Apple ld64, visibility pragmas on Windows). - Make each IP lib's monolithic `.so` depend on the per-module Sparkle dynlibs (`sparkleDynlibLinkArgs`), so the loader dedups them by path and each module initializer runs exactly once (no double-init). Document the underlying Lean/Lake force-load ordering issue in docs/lean-lake-force-load-ordering-issue.md.

Prove the Sparkle RV32 divider correct against its pure-FSM model and the real synthesized circuit, covering signed and unsigned division for all non-zero divisors, divide-by-zero behavior, and done-pulse timing. The contract is generalized to an arbitrary start cycle and arbitrary inputs, and the eight canonical divider results are restated as corollaries of the generic theorems. IP/RV32/Divider.lean extracts the `Signal.loop` body into named definitions (`DivState`, `dividerLoopBody`) so the proofs can reference it; this is a behavior-preserving refactor — the synthesizer `whnf`-reduces it back to a lambda, so the generated Verilog is unchanged.

The `sparkleDynlibLinkArgs` applied to IP.RV32 / IP.BitNet were built entirely from GNU-ld-only constructs (`-l:NAME.so` exact-file linking, `--no-as-needed`/`--as-needed`, `$ORIGIN` rpath) and, unlike the `Sparkle` lib's `moreLinkArgs` right below, were unconditional. Apple ld64 rejects all of them (per-module dynlibs are `.dylib`, not `.so`; rpath origin is `@loader_path`), so any macOS build of those IP libs hard-failed at link. Guard them per-platform exactly like the Sparkle lib: macOS/Windows fall back to Lake's default linking, since the force-load ordering bug they work around is itself Linux/glibc-only. Also fix downstream-smoke.yml so a fork PR actually gets tested: it was pinning `git = <base repo>` / `rev = <fork head sha>`, a commit absent from the base repo, so `lake update` could never fetch it and the job went red without compiling anything. Use the PR head repo's clone_url / full_name (falling back to this repo on push). Add a macOS-only `lake build sparkle/IP.RV32` step to exercise the IP dynlib link path — the previous smoke only built MyBlinky -> Sparkle and never linked the flagged args.

mark-christiaens · 2026-06-28T15:21:00Z

Got rid of the co-author messages.
Have tried to improve the build. Claude points this out though:

The CI not running is a fork-checkout bug in downstream-smoke.yml. It was pinning git = + rev = , but a fork PR's head SHA only exists in the fork, so lake update could never fetch it — the job went red without compiling anything. I changed it to use the PR head repo's clone_url/full_name (falling back to this repo on push events). I also added a macOS-only lake build sparkle/IP.RV32 step, because the existing smoke only built MyBlinky → Sparkle and never linked the flagged sparkleDynlibLinkArgs path at all.

One thing on your side: since pull_request events run the workflow from the base branch, the downstream-smoke.yml fix won't take effect on this PR until it's merged to your default branch — so this PR's macOS job will still be red against the old workflow. If you want to confirm the macOS link before merging, the quickest path is to build the branch locally (lake build sparkle/IP.RV32 on a Mac) or trigger the updated workflow from your branch.

mark-christiaens · 2026-06-28T15:50:08Z

One thing I'm not that happy with, w.r.t. the divider proof, is that it needs a new axiom (in LoopProps.lean). The reason it's needed is that Lean4 can't look beyond the opaque definition of Signal.loop.

Would it be interesting to do Signal.loop differently?:

Offer a default Signal.loop implementation that is quadratic but is implemented in regular Lean.
Offer and alternative implemented_by version of Signal.loop that is fast (probably still using the FFI cache implementation) for simulation.

The advantage would be that the semantics of Signal.loop can still be analyzed by the Lean compiler/prover. So, if you have correctness proofs (like the one for this divider), you would not need additional axioms. I guess that axiom would be replaced by a proof that the quadratic Signal.loop is causal.

junjihashimoto · 2026-07-01T12:55:32Z

@mark-christiaens
The axiom would become a theorem in #81 .
Thx!

…m-smoke) PR #65 (`c59820c`) added `moreLinkArgs` to the `Sparkle` lean_lib to force the `sparkle_barrier` / `sparkle_jit` extern archives whole-into the precompiled `libsparkle_Sparkle.so` — necessary so the `.so` self-resolves `sparkle_cache_get` / `sparkle_eval_at` (the `@[extern]` LICM barriers `Signal.loop`'s memoization uses; without it the interpreter/LSP fails to dlopen the `.so`). But it used a *relative* path `./.lake/build/c_src`. `moreLinkArgs` propagates to every DOWNSTREAM consumer of the `sparkle` package, and there the relative path resolves against the *downstream's* build dir — which has no `c_src` — so the link fails: ld.lld: error: unable to find library -l:libsparkle_barrier.a ld.lld: error: unable to find library -l:libsparkle_jit.a This is why `downstream-smoke` (ubuntu / macos / wsl) went red on `main` starting at the PR #65 merge (`9c0e776`); it was green on the prior commit (`df8560e`). Fix: compute an ABSOLUTE path from the lakefile's own location (`__dir__`), captured as `sparkleCSrcDir`. Whether Sparkle is the root package (`lake build` here) or a git dependency (`<downstream>/.lake/packages/sparkle/…`), the path points at Sparkle's *own* populated `c_src`, so an inheriting downstream link resolves the archives correctly. Also simplifies the Linux arm to pass the absolute `.a` paths directly inside `--whole-archive` (no `-L dir` + `-l:name.so` file search needed). The `Sparkle`-lib force_load remains; only the path form changes. The IP-lib `sparkleDynlibLinkArgs` (per-module `.so` deps for the interpreter/LSP force-load path) is unaffected — it's already per-platform guarded and doesn't reach downstream MyBlinky. Verification: - `nm -D libsparkle_Sparkle.so` shows `sparkle_cache_get` / `sparkle_eval_at` as `T` (defined) — the `.so` is still self-contained. - `lake build` clean; `lake exe test` 13/13. - The emitted arg is now e.g. `-Wl,--whole-archive /abs/.lake/build/c_src/libsparkle_barrier.a …`.

Prove that Divider divides

…oint) `Signal.loop` was `opaque` (a wrapper around the `unsafe` memoizing `loopImpl`), so `(Signal.loop f).val t` could not be unfolded by the kernel. The fixpoint equation `loop f = f (loop f)` — the load- bearing fact for every feedback-circuit proof (e.g. PR #65's RV32 divider) — was therefore a *trusted axiom* (`loop_unfold`). This replaces the opaque wrapper with a *pure* definition and turns `loop_unfold` into a proved theorem, removing the custom axiom from the trust base. ## What changed `Sparkle/Core/Signal.lean`: - `loopGo f t` — the fixpoint value at time `t`, by strong recursion: apply `f` to a signal that recursively supplies the already-computed values for every earlier cycle `i < t` and `default` at `≥ t`. The `if i < t` guard makes it well-founded (`termination_by t`). Total, axiom-free. - `loop f := ⟨loopGo f⟩` — now a `def`, not `opaque`. Still carries `@[implemented_by loopImpl]`, so *execution* uses the O(n) memoizing implementation; only the *logical* value is the pure fixpoint. - `loopGo_eq` — the defining equation, exposed for proofs. `Sparkle/Verification/LoopProps.lean`: - `loop_unfold` goes from `axiom` to `theorem`, proved by rewriting through `loopGo_eq` and discharging the `default` placeholder with `StrictlyCausal` (a strictly causal body never observes cycles `≥ t`, which is exactly why the placeholder is invisible). - Module docstring updated to describe the pure definition. ## Trust base `#print axioms dividerSignal_result_gen` (a downstream RV32 divider theorem) no longer lists `loop_unfold`. Remaining axioms are all Lean-standard: `propext`, `Classical.choice`, `Quot.sound`, `Lean.ofReduceBool` (from `bv_decide`/`native_decide`, pre-existing), and `Lean.trustCompiler` (from `@[implemented_by]` — the standard trust that `loopImpl` computes the same value as `loopGo`). The bespoke fixpoint axiom is gone. ## Performance `@[implemented_by loopImpl]` keeps sim fast: a direct `Signal.loop`-counter samples `.val 2000` in ~0 ms (memoized O(n), confirmed by probe). Matched `lake exe test` runs: main 7m52s vs this branch 8m02s — within noise, no regression. ## Also fixed (surfaced by the first truly-clean build) `lakefile.lean`'s `sparkleModuleDeps` list was stale: - `sparkle_Sparkle_Backend_CppSim.so` → `_CSim.so` (CppSim was removed / renamed to CSim in the C-only-backend work; the `.so` no longer exists, so a clean build's monolithic link failed with "-l:...CppSim.so not found"). - Added the missing `sparkle_Sparkle_Core_SignalLeavesDerive.so` (the `SignalLeaves` deriving handler, added with the per-leaf output-port split, was never registered → clean-build load error "undefined symbol: initialize_..._SignalLeavesDerive"). Both were latent bugs on `main` that only bite a from-scratch `.lake/build` wipe; incremental builds kept the old `.so` around. ## Verification - `lake build` clean. - `lake exe test`: 13/13 lspec pass. - Both `Sparkle.Verification.Divider.{Correct,States33}` build against the new pure `loop` with no proof changes needed — PR #65's divider proof is now the regression test that `loop = loopGo` is the right fixpoint.

…m-smoke) PR #65 (`c59820c`) added `moreLinkArgs` to the `Sparkle` lean_lib to force the `sparkle_barrier` / `sparkle_jit` extern archives whole-into the precompiled `libsparkle_Sparkle.so` — necessary so the `.so` self-resolves `sparkle_cache_get` / `sparkle_eval_at` (the `@[extern]` LICM barriers `Signal.loop`'s memoization uses; without it the interpreter/LSP fails to dlopen the `.so`). But it used a *relative* path `./.lake/build/c_src`. `moreLinkArgs` propagates to every DOWNSTREAM consumer of the `sparkle` package, and there the relative path resolves against the *downstream's* build dir — which has no `c_src` — so the link fails: ld.lld: error: unable to find library -l:libsparkle_barrier.a ld.lld: error: unable to find library -l:libsparkle_jit.a This is why `downstream-smoke` (ubuntu / macos / wsl) went red on `main` starting at the PR #65 merge (`9c0e776`); it was green on the prior commit (`df8560e`). Fix: compute an ABSOLUTE path from the lakefile's own location (`__dir__`), captured as `sparkleCSrcDir`. Whether Sparkle is the root package (`lake build` here) or a git dependency (`<downstream>/.lake/packages/sparkle/…`), the path points at Sparkle's *own* populated `c_src`, so an inheriting downstream link resolves the archives correctly. Also simplifies the Linux arm to pass the absolute `.a` paths directly inside `--whole-archive` (no `-L dir` + `-l:name.so` file search needed). The `Sparkle`-lib force_load remains; only the path form changes. The IP-lib `sparkleDynlibLinkArgs` (per-module `.so` deps for the interpreter/LSP force-load path) is unaffected — it's already per-platform guarded and doesn't reach downstream MyBlinky. Verification: - `nm -D libsparkle_Sparkle.so` shows `sparkle_cache_get` / `sparkle_eval_at` as `T` (defined) — the `.so` is still self-contained. - `lake build` clean; `lake exe test` 13/13. - The emitted arg is now e.g. `-Wl,--whole-archive /abs/.lake/build/c_src/libsparkle_barrier.a …`.

junjihashimoto and others added 4 commits June 28, 2026 16:55

mark-christiaens force-pushed the divider_experiment branch from 9c7809c to 34fe0e1 Compare June 28, 2026 15:14

junjihashimoto merged commit 9c0e776 into Verilean:main Jul 1, 2026
3 of 6 checks passed

junjihashimoto mentioned this pull request Jul 1, 2026

LoopProps: make loop_unfold a theorem, not an axiom (pure loopGo fixpoint) #81

Merged

junjihashimoto added a commit that referenced this pull request Jul 1, 2026

Merge pull request #65 from mark-christiaens/divider_experiment

3139015

Prove that Divider divides

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Prove that Divider divides#65

Prove that Divider divides#65
junjihashimoto merged 4 commits into
Verilean:mainfrom
mark-christiaens:divider_experiment

mark-christiaens commented Jun 25, 2026

Uh oh!

junjihashimoto commented Jun 26, 2026

Uh oh!

mark-christiaens commented Jun 28, 2026

Uh oh!

mark-christiaens commented Jun 28, 2026

Uh oh!

Uh oh!

junjihashimoto commented Jul 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

mark-christiaens commented Jun 25, 2026

Uh oh!

junjihashimoto commented Jun 26, 2026

Uh oh!

mark-christiaens commented Jun 28, 2026

Uh oh!

mark-christiaens commented Jun 28, 2026

Uh oh!

Uh oh!

junjihashimoto commented Jul 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants