/* Autogenerated: 'src/ExtractionOCaml/dettman_multiplication' --lang Java --cmovznz-by-mul --widen-carry --widen-bytes --internal-static --package-name fiat_crypto --class-case UpperCamelCase --no-field-element-typedefs Secp256K1Dettman 32 10 22 6 '2^256 - 4294968273' mul square */
/* curve description: Secp256K1Dettman */
/* machine_wordsize = 32 (from "32") */
/* requested operations: mul, square */
/* n = 10 (from "10") */
/* last_limb_width = 22 (from "22") */
/* last_reduction = 6 (from "6") */
/* s-c = 2^256 - [(1, 4294968273)] (from "2^256 - 4294968273") */
/* inbounds_multiplier: None (from "") */
/*  */
/* Computed values: */
/*  */
/*  */

package fiat_crypto;

public final class FiatSecp256K1Dettman {

static class Box<T> {
  private T value;
  public Box(T value) { this.value = value; }
  public void set(T value) { this.value = value; }
  public T get() { return this.value; }
}



/**
 * The function fiat_Secp256K1Dettman_mul multiplies two field elements. <p>
 * <p>
 * Postconditions: <p>
 *   eval out1 mod 115792089237316195423570985008687907853269984665640564039457584007908834671663 = (eval arg1 * eval arg2) mod 115792089237316195423570985008687907853269984665640564039457584007908834671663 <p>
 * <p>
 * Input Bounds: <p>
 *   arg1: [[0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7ffffe]] <p>
 *   arg2: [[0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7ffffe]] <p>
 * Output Bounds: <p>
 *   out1: [[0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x5fffff]] <p>
 */
public static void fiat_Secp256K1Dettman_mul(int[] out1, final int[] arg1, final int[] arg2) {
  long x1 = (((long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[9]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[8]))).intValue())));
  int x2 = (int) Integer.toUnsignedLong(((Number) ((x1 >>> 26))).intValue());
  int x3 = ((int) Integer.toUnsignedLong(((Number) (x1)).intValue()) & 0x3ffffff);
  long x4 = ((((long) Integer.toUnsignedLong(((Number) ((arg1[0]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[7]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[1]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[6]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[5]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[4]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[3]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[2]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[1]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[0]))).intValue()))))))))) + ((long) Integer.toUnsignedLong(((Number) (x3)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x5 = (int) Integer.toUnsignedLong(((Number) ((x4 >>> 26))).intValue());
  int x6 = ((int) Integer.toUnsignedLong(((Number) (x4)).intValue()) & 0x3ffffff);
  long x7 = ((long) Integer.toUnsignedLong(((Number) (x2)).intValue()) + ((long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[9]))).intValue())));
  int x8 = (int) Integer.toUnsignedLong(((Number) ((x7 >>> 32))).intValue());
  int x9 = ((int) Integer.toUnsignedLong(((Number) (x7)).intValue()) & 0xffffffff);
  long x10 = (((long) Integer.toUnsignedLong(((Number) (x5)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) ((arg1[0]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[8]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[1]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[7]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[6]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[5]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[4]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[3]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[2]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[1]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[0]))).intValue())))))))))) + ((long) Integer.toUnsignedLong(((Number) (x3)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x9)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x11 = (int) Integer.toUnsignedLong(((Number) ((x10 >>> 26))).intValue());
  int x12 = ((int) Integer.toUnsignedLong(((Number) (x10)).intValue()) & 0x3ffffff);
  long x13 = (((long) Integer.toUnsignedLong(((Number) (x11)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) ((arg1[0]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[1]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[8]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[7]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[6]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[5]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[4]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[3]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[2]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[1]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[0]))).intValue()))))))))))) + ((long) Integer.toUnsignedLong(((Number) (x9)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x8)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0xf4400)).intValue())));
  int x14 = (int) Integer.toUnsignedLong(((Number) ((x13 >>> 26))).intValue());
  int x15 = ((int) Integer.toUnsignedLong(((Number) (x13)).intValue()) & 0x3ffffff);
  long x16 = ((long) Integer.toUnsignedLong(((Number) (x14)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) ((arg1[1]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[8]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[7]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[6]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[5]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[4]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[3]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[2]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[1]))).intValue())))))))))) + (long) Integer.toUnsignedLong(((Number) ((x8 << 16))).intValue())));
  int x17 = (int) Integer.toUnsignedLong(((Number) ((x16 >>> 26))).intValue());
  int x18 = ((int) Integer.toUnsignedLong(((Number) (x16)).intValue()) & 0x3ffffff);
  int x19 = (x15 >>> 22);
  int x20 = (x15 & 0x3fffff);
  long x21 = (((long) Integer.toUnsignedLong(((Number) ((arg1[0]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[0]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((x19 + (x18 << 4)))).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d1)).intValue())));
  int x22 = (int) Integer.toUnsignedLong(((Number) ((x21 >>> 26))).intValue());
  int x23 = ((int) Integer.toUnsignedLong(((Number) (x21)).intValue()) & 0x3ffffff);
  long x24 = ((long) Integer.toUnsignedLong(((Number) (x17)).intValue()) + (((long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[8]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[7]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[6]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[5]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[4]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[3]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[2]))).intValue()))))))))));
  int x25 = (int) Integer.toUnsignedLong(((Number) ((x24 >>> 26))).intValue());
  int x26 = ((int) Integer.toUnsignedLong(((Number) (x24)).intValue()) & 0x3ffffff);
  long x27 = (((long) Integer.toUnsignedLong(((Number) (x22)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) ((arg1[0]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[1]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[1]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[0]))).intValue()))) + ((long) Integer.toUnsignedLong(((Number) ((x19 + (x18 << 4)))).intValue()) << 6))) + ((long) Integer.toUnsignedLong(((Number) (x26)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x28 = (int) Integer.toUnsignedLong(((Number) ((x27 >>> 26))).intValue());
  int x29 = ((int) Integer.toUnsignedLong(((Number) (x27)).intValue()) & 0x3ffffff);
  long x30 = ((long) Integer.toUnsignedLong(((Number) (x25)).intValue()) + (((long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[8]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[7]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[6]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[5]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[4]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[3]))).intValue())))))))));
  int x31 = (int) Integer.toUnsignedLong(((Number) ((x30 >>> 26))).intValue());
  int x32 = ((int) Integer.toUnsignedLong(((Number) (x30)).intValue()) & 0x3ffffff);
  long x33 = (((long) Integer.toUnsignedLong(((Number) (x28)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) ((arg1[0]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[2]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[1]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[1]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[0]))).intValue())))) + ((long) Integer.toUnsignedLong(((Number) (x26)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x32)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x34 = (int) Integer.toUnsignedLong(((Number) ((x33 >>> 26))).intValue());
  int x35 = ((int) Integer.toUnsignedLong(((Number) (x33)).intValue()) & 0x3ffffff);
  long x36 = ((long) Integer.toUnsignedLong(((Number) (x31)).intValue()) + (((long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[8]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[7]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[6]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[5]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[4]))).intValue()))))))));
  int x37 = (int) Integer.toUnsignedLong(((Number) ((x36 >>> 26))).intValue());
  int x38 = ((int) Integer.toUnsignedLong(((Number) (x36)).intValue()) & 0x3ffffff);
  long x39 = (((long) Integer.toUnsignedLong(((Number) (x34)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) ((arg1[0]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[3]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[1]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[2]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[1]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[0]))).intValue()))))) + ((long) Integer.toUnsignedLong(((Number) (x32)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x38)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x40 = (int) Integer.toUnsignedLong(((Number) ((x39 >>> 26))).intValue());
  int x41 = ((int) Integer.toUnsignedLong(((Number) (x39)).intValue()) & 0x3ffffff);
  long x42 = ((long) Integer.toUnsignedLong(((Number) (x37)).intValue()) + (((long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[8]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[7]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[6]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[5]))).intValue())))))));
  int x43 = (int) Integer.toUnsignedLong(((Number) ((x42 >>> 26))).intValue());
  int x44 = ((int) Integer.toUnsignedLong(((Number) (x42)).intValue()) & 0x3ffffff);
  long x45 = (((long) Integer.toUnsignedLong(((Number) (x40)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) ((arg1[0]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[4]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[1]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[3]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[2]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[1]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[0]))).intValue())))))) + ((long) Integer.toUnsignedLong(((Number) (x38)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x44)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x46 = (int) Integer.toUnsignedLong(((Number) ((x45 >>> 26))).intValue());
  int x47 = ((int) Integer.toUnsignedLong(((Number) (x45)).intValue()) & 0x3ffffff);
  long x48 = ((long) Integer.toUnsignedLong(((Number) (x43)).intValue()) + (((long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[8]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[7]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[6]))).intValue()))))));
  int x49 = (int) Integer.toUnsignedLong(((Number) ((x48 >>> 26))).intValue());
  int x50 = ((int) Integer.toUnsignedLong(((Number) (x48)).intValue()) & 0x3ffffff);
  long x51 = (((long) Integer.toUnsignedLong(((Number) (x46)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) ((arg1[0]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[5]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[1]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[4]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[3]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[2]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[1]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[0]))).intValue()))))))) + ((long) Integer.toUnsignedLong(((Number) (x44)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x50)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x52 = (int) Integer.toUnsignedLong(((Number) ((x51 >>> 26))).intValue());
  int x53 = ((int) Integer.toUnsignedLong(((Number) (x51)).intValue()) & 0x3ffffff);
  long x54 = ((long) Integer.toUnsignedLong(((Number) (x49)).intValue()) + (((long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[8]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[7]))).intValue())))));
  int x55 = (int) Integer.toUnsignedLong(((Number) ((x54 >>> 32))).intValue());
  int x56 = ((int) Integer.toUnsignedLong(((Number) (x54)).intValue()) & 0xffffffff);
  long x57 = (((long) Integer.toUnsignedLong(((Number) (x52)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) ((arg1[0]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[6]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[1]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[5]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[4]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[3]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[2]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[1]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg2[0]))).intValue())))))))) + ((long) Integer.toUnsignedLong(((Number) (x50)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x56)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x58 = (int) Integer.toUnsignedLong(((Number) ((x57 >>> 26))).intValue());
  int x59 = ((int) Integer.toUnsignedLong(((Number) (x57)).intValue()) & 0x3ffffff);
  long x60 = (((long) Integer.toUnsignedLong(((Number) (x58)).intValue()) + ((long) Integer.toUnsignedLong(((Number) (x6)).intValue()) + ((long) Integer.toUnsignedLong(((Number) (x56)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x55)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0xf4400)).intValue())));
  int x61 = (int) Integer.toUnsignedLong(((Number) ((x60 >>> 26))).intValue());
  int x62 = ((int) Integer.toUnsignedLong(((Number) (x60)).intValue()) & 0x3ffffff);
  long x63 = ((long) Integer.toUnsignedLong(((Number) (x61)).intValue()) + ((long) Integer.toUnsignedLong(((Number) (x12)).intValue()) + ((long) Integer.toUnsignedLong(((Number) (x55)).intValue()) << 16)));
  int x64 = (int) Integer.toUnsignedLong(((Number) ((x63 >>> 26))).intValue());
  int x65 = ((int) Integer.toUnsignedLong(((Number) (x63)).intValue()) & 0x3ffffff);
  int x66 = (x64 + x20);
  out1[0] = x23;
  out1[1] = x29;
  out1[2] = x35;
  out1[3] = x41;
  out1[4] = x47;
  out1[5] = x53;
  out1[6] = x59;
  out1[7] = x62;
  out1[8] = x65;
  out1[9] = x66;
}

/**
 * The function fiat_Secp256K1Dettman_square squares a field element. <p>
 * <p>
 * Postconditions: <p>
 *   eval out1 mod 115792089237316195423570985008687907853269984665640564039457584007908834671663 = (eval arg1 * eval arg1) mod 115792089237316195423570985008687907853269984665640564039457584007908834671663 <p>
 * <p>
 * Input Bounds: <p>
 *   arg1: [[0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7ffffe]] <p>
 * Output Bounds: <p>
 *   out1: [[0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x7fffffe], [0x0 ~&gt; 0x5fffff]] <p>
 */
public static void fiat_Secp256K1Dettman_square(int[] out1, final int[] arg1) {
  int x1 = ((arg1[8]) * 0x2);
  int x2 = ((arg1[7]) * 0x2);
  int x3 = ((arg1[6]) * 0x2);
  int x4 = ((arg1[5]) * 0x2);
  int x5 = ((arg1[4]) * 0x2);
  int x6 = ((arg1[3]) * 0x2);
  int x7 = ((arg1[2]) * 0x2);
  int x8 = ((arg1[1]) * 0x2);
  int x9 = ((arg1[0]) * 0x2);
  long x10 = ((long) Integer.toUnsignedLong(((Number) (x1)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue()));
  int x11 = (int) Integer.toUnsignedLong(((Number) ((x10 >>> 26))).intValue());
  int x12 = ((int) Integer.toUnsignedLong(((Number) (x10)).intValue()) & 0x3ffffff);
  long x13 = ((((long) Integer.toUnsignedLong(((Number) (x9)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x8)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x7)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) (x6)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue()))))) + ((long) Integer.toUnsignedLong(((Number) (x12)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x14 = (int) Integer.toUnsignedLong(((Number) ((x13 >>> 26))).intValue());
  int x15 = ((int) Integer.toUnsignedLong(((Number) (x13)).intValue()) & 0x3ffffff);
  long x16 = ((long) Integer.toUnsignedLong(((Number) (x11)).intValue()) + ((long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue())));
  int x17 = (int) Integer.toUnsignedLong(((Number) ((x16 >>> 32))).intValue());
  int x18 = ((int) Integer.toUnsignedLong(((Number) (x16)).intValue()) & 0xffffffff);
  long x19 = (((long) Integer.toUnsignedLong(((Number) (x14)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) (x9)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x8)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x7)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x6)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue())))))) + ((long) Integer.toUnsignedLong(((Number) (x12)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x18)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x20 = (int) Integer.toUnsignedLong(((Number) ((x19 >>> 26))).intValue());
  int x21 = ((int) Integer.toUnsignedLong(((Number) (x19)).intValue()) & 0x3ffffff);
  long x22 = (((long) Integer.toUnsignedLong(((Number) (x20)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) (x9)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x8)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x7)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x6)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) (x5)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue())))))) + ((long) Integer.toUnsignedLong(((Number) (x18)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x17)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0xf4400)).intValue())));
  int x23 = (int) Integer.toUnsignedLong(((Number) ((x22 >>> 26))).intValue());
  int x24 = ((int) Integer.toUnsignedLong(((Number) (x22)).intValue()) & 0x3ffffff);
  long x25 = ((long) Integer.toUnsignedLong(((Number) (x23)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) (x8)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x7)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x6)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x5)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue())))))) + (long) Integer.toUnsignedLong(((Number) ((x17 << 16))).intValue())));
  int x26 = (int) Integer.toUnsignedLong(((Number) ((x25 >>> 26))).intValue());
  int x27 = ((int) Integer.toUnsignedLong(((Number) (x25)).intValue()) & 0x3ffffff);
  int x28 = (x24 >>> 22);
  int x29 = (x24 & 0x3fffff);
  long x30 = (((long) Integer.toUnsignedLong(((Number) ((arg1[0]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[0]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((x28 + (x27 << 4)))).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d1)).intValue())));
  int x31 = (int) Integer.toUnsignedLong(((Number) ((x30 >>> 26))).intValue());
  int x32 = ((int) Integer.toUnsignedLong(((Number) (x30)).intValue()) & 0x3ffffff);
  long x33 = ((long) Integer.toUnsignedLong(((Number) (x26)).intValue()) + (((long) Integer.toUnsignedLong(((Number) (x7)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x6)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x5)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) (x4)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue()))))));
  int x34 = (int) Integer.toUnsignedLong(((Number) ((x33 >>> 26))).intValue());
  int x35 = ((int) Integer.toUnsignedLong(((Number) (x33)).intValue()) & 0x3ffffff);
  long x36 = (((long) Integer.toUnsignedLong(((Number) (x31)).intValue()) + (((long) Integer.toUnsignedLong(((Number) (x9)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[1]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((x28 + (x27 << 4)))).intValue()) << 6))) + ((long) Integer.toUnsignedLong(((Number) (x35)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x37 = (int) Integer.toUnsignedLong(((Number) ((x36 >>> 26))).intValue());
  int x38 = ((int) Integer.toUnsignedLong(((Number) (x36)).intValue()) & 0x3ffffff);
  long x39 = ((long) Integer.toUnsignedLong(((Number) (x34)).intValue()) + (((long) Integer.toUnsignedLong(((Number) (x6)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x5)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x4)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue()))))));
  int x40 = (int) Integer.toUnsignedLong(((Number) ((x39 >>> 26))).intValue());
  int x41 = ((int) Integer.toUnsignedLong(((Number) (x39)).intValue()) & 0x3ffffff);
  long x42 = (((long) Integer.toUnsignedLong(((Number) (x37)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) (x9)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[1]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[1]))).intValue()))) + ((long) Integer.toUnsignedLong(((Number) (x35)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x41)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x43 = (int) Integer.toUnsignedLong(((Number) ((x42 >>> 26))).intValue());
  int x44 = ((int) Integer.toUnsignedLong(((Number) (x42)).intValue()) & 0x3ffffff);
  long x45 = ((long) Integer.toUnsignedLong(((Number) (x40)).intValue()) + (((long) Integer.toUnsignedLong(((Number) (x5)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x4)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) (x3)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue())))));
  int x46 = (int) Integer.toUnsignedLong(((Number) ((x45 >>> 26))).intValue());
  int x47 = ((int) Integer.toUnsignedLong(((Number) (x45)).intValue()) & 0x3ffffff);
  long x48 = (((long) Integer.toUnsignedLong(((Number) (x43)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) (x9)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) (x8)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue()))) + ((long) Integer.toUnsignedLong(((Number) (x41)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x47)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x49 = (int) Integer.toUnsignedLong(((Number) ((x48 >>> 26))).intValue());
  int x50 = ((int) Integer.toUnsignedLong(((Number) (x48)).intValue()) & 0x3ffffff);
  long x51 = ((long) Integer.toUnsignedLong(((Number) (x46)).intValue()) + (((long) Integer.toUnsignedLong(((Number) (x4)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x3)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[7]))).intValue())))));
  int x52 = (int) Integer.toUnsignedLong(((Number) ((x51 >>> 26))).intValue());
  int x53 = ((int) Integer.toUnsignedLong(((Number) (x51)).intValue()) & 0x3ffffff);
  long x54 = (((long) Integer.toUnsignedLong(((Number) (x49)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) (x9)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x8)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[2]))).intValue())))) + ((long) Integer.toUnsignedLong(((Number) (x47)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x53)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x55 = (int) Integer.toUnsignedLong(((Number) ((x54 >>> 26))).intValue());
  int x56 = ((int) Integer.toUnsignedLong(((Number) (x54)).intValue()) & 0x3ffffff);
  long x57 = ((long) Integer.toUnsignedLong(((Number) (x52)).intValue()) + (((long) Integer.toUnsignedLong(((Number) (x3)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) (x2)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue()))));
  int x58 = (int) Integer.toUnsignedLong(((Number) ((x57 >>> 26))).intValue());
  int x59 = ((int) Integer.toUnsignedLong(((Number) (x57)).intValue()) & 0x3ffffff);
  long x60 = (((long) Integer.toUnsignedLong(((Number) (x55)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) (x9)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x8)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) (x7)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue())))) + ((long) Integer.toUnsignedLong(((Number) (x53)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x59)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x61 = (int) Integer.toUnsignedLong(((Number) ((x60 >>> 26))).intValue());
  int x62 = ((int) Integer.toUnsignedLong(((Number) (x60)).intValue()) & 0x3ffffff);
  long x63 = ((long) Integer.toUnsignedLong(((Number) (x58)).intValue()) + (((long) Integer.toUnsignedLong(((Number) (x2)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[9]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[8]))).intValue()))));
  int x64 = (int) Integer.toUnsignedLong(((Number) ((x63 >>> 32))).intValue());
  int x65 = ((int) Integer.toUnsignedLong(((Number) (x63)).intValue()) & 0xffffffff);
  long x66 = (((long) Integer.toUnsignedLong(((Number) (x61)).intValue()) + ((((long) Integer.toUnsignedLong(((Number) (x9)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[6]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x8)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[5]))).intValue())) + (((long) Integer.toUnsignedLong(((Number) (x7)).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[4]))).intValue())) + ((long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue()) * (long) Integer.toUnsignedLong(((Number) ((arg1[3]))).intValue()))))) + ((long) Integer.toUnsignedLong(((Number) (x59)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x65)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0x3d10)).intValue())));
  int x67 = (int) Integer.toUnsignedLong(((Number) ((x66 >>> 26))).intValue());
  int x68 = ((int) Integer.toUnsignedLong(((Number) (x66)).intValue()) & 0x3ffffff);
  long x69 = (((long) Integer.toUnsignedLong(((Number) (x67)).intValue()) + ((long) Integer.toUnsignedLong(((Number) (x15)).intValue()) + ((long) Integer.toUnsignedLong(((Number) (x65)).intValue()) << 10))) + ((long) Integer.toUnsignedLong(((Number) (x64)).intValue()) * (long) Integer.toUnsignedLong(((Number) (0xf4400)).intValue())));
  int x70 = (int) Integer.toUnsignedLong(((Number) ((x69 >>> 26))).intValue());
  int x71 = ((int) Integer.toUnsignedLong(((Number) (x69)).intValue()) & 0x3ffffff);
  long x72 = ((long) Integer.toUnsignedLong(((Number) (x70)).intValue()) + ((long) Integer.toUnsignedLong(((Number) (x21)).intValue()) + ((long) Integer.toUnsignedLong(((Number) (x64)).intValue()) << 16)));
  int x73 = (int) Integer.toUnsignedLong(((Number) ((x72 >>> 26))).intValue());
  int x74 = ((int) Integer.toUnsignedLong(((Number) (x72)).intValue()) & 0x3ffffff);
  int x75 = (x73 + x29);
  out1[0] = x32;
  out1[1] = x38;
  out1[2] = x44;
  out1[3] = x50;
  out1[4] = x56;
  out1[5] = x62;
  out1[6] = x68;
  out1[7] = x71;
  out1[8] = x74;
  out1[9] = x75;
}

}
