The function divstep computes a divstep.
Preconditions: 0 ≤ eval arg4 < m 0 ≤ eval arg5 < m Postconditions: out1 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then 1 - arg1 else 1 + arg1) twos_complement_eval out2 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then twos_complement_eval arg3 else twos_complement_eval arg2) twos_complement_eval out3 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then ⌊(twos_complement_eval arg3 - twos_complement_eval arg2) / 2⌋ else ⌊(twos_complement_eval arg3 + (twos_complement_eval arg3 mod 2) * twos_complement_eval arg2) / 2⌋) eval (from_montgomery out4) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (2 * eval (from_montgomery arg5)) mod m else (2 * eval (from_montgomery arg4)) mod m) eval (from_montgomery out5) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (eval (from_montgomery arg4) - eval (from_montgomery arg4)) mod m else (eval (from_montgomery arg5) + (twos_complement_eval arg3 mod 2) * eval (from_montgomery arg4)) mod m) 0 ≤ eval out5 < m 0 ≤ eval out5 < m 0 ≤ eval out2 < m 0 ≤ eval out3 < m
Input Bounds: arg1: [0x0 ~> 0xffffffffffffffff] arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] arg4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] arg5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] Output Bounds: out1: [0x0 ~> 0xffffffffffffffff] out2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] out3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] out4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] out5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
pub fn divstep(out1: *u64, out2: *[7]u64, out3: *[7]u64, out4: *[6]u64, out5: *[6]u64, arg1: u64, arg2: [7]u64, arg3: [7]u64, arg4: [6]u64, arg5: [6]u64) voidpub fn divstep(out1: *u64, out2: *[7]u64, out3: *[7]u64, out4: *[6]u64, out5: *[6]u64, arg1: u64, arg2: [7]u64, arg3: [7]u64, arg4: [6]u64, arg5: [6]u64) void {
@setRuntimeSafety(mode == .debug);
var x1: u64 = undefined;
var x2: u1 = undefined;
addcarryxU64(&x1, &x2, 0x0, (~arg1), 0x1);
const x3 = (@as(u1, @truncate((x1 >> 63))) & @as(u1, @truncate(((arg3[0]) & 0x1))));
var x4: u64 = undefined;
var x5: u1 = undefined;
addcarryxU64(&x4, &x5, 0x0, (~arg1), 0x1);
var x6: u64 = undefined;
cmovznzU64(&x6, x3, arg1, x4);
var x7: u64 = undefined;
cmovznzU64(&x7, x3, (arg2[0]), (arg3[0]));
var x8: u64 = undefined;
cmovznzU64(&x8, x3, (arg2[1]), (arg3[1]));
var x9: u64 = undefined;
cmovznzU64(&x9, x3, (arg2[2]), (arg3[2]));
var x10: u64 = undefined;
cmovznzU64(&x10, x3, (arg2[3]), (arg3[3]));
var x11: u64 = undefined;
cmovznzU64(&x11, x3, (arg2[4]), (arg3[4]));
var x12: u64 = undefined;
cmovznzU64(&x12, x3, (arg2[5]), (arg3[5]));
var x13: u64 = undefined;
cmovznzU64(&x13, x3, (arg2[6]), (arg3[6]));
var x14: u64 = undefined;
var x15: u1 = undefined;
addcarryxU64(&x14, &x15, 0x0, 0x1, (~(arg2[0])));
var x16: u64 = undefined;
var x17: u1 = undefined;
addcarryxU64(&x16, &x17, x15, 0x0, (~(arg2[1])));
var x18: u64 = undefined;
var x19: u1 = undefined;
addcarryxU64(&x18, &x19, x17, 0x0, (~(arg2[2])));
var x20: u64 = undefined;
var x21: u1 = undefined;
addcarryxU64(&x20, &x21, x19, 0x0, (~(arg2[3])));
var x22: u64 = undefined;
var x23: u1 = undefined;
addcarryxU64(&x22, &x23, x21, 0x0, (~(arg2[4])));
var x24: u64 = undefined;
var x25: u1 = undefined;
addcarryxU64(&x24, &x25, x23, 0x0, (~(arg2[5])));
var x26: u64 = undefined;
var x27: u1 = undefined;
addcarryxU64(&x26, &x27, x25, 0x0, (~(arg2[6])));
var x28: u64 = undefined;
cmovznzU64(&x28, x3, (arg3[0]), x14);
var x29: u64 = undefined;
cmovznzU64(&x29, x3, (arg3[1]), x16);
var x30: u64 = undefined;
cmovznzU64(&x30, x3, (arg3[2]), x18);
var x31: u64 = undefined;
cmovznzU64(&x31, x3, (arg3[3]), x20);
var x32: u64 = undefined;
cmovznzU64(&x32, x3, (arg3[4]), x22);
var x33: u64 = undefined;
cmovznzU64(&x33, x3, (arg3[5]), x24);
var x34: u64 = undefined;
cmovznzU64(&x34, x3, (arg3[6]), x26);
var x35: u64 = undefined;
cmovznzU64(&x35, x3, (arg4[0]), (arg5[0]));
var x36: u64 = undefined;
cmovznzU64(&x36, x3, (arg4[1]), (arg5[1]));
var x37: u64 = undefined;
cmovznzU64(&x37, x3, (arg4[2]), (arg5[2]));
var x38: u64 = undefined;
cmovznzU64(&x38, x3, (arg4[3]), (arg5[3]));
var x39: u64 = undefined;
cmovznzU64(&x39, x3, (arg4[4]), (arg5[4]));
var x40: u64 = undefined;
cmovznzU64(&x40, x3, (arg4[5]), (arg5[5]));
var x41: u64 = undefined;
var x42: u1 = undefined;
addcarryxU64(&x41, &x42, 0x0, x35, x35);
var x43: u64 = undefined;
var x44: u1 = undefined;
addcarryxU64(&x43, &x44, x42, x36, x36);
var x45: u64 = undefined;
var x46: u1 = undefined;
addcarryxU64(&x45, &x46, x44, x37, x37);
var x47: u64 = undefined;
var x48: u1 = undefined;
addcarryxU64(&x47, &x48, x46, x38, x38);
var x49: u64 = undefined;
var x50: u1 = undefined;
addcarryxU64(&x49, &x50, x48, x39, x39);
var x51: u64 = undefined;
var x52: u1 = undefined;
addcarryxU64(&x51, &x52, x50, x40, x40);
var x53: u64 = undefined;
var x54: u1 = undefined;
subborrowxU64(&x53, &x54, 0x0, x41, 0xecec196accc52973);
var x55: u64 = undefined;
var x56: u1 = undefined;
subborrowxU64(&x55, &x56, x54, x43, 0x581a0db248b0a77a);
var x57: u64 = undefined;
var x58: u1 = undefined;
subborrowxU64(&x57, &x58, x56, x45, 0xc7634d81f4372ddf);
var x59: u64 = undefined;
var x60: u1 = undefined;
subborrowxU64(&x59, &x60, x58, x47, 0xffffffffffffffff);
var x61: u64 = undefined;
var x62: u1 = undefined;
subborrowxU64(&x61, &x62, x60, x49, 0xffffffffffffffff);
var x63: u64 = undefined;
var x64: u1 = undefined;
subborrowxU64(&x63, &x64, x62, x51, 0xffffffffffffffff);
var x65: u64 = undefined;
var x66: u1 = undefined;
subborrowxU64(&x65, &x66, x64, @as(u64, x52), 0x0);
const x67 = (arg4[5]);
const x68 = (arg4[4]);
const x69 = (arg4[3]);
const x70 = (arg4[2]);
const x71 = (arg4[1]);
const x72 = (arg4[0]);
var x73: u64 = undefined;
var x74: u1 = undefined;
subborrowxU64(&x73, &x74, 0x0, 0x0, x72);
var x75: u64 = undefined;
var x76: u1 = undefined;
subborrowxU64(&x75, &x76, x74, 0x0, x71);
var x77: u64 = undefined;
var x78: u1 = undefined;
subborrowxU64(&x77, &x78, x76, 0x0, x70);
var x79: u64 = undefined;
var x80: u1 = undefined;
subborrowxU64(&x79, &x80, x78, 0x0, x69);
var x81: u64 = undefined;
var x82: u1 = undefined;
subborrowxU64(&x81, &x82, x80, 0x0, x68);
var x83: u64 = undefined;
var x84: u1 = undefined;
subborrowxU64(&x83, &x84, x82, 0x0, x67);
var x85: u64 = undefined;
cmovznzU64(&x85, x84, 0x0, 0xffffffffffffffff);
var x86: u64 = undefined;
var x87: u1 = undefined;
addcarryxU64(&x86, &x87, 0x0, x73, (x85 & 0xecec196accc52973));
var x88: u64 = undefined;
var x89: u1 = undefined;
addcarryxU64(&x88, &x89, x87, x75, (x85 & 0x581a0db248b0a77a));
var x90: u64 = undefined;
var x91: u1 = undefined;
addcarryxU64(&x90, &x91, x89, x77, (x85 & 0xc7634d81f4372ddf));
var x92: u64 = undefined;
var x93: u1 = undefined;
addcarryxU64(&x92, &x93, x91, x79, x85);
var x94: u64 = undefined;
var x95: u1 = undefined;
addcarryxU64(&x94, &x95, x93, x81, x85);
var x96: u64 = undefined;
var x97: u1 = undefined;
addcarryxU64(&x96, &x97, x95, x83, x85);
var x98: u64 = undefined;
cmovznzU64(&x98, x3, (arg5[0]), x86);
var x99: u64 = undefined;
cmovznzU64(&x99, x3, (arg5[1]), x88);
var x100: u64 = undefined;
cmovznzU64(&x100, x3, (arg5[2]), x90);
var x101: u64 = undefined;
cmovznzU64(&x101, x3, (arg5[3]), x92);
var x102: u64 = undefined;
cmovznzU64(&x102, x3, (arg5[4]), x94);
var x103: u64 = undefined;
cmovznzU64(&x103, x3, (arg5[5]), x96);
const x104 = @as(u1, @truncate((x28 & 0x1)));
var x105: u64 = undefined;
cmovznzU64(&x105, x104, 0x0, x7);
var x106: u64 = undefined;
cmovznzU64(&x106, x104, 0x0, x8);
var x107: u64 = undefined;
cmovznzU64(&x107, x104, 0x0, x9);
var x108: u64 = undefined;
cmovznzU64(&x108, x104, 0x0, x10);
var x109: u64 = undefined;
cmovznzU64(&x109, x104, 0x0, x11);
var x110: u64 = undefined;
cmovznzU64(&x110, x104, 0x0, x12);
var x111: u64 = undefined;
cmovznzU64(&x111, x104, 0x0, x13);
var x112: u64 = undefined;
var x113: u1 = undefined;
addcarryxU64(&x112, &x113, 0x0, x28, x105);
var x114: u64 = undefined;
var x115: u1 = undefined;
addcarryxU64(&x114, &x115, x113, x29, x106);
var x116: u64 = undefined;
var x117: u1 = undefined;
addcarryxU64(&x116, &x117, x115, x30, x107);
var x118: u64 = undefined;
var x119: u1 = undefined;
addcarryxU64(&x118, &x119, x117, x31, x108);
var x120: u64 = undefined;
var x121: u1 = undefined;
addcarryxU64(&x120, &x121, x119, x32, x109);
var x122: u64 = undefined;
var x123: u1 = undefined;
addcarryxU64(&x122, &x123, x121, x33, x110);
var x124: u64 = undefined;
var x125: u1 = undefined;
addcarryxU64(&x124, &x125, x123, x34, x111);
var x126: u64 = undefined;
cmovznzU64(&x126, x104, 0x0, x35);
var x127: u64 = undefined;
cmovznzU64(&x127, x104, 0x0, x36);
var x128: u64 = undefined;
cmovznzU64(&x128, x104, 0x0, x37);
var x129: u64 = undefined;
cmovznzU64(&x129, x104, 0x0, x38);
var x130: u64 = undefined;
cmovznzU64(&x130, x104, 0x0, x39);
var x131: u64 = undefined;
cmovznzU64(&x131, x104, 0x0, x40);
var x132: u64 = undefined;
var x133: u1 = undefined;
addcarryxU64(&x132, &x133, 0x0, x98, x126);
var x134: u64 = undefined;
var x135: u1 = undefined;
addcarryxU64(&x134, &x135, x133, x99, x127);
var x136: u64 = undefined;
var x137: u1 = undefined;
addcarryxU64(&x136, &x137, x135, x100, x128);
var x138: u64 = undefined;
var x139: u1 = undefined;
addcarryxU64(&x138, &x139, x137, x101, x129);
var x140: u64 = undefined;
var x141: u1 = undefined;
addcarryxU64(&x140, &x141, x139, x102, x130);
var x142: u64 = undefined;
var x143: u1 = undefined;
addcarryxU64(&x142, &x143, x141, x103, x131);
var x144: u64 = undefined;
var x145: u1 = undefined;
subborrowxU64(&x144, &x145, 0x0, x132, 0xecec196accc52973);
var x146: u64 = undefined;
var x147: u1 = undefined;
subborrowxU64(&x146, &x147, x145, x134, 0x581a0db248b0a77a);
var x148: u64 = undefined;
var x149: u1 = undefined;
subborrowxU64(&x148, &x149, x147, x136, 0xc7634d81f4372ddf);
var x150: u64 = undefined;
var x151: u1 = undefined;
subborrowxU64(&x150, &x151, x149, x138, 0xffffffffffffffff);
var x152: u64 = undefined;
var x153: u1 = undefined;
subborrowxU64(&x152, &x153, x151, x140, 0xffffffffffffffff);
var x154: u64 = undefined;
var x155: u1 = undefined;
subborrowxU64(&x154, &x155, x153, x142, 0xffffffffffffffff);
var x156: u64 = undefined;
var x157: u1 = undefined;
subborrowxU64(&x156, &x157, x155, @as(u64, x143), 0x0);
var x158: u64 = undefined;
var x159: u1 = undefined;
addcarryxU64(&x158, &x159, 0x0, x6, 0x1);
const x160 = ((x112 >> 1) | ((x114 << 63) & 0xffffffffffffffff));
const x161 = ((x114 >> 1) | ((x116 << 63) & 0xffffffffffffffff));
const x162 = ((x116 >> 1) | ((x118 << 63) & 0xffffffffffffffff));
const x163 = ((x118 >> 1) | ((x120 << 63) & 0xffffffffffffffff));
const x164 = ((x120 >> 1) | ((x122 << 63) & 0xffffffffffffffff));
const x165 = ((x122 >> 1) | ((x124 << 63) & 0xffffffffffffffff));
const x166 = ((x124 & 0x8000000000000000) | (x124 >> 1));
var x167: u64 = undefined;
cmovznzU64(&x167, x66, x53, x41);
var x168: u64 = undefined;
cmovznzU64(&x168, x66, x55, x43);
var x169: u64 = undefined;
cmovznzU64(&x169, x66, x57, x45);
var x170: u64 = undefined;
cmovznzU64(&x170, x66, x59, x47);
var x171: u64 = undefined;
cmovznzU64(&x171, x66, x61, x49);
var x172: u64 = undefined;
cmovznzU64(&x172, x66, x63, x51);
var x173: u64 = undefined;
cmovznzU64(&x173, x157, x144, x132);
var x174: u64 = undefined;
cmovznzU64(&x174, x157, x146, x134);
var x175: u64 = undefined;
cmovznzU64(&x175, x157, x148, x136);
var x176: u64 = undefined;
cmovznzU64(&x176, x157, x150, x138);
var x177: u64 = undefined;
cmovznzU64(&x177, x157, x152, x140);
var x178: u64 = undefined;
cmovznzU64(&x178, x157, x154, x142);
out1.* = x158;
out2[0] = x7;
out2[1] = x8;
out2[2] = x9;
out2[3] = x10;
out2[4] = x11;
out2[5] = x12;
out2[6] = x13;
out3[0] = x160;
out3[1] = x161;
out3[2] = x162;
out3[3] = x163;
out3[4] = x164;
out3[5] = x165;
out3[6] = x166;
out4[0] = x167;
out4[1] = x168;
out4[2] = x169;
out4[3] = x170;
out4[4] = x171;
out4[5] = x172;
out5[0] = x173;
out5[1] = x174;
out5[2] = x175;
out5[3] = x176;
out5[4] = x177;
out5[5] = x178;
}