Summary
hashing.py (line 10) documents that axiom set hashes are produced "regardless of construction order," but the implementation preserves axiom tuple order, meaning two logically identical axiom sets constructed in different order will hash differently.
Problem
make_canonical_dict() in serialization.py (line 31) sorts dict keys but does not sort lists (line 33: [_normalize(v) for v in obj]).
AxiomSet.canonical_dict() in models.py (line 165) puts axioms in a list comprehension iterating self.axioms — a tuple whose order depends on construction.
The result: two AxiomSet objects with the same axioms in different order produce different canonical dicts and different hashes. This violates the documented guarantee and undermines deterministic evidence chains.
Note: hash_proof already sorts depends_on (line 84) and imported_bundle_hashes (line 90), showing awareness of this class of problem — the same treatment should apply to the axiom list.
Suggested fix
Sort the axiom list by a stable key (e.g., axiom name) in AxiomSet.canonical_dict() before passing to make_canonical_dict. Add a test constructing two AxiomSets with identical axioms in different order and asserting hash equality.
Files
symproof/hashing.py:10 — docstring claimsymproof/serialization.py:27-33 — make_canonical_dict list handlingsymproof/models.py:160-170 — AxiomSet.canonical_dict()
Summary
hashing.py(line 10) documents that axiom set hashes are produced "regardless of construction order," but the implementation preserves axiom tuple order, meaning two logically identical axiom sets constructed in different order will hash differently.Problem
make_canonical_dict()inserialization.py(line 31) sorts dict keys but does not sort lists (line 33:[_normalize(v) for v in obj]).AxiomSet.canonical_dict()inmodels.py(line 165) puts axioms in a list comprehension iteratingself.axioms— a tuple whose order depends on construction.The result: two
AxiomSetobjects with the same axioms in different order produce different canonical dicts and different hashes. This violates the documented guarantee and undermines deterministic evidence chains.Note:
hash_proofalready sortsdepends_on(line 84) andimported_bundle_hashes(line 90), showing awareness of this class of problem — the same treatment should apply to the axiom list.Suggested fix
Sort the axiom list by a stable key (e.g., axiom name) in
AxiomSet.canonical_dict()before passing tomake_canonical_dict. Add a test constructing two AxiomSets with identical axioms in different order and asserting hash equality.Files
symproof/hashing.py:10— docstring claimsymproof/serialization.py:27-33—make_canonical_dictlist handlingsymproof/models.py:160-170—AxiomSet.canonical_dict()