You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Audit and remove reachability-model state that is constructed on every prover run but is not consumed by any active query.
The current model still builds credential_has_destructive and filesystem_readable constraints even though no repository caller reads them. binary_can_write is only consumed by can_write_to_endpoint(), which also has no repository callers.
Context
Identified while reviewing the call chain rooted at prove() after #2395.
Relevant code:
crates/openshell-prover/src/model.rs
crates/openshell-prover/src/registry.rs
crates/openshell-prover/src/policy.rs
Because can_write_to_endpoint() is public, confirm whether it is a supported external API before removing the method or the state that supports it.
Definition of Done
Audit the unused model fields and helper methods against supported public API expectations.
Remove solver variables, maps, and encoding work that no active or supported query requires.
Remove associated dead-code allowances.
Preserve the findings produced by all existing prover fixtures.
Add or update tests demonstrating that active query behavior is unchanged.
This issue has had no activity for 14 days and is now marked stale. It may be closed in 7 days if there is no further activity. Comment or remove the state:stale label to keep it open.
Activity
refactor(prover): remove legacy unused reachability constraints
refactor(prover): remove legacy unused reachability constraints
github-actions commentedon Aug 6, 2026
This issue has had no activity for 14 days and is now marked stale. It may be closed in 7 days if there is no further activity. Comment or remove the state:stale label to keep it open.
refactor(prover): remove legacy unused reachability constraints
refactor(prover): remove legacy unused reachability constraints (NVID…