feat: execute bounded protected-effect integrity checks

[fraware]

Purpose

Turn the new protected-effect obligation family into an executable bounded guarantee using OVK's existing isolated deterministic-worker architecture.

Decision semantics

For protected_effect_integrity:

• pass only when source-profile coverage is complete, an accepted preceding authorization guard exists, and all principal/effect/resource bindings are equal;
• fail when a complete supported path reaches a protected effect without an accepted guard, or when an explicit binding is distinct;
• unknown for partial/unsupported source coverage, unresolved bindings, missing binding dimensions, or malformed abstractions.

The result remains conditional on the declared semantic anchors and supported source profile. This is not a claim of arbitrary Python/FastAPI verification.

Backend routing correction

The existing native Z3 adapter only implements the older route-reachability encoding. It now rejects property kinds outside its declared capability set instead of accepting every authorization-lane obligation.

The deterministic authorization backend explicitly declares support for protected_effect_integrity and carries the property kind + abstraction coverage into the isolated evaluator.

Tests

End-to-end tests cover:

• supported straight-line path -> pass;
• missing guard -> concrete fail;
• mismatched resource identity -> unknown;
• conditional authorization -> unknown due partial semantic coverage;
• deterministic backend selected / incompatible Z3 backend rejected.

Stack

Draft stacked on #32 -> #31 -> #30. Base is feat/fastapi-semantic-v2; current release-candidate work on main remains untouched.