I’m relatively new to using Coq and am currently working on verifying a stack-based virtual machine. My main goal is to ensure that illegal instructions are not generated by the compiler. To get up to speed, I’ve been familiarizing myself with the basics of Coq.
One of my objectives is to verify that the instruction executor only processes valid instructions. For instance, the ADD instruction should only execute if there are at least two elements present on the stack. However, I’ve encountered a stumbling block with the implementation of the exec function. I suspect the issue might stem from the feasibility of implementing the precondition length s > 2 for this function, as it seems this condition might not be verifiable at compile time.
I’m unsure about the best approach to ensure the correctness of such conditions or how to proceed with the implementation under these constraints. Could anyone offer guidance or advice on how to tackle this problem? Any suggestions or teaching materials would be greatly appreciated. Thank you!
1 Inductive instr' : Type :=
2 | PUSH' (s: state) (n : nat) : instr'
3 | ADD' (s : state) :
4 length s > 2 -> instr'.
5
6 Definition exec_instr' (i : instr') : state :=
7 match i with
8 | PUSH' st n => n :: st
9 | ADD' st _ =>
10 let operand2 := hd 0 st in
11 let operand1 := hd 0 (tl st) in
12 (operand1 + operand2) :: (tl (tl st))
13 end.
14
15 Fixpoint exec' (is : list instr') : state :=
16 match is with
17 | [] => []
18 | i₁ :: i₂ :: is' =>
19 let st := exec_instr' i₁ in
20 match i₂ with
21 | PUSH' _ n => exec' (PUSH' st n :: is')
22 | ADD' _ _ => exec' (ADD' st :: []) (* Assistant prompt error appears *)
23 (* | ADD' _ _ => exec' [] *) (* No error *)
24 end
25 | i₁ :: i₂ => [] (* TODO *)
26 end.
27
You are hitting a fundamental aspect of Coq: by design, all functions must terminate, and furthermore you must convince Coq it does. Coq offers general facilities to prove the termination of a function, but one usually relies directly on structural recursion: all recursive calls must be made on substructural arguments.
Concretely in your case, you have at the moment two recursive calls in exec': exec' (PUSH' st n :: is') and exec' (ADD' st :: []). For the function to be obviously terminating by virtue of structural recursion, exec' should be only called on i₂ :: is' or on is'.
So in general, you are in front of one or two cases:
Your function actually may diverge!
Your function is not structurally recursive, but terminates nonetheless.
In the second case, you could keep your function, but work a bit harder to explain it to Coq. The Program and the Equations facilities for instance would permit you in the present case to explain that the length of is decreases strictly at each call.
Other approaches may bypasse the proof of termination, and remain viable in presence of divergence.
One is to provide fuel : add a parameter fuel : nat to your function, that decreases at each call, and stops the execution if it reaches 0.
Finally maybe a more common one when it comes to semantics of languages: rather than to try to define an interpreter, you may instead specify the semantics as the transitive closure of a transition system that you specify as an inductive.
All in all, it sounds like you are starting to get familiar with the system. An introductory textbook such as Software Foundations will probably make things more palatable extremely quick!
If you want to see an example of a little stack machine formalized in Coq, Xavier Leroy’s excellent course material on verified compilation contains one here.
You can solve your immediate problem by separating (as two different parameters) the current instruction and the list of other instructions. The latter will always be is' and will be recognized as a subterm.
You less immedaite problem is that your VM is likely to be able to run non-terminating programs (should you add a jump instruction for instance). So defining its semantic with a function is not really possible except if you add a “fuel” parameter to cap the number of iterations.
Finally it is very weird from the start to have the state of your VM put inside the instructions. You should probably have it a a separate argument, which would solve your immediate problem in a cleaner way.