Struct ProofObligation 

pub struct ProofObligation {
    pub id: Option<String>,
    pub obligation_type: ObligationType,
    pub property: String,
    pub formal: Option<String>,
    pub tolerance: Option<f64>,
    pub applies_to: Option<AppliesTo>,
    pub na_reason: Option<String>,
    pub na_owner: Option<String>,
    pub lean: Option<LeanProof>,
    pub requires: Option<String>,
    pub applies_to_phase: Option<String>,
    pub parent_contract: Option<String>,
}

A proof obligation derived from an equation.

26 obligation types: 19 property types plus 7 Design by Contract types (precondition, postcondition, frame, loop_invariant, loop_variant, old_state, subcontract).

Fields

id: Option<String>

Stable identifier, e.g. GDN-BND-001. Option because 52 contracts predate the convention and carry their own (REG-OB-001, PO-HEH-001, OBLIG-DATA-QUALITY-007-DEAD-OUTPUT-ROW), and because requiring it is a separate, enforcing change.

Until this field existed, id: was written to disk and silently dropped on parse – the struct had no such field and there is no deny_unknown_fields, so 3,612 ids generated by scripts/lib/obligation_ids.py were decoration: no consumer could read one. An obligation with no id cannot be cited by a kani harness, a test, a receipt or a commit, which is the whole point of having one (#3314).

obligation_type: ObligationType

Obligation category. Defaults to Invariant for legacy contracts that predate the DbC split (e.g. eval-harness-humaneval-v1, publish-manifest-v1) which ship with just property:/formal:.

property: String

Human-readable statement of what must hold. Alias statement accepted for legacy diagnostic contracts (e.g. decode-hot-path-prefix-cache-diagnostic-v1) whose POs predate the canonical property: naming.

formal: Option<String>

Formal predicate (Rust/Lean syntax). Alias verification accepted for legacy contracts that ship a shell/pmat-query check instead of a formal predicate.

tolerance: Option<f64>

applies_to: Option<AppliesTo>

na_reason: Option<String>

Why this obligation is NOT a property of code (PMAT-3091) – e.g. a checkpoint fact, an O() with no constant, a throughput claim.

Only meaningful with applies_to: not_applicable, where it is REQUIRED (SCHEMA-021). Present on any other obligation it is decoration – a justification nothing declares – and is an error (SCHEMA-023).

na_owner: Option<String>

Where the claim IS verified, since a unit test cannot (PMAT-3091): a bench, a pv/CI check, or an evidence command.

Same decoration rule as na_reason: required with applies_to: not_applicable (SCHEMA-022), an error without it (SCHEMA-023).

lean: Option<LeanProof>

Phase 7: Lean 4 theorem proving metadata.

requires: Option<String>

Postcondition only: links to a precondition obligation ID.

applies_to_phase: Option<String>

Loop invariant/variant only: references a kernel_structure.phases[] name.

parent_contract: Option<String>

Subcontract only: contract stem being refined (must be in metadata.depends_on).

Implementations

impl ProofObligation

pub fn is_not_applicable(&self) -> bool

true when the obligation is declared applies_to: not_applicable.

Trait Implementations

impl Clone for ProofObligation

fn clone(&self) -> ProofObligation

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ProofObligation

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for ProofObligation

fn default() -> ProofObligation

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for ProofObligation

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Serialize for ProofObligation

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.