Struct Certified 

pub struct Certified<B, P, T> { /* private fields */ }

Explicit trust boundary for externally-certified values.

This type does not silently become Proven<P, T>. Converting from external evidence into a Karpal proof witness is unsafe, making the trust boundary visible in code review.

Implementations

impl<B, P, T> Certified<B, P, T>

pub unsafe fn assume(value: T, certificate: Certificate) -> Certified<B, P, T>

Import an externally checked value.

Safety

The caller must ensure the certificate genuinely establishes property P for value, according to backend B.

pub fn certificate(&self) -> &Certificate

pub fn value(&self) -> &T

pub fn into_inner(self) -> T

pub unsafe fn into_proven(self) -> Proven<P, T>

Convert external evidence into Proven<P, T>.

Safety

This is the explicit trust boundary: the caller accepts the imported certificate as sound.

Trait Implementations

impl<B, P, T> Debug for Certified<B, P, T>

where B: VerificationBackend, T: Debug,

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

Formats the value using the given formatter.