lambda-mountain
lambda-mountain copied to clipboard
andrew-johnson-4
Compact Typed Assembler (5K SLOC)
Preconditions can attach to labels. Postconditions can be unified from all possible branches.
The verifier in Coq could utilize direct definitions provided by Intel. https://www.felixcloutier.com/x86/pop ``` IF StackAddrSize = 32 THEN IF OperandSize = 32 THEN DEST := SS:ESP; (* Copy a doubleword...
LM doesn't deserve trust yet. It would be nice to have an option to verify all asserted properties. This would dovetail nicely with the LSTS Frontend too.
Comparison fragments could be a boolean value or a brach conditional depending on context. ``` if (
Current Breakdown | phase | phase time | cumulative | |--------|--------------|------------| | tokenize | 0.000s | 0.000s | | parse | 0.156s | 0.156s | | preprocess | 0.750s |...
`Verify` fragments and functions are required to prove all properties that they declare or depend on. `Verify` dependencies must also be either `Verify` or `NoVerify`. A compiler flag could be...
Old local variables can be reused for new data if their lifetime is over.
Eventually it would be nice to bundle library definitions and other addons to create specialized compilers. So there could be a "lm-python" compiler that is drop-in compatible with that functionality.