diff --git a/Proofs/AES-GCM/Extracted.lean b/Proofs/AES-GCM/Extracted.lean new file mode 100644 index 00000000..3f4a87b5 --- /dev/null +++ b/Proofs/AES-GCM/Extracted.lean @@ -0,0 +1,3154 @@ +import Arm.BitVec + +set_option maxRecDepth 10000 in +set_option maxHeartbeats 1000000 in +set_option sat.timeout 120 in +theorem GCMInitV8Program.extracted_1 (Hinit : BitVec 128) : + BitVec.extractLsb' 64 128 + (((BitVec.extractLsb' 64 64 (BitVec.extractLsb' 64 128 (Hinit ++ Hinit)) <<< 1 ++ + BitVec.extractLsb' 0 64 (BitVec.extractLsb' 64 128 (Hinit ++ Hinit)) <<< 1 ||| + BitVec.extractLsb' 64 128 + ((BitVec.extractLsb' 64 64 (BitVec.extractLsb' 64 128 (Hinit ++ Hinit)) >>> 63 ++ + BitVec.extractLsb' 0 64 (BitVec.extractLsb' 64 128 (Hinit ++ Hinit)) >>> 63 &&& + 257870231182273679343338569694386847745#128) ++ + (BitVec.extractLsb' 64 64 (BitVec.extractLsb' 64 128 (Hinit ++ Hinit)) >>> 63 ++ + BitVec.extractLsb' 0 64 (BitVec.extractLsb' 64 128 (Hinit ++ Hinit)) >>> 63 &&& + 257870231182273679343338569694386847745#128))) ^^^ + 257870231182273679343338569694386847745#128 &&& + (BitVec.extractLsb' 96 32 + (BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit))).sshiftRight + 31 ++ + (BitVec.extractLsb' 64 32 + (BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit))).sshiftRight + 31 ++ + (BitVec.extractLsb' 32 32 + (BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit))).sshiftRight + 31 ++ + (BitVec.extractLsb' 0 32 + (BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit))).sshiftRight + 31) ++ + ((BitVec.extractLsb' 64 64 (BitVec.extractLsb' 64 128 (Hinit ++ Hinit)) <<< 1 ++ + BitVec.extractLsb' 0 64 (BitVec.extractLsb' 64 128 (Hinit ++ Hinit)) <<< 1 ||| + BitVec.extractLsb' 64 128 + ((BitVec.extractLsb' 64 64 (BitVec.extractLsb' 64 128 (Hinit ++ Hinit)) >>> 63 ++ + BitVec.extractLsb' 0 64 (BitVec.extractLsb' 64 128 (Hinit ++ Hinit)) >>> 63 &&& + 257870231182273679343338569694386847745#128) ++ + (BitVec.extractLsb' 64 64 (BitVec.extractLsb' 64 128 (Hinit ++ Hinit)) >>> 63 ++ + BitVec.extractLsb' 0 64 (BitVec.extractLsb' 64 128 (Hinit ++ Hinit)) >>> 63 &&& + 257870231182273679343338569694386847745#128))) ^^^ + 257870231182273679343338569694386847745#128 &&& + (BitVec.extractLsb' 96 32 + (BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit))).sshiftRight + 31 ++ + (BitVec.extractLsb' 64 32 + (BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit))).sshiftRight + 31 ++ + (BitVec.extractLsb' 32 32 + (BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit))).sshiftRight + 31 ++ + (BitVec.extractLsb' 0 32 + (BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit) ++ + BitVec.extractLsb' 32 32 (BitVec.zeroExtend 64 Hinit))).sshiftRight + 31)) = + BitVec.extractLsb' 0 64 + (0#128 ^^^ + BitVec.extractLsb' + 0 + 128 + (BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1 &&& + 1#129) ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 1 &&& + 1#129) * + 2#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 2 &&& + 1#129) * + 4#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 3 &&& + 1#129) * + 8#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 4 &&& + 1#129) * + 16#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 5 &&& + 1#129) * + 32#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 6 &&& + 1#129) * + 64#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 7 &&& + 1#129) * + 128#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 8 &&& + 1#129) * + 256#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 9 &&& + 1#129) * + 512#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 10 &&& + 1#129) * + 1024#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 11 &&& + 1#129) * + 2048#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 12 &&& + 1#129) * + 4096#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 13 &&& + 1#129) * + 8192#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 14 &&& + 1#129) * + 16384#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 15 &&& + 1#129) * + 32768#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 16 &&& + 1#129) * + 65536#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 17 &&& + 1#129) * + 131072#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 18 &&& + 1#129) * + 262144#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 19 &&& + 1#129) * + 524288#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 20 &&& + 1#129) * + 1048576#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 21 &&& + 1#129) * + 2097152#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 22 &&& + 1#129) * + 4194304#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 23 &&& + 1#129) * + 8388608#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 24 &&& + 1#129) * + 16777216#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 25 &&& + 1#129) * + 33554432#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 26 &&& + 1#129) * + 67108864#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 27 &&& + 1#129) * + 134217728#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 28 &&& + 1#129) * + 268435456#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 29 &&& + 1#129) * + 536870912#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 30 &&& + 1#129) * + 1073741824#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 31 &&& + 1#129) * + 2147483648#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 32 &&& + 1#129) * + 4294967296#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 33 &&& + 1#129) * + 8589934592#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 34 &&& + 1#129) * + 17179869184#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 35 &&& + 1#129) * + 34359738368#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 36 &&& + 1#129) * + 68719476736#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 37 &&& + 1#129) * + 137438953472#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 38 &&& + 1#129) * + 274877906944#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 39 &&& + 1#129) * + 549755813888#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 40 &&& + 1#129) * + 1099511627776#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 41 &&& + 1#129) * + 2199023255552#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 42 &&& + 1#129) * + 4398046511104#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 43 &&& + 1#129) * + 8796093022208#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 44 &&& + 1#129) * + 17592186044416#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 45 &&& + 1#129) * + 35184372088832#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 46 &&& + 1#129) * + 70368744177664#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 47 &&& + 1#129) * + 140737488355328#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 48 &&& + 1#129) * + 281474976710656#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 49 &&& + 1#129) * + 562949953421312#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 50 &&& + 1#129) * + 1125899906842624#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 51 &&& + 1#129) * + 2251799813685248#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 52 &&& + 1#129) * + 4503599627370496#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 53 &&& + 1#129) * + 9007199254740992#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 54 &&& + 1#129) * + 18014398509481984#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 55 &&& + 1#129) * + 36028797018963968#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 56 &&& + 1#129) * + 72057594037927936#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 57 &&& + 1#129) * + 144115188075855872#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 58 &&& + 1#129) * + 288230376151711744#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 59 &&& + 1#129) * + 576460752303423488#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 60 &&& + 1#129) * + 1152921504606846976#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 61 &&& + 1#129) * + 2305843009213693952#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 62 &&& + 1#129) * + 4611686018427387904#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 63 &&& + 1#129) * + 9223372036854775808#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 64 &&& + 1#129) * + 18446744073709551616#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 65 &&& + 1#129) * + 36893488147419103232#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 66 &&& + 1#129) * + 73786976294838206464#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 67 &&& + 1#129) * + 147573952589676412928#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 68 &&& + 1#129) * + 295147905179352825856#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 69 &&& + 1#129) * + 590295810358705651712#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 70 &&& + 1#129) * + 1180591620717411303424#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 71 &&& + 1#129) * + 2361183241434822606848#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 72 &&& + 1#129) * + 4722366482869645213696#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 73 &&& + 1#129) * + 9444732965739290427392#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 74 &&& + 1#129) * + 18889465931478580854784#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 75 &&& + 1#129) * + 37778931862957161709568#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 76 &&& + 1#129) * + 75557863725914323419136#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 77 &&& + 1#129) * + 151115727451828646838272#128 ^^^ + BitVec.extractLsb' + 0 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 78 &&& + 1#129) * + 302231454903657293676544#128 ^^^ + BitVec.extractLsb' + 0 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 79 &&& + 1#129) * + 604462909807314587353088#128 ^^^ + BitVec.extractLsb' + 0 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 80 &&& + 1#129) * + 1208925819614629174706176#128 ^^^ + BitVec.extractLsb' + 0 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 81 &&& + 1#129) * + 2417851639229258349412352#128 ^^^ + BitVec.extractLsb' + 0 128 + ((BitVec.extractLsb' + 0 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 82 &&& + 1#129) * + 4835703278458516698824704#128 ^^^ + BitVec.extractLsb' 0 + 128 + ((BitVec.extractLsb' + 0 64 + Hinit ++ + BitVec.extractLsb' + 64 64 + Hinit ++ + 0#1) >>> + 83 &&& + 1#129) * + 9671406556917033397649408#128 ^^^ + BitVec.extractLsb' 0 + 128 + ((BitVec.extractLsb' + 0 64 + Hinit ++ + BitVec.extractLsb' + 64 64 + Hinit ++ + 0#1) >>> + 84 &&& + 1#129) * + 19342813113834066795298816#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' + 0 64 + Hinit ++ + BitVec.extractLsb' + 64 64 + Hinit ++ + 0#1) >>> + 85 &&& + 1#129) * + 38685626227668133590597632#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 + 64 Hinit ++ + BitVec.extractLsb' + 64 64 + Hinit ++ + 0#1) >>> + 86 &&& + 1#129) * + 77371252455336267181195264#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 + 64 Hinit ++ + BitVec.extractLsb' + 64 64 Hinit ++ + 0#1) >>> + 87 &&& + 1#129) * + 154742504910672534362390528#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 + Hinit ++ + BitVec.extractLsb' + 64 64 Hinit ++ + 0#1) >>> + 88 &&& + 1#129) * + 309485009821345068724781056#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 + Hinit ++ + BitVec.extractLsb' + 64 64 Hinit ++ + 0#1) >>> + 89 &&& + 1#129) * + 618970019642690137449562112#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 + Hinit ++ + BitVec.extractLsb' 64 + 64 Hinit ++ + 0#1) >>> + 90 &&& + 1#129) * + 1237940039285380274899124224#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 + Hinit ++ + BitVec.extractLsb' 64 64 + Hinit ++ + 0#1) >>> + 91 &&& + 1#129) * + 2475880078570760549798248448#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 + Hinit ++ + 0#1) >>> + 92 &&& + 1#129) * + 4951760157141521099596496896#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 + Hinit ++ + 0#1) >>> + 93 &&& + 1#129) * + 9903520314283042199192993792#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 + Hinit ++ + 0#1) >>> + 94 &&& + 1#129) * + 19807040628566084398385987584#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 + Hinit ++ + 0#1) >>> + 95 &&& + 1#129) * + 39614081257132168796771975168#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 96 &&& + 1#129) * + 79228162514264337593543950336#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 97 &&& + 1#129) * + 158456325028528675187087900672#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 98 &&& + 1#129) * + 316912650057057350374175801344#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 99 &&& + 1#129) * + 633825300114114700748351602688#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 100 &&& + 1#129) * + 1267650600228229401496703205376#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 101 &&& + 1#129) * + 2535301200456458802993406410752#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 102 &&& + 1#129) * + 5070602400912917605986812821504#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 103 &&& + 1#129) * + 10141204801825835211973625643008#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 104 &&& + 1#129) * + 20282409603651670423947251286016#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 105 &&& + 1#129) * + 40564819207303340847894502572032#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 106 &&& + 1#129) * + 81129638414606681695789005144064#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 107 &&& + 1#129) * + 162259276829213363391578010288128#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 108 &&& + 1#129) * + 324518553658426726783156020576256#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 109 &&& + 1#129) * + 649037107316853453566312041152512#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 110 &&& + 1#129) * + 1298074214633706907132624082305024#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 111 &&& + 1#129) * + 2596148429267413814265248164610048#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 112 &&& + 1#129) * + 5192296858534827628530496329220096#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 113 &&& + 1#129) * + 10384593717069655257060992658440192#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> + 114 &&& + 1#129) * + 20769187434139310514121985316880384#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> + 115 &&& + 1#129) * + 41538374868278621028243970633760768#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> + 116 &&& + 1#129) * + 83076749736557242056487941267521536#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> + 117 &&& + 1#129) * + 166153499473114484112975882535043072#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 118 &&& + 1#129) * + 332306998946228968225951765070086144#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 119 &&& + 1#129) * + 664613997892457936451903530140172288#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 120 &&& + 1#129) * + 1329227995784915872903807060280344576#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 121 &&& + 1#129) * + 2658455991569831745807614120560689152#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 122 &&& 1#129) * + 5316911983139663491615228241121378304#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 123 &&& 1#129) * + 10633823966279326983230456482242756608#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 124 &&& 1#129) * + 21267647932558653966460912964485513216#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 125 &&& 1#129) * + 42535295865117307932921825928971026432#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 126 &&& 1#129) * + 85070591730234615865843651857942052864#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 127 &&& 1#129) * + 170141183460469231731687303715884105728#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 128 &&& 1#129) * + 257870231182273679343338569694386847745#128) ++ + BitVec.extractLsb' 64 64 + (0#128 ^^^ + BitVec.extractLsb' + 0 + 128 + (BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1 &&& + 1#129) ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 1 &&& + 1#129) * + 2#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 2 &&& + 1#129) * + 4#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 3 &&& + 1#129) * + 8#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 4 &&& + 1#129) * + 16#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 5 &&& + 1#129) * + 32#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 6 &&& + 1#129) * + 64#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 7 &&& + 1#129) * + 128#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 8 &&& + 1#129) * + 256#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 9 &&& + 1#129) * + 512#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 10 &&& + 1#129) * + 1024#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 11 &&& + 1#129) * + 2048#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 12 &&& + 1#129) * + 4096#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 13 &&& + 1#129) * + 8192#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 14 &&& + 1#129) * + 16384#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 15 &&& + 1#129) * + 32768#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 16 &&& + 1#129) * + 65536#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 17 &&& + 1#129) * + 131072#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 18 &&& + 1#129) * + 262144#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 19 &&& + 1#129) * + 524288#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 20 &&& + 1#129) * + 1048576#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 21 &&& + 1#129) * + 2097152#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 22 &&& + 1#129) * + 4194304#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 23 &&& + 1#129) * + 8388608#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 24 &&& + 1#129) * + 16777216#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 25 &&& + 1#129) * + 33554432#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 26 &&& + 1#129) * + 67108864#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 27 &&& + 1#129) * + 134217728#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 28 &&& + 1#129) * + 268435456#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 29 &&& + 1#129) * + 536870912#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 30 &&& + 1#129) * + 1073741824#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 31 &&& + 1#129) * + 2147483648#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 32 &&& + 1#129) * + 4294967296#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 33 &&& + 1#129) * + 8589934592#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 34 &&& + 1#129) * + 17179869184#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 35 &&& + 1#129) * + 34359738368#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 36 &&& + 1#129) * + 68719476736#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 37 &&& + 1#129) * + 137438953472#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 38 &&& + 1#129) * + 274877906944#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 39 &&& + 1#129) * + 549755813888#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 40 &&& + 1#129) * + 1099511627776#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 41 &&& + 1#129) * + 2199023255552#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 42 &&& + 1#129) * + 4398046511104#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 43 &&& + 1#129) * + 8796093022208#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 44 &&& + 1#129) * + 17592186044416#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 45 &&& + 1#129) * + 35184372088832#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 46 &&& + 1#129) * + 70368744177664#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 47 &&& + 1#129) * + 140737488355328#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 48 &&& + 1#129) * + 281474976710656#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 49 &&& + 1#129) * + 562949953421312#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 50 &&& + 1#129) * + 1125899906842624#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 51 &&& + 1#129) * + 2251799813685248#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 52 &&& + 1#129) * + 4503599627370496#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 53 &&& + 1#129) * + 9007199254740992#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 54 &&& + 1#129) * + 18014398509481984#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 55 &&& + 1#129) * + 36028797018963968#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 56 &&& + 1#129) * + 72057594037927936#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 57 &&& + 1#129) * + 144115188075855872#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 58 &&& + 1#129) * + 288230376151711744#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 59 &&& + 1#129) * + 576460752303423488#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 60 &&& + 1#129) * + 1152921504606846976#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 61 &&& + 1#129) * + 2305843009213693952#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 62 &&& + 1#129) * + 4611686018427387904#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 63 &&& + 1#129) * + 9223372036854775808#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 64 &&& + 1#129) * + 18446744073709551616#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 65 &&& + 1#129) * + 36893488147419103232#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 66 &&& + 1#129) * + 73786976294838206464#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 67 &&& + 1#129) * + 147573952589676412928#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 68 &&& + 1#129) * + 295147905179352825856#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 69 &&& + 1#129) * + 590295810358705651712#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 70 &&& + 1#129) * + 1180591620717411303424#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 71 &&& + 1#129) * + 2361183241434822606848#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 72 &&& + 1#129) * + 4722366482869645213696#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 73 &&& + 1#129) * + 9444732965739290427392#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 74 &&& + 1#129) * + 18889465931478580854784#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 75 &&& + 1#129) * + 37778931862957161709568#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 76 &&& + 1#129) * + 75557863725914323419136#128 ^^^ + BitVec.extractLsb' + 0 + 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 77 &&& + 1#129) * + 151115727451828646838272#128 ^^^ + BitVec.extractLsb' + 0 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 78 &&& + 1#129) * + 302231454903657293676544#128 ^^^ + BitVec.extractLsb' + 0 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 79 &&& + 1#129) * + 604462909807314587353088#128 ^^^ + BitVec.extractLsb' + 0 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 80 &&& + 1#129) * + 1208925819614629174706176#128 ^^^ + BitVec.extractLsb' + 0 128 + ((BitVec.extractLsb' + 0 + 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 81 &&& + 1#129) * + 2417851639229258349412352#128 ^^^ + BitVec.extractLsb' + 0 128 + ((BitVec.extractLsb' + 0 64 + Hinit ++ + BitVec.extractLsb' + 64 + 64 + Hinit ++ + 0#1) >>> + 82 &&& + 1#129) * + 4835703278458516698824704#128 ^^^ + BitVec.extractLsb' 0 + 128 + ((BitVec.extractLsb' + 0 64 + Hinit ++ + BitVec.extractLsb' + 64 64 + Hinit ++ + 0#1) >>> + 83 &&& + 1#129) * + 9671406556917033397649408#128 ^^^ + BitVec.extractLsb' 0 + 128 + ((BitVec.extractLsb' + 0 64 + Hinit ++ + BitVec.extractLsb' + 64 64 + Hinit ++ + 0#1) >>> + 84 &&& + 1#129) * + 19342813113834066795298816#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' + 0 64 + Hinit ++ + BitVec.extractLsb' + 64 64 + Hinit ++ + 0#1) >>> + 85 &&& + 1#129) * + 38685626227668133590597632#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 + 64 Hinit ++ + BitVec.extractLsb' + 64 64 + Hinit ++ + 0#1) >>> + 86 &&& + 1#129) * + 77371252455336267181195264#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 + 64 Hinit ++ + BitVec.extractLsb' + 64 64 Hinit ++ + 0#1) >>> + 87 &&& + 1#129) * + 154742504910672534362390528#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 + Hinit ++ + BitVec.extractLsb' + 64 64 Hinit ++ + 0#1) >>> + 88 &&& + 1#129) * + 309485009821345068724781056#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 + Hinit ++ + BitVec.extractLsb' + 64 64 Hinit ++ + 0#1) >>> + 89 &&& + 1#129) * + 618970019642690137449562112#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 + Hinit ++ + BitVec.extractLsb' 64 + 64 Hinit ++ + 0#1) >>> + 90 &&& + 1#129) * + 1237940039285380274899124224#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 + Hinit ++ + BitVec.extractLsb' 64 64 + Hinit ++ + 0#1) >>> + 91 &&& + 1#129) * + 2475880078570760549798248448#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 + Hinit ++ + 0#1) >>> + 92 &&& + 1#129) * + 4951760157141521099596496896#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 + Hinit ++ + 0#1) >>> + 93 &&& + 1#129) * + 9903520314283042199192993792#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 + Hinit ++ + 0#1) >>> + 94 &&& + 1#129) * + 19807040628566084398385987584#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 + Hinit ++ + 0#1) >>> + 95 &&& + 1#129) * + 39614081257132168796771975168#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 96 &&& + 1#129) * + 79228162514264337593543950336#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 97 &&& + 1#129) * + 158456325028528675187087900672#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 98 &&& + 1#129) * + 316912650057057350374175801344#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 99 &&& + 1#129) * + 633825300114114700748351602688#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 100 &&& + 1#129) * + 1267650600228229401496703205376#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 101 &&& + 1#129) * + 2535301200456458802993406410752#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 102 &&& + 1#129) * + 5070602400912917605986812821504#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 103 &&& + 1#129) * + 10141204801825835211973625643008#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 104 &&& + 1#129) * + 20282409603651670423947251286016#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 105 &&& + 1#129) * + 40564819207303340847894502572032#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 106 &&& + 1#129) * + 81129638414606681695789005144064#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 107 &&& + 1#129) * + 162259276829213363391578010288128#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ + BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 108 &&& + 1#129) * + 324518553658426726783156020576256#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 109 &&& + 1#129) * + 649037107316853453566312041152512#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 110 &&& + 1#129) * + 1298074214633706907132624082305024#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 111 &&& + 1#129) * + 2596148429267413814265248164610048#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 112 &&& + 1#129) * + 5192296858534827628530496329220096#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ + 0#1) >>> + 113 &&& + 1#129) * + 10384593717069655257060992658440192#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> + 114 &&& + 1#129) * + 20769187434139310514121985316880384#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> + 115 &&& + 1#129) * + 41538374868278621028243970633760768#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> + 116 &&& + 1#129) * + 83076749736557242056487941267521536#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> + 117 &&& + 1#129) * + 166153499473114484112975882535043072#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 118 &&& + 1#129) * + 332306998946228968225951765070086144#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 119 &&& + 1#129) * + 664613997892457936451903530140172288#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 120 &&& + 1#129) * + 1329227995784915872903807060280344576#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 121 &&& + 1#129) * + 2658455991569831745807614120560689152#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 122 &&& 1#129) * + 5316911983139663491615228241121378304#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 123 &&& 1#129) * + 10633823966279326983230456482242756608#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 124 &&& 1#129) * + 21267647932558653966460912964485513216#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 125 &&& 1#129) * + 42535295865117307932921825928971026432#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 126 &&& 1#129) * + 85070591730234615865843651857942052864#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 127 &&& 1#129) * + 170141183460469231731687303715884105728#128 ^^^ + BitVec.extractLsb' 0 128 + ((BitVec.extractLsb' 0 64 Hinit ++ BitVec.extractLsb' 64 64 Hinit ++ 0#1) >>> 128 &&& 1#129) * + 257870231182273679343338569694386847745#128) := by + bv_decide diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 90fc0d26..86775bdd 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -7,6 +7,7 @@ import Arm.BitVec import Proofs.«AES-GCM».GCMInitV8Pre import Tactics.Sym import Tactics.Aggregate +import Tactics.ExtractGoal import Specs.GCMV8 namespace GCMInitV8Program @@ -33,9 +34,11 @@ theorem gcm_init_v8_program_run_152 (s0 sf : ArmState) sym_n 152 done -set_option maxRecDepth 1000000 in -set_option maxHeartbeats 2000000 in -set_option sat.timeout 180 in +set_option maxRecDepth 100000 in +set_option maxHeartbeats 500000 in +set_option sat.timeout 120 in +set_option pp.deepTerms true in +set_option pp.maxSteps 10000 in -- set_option linter.unusedVariables false in -- set_option profiler true in theorem gcm_init_v8_program_correct (s0 sf : ArmState) @@ -44,7 +47,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) (h_s0_pc : read_pc s0 = gcm_init_v8_program.min) (h_s0_sp_aligned : CheckSPAlignment s0) (h_run : sf = run gcm_init_v8_program.length s0) - (_h_mem : Memory.Region.pairwiseSeparate + (h_mem : Memory.Region.pairwiseSeparate [ ⟨(H_addr s0), 128⟩, ⟨(Htable_addr s0), 2048⟩ ]) : -- effects @@ -110,4 +113,6 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) Nat.zero_mod, Nat.zero_add, Nat.sub_zero, Nat.mul_one, Nat.zero_mul, Nat.one_mul, Nat.reduceSub, BitVec.reduceMul, BitVec.reduceXOr, BitVec.mul_one, Nat.add_one_sub_one, BitVec.one_mul] - bv_decide + extract_goal + sorry + -- bv_decide diff --git a/Tactics.lean b/Tactics.lean index b0107828..3a4c130e 100644 --- a/Tactics.lean +++ b/Tactics.lean @@ -10,3 +10,4 @@ import «Tactics».StepThms import «Tactics».Rename import «Tactics».Name import «Tactics».ClearNamed +import «Tactics».ExtractGoal diff --git a/Tactics/ExtractGoal.lean b/Tactics/ExtractGoal.lean new file mode 100644 index 00000000..80237825 --- /dev/null +++ b/Tactics/ExtractGoal.lean @@ -0,0 +1,171 @@ +/- +Copyright (c) 2017 Simon Hudon. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Simon Hudon, Kyle Miller, Damiano Testa +-/ +import Lean.Elab.Tactic.ElabTerm +import Lean.Meta.Tactic.Cleanup +import Lean.PrettyPrinter +import Batteries.Lean.Meta.Inaccessible + +/-! +# `extract_goal`: Format the current goal as a stand-alone example + +Useful for testing tactics or creating +[minimal working examples](https://leanprover-community.github.io/mwe.html). + +```lean +example (i j k : Nat) (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k := by + extract_goal + +/- +theorem extracted_1 (i j k : Nat) (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k := sorry +-/ +``` + +* TODO: Add tactic code actions? +* Output may produce lines with more than 100 characters + +### Caveat + +Tl;dr: sometimes, using `set_option [your pp option] in extract_goal` may work where `extract_goal` +does not. + +The extracted goal may depend on imports and `pp` options, since it relies on delaboration. +For this reason, the extracted goal may not be equivalent to the given goal. +However, the tactic responds to pretty printing options. +For example, calling `set_option pp.all true in extract_goal` in the examples below actually works. + +```lean +-- `theorem int_eq_nat` is the output of the `extract_goal` from the example below +-- the type ascription is removed and the `↑` is replaced by `Int.ofNat`: +-- Lean infers the correct (false) statement +theorem int_eq_nat {z : Int} : ∃ n, Int.ofNat n = z := sorry + +example {z : Int} : ∃ n : Nat, ↑n = z := by + extract_goal -- produces `int_eq_nat` + apply int_eq_nat -- works +``` + +However, importing `Batteries.Classes.Cast`, makes `extract_goal` produce a different theorem + +```lean +import Batteries.Classes.Cast + +-- `theorem extracted_1` is the output of the `extract_goal` from the example below +-- the type ascription is erased and the `↑` is untouched: +-- Lean infers a different statement, since it fills in `↑` with `id` and uses `n : Int` +theorem extracted_1 {z : Int} : ∃ n, ↑n = z := ⟨_, rfl⟩ + +example {z : Int} : ∃ n : Nat, ↑n = z := by + extract_goal + apply extracted_1 +/- +tactic 'apply' failed, failed to unify + ∃ n, n = ?z +with + ∃ n, ↑n = z +z: Int +⊢ ∃ n, ↑n = z +-/ +``` + +Similarly, the extracted goal may fail to type-check: +```lean +example (a : α) : ∃ f : α → α, f a = a := by + extract_goal + exact ⟨id, rfl⟩ + +theorem extracted_1.{u_1} {α : Sort u_1} (a : α) : ∃ f, f a = a := sorry +-- `f` is uninterpreted: `⊢ ∃ f, sorryAx α true = a` +``` +and also +```lean +import Mathlib.Algebra.Polynomial.Basic + +-- The `extract_goal` below produces this statement: +theorem extracted_1 : X = X := sorry +-- Yet, Lean is unable to figure out what is the coefficients Semiring for `X` +/- +typeclass instance problem is stuck, it is often due to metavariables + Semiring ?m.28495 +-/ + +example : (X : Nat[X]) = X := by + extract_goal +``` +-/ + +namespace Mathlib.Tactic.ExtractGoal + +open Lean Elab Tactic Meta + +/-- Have `extract_goal` extract the full local context. -/ +syntax star := "*" + +/-- Configuration for `extract_goal` for which variables from the context to include. -/ +syntax config := star <|> (colGt ppSpace ident)* + +/-- +- `extract_goal` formats the current goal as a stand-alone theorem or definition after + cleaning up the local context of irrelevant variables. + A variable is *relevant* if (1) it occurs in the target type, (2) there is a relevant variable + that depends on it, or (3) the type of the variable is a proposition that depends on a + relevant variable. + + If the target is `False`, then for convenience `extract_goal` includes all variables. +- `extract_goal *` formats the current goal without cleaning up the local context. +- `extract_goal a b c ...` formats the current goal after removing everything that the given + variables `a`, `b`, `c`, ... do not depend on. +- `extract_goal ... using name` uses the name `name` for the theorem or definition rather than + the autogenerated name. + +The tactic tries to produce an output that can be copy-pasted and just work, +but its success depends on whether the expressions are amenable +to being unambiguously pretty printed. + +The tactic responds to pretty printing options. +For example, `set_option pp.all true in extract_goal` gives the `pp.all` form. +-/ +syntax (name := extractGoal) "extract_goal" config (" using " ident)? : tactic + +elab_rules : tactic + | `(tactic| extract_goal $cfg:config $[using $name?]?) => do + let name ← if let some name := name? + then pure name.getId + else mkAuxName ((← getCurrNamespace) ++ `extracted) 1 + let msg ← withoutModifyingEnv <| withoutModifyingState do + let g ← getMainGoal + let g ← do match cfg with + | `(config| *) => pure g + | `(config| ) => + if (← g.getType >>= instantiateMVars).consumeMData.isConstOf ``False then + -- In a contradiction proof, it is not very helpful to clear all hypotheses! + pure g + else + g.cleanup + | `(config| $fvars:ident*) => + -- Note: `getFVarIds` does `withMainContext` + g.cleanup (toPreserve := (← getFVarIds fvars)) (indirectProps := false) + | _ => throwUnsupportedSyntax + let (g, _) ← g.renameInaccessibleFVars + let (_, g) ← g.revert (clearAuxDeclsInsteadOfRevert := true) (← g.getDecl).lctx.getFVarIds + let ty ← instantiateMVars (← g.getType) + if ty.hasExprMVar then + -- TODO: turn metavariables into new hypotheses? + throwError "Extracted goal has metavariables: {ty}" + let ty ← Term.levelMVarToParam ty + let seenLevels := collectLevelParams {} ty + let levels := (← Term.getLevelNames).filter + fun u => seenLevels.visitedLevel.contains (.param u) + addAndCompile <| Declaration.axiomDecl + { name := name + levelParams := levels + isUnsafe := false + type := ty } + let sig ← addMessageContext <| MessageData.signature name + let cmd := if ← Meta.isProp ty then "theorem" else "def" + pure m!"{cmd} {sig} := sorry" + logInfo msg + +end Mathlib.Tactic.ExtractGoal diff --git a/lake-manifest.json b/lake-manifest.json index 35f79314..74f96cdf 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -60,6 +60,16 @@ "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "", + "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, "configFile": "lakefile.lean"}], "name": "lnsym", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 7175ad63..e3029638 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -45,3 +45,4 @@ lean_exe «lnsym» where require ELFSage from git "https://github.com/draperlaboratory/ELFSage.git" @ "main" require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" +require batteries from git "https://github.com/leanprover-community/batteries" @ "main"