Struct ProofCarryingCode 

pub struct ProofCarryingCode { /* private fields */ }

Proof-carrying code certificate

This combines code with proofs of its safety properties.

Implementations

impl ProofCarryingCode

pub fn new(code: impl Into<String>) -> Self

Create a new proof-carrying code certificate

pub fn add_property(&mut self, property: SafetyProperty)

Add a safety property to be verified

pub fn add_vc(&mut self, vc: VerificationCondition)

Add a verification condition

pub fn attach_proof(&mut self, vc_id: &str, proof_node: ProofNodeId)

Attach a proof for a verification condition

pub fn proof(&self) -> &Proof

Get the underlying proof structure

pub fn proof_mut(&mut self) -> &mut Proof

Get a mutable reference to the proof

pub fn code(&self) -> &str

Get the code

pub fn properties(&self) -> &[SafetyProperty]

Get the certified properties

pub fn verification_conditions(&self) -> &[VerificationCondition]

Get the verification conditions

pub fn is_complete(&self) -> bool

Check if all VCs have proofs

pub fn verified_count(&self) -> usize

Get the number of verified VCs

pub fn total_vc_count(&self) -> usize

Get the total number of VCs

pub fn to_certificate(&self) -> String

Generate a human-readable certificate

Trait Implementations

impl Debug for ProofCarryingCode

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

Formats the value using the given formatter.