V5 · Proof-validity

planarian @ a924e09 · Spec v4.6 · snapshot main · all versions

Ledger bookkeeping helpers (push_tag, tag_string, note_why, archive, set_override, lift_override, record_incident, use_token) are external_body with no postcondition: each receives only the field it updates, so the verified fields are untouched by construction; trusted only to terminate

Sites: txn::ledger

If it is false

These invariants fall: I6, I12.