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