Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
d35ef9e
lean: a second model, for the dangling-path-free subset
imlvts Oct 1, 2026
413e896
differential: a fuzzer for the dangling-path-free subset
imlvts Oct 1, 2026
d0d9430
lean: triage the first 300 inputs of the pruned fuzzer
imlvts Oct 1, 2026
80528d0
lean: classify the dangling-path shape by what did not move
imlvts Oct 1, 2026
1227748
lean: check the pruned findings against fuzz-fixes-v3
imlvts Oct 1, 2026
a40c286
lean: prove the lattice laws for the pruned model
imlvts Oct 2, 2026
68daaec
lean: state the lattice laws as equations
imlvts Oct 2, 2026
ff435c1
lean: name the per-instance laws, and prove non-commutativity at the …
imlvts Oct 2, 2026
09831e3
lean: can a trie be a value? Not PrunedMap; yes CMap
imlvts Oct 2, 2026
2075f94
lean: carry the canonical form in PrunedMap's type
imlvts Oct 2, 2026
da27343
Model: join_map_into merges the value status instead of discarding it
imlvts Oct 2, 2026
84168b1
lean: correct two attributions this model's findings depend on
imlvts Oct 2, 2026
c4fbbcc
Prune the location an empty write leaves behind
imlvts Oct 2, 2026
c4d08ba
Make meet/join value bias independent of node layout
imlvts Sep 15, 2026
dbac8e8
Cherry-pick the value-bias fix, and fuzz the result at scale
imlvts Oct 2, 2026
284f7a8
lean: a 22-byte reproducer for the Identity imprecision
imlvts Oct 2, 2026
7c8df98
Return Identity from the integer psubtract when nothing was subtracted
imlvts Sep 16, 2026
0740f77
lean: record what the psubtract fix leaves behind
imlvts Oct 2, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 36 additions & 0 deletions differential/src/bin/pruned_trace.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
//! Prints the dangling-path-free differential trace for a fuzzer input, from
//! the real crate.
//!
//! pruned_trace <input-file> # or read the bytes from stdin
//!
//! `lean/.lake/build/bin/pruned-oracle` prints the same trace from
//! `PrunedModel`; `lean/pruned_differential.py` runs both and diffs them.
//!
//! `--check` needs no oracle: it asserts the zipper invariants after every
//! operation and, at the end of the run, that the write target contains no
//! dangling path -- which is the whole claim this harness's operation subset
//! makes. See `differential::pruned`.

use differential::pruned::run;
use differential::serve;

fn main() {
let args: Vec<String> = std::env::args().skip(1).collect();
let check = args.iter().any(|a| a == "--check");
// Resident mode: one process, many inputs over stdin. See `serve`.
if args.iter().any(|a| a == "--server") {
serve(check, run);
return;
}
let file = args.iter().find(|a| !a.starts_with("--")).cloned();
let bytes: Vec<u8> = match file {
Some(p) => std::fs::read(p).expect("cannot read input"),
None => {
use std::io::Read;
let mut v = Vec::new();
std::io::stdin().read_to_end(&mut v).unwrap();
v
}
};
print!("{}", run(&bytes, check));
}
5 changes: 5 additions & 0 deletions differential/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,14 @@
//! * [`server`] is the resident-process protocol the driver speaks.
//! * [`repro`] turns an input back into standalone `pathmap` calls.
//! * [`act`] is the `ArenaCompactTree` read source behind `act_trace`.
//! * [`pruned`] is a second, smaller harness: the subset of the API that
//! cannot leave a dangling path, checked against `lean/PrunedModel` and
//! driven by `lean/pruned_differential.py`. See its module docs for why it
//! is not `harness` with a flag.

pub mod act;
pub mod harness;
pub mod pruned;
pub mod repro;
pub mod server;

Expand Down
Loading