Proof fields

Fields may use anonymous types, either to be robust and/or unsafe. This usually encodes the invariant of the struct (or more generally any custom type). Writing to those fields require to update the proof too. More generally, modifying anything that the predicate relies on, requires to update the proof.

/// Vectors of at most 1024 bytes.
pub struct Vec1024 {
    /// Storage of the vector.
    ///
    /// # Robustness
    ///
    /// Points to an allocation of 1024 bytes and is owned.
    ptr: Update<*mut u8>,

    /// Length of the vector.
    ///
    /// # Robustness
    ///
    /// - Always smaller than or equal to 1024.
    /// - The storage prefix of that length is initialized.
    len: Update<usize>,
}

impl Vec1024 {
    pub fn push(&mut self, x: u8) {
        assert!(self.len < 1024);

        // SAFETY: The addition stays within the allocation by the check above.
        // The write is thus also valid.
        unsafe { self.ptr.add(self.len).write(x) };

        // SAFETY: The new length is safe because:
        // - The old length was smaller than 1024 by the check above and only 1
        //   is added, it is thus smaller than or equal to 1024.
        // - The pointed prefix is initialized because it was initialized up to
        //   the last byte and we just wrote the last byte.
        unsafe { self.len += 1 };
    }
}

It is sometimes more convenient to have a single proof field to gather all invariants. One needs to prove the invariant is preserved each time a field (or something else) referred by the predicate is modified.

/// Vectors of at most 1024 bytes.
pub struct Vec1024 {
    ptr: *mut u8,
    len: usize,

    /// Invariant.
    ///
    /// # Robustness
    ///
    /// - The pointer points to an allocation of 1024 bytes and is owned.
    /// - The length is always smaller than or equal to 1024.
    /// - The pointed prefix of size length is initialized.
    inv: Proof,
}

impl Vec1024 {
    pub fn push(&mut self, x: u8) {
        assert!(self.len < 1024);

        // SAFETY: The invariant is trivially preserved (neither the pointer nor
        // the length have been modified). The addition stays within the
        // allocation by the check above. The write is thus also valid.
        unsafe { self.ptr.add(self.len).write(x) };

        // SAFETY: The invariant is preserved:
        // - The length is smaller than or equal to 1024 because it was smaller
        //   than 1024 and only 1 is added.
        // - The pointed prefix is initialized because it was initialized up to
        //   the last byte before and we just wrote the last byte.
        unsafe { self.len += 1 };
    }
}