I am trying to write simple program on ASM (a simple control-flow-graph language) from this tutorial: InteractionTrees -> ASM.v
My final goal is to prove its correctness, using the library's capabilities
Function I am trying to write:
If current_i (which is 42) is less or equal to val (function parameter) - we return current_i, i.e. 42 else we return current_i + 1, so we return 43
registers we will use: 2 - current_i ; 3 - i_leq_val
this is pseudo code below, it contains labels, instructions and jumps:
function asm_forty_two (val : operand) { (* val is parameter *)
0 : (* entry label 0 *)
Istore ("current_i") (Oimm 42) (* %current_i = 42 *)
Bjmp 1 (* jump to label 1 *)
1 : (* internal label 1 *)
Iload 2 current_i (* we load current_i into register #2 *)
ILe 3 2 val (* we load into register #3 result of comparison
of current_i (which is in register 2 and val) *)
Bbrz 3 3 2 (* if in register 3 we have 1 - go to label 3 else
go to label 2 *)
2 : (* internal label 2 *)
Iadd 2 2 (Oimm 1) (* we add 1 to current_i (which is in register #2)
and put it back into register #2 *)
Bjmp 3 (* jump to label 3 *)
3 : (* exit point 3 *)
Bhalt (* return current_i which is 42 or 43 (depends on val)
}
Now I am defining asm (which is record). Is it correct that the type is asm 1 1 , since we have 1 entry point and one exit point?
This code below I am trying to compile inside the library in file ASM.v
Definition asm_forty_two (val : operand) : asm 1 1 :=
{|
internal := 2;
(* in our case fina = 3 : one entry point and 2 internal points *)
code := fun fina => match fina with
| (exist _ 0 _) =>
bbi (Istore ("current_i"%string) (Oimm 42))
(bbb (Bjmp ((exist (fun j : nat => (j < 1 + 1)) 1 _))))
| (exist _ 1 _) => bbi (Iload 2 "current_i"%string)
(bbi (ILe 3 2 val)
(bbb (Bbrz 3
(exist (fun j : nat => _) 3 _)
(exist (fun j : nat => _) 2 _)
)))
| (exist _ 2 _) => bbi (Iadd 2 2 (Oimm 1))
(bbb (Bjmp (exist (fun j : nat => _) 3 _)))
| (exist _ 3 _) => bbb Bhalt
end
|}.
But it wouldn't compile... "non-exhaustive pattern matching" or "unresolved implicit arguments"...
Can I have example of such simple function on ASM, which compiles? Labels should start from 0? How to use fi' notation here?
The exhaustiveness checker for match is really basic. It does not make use of the fact that the nat field is bounded. The simplest solution is to make the last clause a catch-all clause. (Convincing Coq that the remaining branches are not reachable is tedious and unnecessary. And using the Equations library would be better than match if you really wanted to do that.)
There is no output label (your label 3 is internal) and there are 3 internal labels. So the type is asm 1 0. And the inequality proofs in output jumps should be j < 3.
Internal labels are numbered first, then external labels. This is implicit in the definition of asm, in the ordering of operands internal + A and internal + B.
Record asm (A B: nat) : Type :=
{
internal : nat;
code : bks (internal + A) (internal + B)
}.
In your asm code, the entry label 0 is external, while the labels 1,2,3 are internal, so the indices are shifted.
ASM labels | Coq labels
0 | 3 (external)
1 | 0 (internal)
2 | 1 (internal)
3 | 2 (internal)
Since all the labels are literals, the inequality proofs j < 3 can be solved using the tactic simpl; auto. You can use the notation ltac:(simpl; auto) in place of the proof terms of type 0 < 3, 1 < 3, 2 < 3. Also make sure to fill out any holes in the first argument of exist to make those types explicit (otherwise simpl; auto will have an unknown goal).
Definition asm_forty_two (val : operand) : asm 1 0 :=
{|
internal := 3;
code := fun fina => match fina with
| (exist _ 0 _) => bbi (Iload 2 "current_i"%string)
(bbi (ILe 3 2 val)
(bbb (Bbrz 3
(exist (fun j : nat => j < 3) 2 ltac:(simpl; auto))
(exist (fun j : nat => j < 3) 1 ltac:(simpl; auto))
)))
| (exist _ 1 _) => bbi (Iadd 2 2 (Oimm 1))
(bbb (Bjmp (exist (fun j : nat => j < 3) 2 ltac:(simpl; auto))))
| (exist _ 2 _) => bbb Bhalt
| (exist _ _ _) =>
bbi (Istore ("current_i"%string) (Oimm 42))
(bbb (Bjmp ((exist (fun j : nat => (j < 3)) 0 ltac:(simpl; auto)))))
end
|}.