abicoder.ML

structure ABICoder : sig
  type int
  type 'a word
  type abi_type
  type 'a bit0
  type num1
  type char
  type ('a, 'b) sum
  type abi_value
  val decode :
    abi_type -> num1 bit0 bit0 bit0 word list -> (abi_value, (char list)) sum
  val encode : abi_value -> ((num1 bit0 bit0 bit0 word list), (char list)) sum
end = struct

datatype num = One | Bit0 of num | Bit1 of num;

datatype int = Zero_int | Pos of num | Neg of num;

val one_inta : int = Pos One;

type 'a one = {one : 'a};
val one = #one : 'a one -> 'a;

val one_int = {one = one_inta} : int one;

fun plus_num (Bit1 m) (Bit1 n) = Bit0 (plus_num (plus_num m n) One)
  | plus_num (Bit1 m) (Bit0 n) = Bit1 (plus_num m n)
  | plus_num (Bit1 m) One = Bit0 (plus_num m One)
  | plus_num (Bit0 m) (Bit1 n) = Bit1 (plus_num m n)
  | plus_num (Bit0 m) (Bit0 n) = Bit0 (plus_num m n)
  | plus_num (Bit0 m) One = Bit1 m
  | plus_num One (Bit1 n) = Bit0 (plus_num n One)
  | plus_num One (Bit0 n) = Bit1 n
  | plus_num One One = Bit0 One;

fun uminus_int (Neg m) = Pos m
  | uminus_int (Pos m) = Neg m
  | uminus_int Zero_int = Zero_int;

fun bitM One = One
  | bitM (Bit0 n) = Bit1 (bitM n)
  | bitM (Bit1 n) = Bit1 (Bit0 n);

fun dup (Neg n) = Neg (Bit0 n)
  | dup (Pos n) = Pos (Bit0 n)
  | dup Zero_int = Zero_int;

fun plus_inta (Neg m) (Neg n) = Neg (plus_num m n)
  | plus_inta (Neg m) (Pos n) = sub n m
  | plus_inta (Pos m) (Neg n) = sub m n
  | plus_inta (Pos m) (Pos n) = Pos (plus_num m n)
  | plus_inta Zero_int l = l
  | plus_inta k Zero_int = k
and sub (Bit0 m) (Bit1 n) = minus_int (dup (sub m n)) one_inta
  | sub (Bit1 m) (Bit0 n) = plus_inta (dup (sub m n)) one_inta
  | sub (Bit1 m) (Bit1 n) = dup (sub m n)
  | sub (Bit0 m) (Bit0 n) = dup (sub m n)
  | sub One (Bit1 n) = Neg (Bit0 n)
  | sub One (Bit0 n) = Neg (bitM n)
  | sub (Bit1 m) One = Pos (Bit0 m)
  | sub (Bit0 m) One = Pos (bitM m)
  | sub One One = Zero_int
and minus_int (Neg m) (Neg n) = sub n m
  | minus_int (Neg m) (Pos n) = Neg (plus_num m n)
  | minus_int (Pos m) (Neg n) = Pos (plus_num m n)
  | minus_int (Pos m) (Pos n) = sub m n
  | minus_int Zero_int l = uminus_int l
  | minus_int k Zero_int = k;

type 'a plus = {plus : 'a -> 'a -> 'a};
val plus = #plus : 'a plus -> 'a -> 'a -> 'a;

val plus_int = {plus = plus_inta} : int plus;

type 'a zero = {zero : 'a};
val zero = #zero : 'a zero -> 'a;

val zero_int = {zero = Zero_int} : int zero;

type 'a semigroup_add = {plus_semigroup_add : 'a plus};
val plus_semigroup_add = #plus_semigroup_add : 'a semigroup_add -> 'a plus;

type 'a numeral =
  {one_numeral : 'a one, semigroup_add_numeral : 'a semigroup_add};
val one_numeral = #one_numeral : 'a numeral -> 'a one;
val semigroup_add_numeral = #semigroup_add_numeral :
  'a numeral -> 'a semigroup_add;

val semigroup_add_int = {plus_semigroup_add = plus_int} : int semigroup_add;

val numeral_int =
  {one_numeral = one_int, semigroup_add_numeral = semigroup_add_int} :
  int numeral;

fun times_num (Bit1 m) (Bit1 n) =
  Bit1 (plus_num (plus_num m n) (Bit0 (times_num m n)))
  | times_num (Bit1 m) (Bit0 n) = Bit0 (times_num (Bit1 m) n)
  | times_num (Bit0 m) (Bit1 n) = Bit0 (times_num m (Bit1 n))
  | times_num (Bit0 m) (Bit0 n) = Bit0 (Bit0 (times_num m n))
  | times_num One n = n
  | times_num m One = m;

fun times_inta (Neg m) (Neg n) = Pos (times_num m n)
  | times_inta (Neg m) (Pos n) = Neg (times_num m n)
  | times_inta (Pos m) (Neg n) = Neg (times_num m n)
  | times_inta (Pos m) (Pos n) = Pos (times_num m n)
  | times_inta Zero_int l = Zero_int
  | times_inta k Zero_int = Zero_int;

type 'a times = {times : 'a -> 'a -> 'a};
val times = #times : 'a times -> 'a -> 'a -> 'a;

type 'a power = {one_power : 'a one, times_power : 'a times};
val one_power = #one_power : 'a power -> 'a one;
val times_power = #times_power : 'a power -> 'a times;

val times_int = {times = times_inta} : int times;

val power_int = {one_power = one_int, times_power = times_int} : int power;

type 'a ab_semigroup_add = {semigroup_add_ab_semigroup_add : 'a semigroup_add};
val semigroup_add_ab_semigroup_add = #semigroup_add_ab_semigroup_add :
  'a ab_semigroup_add -> 'a semigroup_add;

type 'a semigroup_mult = {times_semigroup_mult : 'a times};
val times_semigroup_mult = #times_semigroup_mult :
  'a semigroup_mult -> 'a times;

type 'a semiring =
  {ab_semigroup_add_semiring : 'a ab_semigroup_add,
    semigroup_mult_semiring : 'a semigroup_mult};
val ab_semigroup_add_semiring = #ab_semigroup_add_semiring :
  'a semiring -> 'a ab_semigroup_add;
val semigroup_mult_semiring = #semigroup_mult_semiring :
  'a semiring -> 'a semigroup_mult;

val ab_semigroup_add_int = {semigroup_add_ab_semigroup_add = semigroup_add_int}
  : int ab_semigroup_add;

val semigroup_mult_int = {times_semigroup_mult = times_int} :
  int semigroup_mult;

val semiring_int =
  {ab_semigroup_add_semiring = ab_semigroup_add_int,
    semigroup_mult_semiring = semigroup_mult_int}
  : int semiring;

type 'a mult_zero = {times_mult_zero : 'a times, zero_mult_zero : 'a zero};
val times_mult_zero = #times_mult_zero : 'a mult_zero -> 'a times;
val zero_mult_zero = #zero_mult_zero : 'a mult_zero -> 'a zero;

val mult_zero_int = {times_mult_zero = times_int, zero_mult_zero = zero_int} :
  int mult_zero;

type 'a monoid_add =
  {semigroup_add_monoid_add : 'a semigroup_add, zero_monoid_add : 'a zero};
val semigroup_add_monoid_add = #semigroup_add_monoid_add :
  'a monoid_add -> 'a semigroup_add;
val zero_monoid_add = #zero_monoid_add : 'a monoid_add -> 'a zero;

type 'a comm_monoid_add =
  {ab_semigroup_add_comm_monoid_add : 'a ab_semigroup_add,
    monoid_add_comm_monoid_add : 'a monoid_add};
val ab_semigroup_add_comm_monoid_add = #ab_semigroup_add_comm_monoid_add :
  'a comm_monoid_add -> 'a ab_semigroup_add;
val monoid_add_comm_monoid_add = #monoid_add_comm_monoid_add :
  'a comm_monoid_add -> 'a monoid_add;

type 'a semiring_0 =
  {comm_monoid_add_semiring_0 : 'a comm_monoid_add,
    mult_zero_semiring_0 : 'a mult_zero, semiring_semiring_0 : 'a semiring};
val comm_monoid_add_semiring_0 = #comm_monoid_add_semiring_0 :
  'a semiring_0 -> 'a comm_monoid_add;
val mult_zero_semiring_0 = #mult_zero_semiring_0 :
  'a semiring_0 -> 'a mult_zero;
val semiring_semiring_0 = #semiring_semiring_0 : 'a semiring_0 -> 'a semiring;

val monoid_add_int =
  {semigroup_add_monoid_add = semigroup_add_int, zero_monoid_add = zero_int} :
  int monoid_add;

val comm_monoid_add_int =
  {ab_semigroup_add_comm_monoid_add = ab_semigroup_add_int,
    monoid_add_comm_monoid_add = monoid_add_int}
  : int comm_monoid_add;

val semiring_0_int =
  {comm_monoid_add_semiring_0 = comm_monoid_add_int,
    mult_zero_semiring_0 = mult_zero_int, semiring_semiring_0 = semiring_int}
  : int semiring_0;

type 'a monoid_mult =
  {semigroup_mult_monoid_mult : 'a semigroup_mult,
    power_monoid_mult : 'a power};
val semigroup_mult_monoid_mult = #semigroup_mult_monoid_mult :
  'a monoid_mult -> 'a semigroup_mult;
val power_monoid_mult = #power_monoid_mult : 'a monoid_mult -> 'a power;

type 'a semiring_numeral =
  {monoid_mult_semiring_numeral : 'a monoid_mult,
    numeral_semiring_numeral : 'a numeral,
    semiring_semiring_numeral : 'a semiring};
val monoid_mult_semiring_numeral = #monoid_mult_semiring_numeral :
  'a semiring_numeral -> 'a monoid_mult;
val numeral_semiring_numeral = #numeral_semiring_numeral :
  'a semiring_numeral -> 'a numeral;
val semiring_semiring_numeral = #semiring_semiring_numeral :
  'a semiring_numeral -> 'a semiring;

type 'a zero_neq_one = {one_zero_neq_one : 'a one, zero_zero_neq_one : 'a zero};
val one_zero_neq_one = #one_zero_neq_one : 'a zero_neq_one -> 'a one;
val zero_zero_neq_one = #zero_zero_neq_one : 'a zero_neq_one -> 'a zero;

type 'a semiring_1 =
  {semiring_numeral_semiring_1 : 'a semiring_numeral,
    semiring_0_semiring_1 : 'a semiring_0,
    zero_neq_one_semiring_1 : 'a zero_neq_one};
val semiring_numeral_semiring_1 = #semiring_numeral_semiring_1 :
  'a semiring_1 -> 'a semiring_numeral;
val semiring_0_semiring_1 = #semiring_0_semiring_1 :
  'a semiring_1 -> 'a semiring_0;
val zero_neq_one_semiring_1 = #zero_neq_one_semiring_1 :
  'a semiring_1 -> 'a zero_neq_one;

val monoid_mult_int =
  {semigroup_mult_monoid_mult = semigroup_mult_int,
    power_monoid_mult = power_int}
  : int monoid_mult;

val semiring_numeral_int =
  {monoid_mult_semiring_numeral = monoid_mult_int,
    numeral_semiring_numeral = numeral_int,
    semiring_semiring_numeral = semiring_int}
  : int semiring_numeral;

val zero_neq_one_int =
  {one_zero_neq_one = one_int, zero_zero_neq_one = zero_int} : int zero_neq_one;

val semiring_1_int =
  {semiring_numeral_semiring_1 = semiring_numeral_int,
    semiring_0_semiring_1 = semiring_0_int,
    zero_neq_one_semiring_1 = zero_neq_one_int}
  : int semiring_1;

datatype rat = Frct of (int * int);

val one_rata : rat = Frct (one_inta, one_inta);

val one_rat = {one = one_rata} : rat one;

fun quotient_of (Frct x) = x;

fun less_eq_num (Bit1 m) (Bit0 n) = less_num m n
  | less_eq_num (Bit1 m) (Bit1 n) = less_eq_num m n
  | less_eq_num (Bit0 m) (Bit1 n) = less_eq_num m n
  | less_eq_num (Bit0 m) (Bit0 n) = less_eq_num m n
  | less_eq_num (Bit1 m) One = false
  | less_eq_num (Bit0 m) One = false
  | less_eq_num One n = true
and less_num (Bit1 m) (Bit0 n) = less_num m n
  | less_num (Bit1 m) (Bit1 n) = less_num m n
  | less_num (Bit0 m) (Bit1 n) = less_eq_num m n
  | less_num (Bit0 m) (Bit0 n) = less_num m n
  | less_num One (Bit1 n) = true
  | less_num One (Bit0 n) = true
  | less_num m One = false;

fun less_eq_int (Neg k) (Neg l) = less_eq_num l k
  | less_eq_int (Neg k) (Pos l) = true
  | less_eq_int (Neg k) Zero_int = true
  | less_eq_int (Pos k) (Neg l) = false
  | less_eq_int (Pos k) (Pos l) = less_eq_num k l
  | less_eq_int (Pos k) Zero_int = false
  | less_eq_int Zero_int (Neg l) = false
  | less_eq_int Zero_int (Pos l) = true
  | less_eq_int Zero_int Zero_int = true;

fun divmod_step_int l (q, r) =
  (if less_eq_int (Pos l) r
    then (plus_inta (times_inta (Pos (Bit0 One)) q) one_inta,
           minus_int r (Pos l))
    else (times_inta (Pos (Bit0 One)) q, r));

fun divmod_int (Bit1 m) (Bit1 n) =
  (if less_num m n then (Zero_int, Pos (Bit1 m))
    else divmod_step_int (Bit1 n) (divmod_int (Bit1 m) (Bit0 (Bit1 n))))
  | divmod_int (Bit0 m) (Bit1 n) =
    (if less_eq_num m n then (Zero_int, Pos (Bit0 m))
      else divmod_step_int (Bit1 n) (divmod_int (Bit0 m) (Bit0 (Bit1 n))))
  | divmod_int (Bit1 m) (Bit0 n) =
    let
      val (q, r) = divmod_int m n;
    in
      (q, plus_inta (times_inta (Pos (Bit0 One)) r) one_inta)
    end
  | divmod_int (Bit0 m) (Bit0 n) = let
                                     val (q, r) = divmod_int m n;
                                   in
                                     (q, times_inta (Pos (Bit0 One)) r)
                                   end
  | divmod_int One (Bit1 n) = (Zero_int, Pos One)
  | divmod_int One (Bit0 n) = (Zero_int, Pos One)
  | divmod_int (Bit1 m) One = (Pos (Bit1 m), Zero_int)
  | divmod_int (Bit0 m) One = (Pos (Bit0 m), Zero_int)
  | divmod_int One One = (Pos One, Zero_int);

fun fst (x1, x2) = x1;

fun of_bool A_ true = one (one_zero_neq_one A_)
  | of_bool A_ false = zero (zero_zero_neq_one A_);

fun equal_num (Bit0 x2) (Bit1 x3) = false
  | equal_num (Bit1 x3) (Bit0 x2) = false
  | equal_num One (Bit1 x3) = false
  | equal_num (Bit1 x3) One = false
  | equal_num One (Bit0 x2) = false
  | equal_num (Bit0 x2) One = false
  | equal_num (Bit1 x3) (Bit1 y3) = equal_num x3 y3
  | equal_num (Bit0 x2) (Bit0 y2) = equal_num x2 y2
  | equal_num One One = true;

fun equal_int (Neg k) (Neg l) = equal_num k l
  | equal_int (Neg k) (Pos l) = false
  | equal_int (Neg k) Zero_int = false
  | equal_int (Pos k) (Neg l) = false
  | equal_int (Pos k) (Pos l) = equal_num k l
  | equal_int (Pos k) Zero_int = false
  | equal_int Zero_int (Neg l) = false
  | equal_int Zero_int (Pos l) = false
  | equal_int Zero_int Zero_int = true;

fun adjust_div (q, r) =
  plus_inta q (of_bool zero_neq_one_int (not (equal_int r Zero_int)));

fun divide_int (Neg m) (Neg n) = fst (divmod_int m n)
  | divide_int (Pos m) (Neg n) = uminus_int (adjust_div (divmod_int m n))
  | divide_int (Neg m) (Pos n) = uminus_int (adjust_div (divmod_int m n))
  | divide_int (Pos m) (Pos n) = fst (divmod_int m n)
  | divide_int k (Neg One) = uminus_int k
  | divide_int k (Pos One) = k
  | divide_int Zero_int k = Zero_int
  | divide_int k Zero_int = Zero_int;

fun less_int (Neg k) (Neg l) = less_num l k
  | less_int (Neg k) (Pos l) = true
  | less_int (Neg k) Zero_int = true
  | less_int (Pos k) (Neg l) = false
  | less_int (Pos k) (Pos l) = less_num k l
  | less_int (Pos k) Zero_int = false
  | less_int Zero_int (Neg l) = false
  | less_int Zero_int (Pos l) = true
  | less_int Zero_int Zero_int = false;

fun snd (x1, x2) = x2;

fun adjust_mod l r = (if equal_int r Zero_int then Zero_int else minus_int l r);

fun modulo_int (Neg m) (Neg n) = uminus_int (snd (divmod_int m n))
  | modulo_int (Pos m) (Neg n) =
    uminus_int (adjust_mod (Pos n) (snd (divmod_int m n)))
  | modulo_int (Neg m) (Pos n) = adjust_mod (Pos n) (snd (divmod_int m n))
  | modulo_int (Pos m) (Pos n) = snd (divmod_int m n)
  | modulo_int k (Neg One) = Zero_int
  | modulo_int k (Pos One) = Zero_int
  | modulo_int Zero_int k = Zero_int
  | modulo_int k Zero_int = k;

fun abs_int i = (if less_int i Zero_int then uminus_int i else i);

fun gcd_int k l =
  abs_int
    (if equal_int l Zero_int then k
      else gcd_int l (modulo_int (abs_int k) (abs_int l)));

fun normalize p =
  (if less_int Zero_int (snd p)
    then let
           val a = gcd_int (fst p) (snd p);
         in
           (divide_int (fst p) a, divide_int (snd p) a)
         end
    else (if equal_int (snd p) Zero_int then (Zero_int, one_inta)
           else let
                  val a = uminus_int (gcd_int (fst p) (snd p));
                in
                  (divide_int (fst p) a, divide_int (snd p) a)
                end));

fun times_rata p q = Frct let
                            val a = quotient_of p;
                            val (aa, c) = a;
                            val b = quotient_of q;
                            val (ba, d) = b;
                          in
                            normalize (times_inta aa ba, times_inta c d)
                          end;

val times_rat = {times = times_rata} : rat times;

val power_rat = {one_power = one_rat, times_power = times_rat} : rat power;

datatype nat = Zero_nat | Suc of nat;

datatype 'a itself = Type;

type 'a len0 = {len_of : 'a itself -> nat};
val len_of = #len_of : 'a len0 -> 'a itself -> nat;

datatype 'a word = Word of int;

fun uint A_ (Word x) = x;

fun equal_worda A_ k l = equal_int (uint A_ k) (uint A_ l);

type 'a equal = {equal : 'a -> 'a -> bool};
val equal = #equal : 'a equal -> 'a -> 'a -> bool;

fun equal_word A_ = {equal = equal_worda A_} : 'a word equal;

fun eq A_ a b = equal A_ a b;

fun equal_list A_ [] (x21 :: x22) = false
  | equal_list A_ (x21 :: x22) [] = false
  | equal_list A_ (x21 :: x22) (y21 :: y22) =
    eq A_ x21 y21 andalso equal_list A_ x22 y22
  | equal_list A_ [] [] = true;

fun equal_nat Zero_nat (Suc x2) = false
  | equal_nat (Suc x2) Zero_nat = false
  | equal_nat (Suc x2) (Suc y2) = equal_nat x2 y2
  | equal_nat Zero_nat Zero_nat = true;

datatype abi_type = Tuint of nat | Tsint of nat | Taddr | Tbool |
  Tfixed of nat * nat | Tufixed of nat * nat | Tfbytes of nat | Tfunction |
  Tfarray of abi_type * nat | Ttuple of abi_type list | Tbytes | Tstring |
  Tarray of abi_type;

fun equal_abi_type () = {equal = equal_abi_typea} : abi_type equal
and equal_abi_typea Tstring (Tarray x13) = false
  | equal_abi_typea (Tarray x13) Tstring = false
  | equal_abi_typea Tbytes (Tarray x13) = false
  | equal_abi_typea (Tarray x13) Tbytes = false
  | equal_abi_typea Tbytes Tstring = false
  | equal_abi_typea Tstring Tbytes = false
  | equal_abi_typea (Ttuple x10) (Tarray x13) = false
  | equal_abi_typea (Tarray x13) (Ttuple x10) = false
  | equal_abi_typea (Ttuple x10) Tstring = false
  | equal_abi_typea Tstring (Ttuple x10) = false
  | equal_abi_typea (Ttuple x10) Tbytes = false
  | equal_abi_typea Tbytes (Ttuple x10) = false
  | equal_abi_typea (Tfarray (x91, x92)) (Tarray x13) = false
  | equal_abi_typea (Tarray x13) (Tfarray (x91, x92)) = false
  | equal_abi_typea (Tfarray (x91, x92)) Tstring = false
  | equal_abi_typea Tstring (Tfarray (x91, x92)) = false
  | equal_abi_typea (Tfarray (x91, x92)) Tbytes = false
  | equal_abi_typea Tbytes (Tfarray (x91, x92)) = false
  | equal_abi_typea (Tfarray (x91, x92)) (Ttuple x10) = false
  | equal_abi_typea (Ttuple x10) (Tfarray (x91, x92)) = false
  | equal_abi_typea Tfunction (Tarray x13) = false
  | equal_abi_typea (Tarray x13) Tfunction = false
  | equal_abi_typea Tfunction Tstring = false
  | equal_abi_typea Tstring Tfunction = false
  | equal_abi_typea Tfunction Tbytes = false
  | equal_abi_typea Tbytes Tfunction = false
  | equal_abi_typea Tfunction (Ttuple x10) = false
  | equal_abi_typea (Ttuple x10) Tfunction = false
  | equal_abi_typea Tfunction (Tfarray (x91, x92)) = false
  | equal_abi_typea (Tfarray (x91, x92)) Tfunction = false
  | equal_abi_typea (Tfbytes x7) (Tarray x13) = false
  | equal_abi_typea (Tarray x13) (Tfbytes x7) = false
  | equal_abi_typea (Tfbytes x7) Tstring = false
  | equal_abi_typea Tstring (Tfbytes x7) = false
  | equal_abi_typea (Tfbytes x7) Tbytes = false
  | equal_abi_typea Tbytes (Tfbytes x7) = false
  | equal_abi_typea (Tfbytes x7) (Ttuple x10) = false
  | equal_abi_typea (Ttuple x10) (Tfbytes x7) = false
  | equal_abi_typea (Tfbytes x7) (Tfarray (x91, x92)) = false
  | equal_abi_typea (Tfarray (x91, x92)) (Tfbytes x7) = false
  | equal_abi_typea (Tfbytes x7) Tfunction = false
  | equal_abi_typea Tfunction (Tfbytes x7) = false
  | equal_abi_typea (Tufixed (x61, x62)) (Tarray x13) = false
  | equal_abi_typea (Tarray x13) (Tufixed (x61, x62)) = false
  | equal_abi_typea (Tufixed (x61, x62)) Tstring = false
  | equal_abi_typea Tstring (Tufixed (x61, x62)) = false
  | equal_abi_typea (Tufixed (x61, x62)) Tbytes = false
  | equal_abi_typea Tbytes (Tufixed (x61, x62)) = false
  | equal_abi_typea (Tufixed (x61, x62)) (Ttuple x10) = false
  | equal_abi_typea (Ttuple x10) (Tufixed (x61, x62)) = false
  | equal_abi_typea (Tufixed (x61, x62)) (Tfarray (x91, x92)) = false
  | equal_abi_typea (Tfarray (x91, x92)) (Tufixed (x61, x62)) = false
  | equal_abi_typea (Tufixed (x61, x62)) Tfunction = false
  | equal_abi_typea Tfunction (Tufixed (x61, x62)) = false
  | equal_abi_typea (Tufixed (x61, x62)) (Tfbytes x7) = false
  | equal_abi_typea (Tfbytes x7) (Tufixed (x61, x62)) = false
  | equal_abi_typea (Tfixed (x51, x52)) (Tarray x13) = false
  | equal_abi_typea (Tarray x13) (Tfixed (x51, x52)) = false
  | equal_abi_typea (Tfixed (x51, x52)) Tstring = false
  | equal_abi_typea Tstring (Tfixed (x51, x52)) = false
  | equal_abi_typea (Tfixed (x51, x52)) Tbytes = false
  | equal_abi_typea Tbytes (Tfixed (x51, x52)) = false
  | equal_abi_typea (Tfixed (x51, x52)) (Ttuple x10) = false
  | equal_abi_typea (Ttuple x10) (Tfixed (x51, x52)) = false
  | equal_abi_typea (Tfixed (x51, x52)) (Tfarray (x91, x92)) = false
  | equal_abi_typea (Tfarray (x91, x92)) (Tfixed (x51, x52)) = false
  | equal_abi_typea (Tfixed (x51, x52)) Tfunction = false
  | equal_abi_typea Tfunction (Tfixed (x51, x52)) = false
  | equal_abi_typea (Tfixed (x51, x52)) (Tfbytes x7) = false
  | equal_abi_typea (Tfbytes x7) (Tfixed (x51, x52)) = false
  | equal_abi_typea (Tfixed (x51, x52)) (Tufixed (x61, x62)) = false
  | equal_abi_typea (Tufixed (x61, x62)) (Tfixed (x51, x52)) = false
  | equal_abi_typea Tbool (Tarray x13) = false
  | equal_abi_typea (Tarray x13) Tbool = false
  | equal_abi_typea Tbool Tstring = false
  | equal_abi_typea Tstring Tbool = false
  | equal_abi_typea Tbool Tbytes = false
  | equal_abi_typea Tbytes Tbool = false
  | equal_abi_typea Tbool (Ttuple x10) = false
  | equal_abi_typea (Ttuple x10) Tbool = false
  | equal_abi_typea Tbool (Tfarray (x91, x92)) = false
  | equal_abi_typea (Tfarray (x91, x92)) Tbool = false
  | equal_abi_typea Tbool Tfunction = false
  | equal_abi_typea Tfunction Tbool = false
  | equal_abi_typea Tbool (Tfbytes x7) = false
  | equal_abi_typea (Tfbytes x7) Tbool = false
  | equal_abi_typea Tbool (Tufixed (x61, x62)) = false
  | equal_abi_typea (Tufixed (x61, x62)) Tbool = false
  | equal_abi_typea Tbool (Tfixed (x51, x52)) = false
  | equal_abi_typea (Tfixed (x51, x52)) Tbool = false
  | equal_abi_typea Taddr (Tarray x13) = false
  | equal_abi_typea (Tarray x13) Taddr = false
  | equal_abi_typea Taddr Tstring = false
  | equal_abi_typea Tstring Taddr = false
  | equal_abi_typea Taddr Tbytes = false
  | equal_abi_typea Tbytes Taddr = false
  | equal_abi_typea Taddr (Ttuple x10) = false
  | equal_abi_typea (Ttuple x10) Taddr = false
  | equal_abi_typea Taddr (Tfarray (x91, x92)) = false
  | equal_abi_typea (Tfarray (x91, x92)) Taddr = false
  | equal_abi_typea Taddr Tfunction = false
  | equal_abi_typea Tfunction Taddr = false
  | equal_abi_typea Taddr (Tfbytes x7) = false
  | equal_abi_typea (Tfbytes x7) Taddr = false
  | equal_abi_typea Taddr (Tufixed (x61, x62)) = false
  | equal_abi_typea (Tufixed (x61, x62)) Taddr = false
  | equal_abi_typea Taddr (Tfixed (x51, x52)) = false
  | equal_abi_typea (Tfixed (x51, x52)) Taddr = false
  | equal_abi_typea Taddr Tbool = false
  | equal_abi_typea Tbool Taddr = false
  | equal_abi_typea (Tsint x2) (Tarray x13) = false
  | equal_abi_typea (Tarray x13) (Tsint x2) = false
  | equal_abi_typea (Tsint x2) Tstring = false
  | equal_abi_typea Tstring (Tsint x2) = false
  | equal_abi_typea (Tsint x2) Tbytes = false
  | equal_abi_typea Tbytes (Tsint x2) = false
  | equal_abi_typea (Tsint x2) (Ttuple x10) = false
  | equal_abi_typea (Ttuple x10) (Tsint x2) = false
  | equal_abi_typea (Tsint x2) (Tfarray (x91, x92)) = false
  | equal_abi_typea (Tfarray (x91, x92)) (Tsint x2) = false
  | equal_abi_typea (Tsint x2) Tfunction = false
  | equal_abi_typea Tfunction (Tsint x2) = false
  | equal_abi_typea (Tsint x2) (Tfbytes x7) = false
  | equal_abi_typea (Tfbytes x7) (Tsint x2) = false
  | equal_abi_typea (Tsint x2) (Tufixed (x61, x62)) = false
  | equal_abi_typea (Tufixed (x61, x62)) (Tsint x2) = false
  | equal_abi_typea (Tsint x2) (Tfixed (x51, x52)) = false
  | equal_abi_typea (Tfixed (x51, x52)) (Tsint x2) = false
  | equal_abi_typea (Tsint x2) Tbool = false
  | equal_abi_typea Tbool (Tsint x2) = false
  | equal_abi_typea (Tsint x2) Taddr = false
  | equal_abi_typea Taddr (Tsint x2) = false
  | equal_abi_typea (Tuint x1) (Tarray x13) = false
  | equal_abi_typea (Tarray x13) (Tuint x1) = false
  | equal_abi_typea (Tuint x1) Tstring = false
  | equal_abi_typea Tstring (Tuint x1) = false
  | equal_abi_typea (Tuint x1) Tbytes = false
  | equal_abi_typea Tbytes (Tuint x1) = false
  | equal_abi_typea (Tuint x1) (Ttuple x10) = false
  | equal_abi_typea (Ttuple x10) (Tuint x1) = false
  | equal_abi_typea (Tuint x1) (Tfarray (x91, x92)) = false
  | equal_abi_typea (Tfarray (x91, x92)) (Tuint x1) = false
  | equal_abi_typea (Tuint x1) Tfunction = false
  | equal_abi_typea Tfunction (Tuint x1) = false
  | equal_abi_typea (Tuint x1) (Tfbytes x7) = false
  | equal_abi_typea (Tfbytes x7) (Tuint x1) = false
  | equal_abi_typea (Tuint x1) (Tufixed (x61, x62)) = false
  | equal_abi_typea (Tufixed (x61, x62)) (Tuint x1) = false
  | equal_abi_typea (Tuint x1) (Tfixed (x51, x52)) = false
  | equal_abi_typea (Tfixed (x51, x52)) (Tuint x1) = false
  | equal_abi_typea (Tuint x1) Tbool = false
  | equal_abi_typea Tbool (Tuint x1) = false
  | equal_abi_typea (Tuint x1) Taddr = false
  | equal_abi_typea Taddr (Tuint x1) = false
  | equal_abi_typea (Tuint x1) (Tsint x2) = false
  | equal_abi_typea (Tsint x2) (Tuint x1) = false
  | equal_abi_typea (Tarray x13) (Tarray y13) = equal_abi_typea x13 y13
  | equal_abi_typea (Ttuple x10) (Ttuple y10) =
    equal_list (equal_abi_type ()) x10 y10
  | equal_abi_typea (Tfarray (x91, x92)) (Tfarray (y91, y92)) =
    equal_abi_typea x91 y91 andalso equal_nat x92 y92
  | equal_abi_typea (Tfbytes x7) (Tfbytes y7) = equal_nat x7 y7
  | equal_abi_typea (Tufixed (x61, x62)) (Tufixed (y61, y62)) =
    equal_nat x61 y61 andalso equal_nat x62 y62
  | equal_abi_typea (Tfixed (x51, x52)) (Tfixed (y51, y52)) =
    equal_nat x51 y51 andalso equal_nat x52 y52
  | equal_abi_typea (Tsint x2) (Tsint y2) = equal_nat x2 y2
  | equal_abi_typea (Tuint x1) (Tuint y1) = equal_nat x1 y1
  | equal_abi_typea Tstring Tstring = true
  | equal_abi_typea Tbytes Tbytes = true
  | equal_abi_typea Tfunction Tfunction = true
  | equal_abi_typea Tbool Tbool = true
  | equal_abi_typea Taddr Taddr = true;
val equal_abi_type = equal_abi_type ();

fun plus_nat (Suc m) n = plus_nat m (Suc n)
  | plus_nat Zero_nat n = n;

fun times_nat Zero_nat n = Zero_nat
  | times_nat (Suc m) n = plus_nat n (times_nat m n);

val one_nat : nat = Suc Zero_nat;

fun nat_of_num (Bit1 n) = let
                            val m = nat_of_num n;
                          in
                            Suc (plus_nat m m)
                          end
  | nat_of_num (Bit0 n) = let
                            val m = nat_of_num n;
                          in
                            plus_nat m m
                          end
  | nat_of_num One = one_nat;

type 'a finite = {};

datatype 'a bit0 = Abs_bit0 of int;

fun len_of_bit0 A_ uu = times_nat (nat_of_num (Bit0 One)) (len_of A_ Type);

type 'a len = {len0_len : 'a len0};
val len0_len = #len0_len : 'a len -> 'a len0;

fun len0_bit0 A_ = {len_of = len_of_bit0 A_} : 'a bit0 len0;

fun len_bit0 A_ = {len0_len = len0_bit0 (len0_len A_)} : 'a bit0 len;

datatype num1 = One_num1;

fun len_of_num1 uu = one_nat;

val len0_num1 = {len_of = len_of_num1} : num1 len0;

val len_num1 = {len0_len = len0_num1} : num1 len;

val one_integera : IntInf.int = (1 : IntInf.int);

val one_integer = {one = one_integera} : IntInf.int one;

val zero_integer = {zero = (0 : IntInf.int)} : IntInf.int zero;

val zero_neq_one_integer =
  {one_zero_neq_one = one_integer, zero_zero_neq_one = zero_integer} :
  IntInf.int zero_neq_one;

datatype char = Chara of bool * bool * bool * bool * bool * bool * bool * bool;

datatype ('a, 'b) sum = Inl of 'a | Inr of 'b;

datatype abi_value = Vuint of nat * int | Vsint of nat * int | Vaddr of int |
  Vbool of bool | Vfixed of nat * nat * rat | Vufixed of nat * nat * rat |
  Vfbytes of nat * num1 bit0 bit0 bit0 word list | Vfunction of int * int |
  Vfarray of abi_type * nat * abi_value list |
  Vtuple of abi_type list * abi_value list |
  Vbytes of num1 bit0 bit0 bit0 word list | Vstring of char list |
  Varray of abi_type * abi_value list;

fun id x = (fn xa => xa) x;

fun nat (Pos k) = nat_of_num k
  | nat Zero_int = Zero_nat
  | nat (Neg k) = Zero_nat;

fun fold f (x :: xs) s = fold f xs (f x s)
  | fold f [] s = s;

fun rev xs = fold (fn a => fn b => a :: b) xs [];

fun drop n [] = []
  | drop n (x :: xs) = (case n of Zero_nat => x :: xs | Suc m => drop m xs);

fun take n [] = []
  | take n (x :: xs) = (case n of Zero_nat => [] | Suc m => x :: take m xs);

fun minus_nat (Suc m) (Suc n) = minus_nat m n
  | minus_nat Zero_nat n = Zero_nat
  | minus_nat m Zero_nat = m;

fun bin_rest w = divide_int w (Pos (Bit0 One));

fun bin_last w = equal_int (modulo_int w (Pos (Bit0 One))) one_inta;

fun bit k b = plus_inta (plus_inta (if b then one_inta else Zero_int) k) k;

fun sbintrunc Zero_nat bin =
  (if bin_last bin then uminus_int one_inta else Zero_int)
  | sbintrunc (Suc n) bin = bit (sbintrunc n (bin_rest bin)) (bin_last bin);

fun sint A_ w =
  sbintrunc (minus_nat (len_of (len0_len A_) Type) one_nat)
    (uint (len0_len A_) w);

fun foldl f a [] = a
  | foldl f a (x :: xs) = foldl f (f a x) xs;

fun foldr f [] = id
  | foldr f (x :: xs) = f x o foldr f xs;

fun of_int a = Frct (a, one_inta);

fun concat xss = foldr (fn a => fn b => a @ b) xss [];

fun less_nat m (Suc n) = less_eq_nat m n
  | less_nat n Zero_nat = false
and less_eq_nat (Suc m) n = less_nat m n
  | less_eq_nat Zero_nat n = true;

fun divmod_nat m n =
  (if equal_nat n Zero_nat orelse less_nat m n then (Zero_nat, m)
    else let
           val a = divmod_nat (minus_nat m n) n;
           val (q, aa) = a;
         in
           (Suc q, aa)
         end);

fun decwrite1 c =
  (if equal_nat c Zero_nat
    then Chara (false, false, false, false, true, true, false, false)
    else (if equal_nat c one_nat
           then Chara (true, false, false, false, true, true, false, false)
           else (if equal_nat c (nat_of_num (Bit0 One))
                  then Chara (false, true, false, false, true, true, false,
                               false)
                  else (if equal_nat c (nat_of_num (Bit1 One))
                         then Chara (true, true, false, false, true, true,
                                      false, false)
                         else (if equal_nat c (nat_of_num (Bit0 (Bit0 One)))
                                then Chara (false, false, true, false, true,
     true, false, false)
                                else (if equal_nat c
   (nat_of_num (Bit1 (Bit0 One)))
                                       then Chara
      (true, false, true, false, true, true, false, false)
                                       else (if equal_nat c
          (nat_of_num (Bit0 (Bit1 One)))
      then Chara (false, true, true, false, true, true, false, false)
      else (if equal_nat c (nat_of_num (Bit1 (Bit1 One)))
             then Chara (true, true, true, false, true, true, false, false)
             else (if equal_nat c (nat_of_num (Bit0 (Bit0 (Bit0 One))))
                    then Chara (false, false, false, true, true, true, false,
                                 false)
                    else (if equal_nat c (nat_of_num (Bit1 (Bit0 (Bit0 One))))
                           then Chara (true, false, false, true, true, true,
false, false)
                           else (raise Fail "undefined")))))))))));

fun decwritea n =
  (if less_nat n (nat_of_num (Bit0 (Bit1 (Bit0 One)))) then [decwrite1 n]
    else let
           val (d, m) = divmod_nat n (nat_of_num (Bit0 (Bit1 (Bit0 One))));
         in
           decwrite1 m :: decwritea d
         end);

fun decwrite n = rev (decwritea n);

fun list_ex p [] = false
  | list_ex p (x :: xs) = p x orelse list_ex p xs;

fun those_err [] = Inl []
  | those_err (Inl h :: t) =
    (case those_err t of Inl ta => Inl (h :: ta) | Inr a => Inr a)
  | those_err (Inr s :: uu) = Inr s;

fun map f [] = []
  | map f (x21 :: x22) = f x21 :: map f x22;

fun replicate Zero_nat x = []
  | replicate (Suc n) x = x :: replicate n x;

fun bin_cat w Zero_nat v = w
  | bin_cat w (Suc n) v = bit (bin_cat w n (bin_rest v)) (bin_last v);

fun bin_rcat n = foldl (fn u => bin_cat u n) Zero_int;

fun power A_ a Zero_nat = one (one_power A_)
  | power A_ a (Suc n) = times (times_power A_) a (power A_ a n);

fun word_of_int A_ k =
  Word (modulo_int k (power power_int (Pos (Bit0 One)) (len_of A_ Type)));

fun word_rcat A_ B_ ws =
  word_of_int B_ (bin_rcat (len_of A_ Type) (map (uint A_) ws));

fun gen_length n (x :: xs) = gen_length (Suc n) xs
  | gen_length n [] = n;

fun modulo_nat m n = snd (divmod_nat m n);

fun list_all p [] = true
  | list_all p (x :: xs) = p x andalso list_all p xs;

fun abi_type_valid (Tuint n) =
  less_nat Zero_nat n andalso
    (less_eq_nat n
       (nat_of_num
         (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))))) andalso
      equal_nat (modulo_nat n (nat_of_num (Bit0 (Bit0 (Bit0 One))))) Zero_nat)
  | abi_type_valid (Tsint n) =
    less_nat Zero_nat n andalso
      (less_eq_nat n
         (nat_of_num
           (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))))) andalso
        equal_nat (modulo_nat n (nat_of_num (Bit0 (Bit0 (Bit0 One))))) Zero_nat)
  | abi_type_valid (Tfixed (m, n)) =
    less_eq_nat (nat_of_num (Bit0 (Bit0 (Bit0 One)))) m andalso
      (less_eq_nat m
         (nat_of_num
           (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))))) andalso
        (equal_nat (modulo_nat m (nat_of_num (Bit0 (Bit0 (Bit0 One)))))
           Zero_nat andalso
          (less_nat Zero_nat n andalso
            less_eq_nat n
              (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit1 (Bit0 One))))))))))
  | abi_type_valid (Tufixed (m, n)) =
    less_eq_nat (nat_of_num (Bit0 (Bit0 (Bit0 One)))) m andalso
      (less_eq_nat m
         (nat_of_num
           (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))))) andalso
        (equal_nat (modulo_nat m (nat_of_num (Bit0 (Bit0 (Bit0 One)))))
           Zero_nat andalso
          (less_nat Zero_nat n andalso
            less_eq_nat n
              (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit1 (Bit0 One))))))))))
  | abi_type_valid (Tfbytes m) =
    less_nat Zero_nat m andalso
      less_eq_nat m (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))
  | abi_type_valid (Tfarray (t, uu)) = abi_type_valid t
  | abi_type_valid (Ttuple ts) = list_all abi_type_valid ts
  | abi_type_valid (Tarray t) = abi_type_valid t
  | abi_type_valid Taddr = true
  | abi_type_valid Tbool = true
  | abi_type_valid Tfunction = true
  | abi_type_valid Tbytes = true
  | abi_type_valid Tstring = true;

fun size_list x = gen_length Zero_nat x;

fun decode_err s (ix, l) =
  s @ [Chara (false, false, false, false, false, true, false, false),
        Chara (true, false, false, false, false, true, true, false),
        Chara (false, false, true, false, true, true, true, false),
        Chara (false, false, false, false, false, true, false, false),
        Chara (false, true, false, false, false, true, true, false),
        Chara (true, false, false, true, true, true, true, false),
        Chara (false, false, true, false, true, true, true, false),
        Chara (true, false, true, false, false, true, true, false),
        Chara (false, false, false, false, false, true, false, false)] @
        decwrite (nat ix) @
          [Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, true, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false)] @
            decwrite (size_list l) @
              [Chara (false, true, true, true, false, true, false, false)];

fun of_nat_aux A_ inc Zero_nat i = i
  | of_nat_aux A_ inc (Suc n) i = of_nat_aux A_ inc n (inc i);

fun of_nat A_ n =
  of_nat_aux A_
    (fn i =>
      plus ((plus_semigroup_add o semigroup_add_numeral o
              numeral_semiring_numeral o semiring_numeral_semiring_1)
             A_)
        i (one ((one_numeral o numeral_semiring_numeral o
                  semiring_numeral_semiring_1)
                 A_)))
    n (zero ((zero_mult_zero o mult_zero_semiring_0 o semiring_0_semiring_1)
              A_));

fun abi_type_isdynamic (Tfarray (t, n)) = abi_type_isdynamic t
  | abi_type_isdynamic Tbytes = true
  | abi_type_isdynamic Tstring = true
  | abi_type_isdynamic (Tarray t) = true
  | abi_type_isdynamic (Ttuple l) = list_ex abi_type_isdynamic l
  | abi_type_isdynamic (Tuint v) = false
  | abi_type_isdynamic (Tsint v) = false
  | abi_type_isdynamic Taddr = false
  | abi_type_isdynamic Tbool = false
  | abi_type_isdynamic (Tfixed (v, va)) = false
  | abi_type_isdynamic (Tufixed (v, va)) = false
  | abi_type_isdynamic (Tfbytes v) = false
  | abi_type_isdynamic Tfunction = false;

fun abi_type_isstatic t = not (abi_type_isdynamic t);

fun abi_static_size (Tuint n) = Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))
  | abi_static_size (Tsint n) = Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))
  | abi_static_size Taddr = Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))
  | abi_static_size Tbool = Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))
  | abi_static_size (Tfixed (uu, uv)) =
    Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))
  | abi_static_size (Tufixed (uw, ux)) =
    Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))
  | abi_static_size (Tfbytes uy) = Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))
  | abi_static_size (Tfarray (t, n)) =
    times_inta (of_nat semiring_1_int n) (abi_static_size t)
  | abi_static_size (Ttuple ts) =
    foldl (fn a => fn x => plus_inta a (abi_static_size x)) Zero_int ts
  | abi_static_size Tfunction = Zero_int
  | abi_static_size Tbytes = Zero_int
  | abi_static_size Tstring = Zero_int
  | abi_static_size (Tarray v) = Zero_int;

fun decode_sint l =
  sint (len_bit0
         (len_bit0
           (len_bit0
             (len_bit0 (len_bit0 (len_bit0 (len_bit0 (len_bit0 len_num1))))))))
    (word_rcat (len0_bit0 (len0_bit0 (len0_bit0 len0_num1)))
      (len0_bit0
        (len0_bit0
          (len0_bit0
            (len0_bit0
              (len0_bit0 (len0_bit0 (len0_bit0 (len0_bit0 len0_num1))))))))
      (take (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))) l));

fun integer_of_int k =
  (if less_int k Zero_int then IntInf.~ (integer_of_int (uminus_int k))
    else (if equal_int k Zero_int then (0 : IntInf.int)
           else let
                  val l =
                    IntInf.* ((2 : IntInf.int), integer_of_int
          (divide_int k (Pos (Bit0 One))));
                  val j = modulo_int k (Pos (Bit0 One));
                in
                  (if equal_int j Zero_int then l
                    else IntInf.+ (l, (1 : IntInf.int)))
                end));

fun bit_cut_integer k =
  (if ((k : IntInf.int) = (0 : IntInf.int)) then ((0 : IntInf.int), false)
    else let
           val (r, s) =
             IntInf.divMod (IntInf.abs k, IntInf.abs (2 : IntInf.int));
         in
           ((if IntInf.< ((0 : IntInf.int), k) then r
              else IntInf.- (IntInf.~ r, s)),
             ((s : IntInf.int) = (1 : IntInf.int)))
         end);

fun char_of_integer k = let
                          val (q0, b0) = bit_cut_integer k;
                          val (q1, b1) = bit_cut_integer q0;
                          val (q2, b2) = bit_cut_integer q1;
                          val (q3, b3) = bit_cut_integer q2;
                          val (q4, b4) = bit_cut_integer q3;
                          val (q5, b5) = bit_cut_integer q4;
                          val (q6, b6) = bit_cut_integer q5;
                          val a = bit_cut_integer q6;
                          val (_, aa) = a;
                        in
                          Chara (b0, b1, b2, b3, b4, b5, b6, aa)
                        end;

fun bytes_to_string bs =
  map (fn b =>
        char_of_integer
          (integer_of_int
            (uint (len0_bit0 (len0_bit0 (len0_bit0 len0_num1))) b)))
    bs;

fun abi_get_type (Vuint (n, uu)) = Tuint n
  | abi_get_type (Vsint (n, uv)) = Tsint n
  | abi_get_type (Vaddr uw) = Taddr
  | abi_get_type (Vbool ux) = Tbool
  | abi_get_type (Vfixed (m, n, uy)) = Tfixed (m, n)
  | abi_get_type (Vufixed (m, n, uz)) = Tufixed (m, n)
  | abi_get_type (Vfbytes (n, va)) = Tfbytes n
  | abi_get_type (Vfunction (vb, vc)) = Tfunction
  | abi_get_type (Vfarray (t, n, vd)) = Tfarray (t, n)
  | abi_get_type (Vtuple (ts, ve)) = Ttuple ts
  | abi_get_type (Vbytes vf) = Tbytes
  | abi_get_type (Vstring vg) = Tstring
  | abi_get_type (Varray (t, vh)) = Tarray t;

fun farray_value_valid_aux t n l =
  equal_nat (size_list l) n andalso
    list_all (fn v => equal_abi_typea (abi_get_type v) t) l;

fun tuple_value_valid_aux ts vs =
  equal_list equal_abi_type (map abi_get_type vs) ts;

fun int_of_fixed n r =
  let
    val (num, den) =
      quotient_of
        (times_rata r
          (power power_rat (of_int (Pos (Bit0 (Bit1 (Bit0 One))))) n));
  in
    (if equal_int den one_inta then SOME num else NONE)
  end;

fun max_uint n = minus_int (power power_int (Pos (Bit0 One)) n) one_inta;

fun ufixed_value_valid m n r =
  (case int_of_fixed n r of NONE => false
    | SOME i => less_eq_int Zero_int i andalso less_eq_int i (max_uint m));

fun fbytes_value_valid n l = equal_nat (size_list l) n;

fun min_sint n =
  times_inta (uminus_int one_inta)
    (power power_int (Pos (Bit0 One)) (minus_nat n one_nat));

fun max_sint n =
  minus_int (power power_int (Pos (Bit0 One)) (minus_nat n one_nat)) one_inta;

fun fixed_value_valid m n r =
  (case int_of_fixed n r of NONE => false
    | SOME i => less_eq_int (min_sint m) i andalso less_eq_int i (max_sint m));

fun uint_value_valid n i =
  less_eq_int Zero_int i andalso less_eq_int i (max_uint n);

fun sint_value_valid n i =
  less_eq_int (min_sint n) i andalso less_eq_int i (max_sint n);

fun addr_value_valid i =
  uint_value_valid
    (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit1 (Bit0 One)))))))) i;

fun divide_rat p q = Frct let
                            val a = quotient_of p;
                            val (aa, c) = a;
                            val b = quotient_of q;
                            val (ba, d) = b;
                          in
                            normalize (times_inta aa d, times_inta c ba)
                          end;

fun decode_uint l =
  uint (len0_bit0
         (len0_bit0
           (len0_bit0
             (len0_bit0
               (len0_bit0 (len0_bit0 (len0_bit0 (len0_bit0 len0_num1))))))))
    (word_rcat (len0_bit0 (len0_bit0 (len0_bit0 len0_num1)))
      (len0_bit0
        (len0_bit0
          (len0_bit0
            (len0_bit0
              (len0_bit0 (len0_bit0 (len0_bit0 (len0_bit0 len0_num1))))))))
      (take (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))) l));

fun decode_ufixed n l =
  let
    val i = decode_uint l;
  in
    divide_rat (of_int i)
      (power power_rat (of_int (Pos (Bit0 (Bit1 (Bit0 One))))) n)
  end;

fun skip_padding n =
  (case divmod_nat n (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))
    of (_, Zero_nat) => n
    | (_, Suc nat) =>
      minus_nat (plus_nat n (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))))
        (Suc nat));

fun check_padding n l =
  let
    val p = skip_padding n;
  in
    less_eq_nat p (size_list l) andalso
      equal_list (equal_word (len0_bit0 (len0_bit0 (len0_bit0 len0_num1))))
        (drop n (take p l))
        (replicate (minus_nat p n)
          (word_of_int (len0_bit0 (len0_bit0 (len0_bit0 len0_num1))) Zero_int))
  end;

fun decode_fbytes n l = (if check_padding n l then SOME (take n l) else NONE);

fun decode_fixed n l =
  let
    val i = decode_sint l;
  in
    divide_rat (of_int i)
      (power power_rat (of_int (Pos (Bit0 (Bit1 (Bit0 One))))) n)
  end;

fun decode_bool l =
  let
    val i = decode_uint l;
  in
    (if equal_int i Zero_int then SOME false
      else (if equal_int i one_inta then SOME true else NONE))
  end;

fun decode_static (Tuint n) (ix, l) =
  let
    val la = drop (nat ix) l;
    val res = decode_uint la;
  in
    (if uint_value_valid n res then Inl (Vuint (n, res))
      else Inr (decode_err
                 [Chara (true, false, false, true, false, false, true, false),
                   Chara (false, true, true, true, false, true, true, false),
                   Chara (false, true, true, false, true, true, true, false),
                   Chara (true, false, false, false, false, true, true, false),
                   Chara (false, false, true, true, false, true, true, false),
                   Chara (true, false, false, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (true, false, true, false, true, true, true, false),
                   Chara (true, false, false, true, false, true, true, false),
                   Chara (false, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, true, true, true, false)]
                 (ix, l)))
  end
  | decode_static (Tsint n) (ix, l) =
    let
      val la = drop (nat ix) l;
      val res = decode_sint la;
    in
      (if sint_value_valid n res then Inl (Vsint (n, res))
        else Inr (decode_err
                   [Chara (true, false, false, true, false, false, true, false),
                     Chara (false, true, true, true, false, true, true, false),
                     Chara (false, true, true, false, true, true, true, false),
                     Chara (true, false, false, false, false, true, true,
                             false),
                     Chara (false, false, true, true, false, true, true, false),
                     Chara (true, false, false, true, false, true, true, false),
                     Chara (false, false, true, false, false, true, true,
                             false),
                     Chara (false, false, false, false, false, true, false,
                             false),
                     Chara (true, true, false, false, true, true, true, false),
                     Chara (true, false, false, true, false, true, true, false),
                     Chara (false, true, true, true, false, true, true, false),
                     Chara (false, false, true, false, true, true, true, false)]
                   (ix, l)))
    end
  | decode_static Taddr (ix, l) =
    let
      val la = drop (nat ix) l;
      val res = decode_uint la;
    in
      (if addr_value_valid res then Inl (Vaddr res)
        else Inr (decode_err
                   [Chara (true, false, false, true, false, false, true, false),
                     Chara (false, true, true, true, false, true, true, false),
                     Chara (false, true, true, false, true, true, true, false),
                     Chara (true, false, false, false, false, true, true,
                             false),
                     Chara (false, false, true, true, false, true, true, false),
                     Chara (true, false, false, true, false, true, true, false),
                     Chara (false, false, true, false, false, true, true,
                             false),
                     Chara (false, false, false, false, false, true, false,
                             false),
                     Chara (true, false, false, false, false, true, true,
                             false),
                     Chara (false, false, true, false, false, true, true,
                             false),
                     Chara (false, false, true, false, false, true, true,
                             false),
                     Chara (false, true, false, false, true, true, true, false),
                     Chara (true, false, true, false, false, true, true, false),
                     Chara (true, true, false, false, true, true, true, false),
                     Chara (true, true, false, false, true, true, true, false)]
                   (ix, l)))
    end
  | decode_static Tbool (ix, l) =
    let
      val la = drop (nat ix) l;
    in
      (case decode_bool la
        of NONE =>
          Inr (decode_err
                [Chara (true, false, false, true, false, false, true, false),
                  Chara (false, true, true, true, false, true, true, false),
                  Chara (false, true, true, false, true, true, true, false),
                  Chara (true, false, false, false, false, true, true, false),
                  Chara (false, false, true, true, false, true, true, false),
                  Chara (true, false, false, true, false, true, true, false),
                  Chara (false, false, true, false, false, true, true, false),
                  Chara (false, false, false, false, false, true, false, false),
                  Chara (false, true, false, false, false, true, true, false),
                  Chara (true, true, true, true, false, true, true, false),
                  Chara (true, true, true, true, false, true, true, false),
                  Chara (false, false, true, true, false, true, true, false)]
                (ix, l))
        | SOME b => Inl (Vbool b))
    end
  | decode_static (Tfixed (m, n)) (ix, l) =
    let
      val la = drop (nat ix) l;
      val res = decode_fixed n la;
    in
      (if fixed_value_valid m n res then Inl (Vfixed (m, n, res))
        else Inr (decode_err
                   [Chara (true, false, false, true, false, false, true, false),
                     Chara (false, true, true, true, false, true, true, false),
                     Chara (false, true, true, false, true, true, true, false),
                     Chara (true, false, false, false, false, true, true,
                             false),
                     Chara (false, false, true, true, false, true, true, false),
                     Chara (true, false, false, true, false, true, true, false),
                     Chara (false, false, true, false, false, true, true,
                             false),
                     Chara (false, false, false, false, false, true, false,
                             false),
                     Chara (false, true, true, false, false, true, true, false),
                     Chara (true, false, false, true, false, true, true, false),
                     Chara (false, false, false, true, true, true, true, false),
                     Chara (true, false, true, false, false, true, true, false),
                     Chara (false, false, true, false, false, true, true,
                             false)]
                   (ix, l)))
    end
  | decode_static (Tufixed (m, n)) (ix, l) =
    let
      val la = drop (nat ix) l;
      val res = decode_ufixed n la;
    in
      (if ufixed_value_valid m n res then Inl (Vufixed (m, n, res))
        else Inr (decode_err
                   [Chara (true, false, false, true, false, false, true, false),
                     Chara (false, true, true, true, false, true, true, false),
                     Chara (false, true, true, false, true, true, true, false),
                     Chara (true, false, false, false, false, true, true,
                             false),
                     Chara (false, false, true, true, false, true, true, false),
                     Chara (true, false, false, true, false, true, true, false),
                     Chara (false, false, true, false, false, true, true,
                             false),
                     Chara (false, false, false, false, false, true, false,
                             false),
                     Chara (true, false, true, false, true, true, true, false),
                     Chara (false, true, true, false, false, true, true, false),
                     Chara (true, false, false, true, false, true, true, false),
                     Chara (false, false, false, true, true, true, true, false),
                     Chara (true, false, true, false, false, true, true, false),
                     Chara (false, false, true, false, false, true, true,
                             false)]
                   (ix, l)))
    end
  | decode_static (Tfbytes n) (ix, l) =
    let
      val la = drop (nat ix) l;
    in
      (case decode_fbytes n la
        of NONE =>
          Inr (decode_err
                [Chara (true, false, false, true, false, true, true, false),
                  Chara (false, true, true, true, false, true, true, false),
                  Chara (false, true, true, false, true, true, true, false),
                  Chara (true, false, false, false, false, true, true, false),
                  Chara (false, false, true, true, false, true, true, false),
                  Chara (true, false, false, true, false, true, true, false),
                  Chara (false, false, true, false, false, true, true, false),
                  Chara (false, false, false, false, false, true, false, false),
                  Chara (false, true, true, false, false, true, true, false),
                  Chara (false, true, false, false, false, true, true, false),
                  Chara (true, false, false, true, true, true, true, false),
                  Chara (false, false, true, false, true, true, true, false),
                  Chara (true, false, true, false, false, true, true, false),
                  Chara (true, true, false, false, true, true, true, false),
                  Chara (false, false, false, false, false, true, false, false),
                  Chara (false, false, false, false, true, true, true, false),
                  Chara (true, false, false, false, false, true, true, false),
                  Chara (false, false, true, false, false, true, true, false),
                  Chara (false, false, true, false, false, true, true, false),
                  Chara (true, false, false, true, false, true, true, false),
                  Chara (false, true, true, true, false, true, true, false),
                  Chara (true, true, true, false, false, true, true, false)]
                (ix, l))
        | SOME res =>
          (if fbytes_value_valid n res then Inl (Vfbytes (n, res))
            else Inr (decode_err
                       [Chara (true, false, false, true, false, false, true,
                                false),
                         Chara (false, true, true, true, false, true, true,
                                 false),
                         Chara (false, true, true, false, true, true, true,
                                 false),
                         Chara (true, false, false, false, false, true, true,
                                 false),
                         Chara (false, false, true, true, false, true, true,
                                 false),
                         Chara (true, false, false, true, false, true, true,
                                 false),
                         Chara (false, false, true, false, false, true, true,
                                 false),
                         Chara (false, false, false, false, false, true, false,
                                 false),
                         Chara (false, true, true, false, false, true, true,
                                 false),
                         Chara (false, true, false, false, false, true, true,
                                 false),
                         Chara (true, false, false, true, true, true, true,
                                 false),
                         Chara (false, false, true, false, true, true, true,
                                 false),
                         Chara (true, false, true, false, false, true, true,
                                 false),
                         Chara (true, true, false, false, true, true, true,
                                 false)]
                       (ix, l))))
    end
  | decode_static (Tfarray (t, n)) (ix, l) =
    (case decode_static_tup (replicate n t) (ix, l)
      of Inl vs =>
        (if farray_value_valid_aux t n vs then Inl (Vfarray (t, n, vs))
          else Inr (decode_err
                     [Chara (true, false, false, true, false, false, true,
                              false),
                       Chara (false, true, true, true, false, true, true,
                               false),
                       Chara (false, true, true, false, true, true, true,
                               false),
                       Chara (true, false, false, false, false, true, true,
                               false),
                       Chara (false, false, true, true, false, true, true,
                               false),
                       Chara (true, false, false, true, false, true, true,
                               false),
                       Chara (false, false, true, false, false, true, true,
                               false),
                       Chara (false, false, false, false, false, true, false,
                               false),
                       Chara (false, true, true, false, false, true, true,
                               false),
                       Chara (true, false, false, false, false, true, true,
                               false),
                       Chara (false, true, false, false, true, true, true,
                               false),
                       Chara (false, true, false, false, true, true, true,
                               false),
                       Chara (true, false, false, false, false, true, true,
                               false),
                       Chara (true, false, false, true, true, true, true,
                               false)]
                     (ix, l)))
      | Inr a => Inr a)
  | decode_static (Ttuple ts) (ix, l) =
    (case decode_static_tup ts (ix, l)
      of Inl vs =>
        (if tuple_value_valid_aux ts vs then Inl (Vtuple (ts, vs))
          else Inr (decode_err
                     [Chara (true, false, false, true, false, false, true,
                              false),
                       Chara (false, true, true, true, false, true, true,
                               false),
                       Chara (false, true, true, false, true, true, true,
                               false),
                       Chara (true, false, false, false, false, true, true,
                               false),
                       Chara (false, false, true, true, false, true, true,
                               false),
                       Chara (true, false, false, true, false, true, true,
                               false),
                       Chara (false, false, true, false, false, true, true,
                               false),
                       Chara (false, false, false, false, false, true, false,
                               false),
                       Chara (false, false, true, false, true, true, true,
                               false),
                       Chara (true, false, true, false, true, true, true,
                               false),
                       Chara (false, false, false, false, true, true, true,
                               false),
                       Chara (false, false, true, true, false, true, true,
                               false),
                       Chara (true, false, true, false, false, true, true,
                               false)]
                     (ix, l)))
      | Inr a => Inr a)
  | decode_static Tfunction (ix, l) =
    Inr (decode_err
          [Chara (false, true, false, false, true, false, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, true, true, true, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, true, true, true, false),
            Chara (false, false, true, false, true, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, true, true, true, false),
            Chara (true, false, false, true, false, true, true, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, false, false, true, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (true, true, false, false, true, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, true, true, true, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, false, true, true, true, true, false),
            Chara (false, true, true, true, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (true, false, true, true, false, true, true, false),
            Chara (true, false, false, true, false, true, true, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (true, false, false, true, true, true, true, false)]
          (ix, l))
  | decode_static Tbytes (ix, l) =
    Inr (decode_err
          [Chara (false, true, false, false, true, false, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, true, true, true, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, true, true, true, false),
            Chara (false, false, true, false, true, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, true, true, true, false),
            Chara (true, false, false, true, false, true, true, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, false, false, true, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (true, true, false, false, true, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, true, true, true, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, false, true, true, true, true, false),
            Chara (false, true, true, true, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (true, false, true, true, false, true, true, false),
            Chara (true, false, false, true, false, true, true, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (true, false, false, true, true, true, true, false)]
          (ix, l))
  | decode_static Tstring (ix, l) =
    Inr (decode_err
          [Chara (false, true, false, false, true, false, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, true, true, true, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, true, true, true, false),
            Chara (false, false, true, false, true, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, true, true, true, false),
            Chara (true, false, false, true, false, true, true, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, false, false, true, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (true, true, false, false, true, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, true, true, true, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, false, true, true, true, true, false),
            Chara (false, true, true, true, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (true, false, true, true, false, true, true, false),
            Chara (true, false, false, true, false, true, true, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (true, false, false, true, true, true, true, false)]
          (ix, l))
  | decode_static (Tarray v) (ix, l) =
    Inr (decode_err
          [Chara (false, true, false, false, true, false, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, true, true, true, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, true, true, true, false),
            Chara (false, false, true, false, true, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, true, true, true, false),
            Chara (true, false, false, true, false, true, true, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, false, false, true, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (true, true, false, false, true, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, true, true, true, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, false, true, true, true, true, false),
            Chara (false, true, true, true, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (true, false, true, true, false, true, true, false),
            Chara (true, false, false, true, false, true, true, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (false, true, false, false, true, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (true, false, false, true, true, true, true, false)]
          (ix, l))
and decode_static_tup [] (ix, l) = Inl []
  | decode_static_tup (t :: ts) (ix, l) =
    (case decode_static t (ix, l)
      of Inl v =>
        (case decode_static_tup ts (plus_inta ix (abi_static_size t), l)
          of Inl vs => Inl (v :: vs) | Inr a => Inr a)
      | Inr a => Inr a);

fun decodea t (ix, l) =
  (if less_int ix Zero_int
    then Inr (decode_err
               [Chara (false, false, true, false, true, false, true, false),
                 Chara (false, true, false, false, true, true, true, false),
                 Chara (true, false, false, true, false, true, true, false),
                 Chara (true, false, true, false, false, true, true, false),
                 Chara (false, false, true, false, false, true, true, false),
                 Chara (false, false, false, false, false, true, false, false),
                 Chara (false, false, true, false, true, true, true, false),
                 Chara (true, true, true, true, false, true, true, false),
                 Chara (false, false, false, false, false, true, false, false),
                 Chara (false, false, true, false, false, true, true, false),
                 Chara (true, false, true, false, false, true, true, false),
                 Chara (true, true, false, false, false, true, true, false),
                 Chara (true, true, true, true, false, true, true, false),
                 Chara (false, false, true, false, false, true, true, false),
                 Chara (true, false, true, false, false, true, true, false),
                 Chara (false, false, false, false, false, true, false, false),
                 Chara (true, false, false, false, false, true, true, false),
                 Chara (false, false, true, false, true, true, true, false),
                 Chara (false, false, false, false, false, true, false, false),
                 Chara (true, false, false, false, false, true, true, false),
                 Chara (false, false, false, false, false, true, false, false),
                 Chara (false, true, true, true, false, true, true, false),
                 Chara (true, false, true, false, false, true, true, false),
                 Chara (true, true, true, false, false, true, true, false),
                 Chara (true, false, false, false, false, true, true, false),
                 Chara (false, false, true, false, true, true, true, false),
                 Chara (true, false, false, true, false, true, true, false),
                 Chara (false, true, true, false, true, true, true, false),
                 Chara (true, false, true, false, false, true, true, false),
                 Chara (false, false, false, false, false, true, false, false),
                 Chara (true, false, false, true, false, true, true, false),
                 Chara (false, true, true, true, false, true, true, false),
                 Chara (false, false, true, false, false, true, true, false),
                 Chara (true, false, true, false, false, true, true, false),
                 Chara (false, false, false, true, true, true, true, false)]
               (ix, l))
    else (if less_int (of_nat semiring_1_int (size_list l)) ix
           then Inr (decode_err
                      [Chara (false, false, true, false, true, false, true,
                               false),
                        Chara (false, true, false, false, true, true, true,
                                false),
                        Chara (true, false, false, true, false, true, true,
                                false),
                        Chara (true, false, true, false, false, true, true,
                                false),
                        Chara (false, false, true, false, false, true, true,
                                false),
                        Chara (false, false, false, false, false, true, false,
                                false),
                        Chara (false, false, true, false, true, true, true,
                                false),
                        Chara (true, true, true, true, false, true, true,
                                false),
                        Chara (false, false, false, false, false, true, false,
                                false),
                        Chara (false, false, true, false, false, true, true,
                                false),
                        Chara (true, false, true, false, false, true, true,
                                false),
                        Chara (true, true, false, false, false, true, true,
                                false),
                        Chara (true, true, true, true, false, true, true,
                                false),
                        Chara (false, false, true, false, false, true, true,
                                false),
                        Chara (true, false, true, false, false, true, true,
                                false),
                        Chara (false, false, false, false, false, true, false,
                                false),
                        Chara (true, false, false, false, false, true, true,
                                false),
                        Chara (false, false, true, false, true, true, true,
                                false),
                        Chara (false, false, false, false, false, true, false,
                                false),
                        Chara (true, false, false, false, false, true, true,
                                false),
                        Chara (false, true, true, true, false, true, true,
                                false),
                        Chara (false, false, false, false, false, true, false,
                                false),
                        Chara (true, false, false, true, false, true, true,
                                false),
                        Chara (false, true, true, true, false, true, true,
                                false),
                        Chara (false, false, true, false, false, true, true,
                                false),
                        Chara (true, false, true, false, false, true, true,
                                false),
                        Chara (false, false, false, true, true, true, true,
                                false),
                        Chara (false, false, false, false, false, true, false,
                                false),
                        Chara (true, true, true, true, false, true, true,
                                false),
                        Chara (true, false, true, false, true, true, true,
                                false),
                        Chara (false, false, true, false, true, true, true,
                                false),
                        Chara (false, false, false, false, false, true, false,
                                false),
                        Chara (true, true, true, true, false, true, true,
                                false),
                        Chara (false, true, true, false, false, true, true,
                                false),
                        Chara (false, false, false, false, false, true, false,
                                false),
                        Chara (false, true, false, false, true, true, true,
                                false),
                        Chara (true, false, false, false, false, true, true,
                                false),
                        Chara (false, true, true, true, false, true, true,
                                false),
                        Chara (true, true, true, false, false, true, true,
                                false),
                        Chara (true, false, true, false, false, true, true,
                                false)]
                      (ix, l))
           else let
                  val la = drop (nat ix) l;
                in
                  (if abi_type_isstatic t
                    then (if less_int (of_nat semiring_1_int (size_list l))
                               (plus_inta (abi_static_size t) ix)
                           then Inr (decode_err
                                      [Chara
 (false, false, true, false, true, false, true, false),
Chara (true, true, true, true, false, true, true, false),
Chara (true, true, true, true, false, true, true, false),
Chara (false, false, false, false, false, true, false, false),
Chara (false, true, true, false, false, true, true, false),
Chara (true, false, true, false, false, true, true, false),
Chara (true, true, true, false, true, true, true, false),
Chara (false, false, false, false, false, true, false, false),
Chara (false, true, false, false, false, true, true, false),
Chara (true, false, false, true, true, true, true, false),
Chara (false, false, true, false, true, true, true, false),
Chara (true, false, true, false, false, true, true, false),
Chara (true, true, false, false, true, true, true, false),
Chara (false, false, false, false, false, true, false, false),
Chara (false, true, true, false, false, true, true, false),
Chara (true, true, true, true, false, true, true, false),
Chara (false, true, false, false, true, true, true, false),
Chara (false, false, false, false, false, true, false, false),
Chara (true, true, true, false, false, true, true, false),
Chara (true, false, false, true, false, true, true, false),
Chara (false, true, true, false, true, true, true, false),
Chara (true, false, true, false, false, true, true, false),
Chara (false, true, true, true, false, true, true, false),
Chara (false, false, false, false, false, true, false, false),
Chara (true, true, false, false, true, true, true, false),
Chara (false, false, true, false, true, true, true, false),
Chara (true, false, false, false, false, true, true, false),
Chara (false, false, true, false, true, true, true, false),
Chara (true, false, false, true, false, true, true, false),
Chara (true, true, false, false, false, true, true, false),
Chara (false, false, false, false, false, true, false, false),
Chara (false, false, true, false, true, true, true, false),
Chara (true, false, false, true, true, true, true, false),
Chara (false, false, false, false, true, true, true, false),
Chara (true, false, true, false, false, true, true, false)]
                                      (ix, l))
                           else (case decode_static t (ix, l)
                                  of Inl v => Inl (v, abi_static_size t)
                                  | Inr a => Inr a))
                    else (case t
                           of Tuint _ =>
                             Inr (decode_err
                                   [Chara (false, false, true, false, true,
    false, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, false, false, true, false,
     true, true, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (true, false, true, false, true,
     true, true, false),
                                     Chara (false, false, true, true, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, true, false, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (true, false, false, false, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false)]
                                   (ix, l))
                           | Tsint _ =>
                             Inr (decode_err
                                   [Chara (false, false, true, false, true,
    false, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, false, false, true, false,
     true, true, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (true, false, true, false, true,
     true, true, false),
                                     Chara (false, false, true, true, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, true, false, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (true, false, false, false, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false)]
                                   (ix, l))
                           | Taddr =>
                             Inr (decode_err
                                   [Chara (false, false, true, false, true,
    false, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, false, false, true, false,
     true, true, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (true, false, true, false, true,
     true, true, false),
                                     Chara (false, false, true, true, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, true, false, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (true, false, false, false, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false)]
                                   (ix, l))
                           | Tbool =>
                             Inr (decode_err
                                   [Chara (false, false, true, false, true,
    false, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, false, false, true, false,
     true, true, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (true, false, true, false, true,
     true, true, false),
                                     Chara (false, false, true, true, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, true, false, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (true, false, false, false, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false)]
                                   (ix, l))
                           | Tfixed (_, _) =>
                             Inr (decode_err
                                   [Chara (false, false, true, false, true,
    false, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, false, false, true, false,
     true, true, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (true, false, true, false, true,
     true, true, false),
                                     Chara (false, false, true, true, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, true, false, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (true, false, false, false, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false)]
                                   (ix, l))
                           | Tufixed (_, _) =>
                             Inr (decode_err
                                   [Chara (false, false, true, false, true,
    false, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, false, false, true, false,
     true, true, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (true, false, true, false, true,
     true, true, false),
                                     Chara (false, false, true, true, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, true, false, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (true, false, false, false, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false)]
                                   (ix, l))
                           | Tfbytes _ =>
                             Inr (decode_err
                                   [Chara (false, false, true, false, true,
    false, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, false, false, true, false,
     true, true, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (true, false, true, false, true,
     true, true, false),
                                     Chara (false, false, true, true, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, true, false, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (true, false, false, false, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false)]
                                   (ix, l))
                           | Tfunction =>
                             Inr (decode_err
                                   [Chara (false, false, true, false, true,
    false, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, false, false, true, false,
     true, true, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, true,
     true, true, false),
                                     Chara (false, false, false, true, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (true, false, true, false, true,
     true, true, false),
                                     Chara (false, false, true, true, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, true, false, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false),
                                     Chara (true, false, false, false, false,
     true, true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (false, false, false, false, false,
     true, false, false),
                                     Chara (true, true, false, false, false,
     true, true, false),
                                     Chara (true, true, true, true, false, true,
     true, false),
                                     Chara (false, false, true, false, false,
     true, true, false),
                                     Chara (true, false, true, false, false,
     true, true, false)]
                                   (ix, l))
                           | Tfarray (ta, n) =>
                             let
                               val ts =
                                 replicate (nat (of_nat semiring_1_int n)) ta;
                             in
                               (case decode_dyn_tuple_heads ts Zero_int (ix, l)
                                 of Inl (vos,
  (idxs, (byteoffset, bytes_parsed)))
                                   => (case
decode_dyn_tuple_tails idxs ts vos byteoffset (ix, l)
of Inl (vs, bytes_parseda) =>
  Inl (Vfarray (ta, n, vs), plus_inta bytes_parsed bytes_parseda)
| Inr a => Inr a)
                                 | Inr a => Inr a)
                             end
                           | Ttuple ts =>
                             (case decode_dyn_tuple_heads ts Zero_int (ix, l)
                               of Inl (vos, (idxs, (byteoffset, bytes_parsed)))
                                 => (case decode_dyn_tuple_tails idxs ts vos
    byteoffset (ix, l)
                                      of Inl (vs, bytes_parseda) =>
Inl (Vtuple (ts, vs), plus_inta bytes_parsed bytes_parseda)
                                      | Inr a => Inr a)
                               | Inr a => Inr a)
                           | Tbytes =>
                             (if less_int (of_nat semiring_1_int (size_list l))
                                   (plus_inta
                                     (Pos (Bit0
    (Bit0 (Bit0 (Bit0 (Bit0 One))))))
                                     ix)
                               then Inr (decode_err
  [Chara (false, false, true, false, true, false, true, false),
    Chara (true, true, true, true, false, true, true, false),
    Chara (true, true, true, true, false, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (false, true, true, false, false, true, true, false),
    Chara (true, false, true, false, false, true, true, false),
    Chara (true, true, true, false, true, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (false, true, false, false, false, true, true, false),
    Chara (true, false, false, true, true, true, true, false),
    Chara (false, false, true, false, true, true, true, false),
    Chara (true, false, true, false, false, true, true, false),
    Chara (true, true, false, false, true, true, true, false),
    Chara (true, true, false, true, true, true, false, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (true, true, false, false, false, true, true, false),
    Chara (true, true, true, true, false, true, true, false),
    Chara (true, false, true, false, true, true, true, false),
    Chara (false, false, true, true, false, true, true, false),
    Chara (false, false, true, false, false, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (false, true, true, true, false, true, true, false),
    Chara (true, true, true, true, false, true, true, false),
    Chara (false, false, true, false, true, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (false, true, false, false, true, true, true, false),
    Chara (true, false, true, false, false, true, true, false),
    Chara (true, false, false, false, false, true, true, false),
    Chara (false, false, true, false, false, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (false, true, false, false, false, true, true, false),
    Chara (true, false, false, true, true, true, true, false),
    Chara (false, false, true, false, true, true, true, false),
    Chara (true, false, true, false, false, true, true, false),
    Chara (true, true, false, false, true, true, true, false),
    Chara (false, false, true, false, true, true, true, false),
    Chara (false, true, false, false, true, true, true, false),
    Chara (true, false, true, false, false, true, true, false),
    Chara (true, false, false, false, false, true, true, false),
    Chara (true, false, true, true, false, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (true, true, false, false, true, true, true, false),
    Chara (true, false, false, true, false, true, true, false),
    Chara (false, true, false, true, true, true, true, false),
    Chara (true, false, true, false, false, true, true, false)]
  (ix, l))
                               else let
                                      val sz =
decode_uint (take (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))) la);
                                    in
                                      (if less_int
    (of_nat semiring_1_int (size_list l))
    (plus_inta (plus_inta sz (Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))) ix)
then Inr (decode_err
           [Chara (false, true, true, false, false, false, true, false),
             Chara (true, false, true, false, false, true, true, false),
             Chara (true, true, true, false, true, true, true, false),
             Chara (true, false, true, false, false, true, true, false),
             Chara (false, true, false, false, true, true, true, false),
             Chara (false, false, false, false, false, true, false, false),
             Chara (false, true, false, false, false, true, true, false),
             Chara (true, false, false, true, true, true, true, false),
             Chara (false, false, true, false, true, true, true, false),
             Chara (true, false, true, false, false, true, true, false),
             Chara (true, true, false, false, true, true, true, false),
             Chara (false, false, false, false, false, true, false, false),
             Chara (false, true, false, false, true, true, true, false),
             Chara (true, false, true, false, false, true, true, false),
             Chara (true, false, true, true, false, true, true, false),
             Chara (true, false, false, false, false, true, true, false),
             Chara (true, false, false, true, false, true, true, false),
             Chara (false, true, true, true, false, true, true, false),
             Chara (true, false, false, true, false, true, true, false),
             Chara (false, true, true, true, false, true, true, false),
             Chara (true, true, true, false, false, true, true, false),
             Chara (false, false, false, false, false, true, false, false),
             Chara (false, false, true, false, true, true, true, false),
             Chara (false, false, false, true, false, true, true, false),
             Chara (true, false, false, false, false, true, true, false),
             Chara (false, true, true, true, false, true, true, false),
             Chara (false, false, false, false, false, true, false, false),
             Chara (false, true, false, false, false, true, true, false),
             Chara (true, false, false, true, true, true, true, false),
             Chara (false, false, true, false, true, true, true, false),
             Chara (true, false, true, false, false, true, true, false),
             Chara (true, true, false, false, true, true, true, false),
             Chara (false, false, true, false, true, true, true, false),
             Chara (false, true, false, false, true, true, true, false),
             Chara (true, false, true, false, false, true, true, false),
             Chara (true, false, false, false, false, true, true, false),
             Chara (true, false, true, true, false, true, true, false),
             Chara (false, false, false, false, false, true, false, false),
             Chara (true, true, false, false, true, true, true, false),
             Chara (true, false, false, true, false, true, true, false),
             Chara (false, true, false, true, true, true, true, false),
             Chara (true, false, true, false, false, true, true, false)]
           (ix, l))
else (if check_padding (nat sz)
           (drop (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))) la)
       then Inl (Vbytes
                   (take (nat sz)
                     (drop (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))
                       la)),
                  plus_inta (of_nat semiring_1_int (skip_padding (nat sz)))
                    (Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))))
       else Inr (decode_err
                  [Chara (true, false, false, true, false, false, true, false),
                    Chara (false, true, true, true, false, true, true, false),
                    Chara (false, true, true, false, true, true, true, false),
                    Chara (true, false, false, false, false, true, true, false),
                    Chara (false, false, true, true, false, true, true, false),
                    Chara (true, false, false, true, false, true, true, false),
                    Chara (false, false, true, false, false, true, true, false),
                    Chara (false, false, false, false, false, true, false,
                            false),
                    Chara (false, true, false, false, false, true, true, false),
                    Chara (true, false, false, true, true, true, true, false),
                    Chara (false, false, true, false, true, true, true, false),
                    Chara (true, false, true, false, false, true, true, false),
                    Chara (true, true, false, false, true, true, true, false),
                    Chara (false, false, false, false, false, true, false,
                            false),
                    Chara (false, false, false, false, true, true, true, false),
                    Chara (true, false, false, false, false, true, true, false),
                    Chara (false, false, true, false, false, true, true, false),
                    Chara (false, false, true, false, false, true, true, false),
                    Chara (true, false, false, true, false, true, true, false),
                    Chara (false, true, true, true, false, true, true, false),
                    Chara (true, true, true, false, false, true, true, false)]
                  (ix, l))))
                                    end)
                           | Tstring =>
                             (if less_int (of_nat semiring_1_int (size_list l))
                                   (plus_inta
                                     (Pos (Bit0
    (Bit0 (Bit0 (Bit0 (Bit0 One))))))
                                     ix)
                               then Inr (decode_err
  [Chara (false, false, true, false, true, false, true, false),
    Chara (true, true, true, true, false, true, true, false),
    Chara (true, true, true, true, false, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (false, true, true, false, false, true, true, false),
    Chara (true, false, true, false, false, true, true, false),
    Chara (true, true, true, false, true, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (false, true, false, false, false, true, true, false),
    Chara (true, false, false, true, true, true, true, false),
    Chara (false, false, true, false, true, true, true, false),
    Chara (true, false, true, false, false, true, true, false),
    Chara (true, true, false, false, true, true, true, false),
    Chara (true, true, false, true, true, true, false, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (true, true, false, false, false, true, true, false),
    Chara (true, true, true, true, false, true, true, false),
    Chara (true, false, true, false, true, true, true, false),
    Chara (false, false, true, true, false, true, true, false),
    Chara (false, false, true, false, false, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (false, true, true, true, false, true, true, false),
    Chara (true, true, true, true, false, true, true, false),
    Chara (false, false, true, false, true, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (false, true, false, false, true, true, true, false),
    Chara (true, false, true, false, false, true, true, false),
    Chara (true, false, false, false, false, true, true, false),
    Chara (false, false, true, false, false, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (true, true, false, false, true, true, true, false),
    Chara (false, false, true, false, true, true, true, false),
    Chara (false, true, false, false, true, true, true, false),
    Chara (true, false, false, true, false, true, true, false),
    Chara (false, true, true, true, false, true, true, false),
    Chara (true, true, true, false, false, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (true, true, false, false, true, true, true, false),
    Chara (true, false, false, true, false, true, true, false),
    Chara (false, true, false, true, true, true, true, false),
    Chara (true, false, true, false, false, true, true, false)]
  (ix, l))
                               else let
                                      val sz =
decode_uint (take (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))) la);
                                    in
                                      (if less_int
    (of_nat semiring_1_int (size_list l))
    (plus_inta (plus_inta sz (Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))) ix)
then Inr (decode_err
           [Chara (false, true, true, false, false, false, true, false),
             Chara (true, false, true, false, false, true, true, false),
             Chara (true, true, true, false, true, true, true, false),
             Chara (true, false, true, false, false, true, true, false),
             Chara (false, true, false, false, true, true, true, false),
             Chara (false, false, false, false, false, true, false, false),
             Chara (false, true, false, false, false, true, true, false),
             Chara (true, false, false, true, true, true, true, false),
             Chara (false, false, true, false, true, true, true, false),
             Chara (true, false, true, false, false, true, true, false),
             Chara (true, true, false, false, true, true, true, false),
             Chara (false, false, false, false, false, true, false, false),
             Chara (false, true, false, false, true, true, true, false),
             Chara (true, false, true, false, false, true, true, false),
             Chara (true, false, true, true, false, true, true, false),
             Chara (true, false, false, false, false, true, true, false),
             Chara (true, false, false, true, false, true, true, false),
             Chara (false, true, true, true, false, true, true, false),
             Chara (true, false, false, true, false, true, true, false),
             Chara (false, true, true, true, false, true, true, false),
             Chara (true, true, true, false, false, true, true, false),
             Chara (false, false, false, false, false, true, false, false),
             Chara (false, false, true, false, true, true, true, false),
             Chara (false, false, false, true, false, true, true, false),
             Chara (true, false, false, false, false, true, true, false),
             Chara (false, true, true, true, false, true, true, false),
             Chara (false, false, false, false, false, true, false, false),
             Chara (true, true, false, false, true, true, true, false),
             Chara (false, false, true, false, true, true, true, false),
             Chara (false, true, false, false, true, true, true, false),
             Chara (true, false, false, true, false, true, true, false),
             Chara (false, true, true, true, false, true, true, false),
             Chara (true, true, true, false, false, true, true, false),
             Chara (false, false, false, false, false, true, false, false),
             Chara (true, true, false, false, true, true, true, false),
             Chara (true, false, false, true, false, true, true, false),
             Chara (false, true, false, true, true, true, true, false),
             Chara (true, false, true, false, false, true, true, false)]
           (ix, l))
else (if check_padding (nat sz)
           (drop (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))) la)
       then Inl (Vstring
                   (bytes_to_string
                     (take (nat sz)
                       (drop (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))
                         la))),
                  plus_inta (of_nat semiring_1_int (skip_padding (nat sz)))
                    (Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))))
       else Inr (decode_err
                  [Chara (true, false, false, true, false, false, true, false),
                    Chara (false, true, true, true, false, true, true, false),
                    Chara (false, true, true, false, true, true, true, false),
                    Chara (true, false, false, false, false, true, true, false),
                    Chara (false, false, true, true, false, true, true, false),
                    Chara (true, false, false, true, false, true, true, false),
                    Chara (false, false, true, false, false, true, true, false),
                    Chara (false, false, false, false, false, true, false,
                            false),
                    Chara (true, true, false, false, true, true, true, false),
                    Chara (false, false, true, false, true, true, true, false),
                    Chara (false, true, false, false, true, true, true, false),
                    Chara (true, false, false, true, false, true, true, false),
                    Chara (false, true, true, true, false, true, true, false),
                    Chara (true, true, true, false, false, true, true, false),
                    Chara (false, false, false, false, false, true, false,
                            false),
                    Chara (false, false, false, false, true, true, true, false),
                    Chara (true, false, false, false, false, true, true, false),
                    Chara (false, false, true, false, false, true, true, false),
                    Chara (false, false, true, false, false, true, true, false),
                    Chara (true, false, false, true, false, true, true, false),
                    Chara (false, true, true, true, false, true, true, false),
                    Chara (true, true, true, false, false, true, true, false)]
                  (ix, l))))
                                    end)
                           | Tarray ta =>
                             (if less_int (of_nat semiring_1_int (size_list l))
                                   (plus_inta
                                     (Pos (Bit0
    (Bit0 (Bit0 (Bit0 (Bit0 One))))))
                                     ix)
                               then Inr (decode_err
  [Chara (false, false, true, false, true, false, true, false),
    Chara (true, true, true, true, false, true, true, false),
    Chara (true, true, true, true, false, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (false, true, true, false, false, true, true, false),
    Chara (true, false, true, false, false, true, true, false),
    Chara (true, true, true, false, true, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (false, true, false, false, false, true, true, false),
    Chara (true, false, false, true, true, true, true, false),
    Chara (false, false, true, false, true, true, true, false),
    Chara (true, false, true, false, false, true, true, false),
    Chara (true, true, false, false, true, true, true, false),
    Chara (true, true, false, true, true, true, false, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (true, true, false, false, false, true, true, false),
    Chara (true, true, true, true, false, true, true, false),
    Chara (true, false, true, false, true, true, true, false),
    Chara (false, false, true, true, false, true, true, false),
    Chara (false, false, true, false, false, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (false, true, true, true, false, true, true, false),
    Chara (true, true, true, true, false, true, true, false),
    Chara (false, false, true, false, true, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (false, true, false, false, true, true, true, false),
    Chara (true, false, true, false, false, true, true, false),
    Chara (true, false, false, false, false, true, true, false),
    Chara (false, false, true, false, false, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (true, false, false, false, false, true, true, false),
    Chara (false, true, false, false, true, true, true, false),
    Chara (false, true, false, false, true, true, true, false),
    Chara (true, false, false, false, false, true, true, false),
    Chara (true, false, false, true, true, true, true, false),
    Chara (false, false, false, false, false, true, false, false),
    Chara (true, true, false, false, true, true, true, false),
    Chara (true, false, false, true, false, true, true, false),
    Chara (false, true, false, true, true, true, true, false),
    Chara (true, false, true, false, false, true, true, false)]
  (ix, l))
                               else let
                                      val n =
decode_uint (take (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))) la);
                                      val ts = replicate (nat n) ta;
                                    in
                                      (case
decode_dyn_tuple_heads ts Zero_int
  (plus_inta ix (Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))), l)
of Inl (vos, (idxs, (byteoffset, bytes_parsed))) =>
  (case decode_dyn_tuple_tails idxs ts vos byteoffset
          (plus_inta ix (Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))), l)
    of Inl (vs, bytes_parseda) =>
      Inl (Varray (ta, vs),
            plus_inta (plus_inta bytes_parsed bytes_parseda)
              (Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))))
    | Inr a => Inr a)
| Inr a => Inr a)
                                    end)))
                end))
and decode_dyn_tuple_heads [] n (ix, l) = Inl ([], ([], (n, Zero_int)))
  | decode_dyn_tuple_heads (th :: tt) n (ix, l) =
    let
      val la = drop (nat (plus_inta ix n)) l;
    in
      (if abi_type_isstatic th
        then (case decodea th (plus_inta ix n, l)
               of Inl (v, bytes_parsed) =>
                 (case decode_dyn_tuple_heads tt
                         (plus_inta n
                           (of_nat semiring_1_int (nat (abi_static_size th))))
                         (ix, l)
                   of Inl (vos, (idxs, (na, bytes_parseda))) =>
                     Inl (SOME v :: vos,
                           (NONE :: idxs,
                             (na, plus_inta bytes_parsed bytes_parseda)))
                   | Inr a => Inr a)
               | Inr a => Inr a)
        else (if less_nat (size_list la)
                   (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))
               then Inr (decode_err
                          [Chara (false, false, true, false, true, false, true,
                                   false),
                            Chara (true, true, true, true, false, true, true,
                                    false),
                            Chara (true, true, true, true, false, true, true,
                                    false),
                            Chara (false, false, false, false, false, true,
                                    false, false),
                            Chara (false, true, true, false, false, true, true,
                                    false),
                            Chara (true, false, true, false, false, true, true,
                                    false),
                            Chara (true, true, true, false, true, true, true,
                                    false),
                            Chara (false, false, false, false, false, true,
                                    false, false),
                            Chara (false, true, false, false, false, true, true,
                                    false),
                            Chara (true, false, false, true, true, true, true,
                                    false),
                            Chara (false, false, true, false, true, true, true,
                                    false),
                            Chara (true, false, true, false, false, true, true,
                                    false),
                            Chara (true, true, false, false, true, true, true,
                                    false),
                            Chara (true, true, false, true, true, true, false,
                                    false),
                            Chara (false, false, false, false, false, true,
                                    false, false),
                            Chara (true, true, false, false, false, true, true,
                                    false),
                            Chara (true, true, true, true, false, true, true,
                                    false),
                            Chara (true, false, true, false, true, true, true,
                                    false),
                            Chara (false, false, true, true, false, true, true,
                                    false),
                            Chara (false, false, true, false, false, true, true,
                                    false),
                            Chara (false, false, false, false, false, true,
                                    false, false),
                            Chara (false, true, true, true, false, true, true,
                                    false),
                            Chara (true, true, true, true, false, true, true,
                                    false),
                            Chara (false, false, true, false, true, true, true,
                                    false),
                            Chara (false, false, false, false, false, true,
                                    false, false),
                            Chara (false, true, false, false, true, true, true,
                                    false),
                            Chara (true, false, true, false, false, true, true,
                                    false),
                            Chara (true, false, false, false, false, true, true,
                                    false),
                            Chara (false, false, true, false, false, true, true,
                                    false),
                            Chara (false, false, false, false, false, true,
                                    false, false),
                            Chara (false, false, true, false, true, true, true,
                                    false),
                            Chara (true, false, true, false, true, true, true,
                                    false),
                            Chara (false, false, false, false, true, true, true,
                                    false),
                            Chara (false, false, true, true, false, true, true,
                                    false),
                            Chara (true, false, true, false, false, true, true,
                                    false),
                            Chara (false, false, false, false, false, true,
                                    false, false),
                            Chara (false, false, false, true, false, true, true,
                                    false),
                            Chara (true, false, true, false, false, true, true,
                                    false),
                            Chara (true, false, false, false, false, true, true,
                                    false),
                            Chara (false, false, true, false, false, true, true,
                                    false)]
                          (ix, l))
               else let
                      val sz =
                        decode_sint
                          (take (nat_of_num
                                  (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))
                            la);
                    in
                      (case decode_dyn_tuple_heads tt
                              (plus_inta n
                                (Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))))
                              (ix, l)
                        of Inl (vos, (idxs, (na, bytes_parsed))) =>
                          Inl (NONE :: vos,
                                (SOME (plus_inta ix sz) :: idxs,
                                  (na, plus_inta bytes_parsed
 (Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))))))
                        | Inr a => Inr a)
                    end))
    end
and decode_dyn_tuple_tails [] [] [] uu (ix, l) = Inl ([], Zero_int)
  | decode_dyn_tuple_tails (NONE :: t) (th :: tt) (SOME vh :: vt) offset (ix, l)
    = (case decode_dyn_tuple_tails t tt vt offset (ix, l)
        of Inl (vs, bytes_parsed) => Inl (vh :: vs, bytes_parsed)
        | Inr a => Inr a)
  | decode_dyn_tuple_tails (SOME toffset :: t) (th :: tt) (NONE :: vt) offset
    (ix, l) =
    let
      val ixa = toffset;
    in
      (case decodea th (ixa, l)
        of Inl (v, bytes_parsed) =>
          let
            val offseta = plus_inta offset bytes_parsed;
          in
            (case decode_dyn_tuple_tails t tt vt offseta (ix, l)
              of Inl (vs, bytes_parseda) =>
                Inl (v :: vs, plus_inta bytes_parsed bytes_parseda)
              | Inr a => Inr a)
          end
        | Inr a => Inr a)
    end
  | decode_dyn_tuple_tails (SOME vb :: va) [] ux uy (ix, l) =
    Inr (decode_err
          [Chara (true, true, false, false, true, false, true, false),
            Chara (false, false, false, true, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (true, false, true, false, true, true, true, false),
            Chara (false, false, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, true, false, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false)]
          (ix, l))
  | decode_dyn_tuple_tails (SOME vb :: va) uw [] uy (ix, l) =
    Inr (decode_err
          [Chara (true, true, false, false, true, false, true, false),
            Chara (false, false, false, true, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (true, false, true, false, true, true, true, false),
            Chara (false, false, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, true, false, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false)]
          (ix, l))
  | decode_dyn_tuple_tails (SOME vb :: va) uw (SOME vd :: vc) uy (ix, l) =
    Inr (decode_err
          [Chara (true, true, false, false, true, false, true, false),
            Chara (false, false, false, true, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (true, false, true, false, true, true, true, false),
            Chara (false, false, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, true, false, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false)]
          (ix, l))
  | decode_dyn_tuple_tails (v :: va) [] ux uy (ix, l) =
    Inr (decode_err
          [Chara (true, true, false, false, true, false, true, false),
            Chara (false, false, false, true, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (true, false, true, false, true, true, true, false),
            Chara (false, false, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, true, false, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false)]
          (ix, l))
  | decode_dyn_tuple_tails (v :: va) uw [] uy (ix, l) =
    Inr (decode_err
          [Chara (true, true, false, false, true, false, true, false),
            Chara (false, false, false, true, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (true, false, true, false, true, true, true, false),
            Chara (false, false, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, true, false, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false)]
          (ix, l))
  | decode_dyn_tuple_tails (NONE :: va) uw (NONE :: vc) uy (ix, l) =
    Inr (decode_err
          [Chara (true, true, false, false, true, false, true, false),
            Chara (false, false, false, true, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (true, false, true, false, true, true, true, false),
            Chara (false, false, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, true, false, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false)]
          (ix, l))
  | decode_dyn_tuple_tails [] (v :: va) ux uy (ix, l) =
    Inr (decode_err
          [Chara (true, true, false, false, true, false, true, false),
            Chara (false, false, false, true, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (true, false, true, false, true, true, true, false),
            Chara (false, false, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, true, false, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false)]
          (ix, l))
  | decode_dyn_tuple_tails uv (v :: va) [] uy (ix, l) =
    Inr (decode_err
          [Chara (true, true, false, false, true, false, true, false),
            Chara (false, false, false, true, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (true, false, true, false, true, true, true, false),
            Chara (false, false, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, true, false, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false)]
          (ix, l))
  | decode_dyn_tuple_tails [] uw (v :: va) uy (ix, l) =
    Inr (decode_err
          [Chara (true, true, false, false, true, false, true, false),
            Chara (false, false, false, true, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (true, false, true, false, true, true, true, false),
            Chara (false, false, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, true, false, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false)]
          (ix, l))
  | decode_dyn_tuple_tails uv [] (v :: va) uy (ix, l) =
    Inr (decode_err
          [Chara (true, true, false, false, true, false, true, false),
            Chara (false, false, false, true, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (true, false, true, false, true, true, true, false),
            Chara (false, false, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, true, false, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false),
            Chara (true, false, false, false, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (false, false, false, false, false, true, false, false),
            Chara (true, true, false, false, false, true, true, false),
            Chara (true, true, true, true, false, true, true, false),
            Chara (false, false, true, false, false, true, true, false),
            Chara (true, false, true, false, false, true, true, false)]
          (ix, l));

fun decode t l =
  (if abi_type_valid t
    then (case decodea t (Zero_int, l) of Inl (v, _) => Inl v | Inr a => Inr a)
    else Inr [Chara (true, false, false, true, false, false, true, false),
               Chara (false, true, true, true, false, true, true, false),
               Chara (false, true, true, false, true, true, true, false),
               Chara (true, false, false, false, false, true, true, false),
               Chara (false, false, true, true, false, true, true, false),
               Chara (true, false, false, true, false, true, true, false),
               Chara (false, false, true, false, false, true, true, false),
               Chara (false, false, false, false, false, true, false, false),
               Chara (true, false, false, false, false, false, true, false),
               Chara (false, true, false, false, false, false, true, false),
               Chara (true, false, false, true, false, false, true, false),
               Chara (false, false, false, false, false, true, false, false),
               Chara (false, false, true, false, true, true, true, false),
               Chara (true, false, false, true, true, true, true, false),
               Chara (false, false, false, false, true, true, true, false),
               Chara (true, false, true, false, false, true, true, false)]);

fun array_value_valid_aux t l =
  uint_value_valid
    (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))))))
    (of_nat semiring_1_int (size_list l)) andalso
    list_all (fn v => equal_abi_typea (abi_get_type v) t) l;

fun function_value_valid i1 i2 =
  uint_value_valid
    (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit1 (Bit0 One)))))))) i1 andalso
    uint_value_valid (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))) i2;

fun string_value_valid s =
  uint_value_valid
    (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))))))
    (of_nat semiring_1_int (size_list s));

fun bytes_value_valid bs =
  uint_value_valid
    (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))))))
    (of_nat semiring_1_int (size_list bs));

fun bool_value_valid b = true;

fun abi_value_valid_aux (Vuint (n, i)) = uint_value_valid n i
  | abi_value_valid_aux (Vsint (n, i)) = sint_value_valid n i
  | abi_value_valid_aux (Vaddr i) = addr_value_valid i
  | abi_value_valid_aux (Vbool b) = bool_value_valid b
  | abi_value_valid_aux (Vfixed (m, n, r)) = fixed_value_valid m n r
  | abi_value_valid_aux (Vufixed (m, n, r)) = ufixed_value_valid m n r
  | abi_value_valid_aux (Vfbytes (n, l)) = fbytes_value_valid n l
  | abi_value_valid_aux (Vfunction (i1, i2)) = function_value_valid i1 i2
  | abi_value_valid_aux (Vfarray (t, n, l)) =
    farray_value_valid_aux t n l andalso list_all abi_value_valid_aux l
  | abi_value_valid_aux (Vtuple (ts, vs)) =
    tuple_value_valid_aux ts vs andalso list_all abi_value_valid_aux vs
  | abi_value_valid_aux (Vbytes bs) = bytes_value_valid bs
  | abi_value_valid_aux (Vstring s) = string_value_valid s
  | abi_value_valid_aux (Varray (t, l)) =
    array_value_valid_aux t l andalso list_all abi_value_valid_aux l;

fun abi_value_valid v =
  abi_type_valid (abi_get_type v) andalso abi_value_valid_aux v;

fun bin_split Zero_nat w = (w, Zero_int)
  | bin_split (Suc n) w = let
                            val (w1, w2) = bin_split n (bin_rest w);
                          in
                            (w1, bit w2 (bin_last w))
                          end;

fun bin_rsplit_aux n m c bs =
  (if equal_nat m Zero_nat orelse equal_nat n Zero_nat then bs
    else let
           val a = bin_split n c;
           val (aa, b) = a;
         in
           bin_rsplit_aux n (minus_nat m n) aa (b :: bs)
         end);

fun bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) [];

fun word_rsplit A_ B_ w =
  map (word_of_int (len0_len B_))
    (bin_rsplit (len_of (len0_len B_) Type) (len_of A_ Type, uint A_ w));

fun encode_int i =
  word_rsplit
    (len0_bit0
      (len0_bit0
        (len0_bit0
          (len0_bit0
            (len0_bit0 (len0_bit0 (len0_bit0 (len0_bit0 len0_num1))))))))
    (len_bit0 (len_bit0 (len_bit0 len_num1)))
    (word_of_int
      (len0_bit0
        (len0_bit0
          (len0_bit0
            (len0_bit0
              (len0_bit0 (len0_bit0 (len0_bit0 (len0_bit0 len0_num1))))))))
      i);

fun apsnd f (x, y) = (x, f y);

fun divmod_integer k l =
  (if ((k : IntInf.int) = (0 : IntInf.int))
    then ((0 : IntInf.int), (0 : IntInf.int))
    else (if IntInf.< ((0 : IntInf.int), l)
           then (if IntInf.< ((0 : IntInf.int), k)
                  then IntInf.divMod (IntInf.abs k, IntInf.abs l)
                  else let
                         val (r, s) =
                           IntInf.divMod (IntInf.abs k, IntInf.abs l);
                       in
                         (if ((s : IntInf.int) = (0 : IntInf.int))
                           then (IntInf.~ r, (0 : IntInf.int))
                           else (IntInf.- (IntInf.~ r, (1 : IntInf.int)),
                                  IntInf.- (l, s)))
                       end)
           else (if ((l : IntInf.int) = (0 : IntInf.int))
                  then ((0 : IntInf.int), k)
                  else apsnd IntInf.~
                         (if IntInf.< (k, (0 : IntInf.int))
                           then IntInf.divMod (IntInf.abs k, IntInf.abs l)
                           else let
                                  val (r, s) =
                                    IntInf.divMod (IntInf.abs k, IntInf.abs l);
                                in
                                  (if ((s : IntInf.int) = (0 : IntInf.int))
                                    then (IntInf.~ r, (0 : IntInf.int))
                                    else (IntInf.- (IntInf.~
              r, (1 : IntInf.int)),
   IntInf.- (IntInf.~ l, s)))
                                end))));

fun int_of_integer k =
  (if IntInf.< (k, (0 : IntInf.int))
    then uminus_int (int_of_integer (IntInf.~ k))
    else (if ((k : IntInf.int) = (0 : IntInf.int)) then Zero_int
           else let
                  val (l, j) = divmod_integer k (2 : IntInf.int);
                  val la = times_inta (Pos (Bit0 One)) (int_of_integer l);
                in
                  (if ((j : IntInf.int) = (0 : IntInf.int)) then la
                    else plus_inta la one_inta)
                end));

fun integer_of_char (Chara (b0, b1, b2, b3, b4, b5, b6, b7)) =
  IntInf.+ (IntInf.* (IntInf.+ (IntInf.* (IntInf.+ (IntInf.* (IntInf.+ (IntInf.* (IntInf.+ (IntInf.* (IntInf.+ (IntInf.* (IntInf.+ (IntInf.* (of_bool
                        zero_neq_one_integer
                        b7, (2 : IntInf.int)), of_bool zero_neq_one_integer
         b6), (2 : IntInf.int)), of_bool zero_neq_one_integer
                                   b5), (2 : IntInf.int)), of_bool
                     zero_neq_one_integer
                     b4), (2 : IntInf.int)), of_bool zero_neq_one_integer
       b3), (2 : IntInf.int)), of_bool zero_neq_one_integer
                                 b2), (2 : IntInf.int)), of_bool
                   zero_neq_one_integer
                   b1), (2 : IntInf.int)), of_bool zero_neq_one_integer b0);

fun string_to_bytes s =
  map (fn c =>
        word_of_int (len0_bit0 (len0_bit0 (len0_bit0 len0_num1)))
          (int_of_integer (integer_of_char c)))
    s;

fun pad_bytes l =
  (case divmod_nat (size_list l)
          (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))
    of (_, Zero_nat) => l
    | (_, Suc rem) =>
      l @ replicate
            (minus_nat (nat_of_num (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))
              (Suc rem))
            (word_of_int (len0_bit0 (len0_bit0 (len0_bit0 len0_num1)))
              Zero_int));

fun encode_fbytes n l = pad_bytes (take n l);

fun encode_fixed n r =
  encode_int
    (fst (quotient_of
           (times_rata r
             (power power_rat (of_int (Pos (Bit0 (Bit1 (Bit0 One))))) n))));

fun encode_bool true = encode_int one_inta
  | encode_bool false = encode_int Zero_int;

fun encode_static (Vuint (n, i)) = Inl (encode_int i)
  | encode_static (Vsint (n, i)) = Inl (encode_int i)
  | encode_static (Vaddr a) = Inl (encode_int a)
  | encode_static (Vbool b) = Inl (encode_bool b)
  | encode_static (Vfixed (m, n, r)) = Inl (encode_fixed n r)
  | encode_static (Vufixed (m, n, r)) = Inl (encode_fixed n r)
  | encode_static (Vfbytes (n, l)) = Inl (encode_fbytes n l)
  | encode_static (Vfarray (t, n, l)) =
    (case those_err (map encode_static l) of Inl bs => Inl (concat bs)
      | Inr a => Inr a)
  | encode_static (Vtuple (ts, vs)) =
    (case those_err (map encode_static vs) of Inl bs => Inl (concat bs)
      | Inr a => Inr a)
  | encode_static (Vfunction (v, va)) =
    Inr [Chara (true, true, false, false, false, false, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, true, false, false, true, true, true, false),
          Chara (false, false, true, false, true, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, false, true, true, true, false),
          Chara (true, false, false, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, true, false, false, true, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, false, true, true, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (true, false, true, true, false, true, true, false),
          Chara (true, false, false, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, true, true, false, true, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (true, false, true, false, true, true, true, false),
          Chara (true, false, true, false, false, true, true, false)]
  | encode_static (Vbytes v) =
    Inr [Chara (true, true, false, false, false, false, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, true, false, false, true, true, true, false),
          Chara (false, false, true, false, true, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, false, true, true, true, false),
          Chara (true, false, false, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, true, false, false, true, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, false, true, true, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (true, false, true, true, false, true, true, false),
          Chara (true, false, false, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, true, true, false, true, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (true, false, true, false, true, true, true, false),
          Chara (true, false, true, false, false, true, true, false)]
  | encode_static (Vstring v) =
    Inr [Chara (true, true, false, false, false, false, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, true, false, false, true, true, true, false),
          Chara (false, false, true, false, true, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, false, true, true, true, false),
          Chara (true, false, false, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, true, false, false, true, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, false, true, true, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (true, false, true, true, false, true, true, false),
          Chara (true, false, false, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, true, true, false, true, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (true, false, true, false, true, true, true, false),
          Chara (true, false, true, false, false, true, true, false)]
  | encode_static (Varray (v, va)) =
    Inr [Chara (true, true, false, false, false, false, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, true, false, false, true, true, true, false),
          Chara (false, false, true, false, true, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, false, true, true, true, false),
          Chara (true, false, false, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, true, false, false, true, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, false, true, true, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (true, false, true, true, false, true, true, false),
          Chara (true, false, false, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, true, true, false, true, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (true, false, true, false, true, true, true, false),
          Chara (true, false, true, false, false, true, true, false)];

fun heads_length [] = Zero_int
  | heads_length (h :: t) =
    let
      val tyh = abi_get_type h;
    in
      (if abi_type_isstatic tyh
        then plus_inta (abi_static_size tyh) (heads_length t)
        else plus_inta (Pos (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One))))))
               (heads_length t))
    end;

fun encodea v =
  (if abi_type_isstatic (abi_get_type v) then encode_static v
    else (case v
           of Vuint (_, _) =>
             Inr [Chara (true, true, false, false, true, false, true, false),
                   Chara (false, false, false, true, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (true, false, true, false, true, true, true, false),
                   Chara (false, false, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, true, false, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, false, false, false, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, false, true, false, true, false, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, true, true, true, false, true, true, false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, true, true, false, false, true, false, false),
                   Chara (true, false, false, true, false, true, false, false)]
           | Vsint (_, _) =>
             Inr [Chara (true, true, false, false, true, false, true, false),
                   Chara (false, false, false, true, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (true, false, true, false, true, true, true, false),
                   Chara (false, false, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, true, false, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, false, false, false, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, false, true, false, true, false, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, true, true, true, false, true, true, false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, true, true, false, false, true, false, false),
                   Chara (true, false, false, true, false, true, false, false)]
           | Vaddr _ =>
             Inr [Chara (true, true, false, false, true, false, true, false),
                   Chara (false, false, false, true, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (true, false, true, false, true, true, true, false),
                   Chara (false, false, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, true, false, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, false, false, false, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, false, true, false, true, false, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, true, true, true, false, true, true, false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, true, true, false, false, true, false, false),
                   Chara (true, false, false, true, false, true, false, false)]
           | Vbool _ =>
             Inr [Chara (true, true, false, false, true, false, true, false),
                   Chara (false, false, false, true, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (true, false, true, false, true, true, true, false),
                   Chara (false, false, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, true, false, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, false, false, false, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, false, true, false, true, false, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, true, true, true, false, true, true, false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, true, true, false, false, true, false, false),
                   Chara (true, false, false, true, false, true, false, false)]
           | Vfixed (_, _, _) =>
             Inr [Chara (true, true, false, false, true, false, true, false),
                   Chara (false, false, false, true, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (true, false, true, false, true, true, true, false),
                   Chara (false, false, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, true, false, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, false, false, false, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, false, true, false, true, false, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, true, true, true, false, true, true, false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, true, true, false, false, true, false, false),
                   Chara (true, false, false, true, false, true, false, false)]
           | Vufixed (_, _, _) =>
             Inr [Chara (true, true, false, false, true, false, true, false),
                   Chara (false, false, false, true, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (true, false, true, false, true, true, true, false),
                   Chara (false, false, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, true, false, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, false, false, false, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, false, true, false, true, false, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, true, true, true, false, true, true, false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, true, true, false, false, true, false, false),
                   Chara (true, false, false, true, false, true, false, false)]
           | Vfbytes (_, _) =>
             Inr [Chara (true, true, false, false, true, false, true, false),
                   Chara (false, false, false, true, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (true, false, true, false, true, true, true, false),
                   Chara (false, false, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, true, false, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, false, false, false, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, false, true, false, true, false, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, true, true, true, false, true, true, false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, true, true, false, false, true, false, false),
                   Chara (true, false, false, true, false, true, false, false)]
           | Vfunction (_, _) =>
             Inr [Chara (true, true, false, false, true, false, true, false),
                   Chara (false, false, false, true, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (true, false, true, false, true, true, true, false),
                   Chara (false, false, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, true, false, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, false, false, false, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, false, false, false, false, true, false,
                           false),
                   Chara (false, false, false, true, false, true, false, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (false, true, true, true, false, true, true, false),
                   Chara (true, true, false, false, false, true, true, false),
                   Chara (true, true, true, true, false, true, true, false),
                   Chara (false, false, true, false, false, true, true, false),
                   Chara (true, false, true, false, false, true, true, false),
                   Chara (true, true, true, false, false, true, false, false),
                   Chara (true, false, false, true, false, true, false, false)]
           | Vfarray (_, _, vs) =>
             (case encode_tuple_tails vs Zero_int (heads_length vs)
               of Inl bvs =>
                 (case encode_tuple_heads vs bvs
                   of Inl (heads, tails) => Inl (heads @ tails)
                   | Inr a => Inr a)
               | Inr a => Inr a)
           | Vtuple (_, vs) =>
             (case encode_tuple_tails vs Zero_int (heads_length vs)
               of Inl bvs =>
                 (case encode_tuple_heads vs bvs
                   of Inl (heads, tails) => Inl (heads @ tails)
                   | Inr a => Inr a)
               | Inr a => Inr a)
           | Vbytes l =>
             Inl (encode_int (of_nat semiring_1_int (size_list l)) @
                   pad_bytes l)
           | Vstring s =>
             let
               val bs = string_to_bytes s;
             in
               Inl (encode_int (of_nat semiring_1_int (size_list bs)) @
                     pad_bytes bs)
             end
           | Varray (_, vs) =>
             (case encode_tuple_tails vs Zero_int (heads_length vs)
               of Inl bvs =>
                 (case encode_tuple_heads vs bvs
                   of Inl (heads, tails) =>
                     Inl (encode_int (of_nat semiring_1_int (size_list vs)) @
                           heads @ tails)
                   | Inr a => Inr a)
               | Inr a => Inr a)))
and encode_tuple_heads [] [] = Inl ([], [])
  | encode_tuple_heads (v :: vs) ((offset, bs) :: bss) =
    (if abi_type_isstatic (abi_get_type v)
      then (case encodea v
             of Inl head1 =>
               (case encode_tuple_heads vs bss
                 of Inl (heads, tails) => Inl (head1 @ heads, bs @ tails)
                 | Inr a => Inr a)
             | Inr a => Inr a)
      else (case encode_tuple_heads vs bss
             of Inl (heads, tails) =>
               Inl (encode_int offset @ heads, bs @ tails)
             | Inr a => Inr a))
  | encode_tuple_heads (v :: va) [] =
    Inr [Chara (true, true, false, false, true, false, true, false),
          Chara (false, false, false, true, false, true, true, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (true, false, true, false, true, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, true, false, false, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, false, false, true, false, true, false, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (true, true, true, false, false, true, false, false),
          Chara (true, true, true, true, true, false, true, false),
          Chara (false, false, true, false, true, true, true, false),
          Chara (true, false, true, false, true, true, true, false),
          Chara (false, false, false, false, true, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (true, true, true, true, true, false, true, false),
          Chara (false, false, false, true, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, true, false, false, true, true, true, false),
          Chara (true, false, false, true, false, true, false, false)]
  | encode_tuple_heads [] (v :: va) =
    Inr [Chara (true, true, false, false, true, false, true, false),
          Chara (false, false, false, true, false, true, true, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (true, false, true, false, true, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, true, false, false, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, false, false, false, false, true, false, false),
          Chara (false, false, false, true, false, true, false, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (false, true, true, true, false, true, true, false),
          Chara (true, true, false, false, false, true, true, false),
          Chara (true, true, true, true, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (true, true, true, false, false, true, false, false),
          Chara (true, true, true, true, true, false, true, false),
          Chara (false, false, true, false, true, true, true, false),
          Chara (true, false, true, false, true, true, true, false),
          Chara (false, false, false, false, true, true, true, false),
          Chara (false, false, true, true, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (true, true, true, true, true, false, true, false),
          Chara (false, false, false, true, false, true, true, false),
          Chara (true, false, true, false, false, true, true, false),
          Chara (true, false, false, false, false, true, true, false),
          Chara (false, false, true, false, false, true, true, false),
          Chara (true, true, false, false, true, true, true, false),
          Chara (true, false, false, true, false, true, false, false)]
and encode_tuple_tails [] uw ux = Inl []
  | encode_tuple_tails (v :: rest) headlen len_total =
    (if abi_type_isstatic (abi_get_type v)
      then (case encode_tuple_tails rest headlen len_total
             of Inl ts => Inl ((plus_inta len_total headlen, []) :: ts)
             | Inr a => Inr a)
      else (case encodea v
             of Inl enc =>
               let
                 val len_totala =
                   plus_inta len_total (of_nat semiring_1_int (size_list enc));
               in
                 (case encode_tuple_tails rest headlen len_totala
                   of Inl ts =>
                     (if sint_value_valid
                           (nat_of_num
                             (Bit0 (Bit0 (Bit0
   (Bit0 (Bit0 (Bit0 (Bit0 (Bit0 One)))))))))
                           (plus_inta len_total headlen)
                       then Inl ((plus_inta len_total headlen, enc) :: ts)
                       else Inr [Chara (true, false, true, false, false, false,
 true, false),
                                  Chara (false, true, true, true, false, true,
  true, false),
                                  Chara (true, true, false, false, false, true,
  true, false),
                                  Chara (true, true, true, true, false, true,
  true, false),
                                  Chara (false, false, true, false, false, true,
  true, false),
                                  Chara (true, false, true, false, false, true,
  true, false),
                                  Chara (false, false, true, false, false, true,
  true, false),
                                  Chara (false, false, false, false, false,
  true, false, false),
                                  Chara (false, true, true, false, true, true,
  true, false),
                                  Chara (true, false, false, false, false, true,
  true, false),
                                  Chara (false, false, true, true, false, true,
  true, false),
                                  Chara (true, false, true, false, true, true,
  true, false),
                                  Chara (true, false, true, false, false, true,
  true, false),
                                  Chara (false, false, false, false, false,
  true, false, false),
                                  Chara (true, false, false, true, false, true,
  true, false),
                                  Chara (true, true, false, false, true, true,
  true, false),
                                  Chara (false, false, false, false, false,
  true, false, false),
                                  Chara (false, false, true, false, true, true,
  true, false),
                                  Chara (true, true, true, true, false, true,
  true, false),
                                  Chara (true, true, true, true, false, true,
  true, false),
                                  Chara (false, false, false, false, false,
  true, false, false),
                                  Chara (false, false, true, true, false, true,
  true, false),
                                  Chara (true, true, true, true, false, true,
  true, false),
                                  Chara (false, true, true, true, false, true,
  true, false),
                                  Chara (true, true, true, false, false, true,
  true, false)])
                   | Inr a => Inr a)
               end
             | Inr a => Inr a));

fun encode v =
  (if abi_value_valid v then encodea v
    else Inr [Chara (true, false, false, true, false, false, true, false),
               Chara (false, true, true, true, false, true, true, false),
               Chara (false, true, true, false, true, true, true, false),
               Chara (true, false, false, false, false, true, true, false),
               Chara (false, false, true, true, false, true, true, false),
               Chara (true, false, false, true, false, true, true, false),
               Chara (false, false, true, false, false, true, true, false),
               Chara (false, false, false, false, false, true, false, false),
               Chara (true, false, false, false, false, false, true, false),
               Chara (false, true, false, false, false, false, true, false),
               Chara (true, false, false, true, false, false, true, false),
               Chara (false, false, false, false, false, true, false, false),
               Chara (false, true, true, false, true, true, true, false),
               Chara (true, false, false, false, false, true, true, false),
               Chara (false, false, true, true, false, true, true, false),
               Chara (true, false, true, false, true, true, true, false),
               Chara (true, false, true, false, false, true, true, false)]);

end; (*struct ABICoder*)