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]] arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] arg4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] arg5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] Output Bounds: out1: [0x0 ~> 0xffffffffffffffff] out2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] out3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] out4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] out5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
pub fn divstep(out1: *u64, out2: *[5]u64, out3: *[5]u64, out4: *[4]u64, out5: *[4]u64, arg1: u64, arg2: [5]u64, arg3: [5]u64, arg4: [4]u64, arg5: [4]u64) voidpub fn divstep(out1: *u64, out2: *[5]u64, out3: *[5]u64, out4: *[4]u64, out5: *[4]u64, arg1: u64, arg2: [5]u64, arg3: [5]u64, arg4: [4]u64, arg5: [4]u64) void {
@setRuntimeSafety(mode == .debug);
var x1: u64 = undefined;
var x2: u1 = undefined;
addcarryxU64(&x1, &x2, 0x0, (~arg1), @as(u64, 0x1));
const x3 = @as(u1, @truncate((x1 >> 63))) & @as(u1, @truncate(((arg3[0]) & @as(u64, 0x1))));
var x4: u64 = undefined;
var x5: u1 = undefined;
addcarryxU64(&x4, &x5, 0x0, (~arg1), @as(u64, 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;
var x13: u1 = undefined;
addcarryxU64(&x12, &x13, 0x0, @as(u64, 0x1), (~(arg2[0])));
var x14: u64 = undefined;
var x15: u1 = undefined;
addcarryxU64(&x14, &x15, x13, @as(u64, 0x0), (~(arg2[1])));
var x16: u64 = undefined;
var x17: u1 = undefined;
addcarryxU64(&x16, &x17, x15, @as(u64, 0x0), (~(arg2[2])));
var x18: u64 = undefined;
var x19: u1 = undefined;
addcarryxU64(&x18, &x19, x17, @as(u64, 0x0), (~(arg2[3])));
var x20: u64 = undefined;
var x21: u1 = undefined;
addcarryxU64(&x20, &x21, x19, @as(u64, 0x0), (~(arg2[4])));
var x22: u64 = undefined;
cmovznzU64(&x22, x3, (arg3[0]), x12);
var x23: u64 = undefined;
cmovznzU64(&x23, x3, (arg3[1]), x14);
var x24: u64 = undefined;
cmovznzU64(&x24, x3, (arg3[2]), x16);
var x25: u64 = undefined;
cmovznzU64(&x25, x3, (arg3[3]), x18);
var x26: u64 = undefined;
cmovznzU64(&x26, x3, (arg3[4]), x20);
var x27: u64 = undefined;
cmovznzU64(&x27, x3, (arg4[0]), (arg5[0]));
var x28: u64 = undefined;
cmovznzU64(&x28, x3, (arg4[1]), (arg5[1]));
var x29: u64 = undefined;
cmovznzU64(&x29, x3, (arg4[2]), (arg5[2]));
var x30: u64 = undefined;
cmovznzU64(&x30, x3, (arg4[3]), (arg5[3]));
var x31: u64 = undefined;
var x32: u1 = undefined;
addcarryxU64(&x31, &x32, 0x0, x27, x27);
var x33: u64 = undefined;
var x34: u1 = undefined;
addcarryxU64(&x33, &x34, x32, x28, x28);
var x35: u64 = undefined;
var x36: u1 = undefined;
addcarryxU64(&x35, &x36, x34, x29, x29);
var x37: u64 = undefined;
var x38: u1 = undefined;
addcarryxU64(&x37, &x38, x36, x30, x30);
var x39: u64 = undefined;
var x40: u1 = undefined;
subborrowxU64(&x39, &x40, 0x0, x31, 0xf3b9cac2fc632551);
var x41: u64 = undefined;
var x42: u1 = undefined;
subborrowxU64(&x41, &x42, x40, x33, 0xbce6faada7179e84);
var x43: u64 = undefined;
var x44: u1 = undefined;
subborrowxU64(&x43, &x44, x42, x35, 0xffffffffffffffff);
var x45: u64 = undefined;
var x46: u1 = undefined;
subborrowxU64(&x45, &x46, x44, x37, 0xffffffff00000000);
var x47: u64 = undefined;
var x48: u1 = undefined;
subborrowxU64(&x47, &x48, x46, @as(u64, x38), @as(u64, 0x0));
const x49 = (arg4[3]);
const x50 = (arg4[2]);
const x51 = (arg4[1]);
const x52 = (arg4[0]);
var x53: u64 = undefined;
var x54: u1 = undefined;
subborrowxU64(&x53, &x54, 0x0, @as(u64, 0x0), x52);
var x55: u64 = undefined;
var x56: u1 = undefined;
subborrowxU64(&x55, &x56, x54, @as(u64, 0x0), x51);
var x57: u64 = undefined;
var x58: u1 = undefined;
subborrowxU64(&x57, &x58, x56, @as(u64, 0x0), x50);
var x59: u64 = undefined;
var x60: u1 = undefined;
subborrowxU64(&x59, &x60, x58, @as(u64, 0x0), x49);
var x61: u64 = undefined;
cmovznzU64(&x61, x60, @as(u64, 0x0), 0xffffffffffffffff);
var x62: u64 = undefined;
var x63: u1 = undefined;
addcarryxU64(&x62, &x63, 0x0, x53, (x61 & 0xf3b9cac2fc632551));
var x64: u64 = undefined;
var x65: u1 = undefined;
addcarryxU64(&x64, &x65, x63, x55, (x61 & 0xbce6faada7179e84));
var x66: u64 = undefined;
var x67: u1 = undefined;
addcarryxU64(&x66, &x67, x65, x57, x61);
var x68: u64 = undefined;
var x69: u1 = undefined;
addcarryxU64(&x68, &x69, x67, x59, (x61 & 0xffffffff00000000));
var x70: u64 = undefined;
cmovznzU64(&x70, x3, (arg5[0]), x62);
var x71: u64 = undefined;
cmovznzU64(&x71, x3, (arg5[1]), x64);
var x72: u64 = undefined;
cmovznzU64(&x72, x3, (arg5[2]), x66);
var x73: u64 = undefined;
cmovznzU64(&x73, x3, (arg5[3]), x68);
const x74 = @as(u1, @truncate((x22 & @as(u64, 0x1))));
var x75: u64 = undefined;
cmovznzU64(&x75, x74, @as(u64, 0x0), x7);
var x76: u64 = undefined;
cmovznzU64(&x76, x74, @as(u64, 0x0), x8);
var x77: u64 = undefined;
cmovznzU64(&x77, x74, @as(u64, 0x0), x9);
var x78: u64 = undefined;
cmovznzU64(&x78, x74, @as(u64, 0x0), x10);
var x79: u64 = undefined;
cmovznzU64(&x79, x74, @as(u64, 0x0), x11);
var x80: u64 = undefined;
var x81: u1 = undefined;
addcarryxU64(&x80, &x81, 0x0, x22, x75);
var x82: u64 = undefined;
var x83: u1 = undefined;
addcarryxU64(&x82, &x83, x81, x23, x76);
var x84: u64 = undefined;
var x85: u1 = undefined;
addcarryxU64(&x84, &x85, x83, x24, x77);
var x86: u64 = undefined;
var x87: u1 = undefined;
addcarryxU64(&x86, &x87, x85, x25, x78);
var x88: u64 = undefined;
var x89: u1 = undefined;
addcarryxU64(&x88, &x89, x87, x26, x79);
var x90: u64 = undefined;
cmovznzU64(&x90, x74, @as(u64, 0x0), x27);
var x91: u64 = undefined;
cmovznzU64(&x91, x74, @as(u64, 0x0), x28);
var x92: u64 = undefined;
cmovznzU64(&x92, x74, @as(u64, 0x0), x29);
var x93: u64 = undefined;
cmovznzU64(&x93, x74, @as(u64, 0x0), x30);
var x94: u64 = undefined;
var x95: u1 = undefined;
addcarryxU64(&x94, &x95, 0x0, x70, x90);
var x96: u64 = undefined;
var x97: u1 = undefined;
addcarryxU64(&x96, &x97, x95, x71, x91);
var x98: u64 = undefined;
var x99: u1 = undefined;
addcarryxU64(&x98, &x99, x97, x72, x92);
var x100: u64 = undefined;
var x101: u1 = undefined;
addcarryxU64(&x100, &x101, x99, x73, x93);
var x102: u64 = undefined;
var x103: u1 = undefined;
subborrowxU64(&x102, &x103, 0x0, x94, 0xf3b9cac2fc632551);
var x104: u64 = undefined;
var x105: u1 = undefined;
subborrowxU64(&x104, &x105, x103, x96, 0xbce6faada7179e84);
var x106: u64 = undefined;
var x107: u1 = undefined;
subborrowxU64(&x106, &x107, x105, x98, 0xffffffffffffffff);
var x108: u64 = undefined;
var x109: u1 = undefined;
subborrowxU64(&x108, &x109, x107, x100, 0xffffffff00000000);
var x110: u64 = undefined;
var x111: u1 = undefined;
subborrowxU64(&x110, &x111, x109, @as(u64, x101), @as(u64, 0x0));
var x112: u64 = undefined;
var x113: u1 = undefined;
addcarryxU64(&x112, &x113, 0x0, x6, @as(u64, 0x1));
const x114 = ((x80 >> 1) | ((x82 << 63) & 0xffffffffffffffff));
const x115 = ((x82 >> 1) | ((x84 << 63) & 0xffffffffffffffff));
const x116 = ((x84 >> 1) | ((x86 << 63) & 0xffffffffffffffff));
const x117 = ((x86 >> 1) | ((x88 << 63) & 0xffffffffffffffff));
const x118 = ((x88 & 0x8000000000000000) | (x88 >> 1));
var x119: u64 = undefined;
cmovznzU64(&x119, x48, x39, x31);
var x120: u64 = undefined;
cmovznzU64(&x120, x48, x41, x33);
var x121: u64 = undefined;
cmovznzU64(&x121, x48, x43, x35);
var x122: u64 = undefined;
cmovznzU64(&x122, x48, x45, x37);
var x123: u64 = undefined;
cmovznzU64(&x123, x111, x102, x94);
var x124: u64 = undefined;
cmovznzU64(&x124, x111, x104, x96);
var x125: u64 = undefined;
cmovznzU64(&x125, x111, x106, x98);
var x126: u64 = undefined;
cmovznzU64(&x126, x111, x108, x100);
out1.* = x112;
out2[0] = x7;
out2[1] = x8;
out2[2] = x9;
out2[3] = x10;
out2[4] = x11;
out3[0] = x114;
out3[1] = x115;
out3[2] = x116;
out3[3] = x117;
out3[4] = x118;
out4[0] = x119;
out4[1] = x120;
out4[2] = x121;
out4[3] = x122;
out5[0] = x123;
out5[1] = x124;
out5[2] = x125;
out5[3] = x126;
}