Commit 942c52dc authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Fix Barrett benchmarks and move to UFDTNIA.

parent c8315233
(set-info :smt-lib-version 2.6)
(set-logic UFDTLIA)
(set-logic UFDTNIA)
(set-info :source |
From the test suite for the Move Prover, a verifier for smart contracts in the
......@@ -106,11 +106,11 @@ as of Dec 17, 2020. Submitted by Clark Barrett <barrett@cs.stanford.edu>.
(assert (= (|l#$ValueArray| $EmptyValueArray) 0))
(assert (= (|v#$ValueArray| $EmptyValueArray) ($MapConstValue $Error)))
(assert (= $StratificationDepth 4))
(assert (forall ((v1 T@$Value) (v2 T@$Value) ) (! (= ($IsEqual_stratified v1 v2) (or (= v1 v2) (and (and (and (is-$Vector v1) (is-$Vector v2)) (= (|l#$ValueArray| (|v#$Vector| v1)) (|l#$ValueArray| (|v#$Vector| v2)))) (forall ((i Int) ) (=> (and (<= 0 i) (< i (|l#$ValueArray| (|v#$Vector| v1)))) ($IsEqual_level1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v1)) i) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v2)) i))))))) :pattern ( ($IsEqual_stratified v1 v2))
(assert (forall ((v1 T@$Value) (v2 T@$Value) ) (! (= ($IsEqual_stratified v1 v2) (or (= v1 v2) (and (and (and ((_ is $Vector) v1) ((_ is $Vector) v2)) (= (|l#$ValueArray| (|v#$Vector| v1)) (|l#$ValueArray| (|v#$Vector| v2)))) (forall ((i Int) ) (=> (and (<= 0 i) (< i (|l#$ValueArray| (|v#$Vector| v1)))) ($IsEqual_level1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v1)) i) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v2)) i))))))) :pattern ( ($IsEqual_stratified v1 v2))
)))
(assert (forall ((v1@@0 T@$Value) (v2@@0 T@$Value) ) (! (= ($IsEqual_level1 v1@@0 v2@@0) (or (= v1@@0 v2@@0) (and (and (and (is-$Vector v1@@0) (is-$Vector v2@@0)) (= (|l#$ValueArray| (|v#$Vector| v1@@0)) (|l#$ValueArray| (|v#$Vector| v2@@0)))) (forall ((i@@0 Int) ) (=> (and (<= 0 i@@0) (< i@@0 (|l#$ValueArray| (|v#$Vector| v1@@0)))) ($IsEqual_level2 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v1@@0)) i@@0) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v2@@0)) i@@0))))))) :pattern ( ($IsEqual_level1 v1@@0 v2@@0))
(assert (forall ((v1@@0 T@$Value) (v2@@0 T@$Value) ) (! (= ($IsEqual_level1 v1@@0 v2@@0) (or (= v1@@0 v2@@0) (and (and (and ((_ is $Vector) v1@@0) ((_ is $Vector) v2@@0)) (= (|l#$ValueArray| (|v#$Vector| v1@@0)) (|l#$ValueArray| (|v#$Vector| v2@@0)))) (forall ((i@@0 Int) ) (=> (and (<= 0 i@@0) (< i@@0 (|l#$ValueArray| (|v#$Vector| v1@@0)))) ($IsEqual_level2 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v1@@0)) i@@0) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v2@@0)) i@@0))))))) :pattern ( ($IsEqual_level1 v1@@0 v2@@0))
)))
(assert (forall ((v1@@1 T@$Value) (v2@@1 T@$Value) ) (! (= ($IsEqual_level2 v1@@1 v2@@1) (or (= v1@@1 v2@@1) (and (and (and (is-$Vector v1@@1) (is-$Vector v2@@1)) (= (|l#$ValueArray| (|v#$Vector| v1@@1)) (|l#$ValueArray| (|v#$Vector| v2@@1)))) (forall ((i@@1 Int) ) (=> (and (<= 0 i@@1) (< i@@1 (|l#$ValueArray| (|v#$Vector| v1@@1)))) (= (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v1@@1)) i@@1) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v2@@1)) i@@1))))))) :pattern ( ($IsEqual_level2 v1@@1 v2@@1))
(assert (forall ((v1@@1 T@$Value) (v2@@1 T@$Value) ) (! (= ($IsEqual_level2 v1@@1 v2@@1) (or (= v1@@1 v2@@1) (and (and (and ((_ is $Vector) v1@@1) ((_ is $Vector) v2@@1)) (= (|l#$ValueArray| (|v#$Vector| v1@@1)) (|l#$ValueArray| (|v#$Vector| v2@@1)))) (forall ((i@@1 Int) ) (=> (and (<= 0 i@@1) (< i@@1 (|l#$ValueArray| (|v#$Vector| v1@@1)))) (= (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v1@@1)) i@@1) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v2@@1)) i@@1))))))) :pattern ( ($IsEqual_level2 v1@@1 v2@@1))
)))
(assert (forall ((p T@$Path) (v T@$Value) ) (! (= ($ReadValue_stratified p v) (ite (= 0 (|size#$Path| p)) v ($ReadValue_level1 p (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v)) (|Select_[$int]$int| (|p#$Path| p) 0))))) :pattern ( ($ReadValue_stratified p v))
)))
......@@ -168,46 +168,46 @@ as of Dec 17, 2020. Submitted by Clark Barrett <barrett@cs.stanford.edu>.
)))
(assert (forall ((ta@@5 T@$TypeValue) (v@@10 T@$Value) (i@@4 T@$Value) (j T@$Value) ) (! (= ($Vector_$swap ta@@5 v@@10 i@@4 j) ($Vector ($ValueArray (|Store_[$int]$Value| (|Store_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@10)) (|i#$Integer| i@@4) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@10)) (|i#$Integer| j))) (|i#$Integer| j) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@10)) (|i#$Integer| i@@4))) (|l#$ValueArray| (|v#$Vector| v@@10))))) :pattern ( ($Vector_$swap ta@@5 v@@10 i@@4 j))
)))
(assert (forall ((v1@@2 T@$Value) (v2@@2 T@$Value) ) (=> (and (and (and (is-$Vector v1@@2) (let ((va (|v#$Vector| v1@@2)))
(assert (forall ((v1@@2 T@$Value) (v2@@2 T@$Value) ) (=> (and (and (and ((_ is $Vector) v1@@2) (let ((va (|v#$Vector| v1@@2)))
(let ((l (|l#$ValueArray| va)))
(and (and (<= 0 l) (<= l $MAX_U64)) (forall ((x Int) ) (! (=> (or (< x 0) (>= x l)) (= (|Select_[$int]$Value| (|v#$ValueArray| va) x) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va) x))
)))))) (and (is-$Vector v2@@2) (let ((va@@0 (|v#$Vector| v2@@2)))
)))))) (and ((_ is $Vector) v2@@2) (let ((va@@0 (|v#$Vector| v2@@2)))
(let ((l@@0 (|l#$ValueArray| va@@0)))
(and (and (<= 0 l@@0) (<= l@@0 $MAX_U64)) (forall ((x@@0 Int) ) (! (=> (or (< x@@0 0) (>= x@@0 l@@0)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@0) x@@0) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@0) x@@0))
))))))) ($IsEqual_stratified v1@@2 v2@@2)) ($IsEqual_stratified ($Hash_sha2_core v1@@2) ($Hash_sha2_core v2@@2)))))
(assert (forall ((v1@@3 T@$Value) (v2@@3 T@$Value) ) (=> (and (and (and (is-$Vector v1@@3) (let ((va@@1 (|v#$Vector| v1@@3)))
(assert (forall ((v1@@3 T@$Value) (v2@@3 T@$Value) ) (=> (and (and (and ((_ is $Vector) v1@@3) (let ((va@@1 (|v#$Vector| v1@@3)))
(let ((l@@1 (|l#$ValueArray| va@@1)))
(and (and (<= 0 l@@1) (<= l@@1 $MAX_U64)) (forall ((x@@1 Int) ) (! (=> (or (< x@@1 0) (>= x@@1 l@@1)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@1) x@@1) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@1) x@@1))
)))))) (and (is-$Vector v2@@3) (let ((va@@2 (|v#$Vector| v2@@3)))
)))))) (and ((_ is $Vector) v2@@3) (let ((va@@2 (|v#$Vector| v2@@3)))
(let ((l@@2 (|l#$ValueArray| va@@2)))
(and (and (<= 0 l@@2) (<= l@@2 $MAX_U64)) (forall ((x@@2 Int) ) (! (=> (or (< x@@2 0) (>= x@@2 l@@2)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@2) x@@2) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@2) x@@2))
))))))) ($IsEqual_stratified ($Hash_sha2_core v1@@3) ($Hash_sha2_core v2@@3))) ($IsEqual_stratified v1@@3 v2@@3))))
(assert (forall ((v1@@4 T@$Value) (v2@@4 T@$Value) ) (=> (and (and (and (is-$Vector v1@@4) (let ((va@@3 (|v#$Vector| v1@@4)))
(assert (forall ((v1@@4 T@$Value) (v2@@4 T@$Value) ) (=> (and (and (and ((_ is $Vector) v1@@4) (let ((va@@3 (|v#$Vector| v1@@4)))
(let ((l@@3 (|l#$ValueArray| va@@3)))
(and (and (<= 0 l@@3) (<= l@@3 $MAX_U64)) (forall ((x@@3 Int) ) (! (=> (or (< x@@3 0) (>= x@@3 l@@3)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@3) x@@3) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@3) x@@3))
)))))) (and (is-$Vector v2@@4) (let ((va@@4 (|v#$Vector| v2@@4)))
)))))) (and ((_ is $Vector) v2@@4) (let ((va@@4 (|v#$Vector| v2@@4)))
(let ((l@@4 (|l#$ValueArray| va@@4)))
(and (and (<= 0 l@@4) (<= l@@4 $MAX_U64)) (forall ((x@@4 Int) ) (! (=> (or (< x@@4 0) (>= x@@4 l@@4)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@4) x@@4) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@4) x@@4))
))))))) ($IsEqual_stratified v1@@4 v2@@4)) ($IsEqual_stratified ($Hash_sha3_core v1@@4) ($Hash_sha3_core v2@@4)))))
(assert (forall ((v1@@5 T@$Value) (v2@@5 T@$Value) ) (=> (and (and (and (is-$Vector v1@@5) (let ((va@@5 (|v#$Vector| v1@@5)))
(assert (forall ((v1@@5 T@$Value) (v2@@5 T@$Value) ) (=> (and (and (and ((_ is $Vector) v1@@5) (let ((va@@5 (|v#$Vector| v1@@5)))
(let ((l@@5 (|l#$ValueArray| va@@5)))
(and (and (<= 0 l@@5) (<= l@@5 $MAX_U64)) (forall ((x@@5 Int) ) (! (=> (or (< x@@5 0) (>= x@@5 l@@5)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@5) x@@5) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@5) x@@5))
)))))) (and (is-$Vector v2@@5) (let ((va@@6 (|v#$Vector| v2@@5)))
)))))) (and ((_ is $Vector) v2@@5) (let ((va@@6 (|v#$Vector| v2@@5)))
(let ((l@@6 (|l#$ValueArray| va@@6)))
(and (and (<= 0 l@@6) (<= l@@6 $MAX_U64)) (forall ((x@@6 Int) ) (! (=> (or (< x@@6 0) (>= x@@6 l@@6)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@6) x@@6) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@6) x@@6))
))))))) ($IsEqual_stratified ($Hash_sha3_core v1@@5) ($Hash_sha3_core v2@@5))) ($IsEqual_stratified v1@@5 v2@@5))))
(assert (forall ((public_key T@$Value) ) (is-$Boolean ($Signature_$ed25519_validate_pubkey public_key))))
(assert (forall ((signature T@$Value) (public_key@@0 T@$Value) (message T@$Value) ) (is-$Boolean ($Signature_$ed25519_verify signature public_key@@0 message))))
(assert (forall ((public_key T@$Value) ) ((_ is $Boolean) ($Signature_$ed25519_validate_pubkey public_key))))
(assert (forall ((signature T@$Value) (public_key@@0 T@$Value) (message T@$Value) ) ((_ is $Boolean) ($Signature_$ed25519_verify signature public_key@@0 message))))
(assert (forall ((v1@@6 T@$Value) (v2@@6 T@$Value) ) (=> ($IsEqual_stratified v1@@6 v2@@6) (= ($BCS_serialize_core v1@@6) ($BCS_serialize_core v2@@6)))))
(assert (forall ((v@@11 T@$Value) ) (= ($BCS_serialize_core_inv ($BCS_serialize_core v@@11)) v@@11)))
(assert (forall ((v@@12 T@$Value) ) (let ((r ($BCS_serialize_core v@@12)))
(and (and (and (is-$Vector r) (let ((va@@7 (|v#$Vector| r)))
(and (and (and ((_ is $Vector) r) (let ((va@@7 (|v#$Vector| r)))
(let ((l@@7 (|l#$ValueArray| va@@7)))
(and (and (<= 0 l@@7) (<= l@@7 $MAX_U64)) (forall ((x@@7 Int) ) (! (=> (or (< x@@7 0) (>= x@@7 l@@7)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@7) x@@7) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@7) x@@7))
)))))) (forall ((i@@5 Int) ) (! (=> (and (<= 0 i@@5) (< i@@5 (|l#$ValueArray| (|v#$Vector| r)))) (and (and (is-$Integer (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| r)) i@@5)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| r)) i@@5)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| r)) i@@5)) $MAX_U8))) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| r)) i@@5))
)))))) (forall ((i@@5 Int) ) (! (=> (and (<= 0 i@@5) (< i@@5 (|l#$ValueArray| (|v#$Vector| r)))) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| r)) i@@5)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| r)) i@@5)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| r)) i@@5)) $MAX_U8))) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| r)) i@@5))
))) (> (|l#$ValueArray| (|v#$Vector| r)) 0)))))
(assert (forall ((v@@13 T@$Value) ) (let ((r@@0 ($BCS_serialize_core v@@13)))
(=> (is-$Address v@@13) (= (|l#$ValueArray| (|v#$Vector| r@@0)) $serialized_address_len)))))
(=> ((_ is $Address) v@@13) (= (|l#$ValueArray| (|v#$Vector| r@@0)) $serialized_address_len)))))
(assert (forall ((i@@6 Int) (|l#0| Int) (|l#1| Int) (|l#2| |T@[Int]$Value|) (|l#3| T@$Value) ) (! (= (|Select_[$int]$Value| (|lambda#0| |l#0| |l#1| |l#2| |l#3|) i@@6) (ite (and (>= i@@6 |l#0|) (< i@@6 |l#1|)) (|Select_[$int]$Value| |l#2| i@@6) |l#3|)) :pattern ( (|Select_[$int]$Value| (|lambda#0| |l#0| |l#1| |l#2| |l#3|) i@@6))
)))
(assert (forall ((j@@0 Int) (|l#0@@0| Int) (|l#1@@0| Int) (|l#2@@0| Int) (|l#3@@0| |T@[Int]$Value|) (|l#4| |T@[Int]$Value|) (|l#5| Int) (|l#6| T@$Value) ) (! (= (|Select_[$int]$Value| (|lambda#1| |l#0@@0| |l#1@@0| |l#2@@0| |l#3@@0| |l#4| |l#5| |l#6|) j@@0) (ite (and (>= j@@0 |l#0@@0|) (< j@@0 |l#1@@0|)) (ite (< j@@0 |l#2@@0|) (|Select_[$int]$Value| |l#3@@0| j@@0) (|Select_[$int]$Value| |l#4| (+ j@@0 |l#5|))) |l#6|)) :pattern ( (|Select_[$int]$Value| (|lambda#1| |l#0@@0| |l#1@@0| |l#2@@0| |l#3@@0| |l#4| |l#5| |l#6|) j@@0))
......@@ -237,7 +237,7 @@ as of Dec 17, 2020. Submitted by Clark Barrett <barrett@cs.stanford.edu>.
(let ((inline$$TestOpaque_opaque_caller_$def_verify$0$anon9_Else_correct (=> (and (not true) (= (ControlFlow 0 8977) 8979)) inline$$TestOpaque_opaque_caller_$def_verify$0$anon6_correct)))
(let ((inline$$TestOpaque_opaque_caller_$def_verify$0$anon9_Then_correct (=> (= (ControlFlow 0 8987) 8979) inline$$TestOpaque_opaque_caller_$def_verify$0$anon6_correct)))
(let ((inline$$TestOpaque_opaque_caller_$def_verify$0$anon7_Else_correct (=> (not $abort_flag@0) (and (=> (= (ControlFlow 0 8971) 8987) inline$$TestOpaque_opaque_caller_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 8971) 8977) inline$$TestOpaque_opaque_caller_$def_verify$0$anon9_Else_correct)))))
(let ((inline$$TestOpaque_opaque_caller_$def_verify$0$anon0_correct (=> (and (not false) (=> (not $abort_flag@0) (|b#$Boolean| ($Boolean ($IsEqual_stratified call2formal@$ret0@0 ($Integer 2)))))) (=> (and (and (is-$Integer call2formal@$ret0@0) (>= (|i#$Integer| call2formal@$ret0@0) 0)) (<= (|i#$Integer| call2formal@$ret0@0) $MAX_U64)) (and (=> (= (ControlFlow 0 8963) 8991) inline$$TestOpaque_opaque_caller_$def_verify$0$anon7_Then_correct) (=> (= (ControlFlow 0 8963) 8971) inline$$TestOpaque_opaque_caller_$def_verify$0$anon7_Else_correct))))))
(let ((inline$$TestOpaque_opaque_caller_$def_verify$0$anon0_correct (=> (and (not false) (=> (not $abort_flag@0) (|b#$Boolean| ($Boolean ($IsEqual_stratified call2formal@$ret0@0 ($Integer 2)))))) (=> (and (and ((_ is $Integer) call2formal@$ret0@0) (>= (|i#$Integer| call2formal@$ret0@0) 0)) (<= (|i#$Integer| call2formal@$ret0@0) $MAX_U64)) (and (=> (= (ControlFlow 0 8963) 8991) inline$$TestOpaque_opaque_caller_$def_verify$0$anon7_Then_correct) (=> (= (ControlFlow 0 8963) 8971) inline$$TestOpaque_opaque_caller_$def_verify$0$anon7_Else_correct))))))
(let ((anon0_correct (=> (= (ControlFlow 0 10033) 8963) inline$$TestOpaque_opaque_caller_$def_verify$0$anon0_correct)))
anon0_correct))))))))))))
))
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment