Pigeons

A proof logging library for VeriPB.

This library is a simple abstraction layer for writing proofs checkable with VeriPB.

Features

• short-keywords: use short rule keywords, e.g., p instead of pol
• serde: add implementations for serde::Serialize and serde::Deserialize for library types

Coverage of VeriPB Syntax

• f: Proof::new
• pol: Proof::operations
• rup: Proof::reverse_unit_prop
• del: Proof::delete_ids, Proof::delete_id_range, Proof::delete_constr
• delc: Proof::delete_core_ids
• deld: Proof::delete_derived_ids
• obju: Proof::update_objective
• red: Proof::redundant
• dom: Proof::dominated
• core: Proof::move_ids_to_core, Proof::move_range_to_core
• sol: Proof::solution
• solx: Proof::exclude_solution
• soli: Proof::improve_solution
• output: Proof::output, Proof::conclude
• conclusion: Proof::conclude, Proof::new_with_conclusion, Proof::update_default_conclusion
• Sub-proofs
• e: Proof::equals
• ea: Proof::equals_add
• eobj: Proof::obj_equals
• i: Proof::implied
• ia: Proof::implied_add
• #: Proof::set_level
• w: Proof::wipe_level
• strengthening_to_core: Proof::strengthening_to_core
• def_order
• load_order