Miscompilation in the Cairo backend

[lukaszcz]

The following is a minimal example of a program that gets miscompiled:

module optbug;

import Stdlib.Prelude open;

type Resource :=
  mkResource@{
    logic : Field;
    label : Field;
    quantity : Field;
    data : Field;
    eph : Bool;
    nonce : Field;
    npk : Field;
    rseed : Field;
  };

type LogicResult :=
  mkResult@{
    -- nullifier of input resource or commitment of output resource
    self_resource_id : Field;
  };

poseidonHashList' : List Field -> Field
  | [] := 0
  | (h :: t) := h +  poseidonHashList' t;

{-# inline: false #-}
poseidonHash2' (x y : Field) : Field := x + y;

main
  (self_resource : Resource)
  (resource_nf_key : Field)
  (merkle_path : List (Pair Field Bool))
  : LogicResult :=

  -- Check the self_resource resource commitment:
  let
    generated_npk : Field := poseidonHash2' resource_nf_key 0;

    is_output_resource :=
      case merkle_path of
        -- merkle_path can not be empty
        | nil := true
        | (_, is_left) :: t := is_left;

    actual_npk :=
      if
        | is_output_resource := Resource.npk self_resource
        | else := generated_npk;

    resource_cm :=
      poseidonHashList'
        [
          actual_npk;
          Resource.nonce self_resource;
          Resource.quantity self_resource;
        ];

    -- Generate the nullifier of self_resource resource
    resource_nullifier_ :=
      poseidonHashList'
        [
          resource_nf_key;
          resource_cm;
        ];
  in mkResult@{
       self_resource_id := resource_nullifier_;
     };

The problem is with the translation from JuvixReg to CASM. One sees that the generated CASM code is incorrect (inconsistent order of arguments passed to the next basic block in br branches). The JuvixReg code is still correct.

Related issue: anoma/aarm-cairo#37