pitbull.toml.example

# pitbull.toml — Pitbull verifier configuration
#
# Place at the verified crate root. Pitbull refuses to verify a crate without
# this file. Every option below has a documented default; leaving an option
# unset accepts the default.
[project]
# Crate name (must match Cargo.toml). Used to scope the verification report.
name = "example-crate"
# PSS-1 PB071: which Pitbull-supported toolchain pair this project pins.
# The string identifies a known-good combination of (Ferrocene release,
# rustc nightly used by Pitbull internals).
toolchain = "pitbull-0.1.0-ferrocene-26.02.0"
[verification]
# Hard timeout per verification condition (seconds). Timeout counts as failure.
vc_timeout_seconds = 60
# Fail closed on COVERAGE GAPS (default true). A coverage gap is a
# safety-relevant check the visitor could not run with no compensating
# obligation (e.g. an unmodelable `p.0 + p.1`, a unary-negation skip, an
# unclassifiable callee). With this true, such a gap drives the wrapper's
# exit code to 1 — so a CI gate keyed on the exit status cannot mistake
# "verified except the parts I could not model" for a clean verification
# (the "no silent skips" posture). Set false to keep coverage gaps as
# stderr-only notes that do not affect the verdict. Transparency notes
# never affect the exit code regardless of this setting.
fail_on_coverage_gaps = true
# The PRELUDE allow-list (fail-closed library boundary). With this true (the
# default), a call into core/std/alloc is accepted only if it is on the
# trusted-total allow-list (is_trusted_total_library_call); any other stdlib
# call emits an untrusted-stdlib coverage gap and fails closed. This inverts
# the historic trust-all-stdlib posture, under which an un-enumerated
# panicking stdlib method was a silent false discharge. In-crate calls and
# user trait-impls are unaffected. Set false to restore trust-all-stdlib
# (e.g. while migrating a crate whose total stdlib surface the prelude does
# not yet enumerate — a total method not on the list is otherwise a
# conservative false REJECT, never a false discharge). See SAFETY-MANUAL §3.6.
strict_library_acceptance = true
# Per-function preconditions surfaced to the SMT solver as hypotheses.
# Keys are fully-qualified function paths; values are arrays of
# predicates.
#
# v0.2 O.2 (this version) accepts a Rust-like predicate grammar:
#   "<ident> <cmp_op> <int_literal>"  e.g.  "x < 100"
#   "<int_literal> <cmp_op> <ident>"  e.g.  "100 > x"  (normalized
#                                                       to ident-first)
# where <cmp_op> is one of < <= > >= == !=.
#
# The visitor parses each predicate, binds the named variable to the
# matching parameter (looked up via the body's `arg_names`), and
# translates the predicate to SMT-LIB with the right signed/unsigned
# BV operator and literal encoding for the parameter's type.
#
# Strings that fail predicate parsing are spliced VERBATIM into the
# SMT problem — the o.1 escape hatch for cases the grammar doesn't
# yet cover. Use raw SMT-LIB sparingly; the predicate form is
# easier to audit.
#
# `#[pitbull::requires("...")]` extraction landed in v0.2 O.3, so
# preconditions can live next to the code they constrain instead of in
# this config file. (This comment said "will add" long after it shipped;
# corrected 2026-08-03.) Both sources are merged for a given function —
# config clauses first, then attribute clauses — and the merged list is
# BOTH what the callee assumes and what its callers must establish.
#
# ## Callers must establish what the callee assumes (PB077)
#
# A precondition is an ASSUMPTION while proving the callee's own body, so
# every CALL to that function must separately establish it, or modular
# verification would be unsound. As of Increment 1 (2026-08-03) Pitbull
# proves this at the call site when the actual arguments are CONSTANT
# integers: `safe_div(10, 5)` discharges against `requires("b > 0")`, and
# `safe_div(10, 0)` is refuted with a counterexample (exit 1). As of
# Increment 2 (2026-08-07) it also proves the forwarding shape, where the
# actual is one of the CALLER's own parameters and the caller's own
# contract supplies the evidence: `fn caller(v: u32) { safe_div(10, v) }`
# under `requires("v > 0")` on `caller` discharges too. As of Increment 3
# (2026-08-08) it also proves a COMPUTED EXPRESSION over constants and/or
# caller parameters, traced back through the caller's own straight-line
# statements: `fn caller(v: u32) { let t = v + 1; safe_div(10, t) }` under
# a caller contract bounding `v` discharges too. A caller whose own
# preconditions are mutually contradictory does not get a free pass — the
# same consistency guard that protects every other obligation kind refuses
# the claim as vacuous rather than discharging it, for all three
# increments alike. Calls it cannot yet encode — a value behind a branch,
# a bitwise op, a raw-SMT-LIB clause anywhere in either contract, a
# `usize` parameter — are reported as a fail-closed coverage gap (also
# exit 1), never silently accepted.
#
# Example: prove `add_two(x: u32, y: u32) -> u32 { x + y }` safe by
# constraining both inputs:
# [verification.preconditions]
# "my_crate::add_two" = ["x < 100", "y < 100"]
#
# Raw SMT-LIB escape hatch (still works, with lex-validation):
# "my_crate::weird" = ["(assert (= lhs #x00000007))"]
#
# ## Audit posture (post-O.2 hardening)
#
# Each precondition string is processed through three checks. The
# rejection path produces a loud `audit-note` in the wrapper's
# stderr — silent skips are forbidden:
#
#   1. Lex-validation (F2): a raw-SMT-LIB string must be exactly
#      one balanced `(assert ...)` form. String literals (`"..."`),
#      comments (`;...`), multi-directive injections
#      (`(check-sat) (assert false)`), and unbalanced parens are
#      all refused.
#
#   2. Translation range (F3): predicate-form preconditions whose
#      literal doesn't fit the operand type (`x < 1_000_000`
#      against a `u8` parameter) produce an audit note rather
#      than silent truncation.
#
#   3. Consistency check (F1, CRITICAL): before discharging any
#      obligation that carries assumptions, Pitbull runs a
#      satisfiability check on the assumption set alone. If the
#      assumptions are contradictory (`(assert false)` or
#      mutually exclusive constraints like `["x < 10", "x > 100"]`),
#      the wrapper logs "REFUSED — preconditions are
#      contradictory" and treats the obligation as undischarged.
#      Without this check, a contradictory hypothesis would make
#      Z3 return `unsat` for any safety property — silently
#      "verifying" unsafe code via vacuous implication.
# Solver agreement threshold. PSS-1 design: require 2-of-3 solvers to return
# UNSAT before accepting a proof obligation. Increase to 3 for highest-assurance
# builds. Decrease only with documented justification.
solver_agreement = 2
# Solvers to run in parallel for the AGREEMENT GATE. ALL configured solvers run;
# an obligation is discharged only when at least `solver_agreement` DISTINCT
# solvers independently return `unsat` AND none returns `sat`. A `sat`/`unsat`
# split is reported as a loud DISAGREEMENT and fails closed (it is NOT
# "fastest answer wins"). Duplicate entries are deduped — a solver cannot vote
# twice. Default pool is ["z3", "cvc5"]; both fully support the QF_BV bit-vector
# logic Pitbull emits.
# NOTE: Alt-Ergo <= 2.4.0 has NO bit-vector theory ("Bitvector not yet
# supported"), so it can never discharge an overflow/index obligation and would
# only dilute the pool — leave it out unless you have a BV-capable build.
solvers = ["z3", "cvc5"]
# Pinned solver versions. ENFORCED (2026-05-29): before dispatch, the wrapper
# runs each pinned solver's `--version` and checks the pinned string appears in
# the output. A solver whose version does NOT match is DROPPED from the
# agreement pool (its vote will not count) with a loud warning — fail-closed,
# since a smaller pool only makes the agreement threshold harder to reach. A
# solver with no entry here runs unchecked (pinning is opt-in, per-solver).
[verification.solver_versions]
z3        = "4.13.4"
cvc5      = "1.2.0"
alt-ergo  = "2.6.0"
[subset]
# PSS-1 PB020: maximum implicit stack allocation, bytes. Default 64 KiB.
# Set lower for tight MCU targets.
stack_allocation_limit_bytes = 65536
# PSS-1 PB052: pointer width of the verification target. Pitbull issues stricter
# arithmetic obligations for narrower platforms.
target_pointer_width = 32
# PSS-1 PB048: panic strategy. Must be "abort" in v0.1.
panic_strategy = "abort"
# PSS-1 PB068: trust budget. Builds fail if trusted_lines / verified_lines
# exceeds this fraction. Default 0.05 (5 percent).
trust_budget_fraction = 0.05
# PSS-1 PB059: proc macros allowed in verified code. ENFORCED (2026-05-29):
# any DERIVE or ATTRIBUTE proc-macro that expands into reachable code and is
# defined in a crate NOT on this list (and not the local crate or a trusted
# toolchain crate — core/std/alloc/proc_macro) causes a PB059 subset rejection.
# Crate names normalize hyphens/underscores (`serde-derive` == `serde_derive`).
# (Function-like `name!{...}` proc-macros are a tracked follow-up.)
allowed_proc_macros = [
    "pitbull-spec",      # our own attribute macros
    "thiserror",         # widely audited, no allocation in derived bodies
    # "serde_derive",    # uncomment after auditing your serde usage profile
]
# PSS-1 PB060: build scripts the project explicitly trusts. Each entry must
# include the SHA-256 of the build.rs file content. Pitbull verifies the hash
# at every run.
[[subset.trusted_build_scripts]]
crate  = "example-build-dep"
sha256 = "0000000000000000000000000000000000000000000000000000000000000000"
reason = "Vendor-audited build script generates constant lookup tables only."
[reachability]
# Entry points that anchor the call graph. Pitbull verifies these and every
# function transitively reachable from them.
verify_roots = [
    "example_crate::verified_api::*",
]
# Items explicitly excluded from reachability (e.g. test-only code).
exclude = [
    "example_crate::tests::*",
]
[reporting]
# Where to write the SARIF report consumed by CI and IDEs.
sarif_path = "target/pitbull/report.sarif"
# Proof certificate directory. Certificates are committed to the repository
# so that `pitbull replay` can re-execute them against current solver
# binaries (defense against solver-bug regression).
certificate_dir = ".pitbull-cache/certs"
# Whether to fail the run if any certificate replay disagrees with a fresh run.
strict_replay = true
[cache]
# Content-addressed proof cache. Required for usable CI; mandatory off for
# qualified releases (those reprove from scratch).
enabled = true
# Cache signing key path. Caches without valid signatures are rejected.
signing_key_path = ".pitbull-cache/signing.key"