I want to prove that a compiler that I wrote for a toy language is correct. I defined a predicate P which relates the runtime configuration of the source toy language and the target toy assembly.
The proof is set up as proving that if the source language’s small-step relation steps from state S1 to state S2, and that P(S1,T1), where T1 is the target language’s runtime configuration, then we can find a T2 such that P(S2,T2), and T1 steps to T2 in target language.
When translating constructs like array creations and functions calls, the number of instructions of the translated code depends on the size of the array/number of function arguments. For example, the translated instructions of x = array<v1,v2,...,vn> is something like mov r1 (translated value of v1); store r2 0 r1;...;mov r1 (translated value for vn); store r2 (n-1) r1;....
When I prove other properties I would manually step through each instruction (because Coq can’t do unification and I have to manually use apply with … for arguments that Coq can’t infer). For variable length instruction sequences I can’t do the same thing, so I’m wondering what I can do.
It would be great if someone can provide some github code examples that does something similar to what I’m trying to do. The reason I mentioned lightweight is because if possible, I don’t want to use heavy libraries with many predefined tactics.
Your sequence of instructions seems to be presented as a list, but it was in fact obtained by concatenation of code fragments for each instruction, probably.
so if you have i1; i2 in the source language, i1 compiles to s1 and
i2 compiles to s2 the result of compilation is s1 ++ s2. If you execute the concatenation, you obtain a sequence of target instructions where you don’t know where the execution of i2 starts. You should formulate you theorems in such a way that i compiles to s appears in the statement, and then you can reason on the relation between executing i and s independently of the length of list s. Your proof becomes robust to the fact that compilation results are variable length.
In my own experiments, I needed to express that the executions of code s1 was sequential, in other words, if s1 ++ s2 executed from state T0 to state T2, then there exists a state T1 such that s1 executes from T0 to T1 and s2 executes from T1 to T2. and then I was able to use the structure of the source code and the fact that that the target code was obtained from compilation of the source code to reason on the execution of the target code. If s1 is the compiled result of i1 and is sequential, I can relate the state T1 (which is the result of executing s1) with the result of executing i1, and then I can proceed with i2.
Working with a language with only structured constructions (while loop, if-then-else, etc), the code produced for any fragment would always be sequential and the proof went through quite well. If you want to reason about programs where Goto statements are allowed in the source language, then I don’t have a solution at hand.
I did work with several compilers between low-level languages in Coq. By low-level, I mean that the languages have the notion of program counter (PC). Hence Goto statements are everywhere in those low-level programs.
With my co-author Yannick Forster, we presented at CPP 2019 a generic compiler with a correctness proof for such languages, that is instantiated on a compiler from Binary Stack Machines to Counter Machines (aka Minsky machines). The paper explaining the compiler can be found here:
Certified Undecidability of Intuitionistic Linear Logic
via Binary Stack Machines and Minsky Machines
The sections you would want to focus on are sections 4, 5, 6 and 7.
The correctness statement for the compiler works both for terminating and non-terminating programs. Btw one of the difficulties in these compilers is the implementations of the linker, but this is now abstracted by the correctness of the generic compiler.
In the corresponding code, we implement a framework to reason with such low-level programs in a modular/compositional way, that is derive properties of whole programs from those of their sub-programs. Section 7 explains how such reasoning works on an example.
Another example would be a FRACTRAN to counter machines compiler described in Synthetic Undecidability of MSELL via
FRACTRAN Mechanised in Coq, in section 3.
More generality, there are several low-level compilers that you can find in the Coq Library of Undecidability Proofs, between (non-exhaustive list)
- PC based Turing machines
- Binary Stack machines
- Minsky machines
- FRACTRAN
- µ-recursive programs