Memory Model

This file defines the memory model.

Main Definitions

• Address - Memory addresses (64-bit)
• Memory - Memory state (functional map from addresses to bytes)
• read_mem_bytes - Read multiple bytes from memory
• write_mem_bytes - Write multiple bytes to memory
• read_word64 - Read a 64-bit word from memory (little-endian)
• write_word64 - Write a 64-bit word to memory (little-endian)

References

This corresponds to the memory component in HOL Light's model. Source: s2n-bignum/common/components.ml (memory-related definitions)

@[reducible, inline]

abbrev Bignum.Address : Type

Memory addresses are 64-bit values.

Equations

• Bignum.Address = Bignum.Word64

def Bignum.Memory : Type

Memory is modeled as a partial function from addresses to bytes. We use Option to represent potentially uninitialized memory.

Equations

• Bignum.Memory = (Bignum.Address → Option UInt8)

def Bignum.Memory.empty : Memory

Empty memory (all addresses uninitialized).

Equations

• Bignum.Memory.empty x✝ = none

def Bignum.Memory.read_byte (mem : Memory) (addr : Address) : Option UInt8

Read a single byte from memory at the given address.

Equations

• mem.read_byte addr = mem addr

def Bignum.Memory.write_byte (mem : Memory) (addr : Address) (byte : UInt8) : Memory

Write a single byte to memory at the given address.

Equations

• mem.write_byte addr byte a = if a = addr then some byte else mem a

def Bignum.Memory.read_bytes (mem : Memory) (addr : Address) (n : ℕ) : Option (List UInt8)

Read n bytes from memory starting at addr. Returns None if any byte is uninitialized.

Equations

• mem.read_bytes addr n = Bignum.Memory.read_bytes.aux mem addr n n []

@[irreducible]

def Bignum.Memory.read_bytes.aux (mem : Memory) (addr : Address) (n i : ℕ) (acc : List UInt8) : Option (List UInt8)

Equations

• One or more equations did not get rendered due to their size.

def Bignum.Memory.write_bytes (mem : Memory) (addr : Address) (bytes : List UInt8) : Memory

Write bytes to memory starting at addr.

Equations

• One or more equations did not get rendered due to their size.

def Bignum.Memory.read_word64 (mem : Memory) (addr : Address) : Option Word64

Read a 64-bit word from memory in little-endian format. The address should be the lowest byte address.

Equations

• One or more equations did not get rendered due to their size.

def Bignum.Memory.write_word64 (mem : Memory) (addr : Address) (w : Word64) : Memory

Write a 64-bit word to memory in little-endian format.

Equations

• mem.write_word64 addr w = mem.write_bytes addr (List.map (fun (i : ℕ) => UInt8.ofNat (w.val / 2 ^ (8 * i) % 256)) (List.range 8))

def Bignum.Memory.read_bignum (mem : Memory) (addr : Address) (n : ℕ) : Option ℕ

Read a bignum (multiple 64-bit words) from memory. The bignum is stored as an array of n words at address addr.

Corresponds to HOL Light's bignum_from_memory. Source: s2n-bignum proofs use this extensively (e.g., bignum_add.ml:91-92)

Equations

• mem.read_bignum addr n = Bignum.Memory.read_bignum.aux mem addr n n 0

@[irreducible]

def Bignum.Memory.read_bignum.aux (mem : Memory) (addr : Address) (n i acc : ℕ) : Option ℕ

Equations

• One or more equations did not get rendered due to their size.

def Bignum.Memory.write_bignum (mem : Memory) (addr : Address) (n val : ℕ) : Memory

Write a bignum to memory as n 64-bit words.

Equations

• One or more equations did not get rendered due to their size.

def Bignum.nonoverlapping (addr1 : Address) (size1 : ℕ) (addr2 : Address) (size2 : ℕ) : Prop

Check if two memory regions do not overlap. This corresponds to HOL Light's nonoverlapping, used extensively in preconditions.

Source: s2n-bignum/common/overlap.ml

Equations

• Bignum.nonoverlapping addr1 size1 addr2 size2 = (Bignum.Word64.val addr1 + size1 ≤ Bignum.Word64.val addr2 ∨ Bignum.Word64.val addr2 + size2 ≤ Bignum.Word64.val addr1)

def Bignum.bytes_loaded (mem : Memory) (addr : Address) (bytes : List UInt8) : Prop

Bytes are loaded at a given address (no alignment requirement).

Equations

• Bignum.bytes_loaded mem addr bytes = ∀ (i : ℕ) (h : i < bytes.length), mem.read_byte (addr + Bignum.Word64.ofNat i) = some bytes[i]

def Bignum.aligned_bytes_loaded (mem : Memory) (addr : Address) (bytes : List UInt8) : Prop

Bytes are loaded and aligned at a given address. Corresponds to HOL Light's aligned_bytes_loaded.

Equations

• Bignum.aligned_bytes_loaded mem addr bytes = (Bignum.Word64.val addr % 4 = 0 ∧ Bignum.bytes_loaded mem addr bytes)

theorem Bignum.aligned_bytes_loaded_implies_bytes_loaded (mem : Memory) (addr : Address) (bytes : List UInt8) : aligned_bytes_loaded mem addr bytes → bytes_loaded mem addr bytes

Aligned bytes loaded implies bytes loaded.