import zkLeanExamples.DefFF

set_option maxHeartbeats  20000000000000000000

--interleaved
def AND_64 : Subtable (ZMod ff) 64 :=
  subtableFromMLE (fun x => 0 + 2147483648*x[0]*x[1] + 1073741824*x[2]*x[3] + 536870912*x[4]*x[5] + 268435456*x[6]*x[7] + 134217728*x[8]*x[9] + 67108864*x[10]*x[11] + 33554432*x[12]*x[13] + 16777216*x[14]*x[15] + 8388608*x[16]*x[17] + 4194304*x[18]*x[19] + 2097152*x[20]*x[21] + 1048576*x[22]*x[23] + 524288*x[24]*x[25] + 262144*x[26]*x[27] + 131072*x[28]*x[29] + 65536*x[30]*x[31] + 32768*x[32]*x[33] + 16384*x[34]*x[35] + 8192*x[36]*x[37] + 4096*x[38]*x[39] + 2048*x[40]*x[41] + 1024*x[42]*x[43] + 512*x[44]*x[45] + 256*x[46]*x[47] + 128*x[48]*x[49] + 64*x[50]*x[51] + 32*x[52]*x[53] + 16*x[54]*x[55] + 8*x[56]*x[57] + 4*x[58]*x[59] + 2*x[60]*x[61] + 1*x[62]*x[63])

lemma and_32_mle_one_chunk_ (bv1 bv2 : BitVec 32) (fv1 fv2 : Vector (ZMod ff) 32) :
    some bvoutput = BVModEq.map_f_to_bv 32 foutput ->
    some (BVModEq.bool_to_bv 32 bv1[31])  = BVModEq.map_f_to_bv 32 fv1[0]  ->
    some (BVModEq.bool_to_bv 32 bv2[31])  =BVModEq.map_f_to_bv 32 fv1[1]  ->
    some (BVModEq.bool_to_bv 32 bv1[30]) = BVModEq.map_f_to_bv 32 fv1[2]  ->
    some (BVModEq.bool_to_bv 32 bv2[30]) = BVModEq.map_f_to_bv 32 fv1[3]  ->
    some (BVModEq.bool_to_bv 32 bv1[29]) = BVModEq.map_f_to_bv 32 fv1[4]  ->
    some (BVModEq.bool_to_bv 32 bv2[29]) = BVModEq.map_f_to_bv 32 fv1[5]  ->
    some (BVModEq.bool_to_bv 32 bv1[28]) = BVModEq.map_f_to_bv 32 fv1[6]  ->
    some (BVModEq.bool_to_bv 32 bv2[28]) = BVModEq.map_f_to_bv 32 fv1[7]  ->
    some (BVModEq.bool_to_bv 32 bv1[27])  = BVModEq.map_f_to_bv 32 fv1[8]  ->
    some (BVModEq.bool_to_bv 32 bv2[27]) = BVModEq.map_f_to_bv 32 fv1[9]  ->
    some (BVModEq.bool_to_bv 32 bv1[26]) = BVModEq.map_f_to_bv 32 fv1[10]  ->
    some (BVModEq.bool_to_bv 32 bv2[26]) = BVModEq.map_f_to_bv 32 fv1[11]  ->
    some (BVModEq.bool_to_bv 32 bv1[25]) = BVModEq.map_f_to_bv 32 fv1[12]  ->
    some (BVModEq.bool_to_bv 32 bv2[25]) = BVModEq.map_f_to_bv 32 fv1[13]  ->
    some (BVModEq.bool_to_bv 32 bv1[24]) = BVModEq.map_f_to_bv 32 fv1[14]  ->
    some (BVModEq.bool_to_bv 32 bv2[24]) = BVModEq.map_f_to_bv 32 fv1[15]  ->
    some (BVModEq.bool_to_bv 32 bv1[23])  = BVModEq.map_f_to_bv 32 fv1[16]  ->
    some (BVModEq.bool_to_bv 32 bv2[23]) = BVModEq.map_f_to_bv 32 fv1[17]  ->
    some (BVModEq.bool_to_bv 32 bv1[22]) = BVModEq.map_f_to_bv 32 fv1[18]  ->
    some (BVModEq.bool_to_bv 32 bv2[22]) = BVModEq.map_f_to_bv 32 fv1[19]  ->
    some (BVModEq.bool_to_bv 32 bv1[21]) = BVModEq.map_f_to_bv 32 fv1[20]  ->
    some (BVModEq.bool_to_bv 32 bv2[21]) = BVModEq.map_f_to_bv 32 fv1[21]  ->
    some (BVModEq.bool_to_bv 32 bv1[20]) = BVModEq.map_f_to_bv 32 fv1[22]  ->
    some (BVModEq.bool_to_bv 32 bv2[20]) = BVModEq.map_f_to_bv 32 fv1[23]  ->
    some (BVModEq.bool_to_bv 32 bv1[19])  = BVModEq.map_f_to_bv 32 fv1[24]  ->
    some (BVModEq.bool_to_bv 32 bv2[19]) = BVModEq.map_f_to_bv 32 fv1[25]  ->
    some (BVModEq.bool_to_bv 32 bv1[18]) = BVModEq.map_f_to_bv 32 fv1[26]  ->
    some (BVModEq.bool_to_bv 32 bv2[18]) = BVModEq.map_f_to_bv 32 fv1[27]  ->
    some (BVModEq.bool_to_bv 32 bv1[17]) = BVModEq.map_f_to_bv 32 fv1[28]  ->
    some (BVModEq.bool_to_bv 32 bv2[17]) = BVModEq.map_f_to_bv 32 fv1[29]  ->
    some (BVModEq.bool_to_bv 32 bv1[16]) = BVModEq.map_f_to_bv 32 fv1[30]  ->
    some (BVModEq.bool_to_bv 32 bv2[16]) = BVModEq.map_f_to_bv 32 fv1[31]  ->
    some (BVModEq.bool_to_bv 32 bv1[15])  = BVModEq.map_f_to_bv 32 fv2[0]  ->
    some (BVModEq.bool_to_bv 32 bv2[15]) = BVModEq.map_f_to_bv 32 fv2[1]  ->
    some (BVModEq.bool_to_bv 32 bv1[14]) = BVModEq.map_f_to_bv 32 fv2[2]  ->
    some (BVModEq.bool_to_bv 32 bv2[14]) = BVModEq.map_f_to_bv 32 fv2[3]  ->
    some (BVModEq.bool_to_bv 32 bv1[13]) = BVModEq.map_f_to_bv 32 fv2[4]  ->
    some (BVModEq.bool_to_bv 32 bv2[13]) = BVModEq.map_f_to_bv 32 fv2[5]  ->
    some (BVModEq.bool_to_bv 32 bv1[12]) = BVModEq.map_f_to_bv 32 fv2[6]  ->
    some (BVModEq.bool_to_bv 32 bv2[12]) = BVModEq.map_f_to_bv 32 fv2[7]  ->
    some (BVModEq.bool_to_bv 32 bv1[11]) = BVModEq.map_f_to_bv 32 fv2[8]  ->
    some (BVModEq.bool_to_bv 32 bv2[11]) = BVModEq.map_f_to_bv 32 fv2[9]  ->
    some (BVModEq.bool_to_bv 32 bv1[10]) = BVModEq.map_f_to_bv 32  fv2[10]  ->
    some (BVModEq.bool_to_bv 32 bv2[10]) = BVModEq.map_f_to_bv 32 fv2[11]  ->
    some (BVModEq.bool_to_bv 32 bv1[9]) = BVModEq.map_f_to_bv 32 fv2[12]  ->
    some (BVModEq.bool_to_bv 32 bv2[9]) = BVModEq.map_f_to_bv 32 fv2[13]  ->
    some (BVModEq.bool_to_bv 32 bv1[8]) = BVModEq.map_f_to_bv 32 fv2[14]  ->
    some (BVModEq.bool_to_bv 32 bv2[8]) = BVModEq.map_f_to_bv 32 fv2[15]  ->
    some (BVModEq.bool_to_bv 32 bv1[7])  = BVModEq.map_f_to_bv 32 fv2[16]  ->
    some (BVModEq.bool_to_bv 32 bv2[7]) =BVModEq.map_f_to_bv 32 fv2[17]  ->
    some (BVModEq.bool_to_bv 32 bv1[6]) = BVModEq.map_f_to_bv 32 fv2[18]  ->
    some (BVModEq.bool_to_bv 32 bv2[6]) = BVModEq.map_f_to_bv 32 fv2[19]  ->
    some (BVModEq.bool_to_bv 32 bv1[5]) = BVModEq.map_f_to_bv 32 fv2[20]  ->
    some (BVModEq.bool_to_bv 32 bv2[5]) = BVModEq.map_f_to_bv 32 fv2[21]  ->
    some (BVModEq.bool_to_bv 32 bv1[4]) = BVModEq.map_f_to_bv 32 fv2[22]  ->
    some (BVModEq.bool_to_bv 32 bv2[4]) = BVModEq.map_f_to_bv 32 fv2[23]  ->
    some (BVModEq.bool_to_bv 32 bv1[3]) = BVModEq.map_f_to_bv 32 fv2[24]  ->
    some (BVModEq.bool_to_bv 32 bv2[3]) = BVModEq.map_f_to_bv 32 fv2[25]  ->
    some (BVModEq.bool_to_bv 32 bv1[2]) = BVModEq.map_f_to_bv 32  fv2[26]  ->
    some (BVModEq.bool_to_bv 32 bv2[2]) = BVModEq.map_f_to_bv 32 fv2[27]  ->
    some (BVModEq.bool_to_bv 32 bv1[1]) = BVModEq.map_f_to_bv 32 fv2[28]  ->
    some (BVModEq.bool_to_bv 32 bv2[1]) = BVModEq.map_f_to_bv 32 fv2[29]  ->
    some (BVModEq.bool_to_bv 32 bv1[0]) = BVModEq.map_f_to_bv 32 fv2[30]  ->
    some (BVModEq.bool_to_bv 32 bv2[0]) = BVModEq.map_f_to_bv 32 fv2[31]  ->
  (bvoutput = (bv1 &&& bv2))
  =
  (foutput = evalSubtable AND_64 (Vector.append fv1 fv2))
:= by
 unfold AND_64
 unfold evalSubtable
 simp (config := { failIfUnchanged := false })
 unfold subtableFromMLE
 simp (config := { failIfUnchanged := false })
 unfold Vector.append
 simp (config := { failIfUnchanged := false })
 solveMLE 32
