Skip to content
GitLab
Commit 3ab5cbd5 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

added 64- 80- and 96-bit karatsuba versions

parent 5d08ecc9
Expand all Hide whitespace changes
Inline Side-by-side
avr_code2.mlw 0 → 100644
View file @ 3ab5cbd5
This diff is collapsed.
avr_code2/why3session.xml 0 → 100644
View file @ 3ab5cbd5
This diff is collapsed.
avr_code3.mlw 0 → 100644
View file @ 3ab5cbd5
module BV_asr_Lemmas
use import bv.BV8
use import int.Int
use import bv.Pow2int
use import int.EuclideanDivision
lemma asr_0: eq (asr zeros 1) zeros
lemma asr_1: eq (asr (of_int 1) 1) zeros
lemma asr_f: eq (asr ones 1) ones
lemma xor_0: forall w. 0 <= w < 256 -> to_uint (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> to_uint (bw_xor (of_int w) ones) = 255 - w
lemma or_0: forall w. bw_or zeros w = w
lemma pow2_72: pow2 72 = 0x1000000000000000000
lemma pow2_80: pow2 80 = 0x100000000000000000000
lemma pow2_88: pow2 88 = 0x10000000000000000000000
lemma pow2_96: pow2 96 = 0x1000000000000000000000000
lemma pow2_104: pow2 104 = 0x100000000000000000000000000
lemma pow2_112: pow2 112 = 0x10000000000000000000000000000
lemma pow2_120: pow2 120 = 0x1000000000000000000000000000000
lemma pow2_128: pow2 128 = 0x100000000000000000000000000000000
lemma pow2_136: pow2 136 = 0x10000000000000000000000000000000000
lemma pow2_144: pow2 144 = 0x1000000000000000000000000000000000000
lemma pow2_152: pow2 152 = 0x100000000000000000000000000000000000000
lemma pow2_160: pow2 160 = 0x10000000000000000000000000000000000000000
lemma pow2_168: pow2 168 = 0x1000000000000000000000000000000000000000000
lemma pow2_176: pow2 176 = 0x100000000000000000000000000000000000000000000
lemma pow2_184: pow2 184 = 0x10000000000000000000000000000000000000000000000
lemma pow2_192: pow2 192 = 0x1000000000000000000000000000000000000000000000000
lemma pow2_200: pow2 200 = 0x100000000000000000000000000000000000000000000000000
lemma pow2_208: pow2 208 = 0x10000000000000000000000000000000000000000000000000000
lemma pow2_216: pow2 216 = 0x1000000000000000000000000000000000000000000000000000000
lemma pow2_224: pow2 224 = 0x100000000000000000000000000000000000000000000000000000000
lemma pow2_232: pow2 232 = 0x10000000000000000000000000000000000000000000000000000000000
lemma pow2_240: pow2 240 = 0x1000000000000000000000000000000000000000000000000000000000000
lemma pow2_248: pow2 248 = 0x100000000000000000000000000000000000000000000000000000000000000
end
module AvrModelLemmas
use import int.Int
use import map.Map
use import int.EuclideanDivision
use import bv.Pow2int
lemma register_file_invariant_strengthen:
forall m: map int int. (forall i. 0 <= m[i] < 256) -> (forall i j. 0 <= m[i]*m[j] <= 255*255)
lemma pow_split: forall k. k >= 0 -> pow2 (2*k) = pow2 k*pow2 k
end
module KaratAvr
use import avrmodel2.AVRint
use import int.Int
use import int.EuclideanDivision
use import bv.Pow2int
use import AvrModelLemmas
use BV_asr_Lemmas
use bv.BV8
function (+:) (x y: int): int = x + pow2 8*y
function (:+) (x y: int): int = pow2 8*x + y
let mul16 (): unit
ensures { uint 4 reg 12 = old(uint 2 reg 2 * uint 2 reg 7) }
=
clr r23;
mul r3 r8;
movw r14 r0;
mul r2 r7;
movw r12 r0;
mul r2 r8;
add r13 r0;
adc r14 r1;
adc r15 r23;
mul r3 r7;
add r13 r0;
adc r14 r1;
adc r15 r23
use import int.Abs
use avrmodel2.Shadow as S
lemma mul_bound_preserve:
forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l
let karatsuba80_marked()
requires { 32 <= uint 2 reg rX < pow2 15 }
requires { 32 <= uint 2 reg rY < pow2 15 }
requires { 32 <= uint 2 reg rZ < pow2 15 }
requires { uint 2 reg rZ <= uint 2 reg rX \/ uint 2 reg rZ >= uint 2 reg rX+10 }
requires { uint 2 reg rZ <= uint 2 reg rY \/ uint 2 reg rZ >= uint 2 reg rY+10 }
ensures { uint 20 mem (old (uint 2 reg rZ)) = old (uint 10 mem (uint 2 reg rX) * uint 10 mem (uint 2 reg rY)) }
=
'S:
(* init rZero registers *)
clr r18;
clr r19;
movw r20 r18;
(* compute l *)
ld_inc r2 rX;
ld_inc r3 rX;
ld_inc r4 rX;
ld_inc r5 rX;
ld_inc r6 rX;
ldd r7 rY 0;
ldd r8 rY 1;
ldd r9 rY 2;
ldd r10 rY 3;
ldd r11 rY 4;
'L00:
S.init();
abstract ensures { S.synchronized S.shadow reg }
ensures { uint 10 reg 12 = old(uint 5 reg 2 * uint 5 reg 7) }
'B:
mul r2 r9;
movw r14 r0;
mul r2 r7;
movw r12 r0;
mul r2 r8;
add r13 r0;
adc r14 r1;
adc r15 r21;
mul r2 r11;
movw r16 r0;
mul r2 r10;
add r15 r0;
adc r16 r1;
adc r17 r21;
mul r3 r9;
movw r24 r0;
mul r3 r7;
add r13 r0;
adc r14 r1;
adc r15 r24;
adc r25 r21;
mul r3 r8;
add r14 r0;
adc r15 r1;
adc r25 r21;
mul r3 r11;
add r16 r25;
adc r17 r0;
adc r18 r1;
mul r3 r10;
add r16 r0;
adc r17 r1;
adc r18 r21;
mul r4 r9;
movw r24 r0;
mul r4 r7;
add r14 r0;
adc r15 r1;
adc r16 r24;
adc r25 r21;
mul r4 r8;
add r15 r0;
adc r16 r1;
adc r25 r21;
mul r4 r11;
add r17 r25;
adc r18 r0;
adc r19 r1;
mul r4 r10;
add r17 r0;
adc r18 r1;
adc r19 r21;
mul r5 r9;
movw r24 r0;
mul r5 r7;
add r15 r0;
adc r16 r1;
adc r17 r24;
adc r25 r21;
mul r5 r8;
add r16 r0;
adc r17 r1;
adc r25 r21;
mul r5 r11;
add r18 r25;
adc r19 r0;
adc r20 r1;
mul r5 r10;
add r18 r0;
adc r19 r1;
adc r20 r21;
mul r6 r9;
movw r24 r0;
mul r6 r7;
add r16 r0;
adc r17 r1;
adc r18 r24;
adc r25 r21;
mul r6 r8;
add r17 r0;
adc r18 r1;
adc r25 r21;
mul r6 r10;
add r19 r0;
adc r20 r1;
adc r21 r21;
mul r6 r11;
add r19 r25;
adc r20 r0;
adc r21 r1;
S.modify_r0(); S.modify_r1();
S.modify_r24(); S.modify_r25();
S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17(); S.modify_r18(); S.modify_r19(); S.modify_r20(); S.modify_r21();
end;
'L00':
std rZ 0 r12;
std rZ 1 r13;
std rZ 2 r14;
std rZ 3 r15;
std rZ 4 r16;
(* load a5..a9 and b5..b9 *)
ld_inc r12 rX;
ld_inc r13 rX;
ld_inc r14 rX;
ld_inc r15 rX;
ld_inc r16 rX;
ldd r23 rY 5;
ldd r24 rY 6;
ldd r25 rY 7;
ldd r26 rY 8;
ldd r27 rY 9;
'L11:
(*TODO *)
assert { at(uint 5 reg 7)'L00 + pow2 40*at(uint 5 reg 23)'L11 = at(uint 10 mem (uint 2 reg rY))'S };
assert { at(uint 5 reg 2*uint 5 reg 7)'L00 = at(uint 5 reg 2*uint 5 reg 7)'L11 };
assert { at(uint 5 reg 2 + pow2 40*uint 5 reg 12)'L11 = at(uint 10 mem (uint 2 reg rX))'S };
S.init();
abstract ensures { S.synchronized S.shadow reg }
ensures { uint 5 reg 2 = old (abs (uint 5 reg 2 - uint 5 reg 12)) }
ensures { uint 5 reg 7 = old (abs (uint 5 reg 7 - uint 5 reg 23)) }
ensures { ?tf = 0 <-> at((uint 5 reg 2 < uint 5 reg 12) <-> (uint 5 reg 7 < uint 5 reg 23))'L11 }
ensures { reg[22] = 0 } (* strange location! *)
(* subtract a0 a5 *)
sub r2 r12;
sbc r3 r13;
sbc r4 r14;
sbc r5 r15;
sbc r6 r16;
(* 0xff if carry and 0x00 if no carry *)
sbc r0 r0;
(* subtract b0 b5 *)
sub r7 r23;
sbc r8 r24;
sbc r9 r25;
sbc r10 r26;
sbc r11 r27;
(* 0xff if carry and 0x00 if no carry *)
sbc r1 r1;
(* absolute values *)
eor r2 r0;
eor r3 r0;
eor r4 r0;
eor r5 r0;
eor r6 r0;
eor r7 r1;
eor r8 r1;
eor r9 r1;
eor r10 r1;
eor r11 r1;
clr r22;
sub r2 r0;
sbc r3 r0;
sbc r4 r0;
sbc r5 r0;
sbc r6 r0;
sub r7 r1;
sbc r8 r1;
sbc r9 r1;
sbc r10 r1;
sbc r11 r1 ;
eor r0 r1;
bst r0 0 ;
S.modify_r0(); S.modify_r1(); S.modify_r22();
S.modify_r2(); S.modify_r3(); S.modify_r4(); S.modify_r5(); S.modify_r6();
S.modify_r7(); S.modify_r8(); S.modify_r9(); S.modify_r10(); S.modify_r11();
end;
S.init();
abstract ensures { S.synchronized S.shadow reg }
ensures { uint 10 reg 17 = old (uint 5 reg 17 + uint 5 reg 12*uint 5 reg 23) }
(* compute h (l5 l6 l7 l8 l9) *)
mul r23 r14;
movw r28 r0;
mul r23 r12;
add r17 r0 ;
adc r18 r1;
adc r19 r28;
adc r29 r22;
mul r23 r13;
add r18 r0;
adc r19 r1;
adc r29 r22;
mul r23 r15;
add r20 r0;
adc r21 r1;
adc r22 r22;
mul r23 r16;
add r20 r29;
adc r21 r0;
adc r22 r1;
clr r23;
mul r24 r14;
movw r28 r0;
mul r24 r12;
add r18 r0;
adc r19 r1;
adc r20 r28;
adc r29 r23;
mul r24 r13;
add r19 r0;
adc r20 r1;
adc r29 r23;
mul r24 r15;
add r21 r0;
adc r22 r1;
adc r23 r23;
mul r24 r16;
add r21 r29;
adc r22 r0;
adc r23 r1;
clr r24;
mul r25 r14;
movw r28 r0;
mul r25 r12;
add r19 r0;
adc r20 r1;
adc r21 r28;
adc r29 r24;
mul r25 r13;
add r20 r0;
adc r21 r1;
adc r29 r24;
mul r25 r15;
add r22 r0;
adc r23 r1;
adc r24 r24;
mul r25 r16;
add r22 r29;
adc r23 r0;
adc r24 r1;
clr r25;
mul r26 r14;
movw r28 r0;
mul r26 r12;
add r20 r0;
adc r21 r1;
adc r22 r28;
adc r29 r25;
mul r26 r13;
add r21 r0;
adc r22 r1;
adc r29 r25;
mul r26 r15;
add r23 r0;
adc r24 r1;
adc r25 r25;
mul r26 r16;
add r23 r29;
adc r24 r0;
adc r25 r1;
clr r26;
mul r27 r14;
movw r28 r0;
mul r27 r12;
add r21 r0;
adc r22 r1;
adc r23 r28;
adc r29 r26;
mul r27 r13;
add r22 r0;
adc r23 r1;
adc r29 r26;
mul r27 r15;
add r24 r0;
adc r25 r1;
adc r26 r26;
mul r27 r16;
add r24 r29;
adc r25 r0;
adc r26 r1;
S.modify_r0(); S.modify_r1();
S.modify_r17(); S.modify_r18(); S.modify_r19(); S.modify_r20(); S.modify_r21(); S.modify_r22(); S.modify_r23(); S.modify_r24(); S.modify_r25(); S.modify_r26();
S.modify_r28(); S.modify_r29();
end;
S.init();
abstract ensures { S.synchronized S.shadow reg }
ensures { uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = old (uint 5 reg 2*uint 5 reg 7) }
(* compute m *)
clr r27;
mul r2 r9;
movw r14 r0;
mul r2 r7;
movw r12 r0;
mul r2 r8;
add r13 r0;
adc r14 r1;
adc r15 r27;
mul r2 r11;
mov r16 r0;
mov r27 r1;
mul r2 r10;
add r15 r0;
adc r16 r1;
clr r2;
adc r27 r2;
mul r3 r9;
movw r28 r0;
mul r3 r7;
add r13 r0;
adc r14 r1;
adc r15 r28;
adc r29 r2;
mul r3 r8;
add r14 r0;
adc r15 r1;
adc r29 r2;
mul r3 r10;
add r16 r0;
adc r27 r1;
adc r2 r2;
mul r3 r11;
add r16 r29;
adc r27 r0;
adc r2 r1;
clr r3;
mul r4 r9;
movw r28 r0;
mul r4 r7;
add r14 r0;
adc r15 r1;
adc r16 r28;
adc r29 r3;
mul r4 r8;
add r15 r0;
adc r16 r1;
adc r29 r3;
mul r4 r10;
add r27 r0;
adc r2 r1;
adc r3 r3;
mul r4 r11;
add r27 r29;
adc r2 r0;
adc r3 r1;
clr r4;
mul r5 r9;
movw r28 r0;
mul r5 r7;
add r15 r0;
adc r16 r1;
adc r27 r28;
adc r29 r4;
mul r5 r8;
add r16 r0;
adc r27 r1;
adc r29 r4;
mul r5 r10;
add r2 r0;
adc r3 r1;
adc r4 r4;
mul r5 r11;
add r2 r29;
adc r3 r0;
adc r4 r1;
clr r5;
mul r6 r9;
movw r28 r0;
mul r6 r7;
add r16 r0;
adc r27 r1;
adc r2 r28;
adc r29 r5;
mul r6 r8;
add r27 r0;
adc r2 r1;
adc r29 r5;
mul r6 r10;
add r3 r0;
adc r4 r1;
adc r5 r5;
mul r6 r11;
add r3 r29;
adc r4 r0;
adc r5 r1;
S.modify_r0(); S.modify_r1();
S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16();
S.modify_r2(); S.modify_r3(); S.modify_r4(); S.modify_r5();
S.modify_r27(); S.modify_r28(); S.modify_r29();
end;
(* add l5 h0 to l0 and h5 *)
ldd r7 rZ 0;
ldd r8 rZ 1;
ldd r9 rZ 2;
ldd r10 rZ 3;
ldd r11 rZ 4 ;
assert { uint 5 reg 7 = at (uint 5 reg 12)'L00' };
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { old(uint 5 reg 7) + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 + ?cf*pow2 120 = (pow2 40+1)*(at(uint 5 reg 2*uint 5 reg 7)'L00 + at(pow2 40*uint 5 reg 12*uint 5 reg 23)'L11) }
'B:
add r7 r17;
adc r8 r18;
adc r9 r19;
adc r10 r20;
adc r11 r21;
adc r17 r22;
adc r18 r23;
adc r19 r24;
adc r20 r25;
adc r21 r26;
assert { uint 5 reg 7 + pow2 40*uint 5 reg 17 + ?cf*pow2 80
= at(uint 5 reg 7 + pow2 40*uint 5 reg 17 + uint 10 reg 17) 'B };
(* store carrrY later in r0 *)
S.modify_r7(); S.modify_r8(); S.modify_r9(); S.modify_r10(); S.modify_r11();
S.modify_r17(); S.modify_r18(); S.modify_r19(); S.modify_r20(); S.modify_r21();
end;
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = ?cf*(pow2 80 - 1) - at((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23))'L11 }
ensures { let cor = reg[28] + (pow2 8+pow2 16+pow2 24+pow2 32)*reg[0] in cor = old ?cf - ?cf \/ cor = pow2 40 + old ?cf - ?cf }
(*
ensures { let cor = reg[28] + (pow2 8+pow2 16+pow2 24+pow2 32)*reg[0] in cor = if ?cf <= old ?cf then old ?cf - ?cf else pow2 40 + old ?cf - ?cf }
*)
'B:
(* process sign bit *)
clr r28;
clr r29;
bld r29 0;
dec r29;
assert { reg[29] = 0xFF*(1 - ?tf) };
(* merge carry and borrow *)
adc r28 r29;
mov r0 r28;
asr r0;
(* invert all bits or do nothing *)
eor r12 r29;
eor r13 r29;
eor r14 r29;
eor r15 r29;
eor r16 r29;
eor r27 r29;
eor r2 r29;
eor r3 r29;
eor r4 r29;
eor r5 r29;
assert { reg[29] = 0x00 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = at(uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2)'B };
assert { reg[29] = 0xFF -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = pow2 80 - 1 - at(uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2)'B };
add r29 r29; (* sets carry flag if r29 = 0xff *)
assert { ?cf = 1 - ?tf };
check { ?cf = 1 <-> at((uint 5 reg 2 < uint 5 reg 12) <-> (uint 5 reg 7 < uint 5 reg 23))'L11 };
check { ?cf = 0 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = at(uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2)'B };
check { ?cf = 1 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = pow2 80 - 1 - at(uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2)'B };
(*
check { ?cf = 0 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = at(uint 5 reg 2*uint 5 reg 7)'Tmp };
check { ?cf = 1 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = pow2 80 - 1 - at(uint 5 reg 2*uint 5 reg 7)'Tmp };
*)
assert { ?cf = 0 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = at(abs (uint 5 reg 2 - uint 5 reg 12)*abs(uint 5 reg 7 - uint 5 reg 23))'L11 };
assert { ?cf = 1 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = pow2 80 - 1 - at(abs (uint 5 reg 2 - uint 5 reg 12)*abs(uint 5 reg 7 - uint 5 reg 23))'L11 };
check { ?cf = 0 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = - at((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23))'L11 };
check { ?cf = 1 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = pow2 80 - 1 - at((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23))'L11 };
check { ?cf = 0 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = ?cf*(pow2 80 - 1) - at((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23))'L11 };
check { ?cf = 1 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = ?cf*(pow2 80 - 1) - at((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23))'L11 };
S.modify_r0();
S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16();
S.modify_r27();
S.modify_r2(); S.modify_r3(); S.modify_r4(); S.modify_r5();
S.modify_r28(); S.modify_r29();
end;
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 5 reg 7 + pow2 40*uint 10 reg 17 + ?cf*pow2 120 = old(uint 5 reg 7 + pow2 40*uint 10 reg 17 + uint 5 reg 12 + ?cf + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 + pow2 80*reg[28] + (pow2 88 + pow2 96 + pow2 104 + pow2 112)*reg[0] ) }
(* add in m *)
adc r7 r12;
adc r8 r13;
adc r9 r14;
adc r10 r15;
adc r11 r16;
adc r17 r27;
adc r18 r2;
adc r19 r3;
adc r20 r4;
adc r21 r5;
(* propagate carry/borrow *)
adc r22 r28;
adc r23 r0;
adc r24 r0;
adc r25 r0;
adc r26 r0;
S.modify_r7(); S.modify_r8(); S.modify_r9(); S.modify_r10(); S.modify_r11();
S.modify_r17(); S.modify_r18(); S.modify_r19(); S.modify_r20(); S.modify_r21();
S.modify_r22(); S.modify_r23(); S.modify_r24(); S.modify_r25(); S.modify_r26();
end;
(*
check { at(uint 5 reg 12)'L00' + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 + ?cf*pow2 160
= at( (uint 5 reg 2 + pow2 40*uint 5 reg 12)*(uint 5 reg 7 + pow2 40*uint 5 reg 23) )'L11
\/
at(uint 5 reg 12)'L00' + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 + ?cf*pow2 160
= at( (uint 5 reg 2 + pow2 40*uint 5 reg 12)*(uint 5 reg 7 + pow2 40*uint 5 reg 23) )'L11 + pow2 160
};
*)
assert { 0 <= at(uint 5 reg 2 + pow2 40*uint 5 reg 12)'L11 <= pow2 80-1 };
assert { 0 <= at(uint 5 reg 7 + pow2 40*uint 5 reg 23)'L11 <= pow2 80-1 };
assert { 0 <= at(uint 5 reg 2 + pow2 40*uint 5 reg 12)'L11 * at(uint 5 reg 7 + pow2 40*uint 5 reg 23)'L11 <= (pow2 80-1)*(pow2 80-1) };
assert { "expl:hack" 0 <= uint 10 reg 17 by 0 <= uint 5 reg 17 /\ 0 <= uint 5 reg 22 };
(*
check { 0 <= at (uint 5 reg 12)'L00' + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 < pow2 160 };
check { 0 <= (pow2 40+1)*(at(uint 5 reg 2*uint 5 reg 7 + pow2 40*uint 5 reg 12*uint 5 reg 23)'L11)
+ pow2 40 * (- at((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23)) 'L11) < pow2 160 };
check {
at (uint 5 reg 12)'L00' + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 + ?cf*pow2 160
= (pow2 40+1)*(at(uint 5 reg 2*uint 5 reg 7 + pow2 40*uint 5 reg 12*uint 5 reg 23)'L11)
- pow2 40 * at((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23)) 'L11
+ ?cf*pow2 160
};