|
|
|---|
|
|
|
|---|
J S. Moore, Piton: A Mechanically Verified Assembly-Level Language,
J S. Moore, Automated Reasoning Series, Kluwer Academic Publishers, 1996.
Relevance: verified assembler/linker/loader and a
component of the CLI Verified Stack
The verified
assembler/linker/loader in the final version of the CLI Stack (see bib::bhmy89) is described here. See also the 1991 Nqthm script
Of particular interest to users who wish to verify the correct implementation of one programming language on top of a state machine is decomposition of the main theorem into “commuting diagrams” that stack various layers of abstraction between the assembly language and the binary image. Among other things these layers of abstraction solve the problem of “hidden resources,” in which the lower level machine state has resources that are not reflected in the upper level. For example at the high level, if one pushes items on the high level stack and then pops them off, there is no change to the stack when viewed from the high level. But the low level machine still records, in the region of memory dedicated to the stack but beyond the current top of stack, the items last pushed. Furthermore, those residual values can be accessed by the low level machine. So one has to prove that they are not. The Piton proof dealt with this by imposing an intermediate abstract machine just above the low level machine but with an instruction set in which it is impossible to access beyond the top of stack.