Skip to content

zipper_merge_dnf: empty clause is silently bottom, the algebra says top #64

Description

@MesTTo

clause_mask in experimental/zipper_algebra.rs returns ByteMask::EMPTY when a clause has no members, so an empty clause contributes nothing to the merge. As DNF algebra the empty conjunction is top (the identity of meet), which over pathsets is the everything-set and not representable as a finite trie, so PathMap cannot honor it; but honoring it silently as bottom inverts its meaning. Today Clause::FULL and the dnf! macro never produce one, so nothing is wrong in-tree; the hazard is a programmatic Clause builder that filters members down to none and silently flips from "always contributes" to "never contributes". One line settles it either way: a debug_assert!(!clause.is_empty()) in zipper_merge_dnf, or a doc sentence on Clause stating the empty clause is treated as bottom by convention.

Metadata

Metadata

Labels

No labels
No labels

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions