98 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
99 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
100 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
101 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
102 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
103 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
104 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
105 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
106 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
107 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
108 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
109 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
110 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
111 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
112 };
113
114 // Maximum size of cache of powers of 5 as FDBigIntegers.
115 private static final int MAX_FIVE_POW = 340;
116
117 // Cache of big powers of 5 as FDBigIntegers.
118 private static final FDBigInteger POW_5_CACHE[];
119
120 // Initialize FDBigInteger cache of powers of 5.
121 static {
122 POW_5_CACHE = new FDBigInteger[MAX_FIVE_POW];
123 int i = 0;
124 while (i < SMALL_5_POW.length) {
125 FDBigInteger pow5 = new FDBigInteger(new int[]{SMALL_5_POW[i]}, 0);
126 pow5.makeImmutable();
127 POW_5_CACHE[i] = pow5;
128 i++;
129 }
130 FDBigInteger prev = POW_5_CACHE[i - 1];
131 while (i < MAX_FIVE_POW) {
132 POW_5_CACHE[i] = prev = prev.mult(5);
133 prev.makeImmutable();
134 i++;
135 }
136 }
137
138 // Zero as an FDBigInteger.
139 public static final FDBigInteger ZERO = new FDBigInteger(new int[0], 0);
140
141 // Ensure ZERO is immutable.
142 static {
143 ZERO.makeImmutable();
144 }
145
146 // Constant for casting an int to a long via bitwise AND.
147 private static final long LONG_MASK = 0xffffffffL;
148
149 //@ spec_public non_null;
150 private int data[]; // value: data[0] is least significant
151 //@ spec_public;
152 private int offset; // number of least significant zero padding ints
153 //@ spec_public;
154 private int nWords; // data[nWords-1]!=0, all values above are zero
155 // if nWords==0 -> this FDBigInteger is zero
156 //@ spec_public;
157 private boolean isImmutable = false;
158
159 /*@
160 @ public invariant 0 <= nWords && nWords <= data.length && offset >= 0;
161 @ public invariant nWords == 0 ==> offset == 0;
162 @ public invariant nWords > 0 ==> data[nWords - 1] != 0;
163 @ public invariant (\forall int i; nWords <= i && i < data.length; data[i] == 0);
164 @ public pure model \bigint value() {
165 @ return AP(data, nWords) << (offset*32);
166 @ }
167 @*/
168
169 /**
170 * Constructs an <code>FDBigInteger</code> from data and padding. The
400 return (zeros < 4) ? 28 + zeros : zeros - 4;
401 }
402
403 // TODO: Why is anticount param needed if it is always 32 - bitcount?
404 /**
405 * Left shifts the contents of one int array into another.
406 *
407 * @param src The source array.
408 * @param idx The initial index of the source array.
409 * @param result The destination array.
410 * @param bitcount The left shift.
411 * @param anticount The left anti-shift, e.g., <code>32-bitcount</code>.
412 * @param prev The prior source value.
413 */
414 /*@
415 @ requires 0 < bitcount && bitcount < 32 && anticount == 32 - bitcount;
416 @ requires src.length >= idx && result.length > idx;
417 @ assignable result[*];
418 @ ensures AP(result, \old(idx + 1)) == \old((AP(src, idx) + UNSIGNED(prev) << (idx*32)) << bitcount);
419 @*/
420 private static void leftShift(int[] src, int idx, int result[], int bitcount, int anticount, int prev){
421 for (; idx > 0; idx--) {
422 int v = (prev << bitcount);
423 prev = src[idx - 1];
424 v |= (prev >>> anticount);
425 result[idx] = v;
426 }
427 int v = prev << bitcount;
428 result[0] = v;
429 }
430
431 /**
432 * Shifts this <code>FDBigInteger</code> to the left. The shift is performed
433 * in-place unless the <code>FDBigInteger</code> is immutable in which case
434 * a new instance of <code>FDBigInteger</code> is returned.
435 *
436 * @param shift The number of bits to shift left.
437 * @return The shifted <code>FDBigInteger</code>.
438 */
439 /*@
440 @ requires this.value() == 0 || shift == 0;
|
98 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
99 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
100 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
101 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
102 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
103 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
104 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
105 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
106 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
107 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
108 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
109 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
110 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
111 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,
112 };
113
114 // Maximum size of cache of powers of 5 as FDBigIntegers.
115 private static final int MAX_FIVE_POW = 340;
116
117 // Cache of big powers of 5 as FDBigIntegers.
118 private static final FDBigInteger[] POW_5_CACHE;
119
120 // Initialize FDBigInteger cache of powers of 5.
121 static {
122 POW_5_CACHE = new FDBigInteger[MAX_FIVE_POW];
123 int i = 0;
124 while (i < SMALL_5_POW.length) {
125 FDBigInteger pow5 = new FDBigInteger(new int[]{SMALL_5_POW[i]}, 0);
126 pow5.makeImmutable();
127 POW_5_CACHE[i] = pow5;
128 i++;
129 }
130 FDBigInteger prev = POW_5_CACHE[i - 1];
131 while (i < MAX_FIVE_POW) {
132 POW_5_CACHE[i] = prev = prev.mult(5);
133 prev.makeImmutable();
134 i++;
135 }
136 }
137
138 // Zero as an FDBigInteger.
139 public static final FDBigInteger ZERO = new FDBigInteger(new int[0], 0);
140
141 // Ensure ZERO is immutable.
142 static {
143 ZERO.makeImmutable();
144 }
145
146 // Constant for casting an int to a long via bitwise AND.
147 private static final long LONG_MASK = 0xffffffffL;
148
149 //@ spec_public non_null;
150 private int[] data; // value: data[0] is least significant
151 //@ spec_public;
152 private int offset; // number of least significant zero padding ints
153 //@ spec_public;
154 private int nWords; // data[nWords-1]!=0, all values above are zero
155 // if nWords==0 -> this FDBigInteger is zero
156 //@ spec_public;
157 private boolean isImmutable = false;
158
159 /*@
160 @ public invariant 0 <= nWords && nWords <= data.length && offset >= 0;
161 @ public invariant nWords == 0 ==> offset == 0;
162 @ public invariant nWords > 0 ==> data[nWords - 1] != 0;
163 @ public invariant (\forall int i; nWords <= i && i < data.length; data[i] == 0);
164 @ public pure model \bigint value() {
165 @ return AP(data, nWords) << (offset*32);
166 @ }
167 @*/
168
169 /**
170 * Constructs an <code>FDBigInteger</code> from data and padding. The
400 return (zeros < 4) ? 28 + zeros : zeros - 4;
401 }
402
403 // TODO: Why is anticount param needed if it is always 32 - bitcount?
404 /**
405 * Left shifts the contents of one int array into another.
406 *
407 * @param src The source array.
408 * @param idx The initial index of the source array.
409 * @param result The destination array.
410 * @param bitcount The left shift.
411 * @param anticount The left anti-shift, e.g., <code>32-bitcount</code>.
412 * @param prev The prior source value.
413 */
414 /*@
415 @ requires 0 < bitcount && bitcount < 32 && anticount == 32 - bitcount;
416 @ requires src.length >= idx && result.length > idx;
417 @ assignable result[*];
418 @ ensures AP(result, \old(idx + 1)) == \old((AP(src, idx) + UNSIGNED(prev) << (idx*32)) << bitcount);
419 @*/
420 private static void leftShift(int[] src, int idx, int[] result, int bitcount, int anticount, int prev){
421 for (; idx > 0; idx--) {
422 int v = (prev << bitcount);
423 prev = src[idx - 1];
424 v |= (prev >>> anticount);
425 result[idx] = v;
426 }
427 int v = prev << bitcount;
428 result[0] = v;
429 }
430
431 /**
432 * Shifts this <code>FDBigInteger</code> to the left. The shift is performed
433 * in-place unless the <code>FDBigInteger</code> is immutable in which case
434 * a new instance of <code>FDBigInteger</code> is returned.
435 *
436 * @param shift The number of bits to shift left.
437 * @return The shifted <code>FDBigInteger</code>.
438 */
439 /*@
440 @ requires this.value() == 0 || shift == 0;
|