Fortress

Необходимо добавить в библиотеку следующие параметризованные операции:

1. ((_ zero_extend i) (_ BitVec m) (_ BitVec m+i))
- ((_ zero_extend i) x) means extend x with zeroes to the (unsigned)
equivalent bitvector of size m+i

2. ((_ sign_extend i) (_ BitVec m) (_ BitVec m+i))
- ((_ sign_extend i) x) means extend x to the (signed) equivalent bitvector
of size m+i

3. ((_ rotate_left i) (_ BitVec m) (_ BitVec m))
- ((_ rotate_left i) x) means rotate bits of x to the left i times

4. ((_ rotate_right i) (_ BitVec m) (_ BitVec m))
- ((_ rotate_right i) x) means rotate bits of x to the right i times

Операции 3 и 4 уже были добавлены в библиотеку, необходимо разработать тесты, проверяющие корректность этого добавления.