Implement Z3 authorization reachability example

[fraware]

Goal

Implement the first SMT-backed example for authorization regression.

Scope

• Add ovk/adapters/z3/ implementation.
• Define a small route-reachability abstraction.
• Encode the no-admin-route-bypass template.
• Return a counterexample when a non-admin user can reach an admin-only route.
• Generate a regression test fixture from the counterexample.

Acceptance criteria

• The example in examples/auth_regression/ can be converted into a satisfiability query.
• A bypass produces a normalized evidence object with status=fail.
• Query polarity is recorded in the obligation and evidence.

[fraware]

Progress update:

• Added a Z3-style authorization reachability adapter.
• Added failing and passing authorization fixtures.
• Added adapter tests.
• Added an optional z3-solver path that returns unknown if the solver is unavailable.
• Added benchmark seed cases and a scorer that runs in CI.

Next hardening step: replace the deterministic abstraction with full SMT obligation generation while preserving the current evidence shape.