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?