Enum MemorySafetyProof 

pub enum MemorySafetyProof {
    AllocProof {
        viewtype: String,
    },
    FreeProof {
        ptr_id: String,
    },
    BorrowProof {
        ptr_id: String,
        mutable: bool,
    },
    BoundsProof {
        buffer_id: String,
        index_expr: String,
    },
    NullCheckProof {
        ptr_id: String,
    },
}

A compile-time proof that a memory operation is safe.

ATS2 requires explicit proof terms for memory operations. Each proof corresponds to a specific safety property:

• AllocProof: the allocation succeeded (non-null for non-nullable types)
• FreeProof: the pointer is valid and owned, so freeing is safe
• BorrowProof: the pointer is valid for the duration of the borrow
• BoundsProof: array index is within the allocated bounds
• NullCheckProof: a nullable pointer has been checked for NULL

Variants

AllocProof

Proves that an allocation returned a valid (non-null) pointer.

Fields

viewtype: String

The viewtype of the allocated resource.

FreeProof

Proves that a pointer is valid and owned, permitting deallocation.

Fields

ptr_id: String

The linear pointer being freed.

BorrowProof

Proves that a borrowed pointer remains valid for the borrow’s scope.

Fields

ptr_id: String

The linear pointer being borrowed.

mutable: bool

Whether the borrow is read-only or read-write.

BoundsProof

Proves that an index is within the bounds of a sized buffer.

Fields

buffer_id: String

The buffer being indexed.

index_expr: String

The index expression.

NullCheckProof

Proves that a nullable pointer has been checked for NULL.

Fields

ptr_id: String

The nullable pointer that was checked.

Implementations

impl MemorySafetyProof

pub fn to_ats2_proof(&self) -> String

Generates the ATS2 proof term string for this proof.

Trait Implementations

impl Clone for MemorySafetyProof

fn clone(&self) -> MemorySafetyProof

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for MemorySafetyProof

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for MemorySafetyProof

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for MemorySafetyProof

fn eq(&self, other: &MemorySafetyProof) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for MemorySafetyProof

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for MemorySafetyProof

impl StructuralPartialEq for MemorySafetyProof