# Generated by tools/generators/blake2b_gen.py; do not edit by hand.
import Base
import ./types.bend as T
import ./lane.bend as L

# G (RFC 7693 section 3.1) on four words and two message words.
def g(a: T.Lane, +b: T.Lane, c: T.Lane, d: T.Lane, x: T.Lane, y: T.Lane) -> T.Quad:
  +a1 = L.add(L.add(a,b),x)
  +d1 = L.rot32(L.xor(d,a1))
  +c1 = L.add(c,d1)
  +b1 = L.rot24(L.xor(b,c1))
  +a2 = L.add(L.add(a1,b1),y)
  +d2 = L.rot16(L.xor(d1,a2))
  +c2 = L.add(c1,d2)
  +b2 = L.rot63(L.xor(b1,c2))
  T.Q{a2,b2,c2,d2}

def column0_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_7,t4_11,t4_15}:
      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}

def column0_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_6,t3_10,t3_14}:
      column0_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)

def column0_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_5,t2_9,t2_13}:
      column0_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)

def column0_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_4,t1_8,t1_12}:
      column0_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)

# Round 0, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
def column0(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      column0_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)

def diagonal0_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_4,t4_9,t4_14}:
      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}

def diagonal0_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_7,t3_8,t3_13}:
      diagonal0_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)

def diagonal0_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_6,t2_11,t2_12}:
      diagonal0_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)

def diagonal0_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_5,t1_10,t1_15}:
      diagonal0_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)

# Round 0, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
def diagonal0(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      diagonal0_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)

# Round 0 uses the message schedule SIGMA[0], fixed at compile time.
def round0(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
  diagonal0(column0(v,m0,m1,m2,m3,m4,m5,m6,m7),m8,m9,m10,m11,m12,m13,m14,m15)

def column1_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_7,t4_11,t4_15}:
      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}

def column1_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_6,t3_10,t3_14}:
      column1_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)

def column1_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_5,t2_9,t2_13}:
      column1_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)

def column1_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_4,t1_8,t1_12}:
      column1_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)

# Round 1, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
def column1(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      column1_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)

def diagonal1_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_4,t4_9,t4_14}:
      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}

def diagonal1_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_7,t3_8,t3_13}:
      diagonal1_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)

def diagonal1_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_6,t2_11,t2_12}:
      diagonal1_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)

def diagonal1_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_5,t1_10,t1_15}:
      diagonal1_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)

# Round 1, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
def diagonal1(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      diagonal1_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)

# Round 1 uses the message schedule SIGMA[1], fixed at compile time.
def round1(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
  diagonal1(column1(v,m14,m10,m4,m8,m9,m15,m13,m6),m1,m12,m0,m2,m11,m7,m5,m3)

def column2_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_7,t4_11,t4_15}:
      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}

def column2_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_6,t3_10,t3_14}:
      column2_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)

def column2_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_5,t2_9,t2_13}:
      column2_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)

def column2_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_4,t1_8,t1_12}:
      column2_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)

# Round 2, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
def column2(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      column2_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)

def diagonal2_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_4,t4_9,t4_14}:
      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}

def diagonal2_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_7,t3_8,t3_13}:
      diagonal2_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)

def diagonal2_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_6,t2_11,t2_12}:
      diagonal2_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)

def diagonal2_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_5,t1_10,t1_15}:
      diagonal2_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)

# Round 2, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
def diagonal2(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      diagonal2_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)

# Round 2 uses the message schedule SIGMA[2], fixed at compile time.
def round2(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
  diagonal2(column2(v,m11,m8,m12,m0,m5,m2,m15,m13),m10,m14,m3,m6,m7,m1,m9,m4)

def column3_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_7,t4_11,t4_15}:
      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}

def column3_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_6,t3_10,t3_14}:
      column3_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)

def column3_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_5,t2_9,t2_13}:
      column3_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)

def column3_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_4,t1_8,t1_12}:
      column3_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)

# Round 3, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
def column3(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      column3_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)

def diagonal3_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_4,t4_9,t4_14}:
      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}

def diagonal3_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_7,t3_8,t3_13}:
      diagonal3_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)

def diagonal3_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_6,t2_11,t2_12}:
      diagonal3_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)

def diagonal3_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_5,t1_10,t1_15}:
      diagonal3_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)

# Round 3, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
def diagonal3(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      diagonal3_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)

# Round 3 uses the message schedule SIGMA[3], fixed at compile time.
def round3(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
  diagonal3(column3(v,m7,m9,m3,m1,m13,m12,m11,m14),m2,m6,m5,m10,m4,m0,m15,m8)

def column4_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_7,t4_11,t4_15}:
      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}

def column4_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_6,t3_10,t3_14}:
      column4_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)

def column4_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_5,t2_9,t2_13}:
      column4_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)

def column4_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_4,t1_8,t1_12}:
      column4_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)

# Round 4, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
def column4(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      column4_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)

def diagonal4_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_4,t4_9,t4_14}:
      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}

def diagonal4_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_7,t3_8,t3_13}:
      diagonal4_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)

def diagonal4_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_6,t2_11,t2_12}:
      diagonal4_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)

def diagonal4_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_5,t1_10,t1_15}:
      diagonal4_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)

# Round 4, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
def diagonal4(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      diagonal4_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)

# Round 4 uses the message schedule SIGMA[4], fixed at compile time.
def round4(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
  diagonal4(column4(v,m9,m0,m5,m7,m2,m4,m10,m15),m14,m1,m11,m12,m6,m8,m3,m13)

def column5_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_7,t4_11,t4_15}:
      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}

def column5_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_6,t3_10,t3_14}:
      column5_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)

def column5_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_5,t2_9,t2_13}:
      column5_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)

def column5_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_4,t1_8,t1_12}:
      column5_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)

# Round 5, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
def column5(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      column5_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)

def diagonal5_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_4,t4_9,t4_14}:
      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}

def diagonal5_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_7,t3_8,t3_13}:
      diagonal5_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)

def diagonal5_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_6,t2_11,t2_12}:
      diagonal5_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)

def diagonal5_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_5,t1_10,t1_15}:
      diagonal5_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)

# Round 5, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
def diagonal5(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      diagonal5_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)

# Round 5 uses the message schedule SIGMA[5], fixed at compile time.
def round5(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
  diagonal5(column5(v,m2,m12,m6,m10,m0,m11,m8,m3),m4,m13,m7,m5,m15,m14,m1,m9)

def column6_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_7,t4_11,t4_15}:
      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}

def column6_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_6,t3_10,t3_14}:
      column6_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)

def column6_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_5,t2_9,t2_13}:
      column6_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)

def column6_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_4,t1_8,t1_12}:
      column6_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)

# Round 6, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
def column6(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      column6_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)

def diagonal6_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_4,t4_9,t4_14}:
      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}

def diagonal6_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_7,t3_8,t3_13}:
      diagonal6_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)

def diagonal6_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_6,t2_11,t2_12}:
      diagonal6_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)

def diagonal6_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_5,t1_10,t1_15}:
      diagonal6_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)

# Round 6, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
def diagonal6(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      diagonal6_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)

# Round 6 uses the message schedule SIGMA[6], fixed at compile time.
def round6(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
  diagonal6(column6(v,m12,m5,m1,m15,m14,m13,m4,m10),m0,m7,m6,m3,m9,m2,m8,m11)

def column7_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_7,t4_11,t4_15}:
      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}

def column7_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_6,t3_10,t3_14}:
      column7_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)

def column7_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_5,t2_9,t2_13}:
      column7_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)

def column7_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_4,t1_8,t1_12}:
      column7_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)

# Round 7, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
def column7(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      column7_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)

def diagonal7_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_4,t4_9,t4_14}:
      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}

def diagonal7_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_7,t3_8,t3_13}:
      diagonal7_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)

def diagonal7_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_6,t2_11,t2_12}:
      diagonal7_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)

def diagonal7_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_5,t1_10,t1_15}:
      diagonal7_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)

# Round 7, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
def diagonal7(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      diagonal7_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)

# Round 7 uses the message schedule SIGMA[7], fixed at compile time.
def round7(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
  diagonal7(column7(v,m13,m11,m7,m14,m12,m1,m3,m9),m5,m0,m15,m4,m8,m6,m2,m10)

def column8_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_7,t4_11,t4_15}:
      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}

def column8_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_6,t3_10,t3_14}:
      column8_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)

def column8_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_5,t2_9,t2_13}:
      column8_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)

def column8_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_4,t1_8,t1_12}:
      column8_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)

# Round 8, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
def column8(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      column8_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)

def diagonal8_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_4,t4_9,t4_14}:
      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}

def diagonal8_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_7,t3_8,t3_13}:
      diagonal8_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)

def diagonal8_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_6,t2_11,t2_12}:
      diagonal8_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)

def diagonal8_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_5,t1_10,t1_15}:
      diagonal8_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)

# Round 8, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
def diagonal8(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      diagonal8_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)

# Round 8 uses the message schedule SIGMA[8], fixed at compile time.
def round8(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
  diagonal8(column8(v,m6,m15,m14,m9,m11,m3,m0,m8),m12,m2,m13,m7,m1,m4,m10,m5)

def column9_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_7,t4_11,t4_15}:
      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}

def column9_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_6,t3_10,t3_14}:
      column9_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)

def column9_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_5,t2_9,t2_13}:
      column9_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)

def column9_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_4,t1_8,t1_12}:
      column9_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)

# Round 9, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
def column9(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      column9_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)

def diagonal9_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_4,t4_9,t4_14}:
      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}

def diagonal9_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_7,t3_8,t3_13}:
      diagonal9_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)

def diagonal9_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_6,t2_11,t2_12}:
      diagonal9_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)

def diagonal9_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_5,t1_10,t1_15}:
      diagonal9_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)

# Round 9, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
def diagonal9(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      diagonal9_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)

# Round 9 uses the message schedule SIGMA[9], fixed at compile time.
def round9(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
  diagonal9(column9(v,m10,m2,m8,m4,m7,m6,m1,m5),m15,m11,m9,m14,m3,m12,m13,m0)

def column10_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_7,t4_11,t4_15}:
      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}

def column10_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_6,t3_10,t3_14}:
      column10_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)

def column10_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_5,t2_9,t2_13}:
      column10_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)

def column10_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_4,t1_8,t1_12}:
      column10_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)

# Round 10, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
def column10(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      column10_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)

def diagonal10_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_4,t4_9,t4_14}:
      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}

def diagonal10_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_7,t3_8,t3_13}:
      diagonal10_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)

def diagonal10_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_6,t2_11,t2_12}:
      diagonal10_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)

def diagonal10_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_5,t1_10,t1_15}:
      diagonal10_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)

# Round 10, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
def diagonal10(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      diagonal10_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)

# Round 10 uses the message schedule SIGMA[0], fixed at compile time.
def round10(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
  diagonal10(column10(v,m0,m1,m2,m3,m4,m5,m6,m7),m8,m9,m10,m11,m12,m13,m14,m15)

def column11_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_7,t4_11,t4_15}:
      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}

def column11_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_6,t3_10,t3_14}:
      column11_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)

def column11_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_5,t2_9,t2_13}:
      column11_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)

def column11_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_4,t1_8,t1_12}:
      column11_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)

# Round 11, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
def column11(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      column11_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)

def diagonal11_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
  match q:
    case T.Q{t4_3,t4_4,t4_9,t4_14}:
      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}

def diagonal11_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t3_2,t3_7,t3_8,t3_13}:
      diagonal11_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)

def diagonal11_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t2_1,t2_6,t2_11,t2_12}:
      diagonal11_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)

def diagonal11_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match q:
    case T.Q{t1_0,t1_5,t1_10,t1_15}:
      diagonal11_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)

# Round 11, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
def diagonal11(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
  match v:
    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
      diagonal11_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)

# Round 11 uses the message schedule SIGMA[1], fixed at compile time.
def round11(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
  diagonal11(column11(v,m14,m10,m4,m8,m9,m15,m13,m6),m1,m12,m0,m2,m11,m7,m5,m3)

def rounds(v: T.State, +m0: T.Lane, +m1: T.Lane, +m2: T.Lane, +m3: T.Lane, +m4: T.Lane, +m5: T.Lane, +m6: T.Lane, +m7: T.Lane, +m8: T.Lane, +m9: T.Lane, +m10: T.Lane, +m11: T.Lane, +m12: T.Lane, +m13: T.Lane, +m14: T.Lane, +m15: T.Lane) -> T.State:
  round11(round10(round9(round8(round7(round6(round5(round4(round3(round2(round1(round0(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)

# v = h[0..7] || IV[0..7], v12 ^= t low 64 bits, v13 ^= t high 64 bits; a block that is not the last.
def start(h: T.Chain, t: T.Counter) -> T.State:
  match h t:
    case T.H{h0,h1,h2,h3,h4,h5,h6,h7} T.C{t0,t1,t2,t3}:
      T.V{h0,h1,h2,h3,h4,h5,h6,h7,T.W{4089235720,1779033703},T.W{2227873595,3144134277},T.W{4271175723,1013904242},T.W{1595750129,2773480762},L.xor(T.W{2917565137,1359893119},T.W{t0,t1}),L.xor(T.W{725511199,2600822924},T.W{t2,t3}),T.W{4215389547,528734635},T.W{327033209,1541459225}}

# v = h[0..7] || IV[0..7], v12 ^= t low 64 bits, v13 ^= t high 64 bits; the last block (v14 inverted).
def start_last(h: T.Chain, t: T.Counter) -> T.State:
  match h t:
    case T.H{h0,h1,h2,h3,h4,h5,h6,h7} T.C{t0,t1,t2,t3}:
      T.V{h0,h1,h2,h3,h4,h5,h6,h7,T.W{4089235720,1779033703},T.W{2227873595,3144134277},T.W{4271175723,1013904242},T.W{1595750129,2773480762},L.xor(T.W{2917565137,1359893119},T.W{t0,t1}),L.xor(T.W{725511199,2600822924},T.W{t2,t3}),L.xor(T.W{4215389547,528734635},T.W{4294967295,4294967295}),T.W{327033209,1541459225}}

# h[i] ^= v[i] ^ v[i+8].
def finish(h: T.Chain, v: T.State) -> T.Chain:
  match h v:
    case T.H{h0,h1,h2,h3,h4,h5,h6,h7} T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}:
      T.H{L.xor(L.xor(h0,v0),v8),L.xor(L.xor(h1,v1),v9),L.xor(L.xor(h2,v2),v10),L.xor(L.xor(h3,v3),v11),L.xor(L.xor(h4,v4),v12),L.xor(L.xor(h5,v5),v13),L.xor(L.xor(h6,v6),v14),L.xor(L.xor(h7,v7),v15)}

# The compression function F on one block of 32 little-endian words.
def compress(+h: T.Chain, t: T.Counter, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, w27: U32, w28: U32, w29: U32, w30: U32, w31: U32) -> T.Chain:
  finish(h,rounds(start(h,t),T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}))

# The compression function F on one block of 32 little-endian words.
def compress_last(+h: T.Chain, t: T.Counter, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, w27: U32, w28: U32, w29: U32, w30: U32, w31: U32) -> T.Chain:
  finish(h,rounds(start_last(h,t),T.W{w0,w1},T.W{w2,w3},T.W{w4,w5},T.W{w6,w7},T.W{w8,w9},T.W{w10,w11},T.W{w12,w13},T.W{w14,w15},T.W{w16,w17},T.W{w18,w19},T.W{w20,w21},T.W{w22,w23},T.W{w24,w25},T.W{w26,w27},T.W{w28,w29},T.W{w30,w31}))

# t += x on the 128-bit counter.
def bump(c: T.Counter, +x: U32) -> T.Counter:
  match c:
    case T.C{c0,c1,c2,c3}:
      +s0 = U32.add(c0,x)
      +k0 = Bool.to_u32(U32.is_lt(s0,x))
      +s1 = U32.add(c1,k0)
      +k1 = Bool.to_u32(U32.is_lt(s1,k0))
      +s2 = U32.add(c2,k1)
      T.C{s0,s1,s2,U32.add(c3,Bool.to_u32(U32.is_lt(s2,k1)))}