TBD: Split this? Fixes for no-dangling-path - #155

Draft

imlvts wants to merge 18 commits into

Adam-Vandervorst:masterfrom

imlvts:fix/dangling-paths

Commits on Oct 2, 2026

lean: a second model, for the dangling-path-free subset

imlvts
and
claude
committed
d35ef9e
differential: a fuzzer for the dangling-path-free subset

imlvts
and
claude
committed
413e896
lean: triage the first 300 inputs of the pruned fuzzer

imlvts
and
claude
committed
d0d9430
lean: classify the dangling-path shape by what did not move

imlvts
and
claude
committed
80528d0
lean: check the pruned findings against fuzz-fixes-v3

imlvts
and
claude
committed
1227748
lean: prove the lattice laws for the pruned model

imlvts
and
claude
committed
a40c286
lean: state the lattice laws as equations

imlvts
and
claude
committed
68daaec
lean: name the per-instance laws, and prove non-commutativity at the trie level

imlvts
and
claude
committed
ff435c1
lean: can a trie be a value? Not PrunedMap; yes CMap

imlvts
and
claude
committed
09831e3
lean: carry the canonical form in PrunedMap's type

imlvts
and
claude
committed
2075f94
Model: join_map_into merges the value status instead of discarding it

imlvts
and
claude
committed
da27343
lean: correct two attributions this model's findings depend on

imlvts
and
claude
committed
84168b1
Prune the location an empty write leaves behind

imlvts
and
claude
committed
c4fbbcc
Make meet/join value bias independent of node layout

imlvts
and
claude
committed
c4d08ba
Cherry-pick the value-bias fix, and fuzz the result at scale

imlvts
and
claude
committed
dbac8e8
lean: a 22-byte reproducer for the Identity imprecision

imlvts
and
claude
committed
284f7a8
Return Identity from the integer psubtract when nothing was subtracted

imlvts
and
claude
committed
7c8df98
lean: record what the psubtract fix leaves behind

imlvts
and
claude
committed
0740f77

Navigation Menu

TBD: Split this? Fixes for no-dangling-path - #155

TBD: Split this? Fixes for no-dangling-path#155
imlvts wants to merge 18 commits into
Adam-Vandervorst:masterfrom
imlvts:fix/dangling-paths

Commits on Oct 2, 2026

lean: a second model, for the dangling-path-free subset

differential: a fuzzer for the dangling-path-free subset

lean: triage the first 300 inputs of the pruned fuzzer

lean: classify the dangling-path shape by what did not move

lean: check the pruned findings against fuzz-fixes-v3

lean: prove the lattice laws for the pruned model

lean: state the lattice laws as equations

lean: name the per-instance laws, and prove non-commutativity at the trie level

lean: can a trie be a value? Not PrunedMap; yes CMap

lean: carry the canonical form in PrunedMap's type

Model: join_map_into merges the value status instead of discarding it

lean: correct two attributions this model's findings depend on

Prune the location an empty write leaves behind

Make meet/join value bias independent of node layout

Cherry-pick the value-bias fix, and fuzz the result at scale

lean: a 22-byte reproducer for the Identity imprecision

Return Identity from the integer psubtract when nothing was subtracted

lean: record what the psubtract fix leaves behind