refactor(prover): remove legacy unused reachability constraints#2441
Open
eviehoward wants to merge 3 commits into
Open
refactor(prover): remove legacy unused reachability constraints#2441eviehoward wants to merge 3 commits into
eviehoward wants to merge 3 commits into
Conversation
Remove can_write_to_endpoint() and the solver variables and encoding methods that exist solely to support it. No active query calls this method; confirmed zero callers across the monorepo. Crate is not published externally, so no public API concern. Removed as root cause: - can_write_to_endpoint(): zero callers in the codebase Removed as direct consumers of can_write_to_endpoint(): - binary_can_write: only read inside can_write_to_endpoint() - credential_has_write: only read inside can_write_to_endpoint() Removed as directly dead (no query ever read them): - credential_has_destructive: flagged by compiler, silenced with #[allow(dead_code)] rather than removed - filesystem_readable: flagged by compiler, silenced with #[allow(dead_code)] rather than removed Removed as now-empty encoding methods: - encode_credentials(): exclusively populated credential_has_write and credential_has_destructive - encode_filesystem(): exclusively populated filesystem_readable Also removed two #[allow(dead_code)] allowances and the corresponding HashMap::new() initialisers and build() call sites. Active query behavior is unchanged. All existing prover tests pass without modification and cover all four finding categories end-to-end. No new tests added as they would duplicate existing coverage exactly. Note: removing encode_credentials() leaves write_actions_for_scopes() and destructive_actions_for_scopes() in credentials.rs with no callers. Left as a follow-up outside the scope of this change. Closes NVIDIA#2412 Signed-off-by: Evie Howard <evhoward@redhat.com>
…gistry BinaryProtocol::can_write(), BinaryCapability::can_write(), and write_mechanisms() lost their only callers when can_write_to_endpoint() and its supporting model fields were removed. Delete the now-dead methods. write_mechanisms() had no callers prior to this series; the two can_write() methods were made dead by the preceding model.rs cleanup. Signed-off-by: Evie Howard <evhoward@redhat.com>
The module doc incorrectly listed write-bypass violation detection as a prover capability. The prover only checks reachability queries; write-bypass detection was never implemented. Signed-off-by: Evie Howard <evhoward@redhat.com>
eviehoward
requested review from
a team,
derekwaynecarr,
maxamillion and
mrunalp
as code owners
July 23, 2026 11:12
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Removes
can_write_to_endpoint()and the solver variables and encoding methods that exist solely to support it. The active query layer usescan_exfil_via_endpoint()and direct credential lookups exclusively; the removed Z3 encodings were scaffolding for query categories that were never implemented or were later cut. Confirmed zero callers across the monorepo; crate is not published externally and no release notes reference its public API surface.Also removes three dead write-capability helpers from
registry.rsthat lost their only callers as a direct consequence of themodel.rscleanup.Related Issue
Closes #2412
Changes
can_write_to_endpoint()— zero callers confirmed across the monorepobinary_can_write,credential_has_write— only consumed bycan_write_to_endpoint()credential_has_destructive,filesystem_readable— directly dead, previously silenced with#[allow(dead_code)]encode_credentials(),encode_filesystem()— exclusively populated the above fields#[allow(dead_code)]allowances,HashMap::new()initialisers, and theencode_credentials()/encode_filesystem()calls insidebuild().BinaryProtocol::can_write(),BinaryCapability::can_write()— made dead by themodel.rscleanup abovewrite_mechanisms()— pre-existing dead code, no callers prior to this seriesFollow-up Dead Code
This PR leaves behind two dead code clusters that are out of scope here but should be tracked:
can_write()andwrite_mechanisms()orphaned their only consumers ofBinaryProtocol::actions,BinaryAction, andActionType::Write/Destructive. The data is still loaded from YAML at parse time but never queried.write_actions_for_scopesanddestructive_actions_for_scopeswere killed here (their sole callerencode_credentials()was removed). The cascade beneath them -actions_for_scopes,ApiCapability,ApiAction, and all associated loaders and serde types - was already dead before this PR. This is the full API registry subsystem in credentials.rs, which was never fully wired up.To avoid scope creep I have omitted these from this PR but can address it here if preferred - left as a follow-up outside scope of this PR for now.
Testing
mise run pre-commitpassescargo test -p openshell-proverpasses. No new tests added — existing tests (test_findings_for_github_policy,test_wildcard_endpoint_covering_credential_host_emits_credential_reach,test_known_metadata_hostname_emits_link_local_finding,test_empty_policy_no_findings) cover all four active finding categories end-to-end.can_write_to_endpoint()was never invoked byprove()or any live query path — no test could have detected its presence or absence.Checklist