x402_verify_zk_or_bitvec
Formally verify ZK circuit witness uniqueness for soundness or detect BitVector integer cast truncation with Z3 proofs.
Instructions
Paid tool (30000 Base USDC atomic): Formal Z3 verification of ZK circuit witness uniqueness (soundness) or BitVector integer cast truncation.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| expr | No | Expression for bitvec check (e.g. 'a + b') | |
| mode | No | ||
| output_var | No | ||
| witness_vars | No | ||
| paymentHeader | No | x402 Base64 or JSON payment authorization string (if not in _meta.x402Payment) | |
| preconditions | No | ||
| public_inputs | No | ||
| var_bitwidths | No | Dictionary of variable bitwidths (e.g. {'a': 8, 'b': 8}) | |
| target_bitwidth | No | ||
| constraints_exprs | No |