default Order dec

$include <exception_basic.sail>
$include <flow.sail>
$include <vector_dec.sail>

function main (() : unit) -> unit = {
  assert(replicate_bits(1^0x0, 0) == 0^0x0, "replicate_bits(1^0x0, 0) == 0^0x0");
  assert(replicate_bits(1^0x0, 1) == 1^0x0, "replicate_bits(1^0x0, 1) == 1^0x0");
  assert(replicate_bits(1^0x0, 10) == 10^0x0, "replicate_bits(1^0x0, 10) == 10^0x0");
  assert(replicate_bits(1^0x0, 11) == 11^0x0, "replicate_bits(1^0x0, 11) == 11^0x0");
  assert(replicate_bits(1^0x0, 12) == 12^0x0, "replicate_bits(1^0x0, 12) == 12^0x0");
  assert(replicate_bits(1^0x0, 13) == 13^0x0, "replicate_bits(1^0x0, 13) == 13^0x0");
  assert(replicate_bits(1^0x0, 14) == 14^0x0, "replicate_bits(1^0x0, 14) == 14^0x0");
  assert(replicate_bits(1^0x0, 16) == 16^0x0, "replicate_bits(1^0x0, 16) == 16^0x0");
  assert(replicate_bits(1^0x0, 18) == 18^0x0, "replicate_bits(1^0x0, 18) == 18^0x0");
  assert(replicate_bits(1^0x0, 2) == 2^0x0, "replicate_bits(1^0x0, 2) == 2^0x0");
  assert(replicate_bits(1^0x0, 20) == 20^0x0, "replicate_bits(1^0x0, 20) == 20^0x0");
  assert(replicate_bits(1^0x0, 21) == 21^0x0, "replicate_bits(1^0x0, 21) == 21^0x0");
  assert(replicate_bits(1^0x0, 22) == 22^0x0, "replicate_bits(1^0x0, 22) == 22^0x0");
  assert(replicate_bits(1^0x0, 24) == 24^0x0, "replicate_bits(1^0x0, 24) == 24^0x0");
  assert(replicate_bits(1^0x0, 25) == 25^0x0, "replicate_bits(1^0x0, 25) == 25^0x0");
  assert(replicate_bits(1^0x0, 26) == 26^0x0, "replicate_bits(1^0x0, 26) == 26^0x0");
  assert(replicate_bits(1^0x0, 28) == 28^0x0, "replicate_bits(1^0x0, 28) == 28^0x0");
  assert(replicate_bits(1^0x0, 29) == 29^0x0, "replicate_bits(1^0x0, 29) == 29^0x0");
  assert(replicate_bits(1^0x0, 3) == 3^0x0, "replicate_bits(1^0x0, 3) == 3^0x0");
  assert(replicate_bits(1^0x0, 30) == 30^0x0, "replicate_bits(1^0x0, 30) == 30^0x0");
  assert(replicate_bits(1^0x0, 31) == 31^0x0, "replicate_bits(1^0x0, 31) == 31^0x0");
  assert(replicate_bits(1^0x0, 32) == 32^0x0, "replicate_bits(1^0x0, 32) == 32^0x0");
  assert(replicate_bits(1^0x0, 34) == 34^0x0, "replicate_bits(1^0x0, 34) == 34^0x0");
  assert(replicate_bits(1^0x0, 36) == 36^0x0, "replicate_bits(1^0x0, 36) == 36^0x0");
  assert(replicate_bits(1^0x0, 38) == 38^0x0, "replicate_bits(1^0x0, 38) == 38^0x0");
  assert(replicate_bits(1^0x0, 4) == 4^0x0, "replicate_bits(1^0x0, 4) == 4^0x0");
  assert(replicate_bits(1^0x0, 40) == 40^0x0, "replicate_bits(1^0x0, 40) == 40^0x0");
  assert(replicate_bits(1^0x0, 42) == 42^0x0, "replicate_bits(1^0x0, 42) == 42^0x0");
  assert(replicate_bits(1^0x0, 43) == 43^0x0, "replicate_bits(1^0x0, 43) == 43^0x0");
  assert(replicate_bits(1^0x0, 44) == 44^0x0, "replicate_bits(1^0x0, 44) == 44^0x0");
  assert(replicate_bits(1^0x0, 46) == 46^0x0, "replicate_bits(1^0x0, 46) == 46^0x0");
  assert(replicate_bits(1^0x0, 47) == 47^0x0, "replicate_bits(1^0x0, 47) == 47^0x0");
  assert(replicate_bits(1^0x0, 48) == 48^0x0, "replicate_bits(1^0x0, 48) == 48^0x0");
  assert(replicate_bits(1^0x0, 5) == 5^0x0, "replicate_bits(1^0x0, 5) == 5^0x0");
  assert(replicate_bits(1^0x0, 50) == 50^0x0, "replicate_bits(1^0x0, 50) == 50^0x0");
  assert(replicate_bits(1^0x0, 52) == 52^0x0, "replicate_bits(1^0x0, 52) == 52^0x0");
  assert(replicate_bits(1^0x0, 54) == 54^0x0, "replicate_bits(1^0x0, 54) == 54^0x0");
  assert(replicate_bits(1^0x0, 55) == 55^0x0, "replicate_bits(1^0x0, 55) == 55^0x0");
  assert(replicate_bits(1^0x0, 56) == 56^0x0, "replicate_bits(1^0x0, 56) == 56^0x0");
  assert(replicate_bits(1^0x0, 57) == 57^0x0, "replicate_bits(1^0x0, 57) == 57^0x0");
  assert(replicate_bits(1^0x0, 58) == 58^0x0, "replicate_bits(1^0x0, 58) == 58^0x0");
  assert(replicate_bits(1^0x0, 6) == 6^0x0, "replicate_bits(1^0x0, 6) == 6^0x0");
  assert(replicate_bits(1^0x0, 60) == 60^0x0, "replicate_bits(1^0x0, 60) == 60^0x0");
  assert(replicate_bits(1^0x0, 62) == 62^0x0, "replicate_bits(1^0x0, 62) == 62^0x0");
  assert(replicate_bits(1^0x0, 64) == 64^0x0, "replicate_bits(1^0x0, 64) == 64^0x0");
  assert(replicate_bits(1^0x0, 7) == 7^0x0, "replicate_bits(1^0x0, 7) == 7^0x0");
  assert(replicate_bits(1^0x0, 8) == 8^0x0, "replicate_bits(1^0x0, 8) == 8^0x0");
  assert(replicate_bits(1^0x1, 1) == 1^0x1, "replicate_bits(1^0x1, 1) == 1^0x1");
  assert(replicate_bits(1^0x1, 16) == 16^0xffff, "replicate_bits(1^0x1, 16) == 16^0xffff");
  assert(replicate_bits(1^0x1, 2) == 2^0x3, "replicate_bits(1^0x1, 2) == 2^0x3");
  assert(replicate_bits(1^0x1, 3) == 3^0x7, "replicate_bits(1^0x1, 3) == 3^0x7");
  assert(replicate_bits(1^0x1, 32) == 32^0xffffffff, "replicate_bits(1^0x1, 32) == 32^0xffffffff");
  assert(replicate_bits(1^0x1, 36) == 36^0xfffffffff, "replicate_bits(1^0x1, 36) == 36^0xfffffffff");
  assert(replicate_bits(1^0x1, 4) == 4^0xf, "replicate_bits(1^0x1, 4) == 4^0xf");
  assert(replicate_bits(1^0x1, 43) == 43^0x7ffffffffff, "replicate_bits(1^0x1, 43) == 43^0x7ffffffffff");
  assert(replicate_bits(1^0x1, 48) == 48^0xffffffffffff, "replicate_bits(1^0x1, 48) == 48^0xffffffffffff");
  assert(replicate_bits(1^0x1, 5) == 5^0x1f, "replicate_bits(1^0x1, 5) == 5^0x1f");
  assert(replicate_bits(1^0x1, 57) == 57^0x1ffffffffffffff, "replicate_bits(1^0x1, 57) == 57^0x1ffffffffffffff");
  assert(replicate_bits(1^0x1, 6) == 6^0x3f, "replicate_bits(1^0x1, 6) == 6^0x3f");
  assert(replicate_bits(1^0x1, 64) == 64^0xffffffffffffffff, "replicate_bits(1^0x1, 64) == 64^0xffffffffffffffff");
  assert(replicate_bits(1^0x1, 8) == 8^0xff, "replicate_bits(1^0x1, 8) == 8^0xff");
  assert(replicate_bits(16^0x0, 4) == 64^0x0, "replicate_bits(16^0x0, 4) == 64^0x0");
  assert(replicate_bits(16^0xff, 4) == 64^0xff00ff00ff00ff, "replicate_bits(16^0xff, 4) == 64^0xff00ff00ff00ff");
  assert(replicate_bits(16^0xff00, 4) == 64^0xff00ff00ff00ff00, "replicate_bits(16^0xff00, 4) == 64^0xff00ff00ff00ff00");
  assert(replicate_bits(16^0xffff, 4) == 64^0xffffffffffffffff, "replicate_bits(16^0xffff, 4) == 64^0xffffffffffffffff");
  assert(replicate_bits(2^0x0, 32) == 64^0x0, "replicate_bits(2^0x0, 32) == 64^0x0");
  assert(replicate_bits(2^0x1, 32) == 64^0x5555555555555555, "replicate_bits(2^0x1, 32) == 64^0x5555555555555555");
  assert(replicate_bits(2^0x2, 32) == 64^0xaaaaaaaaaaaaaaaa, "replicate_bits(2^0x2, 32) == 64^0xaaaaaaaaaaaaaaaa");
  assert(replicate_bits(2^0x3, 32) == 64^0xffffffffffffffff, "replicate_bits(2^0x3, 32) == 64^0xffffffffffffffff");
  assert(replicate_bits(32^0x0, 2) == 64^0x0, "replicate_bits(32^0x0, 2) == 64^0x0");
  assert(replicate_bits(32^0xffff, 2) == 64^0xffff0000ffff, "replicate_bits(32^0xffff, 2) == 64^0xffff0000ffff");
  assert(replicate_bits(32^0xffff0000, 2) == 64^0xffff0000ffff0000, "replicate_bits(32^0xffff0000, 2) == 64^0xffff0000ffff0000");
  assert(replicate_bits(32^0xffffffff, 2) == 64^0xffffffffffffffff, "replicate_bits(32^0xffffffff, 2) == 64^0xffffffffffffffff");
  assert(replicate_bits(4^0x0, 16) == 64^0x0, "replicate_bits(4^0x0, 16) == 64^0x0");
  assert(replicate_bits(4^0x3, 16) == 64^0x3333333333333333, "replicate_bits(4^0x3, 16) == 64^0x3333333333333333");
  assert(replicate_bits(4^0xc, 16) == 64^0xcccccccccccccccc, "replicate_bits(4^0xc, 16) == 64^0xcccccccccccccccc");
  assert(replicate_bits(4^0xf, 16) == 64^0xffffffffffffffff, "replicate_bits(4^0xf, 16) == 64^0xffffffffffffffff");
  assert(replicate_bits(64^0x0, 1) == 64^0x0, "replicate_bits(64^0x0, 1) == 64^0x0");
  assert(replicate_bits(64^0xffffffff, 1) == 64^0xffffffff, "replicate_bits(64^0xffffffff, 1) == 64^0xffffffff");
  assert(replicate_bits(64^0xffffffff00000000, 1) == 64^0xffffffff00000000, "replicate_bits(64^0xffffffff00000000, 1) == 64^0xffffffff00000000");
  assert(replicate_bits(64^0xffffffffffffffff, 1) == 64^0xffffffffffffffff, "replicate_bits(64^0xffffffffffffffff, 1) == 64^0xffffffffffffffff");
  assert(replicate_bits(8^0x0, 8) == 64^0x0, "replicate_bits(8^0x0, 8) == 64^0x0");
  assert(replicate_bits(8^0xf, 8) == 64^0xf0f0f0f0f0f0f0f, "replicate_bits(8^0xf, 8) == 64^0xf0f0f0f0f0f0f0f");
  assert(replicate_bits(8^0xf0, 8) == 64^0xf0f0f0f0f0f0f0f0, "replicate_bits(8^0xf0, 8) == 64^0xf0f0f0f0f0f0f0f0");
  assert(replicate_bits(8^0xff, 8) == 64^0xffffffffffffffff, "replicate_bits(8^0xff, 8) == 64^0xffffffffffffffff");
}