Lean Model for PathMap with no dangling paths - #154

Open

imlvts wants to merge 12 commits into

Adam-Vandervorst:masterfrom

imlvts:spec/pruned-model

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