pyk.proof.proof module

class CompositeSummary(_summaries: 'Iterable[ProofSummary]')[source]

Bases: ProofSummary

property lines: list[str]
summaries: tuple[ProofSummary, ...]
class FailureInfo[source]

Bases: object

class Proof(id: str, proof_dir: Path | None = None, subproof_ids: Iterable[str] = (), admitted: bool = False)[source]

Bases: ABC

add_subproof(proof: Proof) → None[source]
admit() → None[source]
admitted: bool
abstract property can_progress: bool
abstract commit(result: StepResult) → None[source]
property dict: dict[str, Any]
property digest: str
property failed: bool
failure_info: FailureInfo | None
fetch_subproof(proof_id: str, force_reread: bool = False, uptodate_check_method: str = 'timestamp') → Proof[source]

Get a subproof, re-reading from disk if it’s not up-to-date

fetch_subproof_data(proof_id: str, force_reread: bool = False, uptodate_check_method: str = 'timestamp') → Proof[source]

Get a subproof, re-reading from disk if it’s not up-to-date

abstract classmethod from_dict(dct: Mapping[str, Any], proof_dir: Path | None = None) → Proof[source]
id: str
property json: str
abstract property own_status: ProofStatus
property passed: bool
static proof_data_exists(id: str, proof_dir: Path) → bool[source]
proof_dir: Path | None
static proof_exists(id: str, proof_dir: Path) → bool[source]
property proof_subdir: Path | None
classmethod read_proof(id: str, proof_dir: Path) → Proof[source]
static read_proof_data(proof_dir: Path, id: str) → Proof[source]
read_subproof(proof_id: str) → None[source]
read_subproof_data(proof_id: str) → None[source]
remove_subproof(proof_id: str) → None[source]
property status: ProofStatus
property subproof_ids: list[str]
property subproofs: Iterable[Proof]

Return the subproofs, re-reading from disk the ones that changed

property subproofs_status: ProofStatus
property summary: ProofSummary
property up_to_date: bool

Check that the proof’s representation on disk is up-to-date.

write_proof(subproofs: bool = False) → None[source]
abstract write_proof_data() → None[source]
class ProofStatus(value)[source]

Bases: Enum

An enumeration.

FAILED = 'failed'
PASSED = 'passed'
PENDING = 'pending'
class ProofSummary[source]

Bases: ABC

id: str
abstract property lines: list[str]
status: ProofStatus
class Prover(kcfg_explore: KCFGExplore)[source]

Bases: object

advance_proof(max_iterations: int | None = None, fail_fast: bool = False) → None[source]
abstract failure_info() → FailureInfo[source]
kcfg_explore: KCFGExplore
proof: Proof
abstract step_proof() → Iterable[StepResult][source]
class StepResult[source]

Bases: object