chore: use dylib facet for shared library

scripts/test.sh

@@ -8,7 +8,7 @@ lake build mceliece
 cmp --silent tests/mceliece/kat_kem.req.golden tmp/kat_kem.req || echo "Req files are different"
 cmp --silent tests/mceliece/kat_kem.rsp.golden tmp/kat_kem.rsp || echo "Rsp files are different"
 
-lake build Smt:shared
+lake build +Smt:dynlib
 lake run runTest tests/aes/GF256Pow.lean
 # TODO: times out
 # lake run runTest tests/aes/SBox.lean

tests/aes/GF256Pow.expected

@@ -3,9 +3,9 @@ goal: GF256.pow2 8 x = x
 query:
 (define-sort Nat () Int)
 (define-fun Nat.sub ((x Nat) (y Nat)) Nat (ite (< x y) 0 (- x y)))
-(assert (forall ((_uniq.7863 Nat)) (=> (>= _uniq.7863 0) (forall ((_uniq.7864 Nat)) (=> (>= _uniq.7864 0) (>= (Nat.sub _uniq.7863 _uniq.7864) 0))))))
+(assert (forall ((_uniq.7776 Nat)) (=> (>= _uniq.7776 0) (forall ((_uniq.7777 Nat)) (=> (>= _uniq.7777 0) (>= (Nat.sub _uniq.7776 _uniq.7777) 0))))))
 (define-fun |GF2BVPoly.polyMod.«16».«8»| ((x (_ BitVec 16)) (y (_ BitVec 9))) (_ BitVec 8) (let ((ret #b00000000)) (let ((pow (ite (= (not (= ((_ extract 8 8) #b000000001) #b0)) true) (bvxor #b000000001 y) #b000000001))) (let ((ret_1 (ite (= (not (= ((_ extract 0 0) x) #b0)) true) (bvxor ret (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow) #b00000000)) ret))) (let ((pow_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow #b000000001)) #b0)) true) (bvxor (bvshl pow #b000000001) y) (bvshl pow #b000000001)))) (let ((ret_2 (ite (= (not (= ((_ extract 1 1) x) #b0)) true) (bvxor ret_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_1) #b00000000)) ret_1))) (let ((pow_2 (ite (= (not (= ((_ extract 8 8) (bvshl pow_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_1 #b000000001) y) (bvshl pow_1 #b000000001)))) (let ((ret_3 (ite (= (not (= ((_ extract 2 2) x) #b0)) true) (bvxor ret_2 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_2) #b00000000)) ret_2))) (let ((pow_3 (ite (= (not (= ((_ extract 8 8) (bvshl pow_2 #b000000001)) #b0)) true) (bvxor (bvshl pow_2 #b000000001) y) (bvshl pow_2 #b000000001)))) (let ((ret_4 (ite (= (not (= ((_ extract 3 3) x) #b0)) true) (bvxor ret_3 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_3) #b00000000)) ret_3))) (let ((pow_4 (ite (= (not (= ((_ extract 8 8) (bvshl pow_3 #b000000001)) #b0)) true) (bvxor (bvshl pow_3 #b000000001) y) (bvshl pow_3 #b000000001)))) (let ((ret_5_1 (ite (= (not (= ((_ extract 4 4) x) #b0)) true) (bvxor ret_4 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_4) #b00000000)) ret_4))) (let ((pow_5_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_4 #b000000001)) #b0)) true) (bvxor (bvshl pow_4 #b000000001) y) (bvshl pow_4 #b000000001)))) (let ((ret_6 (ite (= (not (= ((_ extract 5 5) x) #b0)) true) (bvxor ret_5_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_5_1) #b00000000)) ret_5_1))) (let ((pow_6 (ite (= (not (= ((_ extract 8 8) (bvshl pow_5_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_5_1 #b000000001) y) (bvshl pow_5_1 #b000000001)))) (let ((ret_6_1 (ite (= (not (= ((_ extract 5 5) x) #b0)) true) (bvxor ret_5_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_5_1) #b00000000)) ret_5_1))) (let ((pow_6_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_5_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_5_1 #b000000001) y) (bvshl pow_5_1 #b000000001)))) (let ((ret_7 (ite (= (not (= ((_ extract 6 6) x) #b0)) true) (bvxor ret_6 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_6) #b00000000)) ret_6))) (let ((pow_7 (ite (= (not (= ((_ extract 8 8) (bvshl pow_6 #b000000001)) #b0)) true) (bvxor (bvshl pow_6 #b000000001) y) (bvshl pow_6 #b000000001)))) (let ((ret_7_1 (ite (= (not (= ((_ extract 6 6) x) #b0)) true) (bvxor ret_6_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_6_1) #b00000000)) ret_6_1))) (let ((pow_7_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_6_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_6_1 #b000000001) y) (bvshl pow_6_1 #b000000001)))) (let ((ret_8 (ite (= (not (= ((_ extract 7 7) x) #b0)) true) (bvxor ret_7 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_7) #b00000000)) ret_7))) (let ((pow_8 (ite (= (not (= ((_ extract 8 8) (bvshl pow_7 #b000000001)) #b0)) true) (bvxor (bvshl pow_7 #b000000001) y) (bvshl pow_7 #b000000001)))) (let ((ret_8_1 (ite (= (not (= ((_ extract 7 7) x) #b0)) true) (bvxor ret_7_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_7_1) #b00000000)) ret_7_1))) (let ((pow_8_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_7_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_7_1 #b000000001) y) (bvshl pow_7_1 #b000000001)))) (let ((ret_9 (ite (= (not (= ((_ extract 8 8) x) #b0)) true) (bvxor ret_8 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_8) #b00000000)) ret_8))) (let ((pow_9 (ite (= (not (= ((_ extract 8 8) (bvshl pow_8 #b000000001)) #b0)) true) (bvxor (bvshl pow_8 #b000000001) y) (bvshl pow_8 #b000000001)))) (let ((ret_9_1 (ite (= (not (= ((_ extract 8 8) x) #b0)) true) (bvxor ret_8_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_8_1) #b00000000)) ret_8_1))) (let ((pow_9_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_8_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_8_1 #b000000001) y) (bvshl pow_8_1 #b000000001)))) (let ((ret_5 (ite (= (not (= ((_ extract 9 9) x) #b0)) true) (bvxor ret_9_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_9_1) #b00000000)) ret_9_1))) (let ((pow_5 (ite (= (not (= ((_ extract 8 8) (bvshl pow_9_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_9_1 #b000000001) y) (bvshl pow_9_1 #b000000001)))) (let ((ret_10 (ite (= (not (= ((_ extract 10 10) x) #b0)) true) (bvxor ret_5 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_5) #b00000000)) ret_5))) (let ((pow_10 (ite (= (not (= ((_ extract 8 8) (bvshl pow_5 #b000000001)) #b0)) true) (bvxor (bvshl pow_5 #b000000001) y) (bvshl pow_5 #b000000001)))) (let ((ret_11 (ite (= (not (= ((_ extract 11 11) x) #b0)) true) (bvxor ret_10 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_10) #b00000000)) ret_10))) (let ((pow_11 (ite (= (not (= ((_ extract 8 8) (bvshl pow_10 #b000000001)) #b0)) true) (bvxor (bvshl pow_10 #b000000001) y) (bvshl pow_10 #b000000001)))) (let ((ret_12 (ite (= (not (= ((_ extract 12 12) x) #b0)) true) (bvxor ret_11 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_11) #b00000000)) ret_11))) (let ((pow_12 (ite (= (not (= ((_ extract 8 8) (bvshl pow_11 #b000000001)) #b0)) true) (bvxor (bvshl pow_11 #b000000001) y) (bvshl pow_11 #b000000001)))) (let ((ret_13 (ite (= (not (= ((_ extract 13 13) x) #b0)) true) (bvxor ret_12 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_12) #b00000000)) ret_12))) (let ((pow_13 (ite (= (not (= ((_ extract 8 8) (bvshl pow_12 #b000000001)) #b0)) true) (bvxor (bvshl pow_12 #b000000001) y) (bvshl pow_12 #b000000001)))) (let ((ret_14 (ite (= (not (= ((_ extract 14 14) x) #b0)) true) (bvxor ret_13 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_13) #b00000000)) ret_13))) (let ((pow_14 (ite (= (not (= ((_ extract 8 8) (bvshl pow_13 #b000000001)) #b0)) true) (bvxor (bvshl pow_13 #b000000001) y) (bvshl pow_13 #b000000001)))) (let ((ret_15 (ite (= (not (= ((_ extract 15 15) x) #b0)) true) (bvxor ret_14 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_14) #b00000000)) ret_14))) (let ((pow_15 (ite (= (not (= ((_ extract 8 8) (bvshl pow_14 #b000000001)) #b0)) true) (bvxor (bvshl pow_14 #b000000001) y) (bvshl pow_14 #b000000001)))) (ite (= y #b000000000) #b00000000 ret_15))))))))))))))))))))))))))))))))))))))))))))
-(define-fun |GF2BVPoly.polyMul.«8».«8»| ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 16) (let ((v (let ((v_1 (bvshl #b0000000000000000 #b0000000000000001))) (let ((v_1_1 (concat #b00000000 a))) (let ((v_1_1_1 (bvshl #b0000000000000000 #b0000000000000001))) (ite (= (not (= ((_ extract 7 7) b) #b0)) true) (bvxor v_1_1_1 v_1_1) v_1)))))) (let ((v_1 (let ((v_1_1 (bvshl v #b0000000000000001))) (let ((v_1_1_1 (concat #b00000000 a))) (let ((v_1_1_1_1 (bvshl v #b0000000000000001))) (ite (= (not (= ((_ extract 6 6) b) #b0)) true) (bvxor v_1_1_1_1 v_1_1_1) v_1_1)))))) (let ((v_2 (let ((v_2_1 (bvshl v_1 #b0000000000000001))) (let ((v_2_1_1 (concat #b00000000 a))) (let ((v_2_1_1_1 (bvshl v_1 #b0000000000000001))) (ite (= (not (= ((_ extract 5 5) b) #b0)) true) (bvxor v_2_1_1_1 v_2_1_1) v_2_1)))))) (let ((v_3 (let ((v_3_1 (bvshl v_2 #b0000000000000001))) (let ((v_3_1_1 (concat #b00000000 a))) (let ((v_3_1_1_1 (bvshl v_2 #b0000000000000001))) (ite (= (not (= ((_ extract 4 4) b) #b0)) true) (bvxor v_3_1_1_1 v_3_1_1) v_3_1)))))) (let ((v_4 (let ((v_4_1 (bvshl v_3 #b0000000000000001))) (let ((v_4_1_1 (concat #b00000000 a))) (let ((v_4_1_1_1 (bvshl v_3 #b0000000000000001))) (ite (= (not (= ((_ extract 3 3) b) #b0)) true) (bvxor v_4_1_1_1 v_4_1_1) v_4_1)))))) (let ((v_5 (let ((v_5_1 (bvshl v_4 #b0000000000000001))) (let ((v_5_1_1 (concat #b00000000 a))) (let ((v_5_1_1_1 (bvshl v_4 #b0000000000000001))) (ite (= (not (= ((_ extract 2 2) b) #b0)) true) (bvxor v_5_1_1_1 v_5_1_1) v_5_1)))))) (let ((v_6 (let ((v_6_1 (bvshl v_5 #b0000000000000001))) (let ((v_6_1_1 (concat #b00000000 a))) (let ((v_6_1_1_1 (bvshl v_5 #b0000000000000001))) (ite (= (not (= ((_ extract 1 1) b) #b0)) true) (bvxor v_6_1_1_1 v_6_1_1) v_6_1)))))) (let ((v_7 (let ((v_7_1 (bvshl v_6 #b0000000000000001))) (let ((v_7_1_1 (concat #b00000000 a))) (let ((v_7_1_1_1 (bvshl v_6 #b0000000000000001))) (ite (= (not (= ((_ extract 0 0) b) #b0)) true) (bvxor v_7_1_1_1 v_7_1_1) v_7_1)))))) v_7)))))))))
+(define-fun |GF2BVPoly.polyMul.«8».«8»| ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 16) (let ((ret (let ((tmp (bvshl #b0000000000000000 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl #b0000000000000000 #b0000000000000001))) (ite (= (not (= ((_ extract 7 7) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_1 (let ((tmp (bvshl ret #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret #b0000000000000001))) (ite (= (not (= ((_ extract 6 6) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_2 (let ((tmp (bvshl ret_1 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_1 #b0000000000000001))) (ite (= (not (= ((_ extract 5 5) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_3 (let ((tmp (bvshl ret_2 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_2 #b0000000000000001))) (ite (= (not (= ((_ extract 4 4) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_4 (let ((tmp (bvshl ret_3 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_3 #b0000000000000001))) (ite (= (not (= ((_ extract 3 3) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_5 (let ((tmp (bvshl ret_4 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_4 #b0000000000000001))) (ite (= (not (= ((_ extract 2 2) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_6 (let ((tmp (bvshl ret_5 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_5 #b0000000000000001))) (ite (= (not (= ((_ extract 1 1) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_7 (let ((tmp (bvshl ret_6 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_6 #b0000000000000001))) (ite (= (not (= ((_ extract 0 0) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) ret_7)))))))))
 (define-fun GaloisField2k.mul.GF256 ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 8) (|GF2BVPoly.polyMod.«16».«8»| (|GF2BVPoly.polyMul.«8».«8»| a b) (bvor #b100000000 (concat #b0 #b00011011))))
 (define-fun-rec GF256.pow2 ((k Nat) (x (_ BitVec 8))) (_ BitVec 8) (ite (= k 0) x (GaloisField2k.mul.GF256 (GF256.pow2 (Nat.sub k 1) x) (GF256.pow2 (Nat.sub k 1) x))))
 (declare-const x (_ BitVec 8))