Add native Z3 parity for authorization reachability

[fraware]

The deterministic authorization adapter already builds obligations, returns normalized evidence, and fails closed on invalid abstractions.

Add an optional native Z3 execution path and parity tests for pass, fail, and unknown cases. Record solver version, query polarity, and which path produced the result.

[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.

[fraware]

Re-scoped after auditing main: the deterministic authorization path already builds obligations and normalized evidence. The remaining work is native Z3 parity with solver provenance.