Lambda Mountain (LM) is a small portable assembler, suitable for embedded AOT or JIT compilation. In the most recent development push we are hoping to formally model and prove correctness of a large subset of the language.
Starting With The Memory Model
To start with modelling the actual computer we will eventually model individual instructions. However, many instructions modify or depend on the register and memory state of the computer, so we will start with that.
Require Import Coq.Numbers.BinNums.
(* Memory Is Denominated in Bytes *)
Structure RegionByte := {
tt : N; (* The type of this region represented as an Ordinal *)
tt_byte : N; (* The type-byte-index of this byte *)
}.
(* Knowledge of a Memory Region is a Partial Function *)
Structure Region := {
known : Z -> RegionByte;
}.
(* Simplified Memory State assumes that
1. stack space is sufficient (effectively infinite)
2. sys_brk always succeeds at acquiring more memory (effectively infinite)
*)
Structure MemoryState := {
register_state : Region;
stack_state : Region;
frame_state : Region;
heap_state : Region;
}.This short snippet is all we need to declare our simplified memory model. In this model we assume that stack and heap space are infinite. We do this because it would be impossible to specifically predict when an overflow would happen due to possible branches in code. However, we still want to prove local correctness so we assume that memory is not an issue.
We define three terms here. First each byte of memory can be typed with a RegionByte. Next, we break memory into Regions that carry partial information about what is stored there. Finally, our memory model is broken into four sections for registers, stack relative data, frame relative data, and heap data.
Conclusion
We will separately prove some additional assumptions such as not overwriting frame data with stack data. However, this is basically as complicated as our typed memory model will get. See, formalism doesn’t have to be scary!
