Context
The probe KB property P14 (Deterministic output) now explicitly requires that array fields like dependencies, type-dependencies, and term-dependencies are sorted in a stable, deterministic order.
In both probe-verus and probe-rust, the dependencies-with-locations array was non-deterministic because it was built by iterating over a HashSet. probe-verus fixed this by sorting by (line, code-name).
Request
Audit the probe-lean extract implementation (ProbeLean/Atomize.lean and related files) to verify:
- Are
dependencies, type-dependencies, and term-dependencies arrays generated in a deterministic order?
- If they use any unordered collection (e.g.,
HashMap, HashSet, or Lean's Std.HashMap), is the result sorted before serialization?
- If non-deterministic, apply a stable sort (e.g., by declaration name or source position).
References
Context
The probe KB property P14 (Deterministic output) now explicitly requires that array fields like
dependencies,type-dependencies, andterm-dependenciesare sorted in a stable, deterministic order.In both probe-verus and probe-rust, the
dependencies-with-locationsarray was non-deterministic because it was built by iterating over aHashSet. probe-verus fixed this by sorting by(line, code-name).Request
Audit the probe-lean extract implementation (
ProbeLean/Atomize.leanand related files) to verify:dependencies,type-dependencies, andterm-dependenciesarrays generated in a deterministic order?HashMap,HashSet, or Lean'sStd.HashMap), is the result sorted before serialization?References
kb/engineering/properties.md