The Lean model and the fuzzer were merged as-is because they provide valuable feedback for the library.
However, Lean model has known warts, primarily because it tries to follow PathMap. Otherwise differential fuzzing would not give any useful feedback.
The model needs to be inspected for inconsistencies/unexpected behavior.
Here's a list of things to look at: long version
AlgStatus.merge it's copied from ring.rs, but not separately derivedu64Ops copies the crate's left-biased u64 lattice, where join and meet ignore the second operand. The Element paths of the model's result resolution are never exercised by that instance.prunePath is "logically inconsistent" and will be masked outtoNextKPath picked one of two disagreeing implementations. follows the native ReadZipper fallback to the zipper root when the focus is shallower than k, where the trait default returns false.dropHead discards values at depth exactly k. Nothing documents that, and the fixtures confirming it are copied from the crate's own tests.joinMapInto reproduces two asymmetries with join_into: a short-circuit that throws away the value status after writing the value, and a "node exists" test where join_into tests "node empty". The harness masks its status most of the time anyway.meet2 never reports Identity because a comment in the implementation says so, even though the doc for the status says it could.
TODO: create an issue for each of these?
The Lean model and the fuzzer were merged as-is because they provide valuable feedback for the library.
However, Lean model has known warts, primarily because it tries to follow PathMap. Otherwise differential fuzzing would not give any useful feedback.
The model needs to be inspected for inconsistencies/unexpected behavior.
Here's a list of things to look at: long version
AlgStatus.mergeit's copied from ring.rs, but not separately derivedu64Opscopies the crate's left-biasedu64lattice, wherejoinandmeetignore the second operand. The Element paths of the model's result resolution are never exercised by that instance.prunePathis "logically inconsistent" and will be masked outtoNextKPathpicked one of two disagreeing implementations. follows the nativeReadZipperfallback to the zipper root when the focus is shallower than k, where the trait default returns false.dropHeaddiscards values at depth exactly k. Nothing documents that, and the fixtures confirming it are copied from the crate's own tests.joinMapIntoreproduces two asymmetries withjoin_into: a short-circuit that throws away the value status after writing the value, and a "node exists" test where join_into tests "node empty". The harness masks its status most of the time anyway.meet2never reports Identity because a comment in the implementation says so, even though the doc for the status says it could.TODO: create an issue for each of these?