Given
CONSTANTS MemLength, MemWidth
VARIABLE mem
Where MemLength is the largest index possible in the memory, MemWidth is the number of bits at each location, and mem is the current memory state, you can define:
Memory == [0 .. (MemLength - 1) -> [0 .. (MemWidth - 1) -> {0, 1}]]
Init == mem = [0 .. (MemLength - 1) |-> [0 .. (MemWidth - 1) |-> 0]]
TypeInvariant == mem \in Memory
It's a good idea to parameterize this with constants because you can probably do the math to figure out the Memory set is absolutely enormous, on the order of 2^(MemLength * MemWidth). So you'd probably want to top out at 3 x 4 or something at most.
You can read a specific bit by double-indexing, like
mem[2][7]
And you can update a bit like
Next == mem' = [mem EXCEPT ![2][7] = 1]
Andrew