diff --git a/heapster-saw/examples/arrays.sawcore b/heapster-saw/examples/arrays.sawcore index 7c20a89268..6b1f16867b 100644 --- a/heapster-saw/examples/arrays.sawcore +++ b/heapster-saw/examples/arrays.sawcore @@ -2,3 +2,40 @@ module arrays where import Prelude; + +-- The helper function for noErrorsContains0 +-- +-- noErrorsContains0H len i v = +-- orM (exists x. returnM x) (noErrorsContains0H len (i+1) v) +noErrorsContains0H : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) -> + CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool); +noErrorsContains0H len_top i_top v_top = + letRecM + (LRT_Cons + (LRT_Fun (Vec 64 Bool) (\ (len:Vec 64 Bool) -> + LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) -> + LRT_Fun (BVVec 64 len (Vec 64 Bool)) (\ (_:BVVec 64 len (Vec 64 Bool)) -> + LRT_Ret (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool))))) + LRT_Nil) + (BVVec 64 len_top (Vec 64 Bool) * Vec 64 Bool) + (\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) -> + CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) -> + ((\ (len:Vec 64 Bool) (i:Vec 64 Bool) (v:BVVec 64 len (Vec 64 Bool)) -> + precondHint + (CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) + (and (bvsle 64 0x0000000000000000 i) + (bvsle 64 i 0x0fffffffffffffff)) + (orM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool) + (existsM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool) + (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool) + (returnM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool))) + (f len (bvAdd 64 i 0x0000000000000001) v))), ())) + (\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) -> + CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) -> + f len_top i_top v_top); + +-- The specification that contains0 has no errors +noErrorsContains0 : (len:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) -> + CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool); +noErrorsContains0 len v = + noErrorsContains0H len 0x0000000000000000 v; diff --git a/heapster-saw/examples/arrays_mr_solver.saw b/heapster-saw/examples/arrays_mr_solver.saw index 838e1d2874..eaa38a79f7 100644 --- a/heapster-saw/examples/arrays_mr_solver.saw +++ b/heapster-saw/examples/arrays_mr_solver.saw @@ -16,4 +16,8 @@ let run_test name test expected = // Test that contains0 |= contains0 contains0 <- parse_core_mod "arrays" "contains0"; -run_test "contains0 |= contains0" (mr_solver contains0 contains0) true; +// run_test "contains0 |= contains0" (mr_solver contains0 contains0) true; + +noErrorsContains0 <- parse_core_mod "arrays" "noErrorsContains0"; +run_test "contains0 |= noErrorsContains0" + (mr_solver_debug 0 contains0 noErrorsContains0) true; diff --git a/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v b/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v index a57aee7096..175ebcd520 100644 --- a/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v +++ b/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v @@ -131,6 +131,9 @@ Definition ecRatio : SAWCoreScaffolding.Integer -> SAWCoreScaffolding.Integer -> Definition eqRational : Rational -> Rational -> SAWCoreScaffolding.Bool := fun (x : unit : Type) (y : unit : Type) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: (==) Rational"%string. +Definition leRational : Rational -> Rational -> SAWCoreScaffolding.Bool := + fun (x : unit : Type) (y : unit : Type) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: (<=) Rational"%string. + Definition ltRational : Rational -> Rational -> SAWCoreScaffolding.Bool := fun (x : unit : Type) (y : unit : Type) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: (<) Rational"%string. @@ -219,6 +222,9 @@ Definition errorBinary : forall (s : SAWCoreScaffolding.String), forall (a : Typ Definition boolCmp : SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool := fun (x : SAWCoreScaffolding.Bool) (y : SAWCoreScaffolding.Bool) (k : SAWCoreScaffolding.Bool) => if x then SAWCoreScaffolding.and y k else SAWCoreScaffolding.or y k. +Definition boolLt : SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool := + fun (x : SAWCoreScaffolding.Bool) (y : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.and (SAWCoreScaffolding.not x) y. + Definition integerCmp : SAWCoreScaffolding.Integer -> SAWCoreScaffolding.Integer -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool := fun (x : SAWCoreScaffolding.Integer) (y : SAWCoreScaffolding.Integer) (k : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.or (SAWCoreScaffolding.intLt x y) (SAWCoreScaffolding.and (SAWCoreScaffolding.intEq x y) k). @@ -235,12 +241,25 @@ Definition vecCmp : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), fora fun (n : SAWCoreScaffolding.Nat) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (f : a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (xs : SAWCoreVectorsAsCoqVectors.Vec n a) (ys : SAWCoreVectorsAsCoqVectors.Vec n a) (k : SAWCoreScaffolding.Bool) => let var__0 := SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool in SAWCoreVectorsAsCoqVectors.foldr var__0 SAWCoreScaffolding.Bool n (fun (f1 : var__0) => f1) k (SAWCorePrelude.zipWith a a var__0 f n xs ys). +Definition vecLt : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) -> (a -> a -> SAWCoreScaffolding.Bool) -> SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Bool := + fun (n : SAWCoreScaffolding.Nat) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (f : a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (g : a -> a -> SAWCoreScaffolding.Bool) (xs : SAWCoreVectorsAsCoqVectors.Vec n a) (ys : SAWCoreVectorsAsCoqVectors.Vec n a) => let var__0 := SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool in + SAWCoreVectorsAsCoqVectors.foldr var__0 SAWCoreScaffolding.Bool n (fun (f1 : var__0) => f1) SAWCoreScaffolding.false (SAWCorePrelude.zipWith a a var__0 f n xs ys). + Definition unitCmp : (unit : Type) -> (unit : Type) -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool := - fun (_1 : unit : Type) (_2 : unit : Type) (_3 : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.false. + fun (_1 : unit : Type) (_2 : unit : Type) (k : SAWCoreScaffolding.Bool) => k. + +Definition unitLe : (unit : Type) -> (unit : Type) -> SAWCoreScaffolding.Bool := + fun (_1 : unit : Type) (_2 : unit : Type) => SAWCoreScaffolding.true. + +Definition unitLt : (unit : Type) -> (unit : Type) -> SAWCoreScaffolding.Bool := + fun (_1 : unit : Type) (_2 : unit : Type) => SAWCoreScaffolding.false. Definition pairCmp : forall (a : Type), forall (b : Type), (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) -> (b -> b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) -> prod a b -> prod a b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool := fun (a : Type) (b : Type) (f : a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (g : b -> b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (x12 : prod a b) (y12 : prod a b) (k : SAWCoreScaffolding.Bool) => f (fst x12) (fst y12) (g (snd x12) (snd y12) k). +Definition pairLt : forall (a : Type), forall (b : Type), (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) -> (b -> b -> SAWCoreScaffolding.Bool) -> prod a b -> prod a b -> SAWCoreScaffolding.Bool := + fun (a : Type) (b : Type) (f : a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (g : b -> b -> SAWCoreScaffolding.Bool) (x : prod a b) (y : prod a b) => f (fst x) (fst y) (g (snd x) (snd y)). + Definition PEq : Type -> Type := fun (a : Type) => RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil. @@ -278,55 +297,61 @@ Definition PEqPair : forall (a : Type), forall (b : Type), PEq a -> PEq b -> PEq fun (a : Type) (b : Type) (pa : RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (pb : RecordTypeCons "eq" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil) => RecordCons "eq" (SAWCorePrelude.pairEq a b (RecordProj pa "eq") (RecordProj pb "eq")) RecordNil. Definition PCmp : Type -> Type := - fun (a : Type) => RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (PEq a) RecordTypeNil). + fun (a : Type) => let var__0 := a -> a -> SAWCoreScaffolding.Bool in + RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (PEq a) (RecordTypeCons "le" var__0 (RecordTypeCons "lt" var__0 RecordTypeNil))). Definition PCmpBit : PCmp SAWCoreScaffolding.Bool := - RecordCons "cmp" boolCmp (RecordCons "cmpEq" PEqBit RecordNil). + RecordCons "cmp" boolCmp (RecordCons "cmpEq" PEqBit (RecordCons "le" implies (RecordCons "lt" boolLt RecordNil))). Definition PCmpInteger : PCmp SAWCoreScaffolding.Integer := - RecordCons "cmp" integerCmp (RecordCons "cmpEq" PEqInteger RecordNil). + RecordCons "cmp" integerCmp (RecordCons "cmpEq" PEqInteger (RecordCons "le" SAWCoreScaffolding.intLe (RecordCons "lt" SAWCoreScaffolding.intLt RecordNil))). Definition PCmpRational : PCmp Rational := - RecordCons "cmp" rationalCmp (RecordCons "cmpEq" PEqRational RecordNil). + RecordCons "cmp" rationalCmp (RecordCons "cmpEq" PEqRational (RecordCons "le" leRational (RecordCons "lt" ltRational RecordNil))). Definition PCmpVec : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PCmp a -> PCmp (SAWCoreVectorsAsCoqVectors.Vec n a) := - fun (n : SAWCoreScaffolding.Nat) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) => RecordCons "cmp" (vecCmp n a (RecordProj pa "cmp")) (RecordCons "cmpEq" (PEqVec n a (RecordProj pa "cmpEq")) RecordNil). + fun (n : SAWCoreScaffolding.Nat) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => let var__0 := SAWCoreVectorsAsCoqVectors.Vec n a in + RecordCons "cmp" (vecCmp n a (RecordProj pa "cmp")) (RecordCons "cmpEq" (PEqVec n a (RecordProj pa "cmpEq")) (RecordCons "le" (fun (x : var__0) (y : SAWCoreVectorsAsCoqVectors.Vec n a) => vecCmp n a (RecordProj pa "cmp") x y SAWCoreScaffolding.true) (RecordCons "lt" (fun (x : var__0) (y : SAWCoreVectorsAsCoqVectors.Vec n a) => vecCmp n a (RecordProj pa "cmp") x y SAWCoreScaffolding.false) RecordNil))). Definition PCmpSeq : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PCmp a -> PCmp (seq n a) := - fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PCmp a -> PCmp (seq n1 a)) (fun (n1 : SAWCoreScaffolding.Nat) => PCmpVec n1) (fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) => SAWCoreScaffolding.error (PCmp (SAWCorePrelude.Stream a)) "invalid Cmp instance"%string) n. + fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PCmp a -> PCmp (seq n1 a)) (fun (n1 : SAWCoreScaffolding.Nat) => PCmpVec n1) (fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => SAWCoreScaffolding.error (PCmp (SAWCorePrelude.Stream a)) "invalid Cmp instance"%string) n. Definition PCmpWord : forall (n : SAWCoreScaffolding.Nat), PCmp (SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) := - fun (n : SAWCoreScaffolding.Nat) => RecordCons "cmp" (bvCmp n) (RecordCons "cmpEq" (PEqWord n) RecordNil). + fun (n : SAWCoreScaffolding.Nat) => RecordCons "cmp" (bvCmp n) (RecordCons "cmpEq" (PEqWord n) (RecordCons "le" (SAWCoreVectorsAsCoqVectors.bvule n) (RecordCons "lt" (SAWCoreVectorsAsCoqVectors.bvult n) RecordNil))). Definition PCmpSeqBool : forall (n : Num), PCmp (seq n SAWCoreScaffolding.Bool) := fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => PCmp (seq n1 SAWCoreScaffolding.Bool)) (fun (n1 : SAWCoreScaffolding.Nat) => PCmpWord n1) (SAWCoreScaffolding.error (PCmp (SAWCorePrelude.Stream SAWCoreScaffolding.Bool)) "invalid Cmp instance"%string) n. Definition PCmpUnit : PCmp (unit : Type) := - RecordCons "cmp" unitCmp (RecordCons "cmpEq" PEqUnit RecordNil). + RecordCons "cmp" unitCmp (RecordCons "cmpEq" PEqUnit (RecordCons "le" unitLe (RecordCons "lt" unitLt RecordNil))). Definition PCmpPair : forall (a : Type), forall (b : Type), PCmp a -> PCmp b -> PCmp (prod a b) := - fun (a : Type) (b : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (pb : RecordTypeCons "cmp" (b -> b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) => RecordCons "cmp" (pairCmp a b (RecordProj pa "cmp") (RecordProj pb "cmp")) (RecordCons "cmpEq" (PEqPair a b (RecordProj pa "cmpEq") (RecordProj pb "cmpEq")) RecordNil). + fun (a : Type) (b : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (pb : RecordTypeCons "cmp" (b -> b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (b -> b -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => let var__0 := RecordProj pa "cmp" in + RecordCons "cmp" (pairCmp a b var__0 (RecordProj pb "cmp")) (RecordCons "cmpEq" (PEqPair a b (RecordProj pa "cmpEq") (RecordProj pb "cmpEq")) (RecordCons "le" (pairLt a b var__0 (RecordProj pb "le")) (RecordCons "lt" (pairLt a b var__0 (RecordProj pb "lt")) RecordNil))). Definition PSignedCmp : Type -> Type := - fun (a : Type) => RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (PEq a) RecordTypeNil). + fun (a : Type) => let var__0 := a -> a -> SAWCoreScaffolding.Bool in + RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (PEq a) (RecordTypeCons "sle" var__0 (RecordTypeCons "slt" var__0 RecordTypeNil))). Definition PSignedCmpVec : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PSignedCmp a -> PSignedCmp (SAWCoreVectorsAsCoqVectors.Vec n a) := - fun (n : SAWCoreScaffolding.Nat) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) => RecordCons "scmp" (vecCmp n a (RecordProj pa "scmp")) (RecordCons "signedCmpEq" (PEqVec n a (RecordProj pa "signedCmpEq")) RecordNil). + fun (n : SAWCoreScaffolding.Nat) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "sle" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "slt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => let var__0 := SAWCoreVectorsAsCoqVectors.Vec n a in + RecordCons "scmp" (vecCmp n a (RecordProj pa "scmp")) (RecordCons "signedCmpEq" (PEqVec n a (RecordProj pa "signedCmpEq")) (RecordCons "sle" (fun (x : var__0) (y : SAWCoreVectorsAsCoqVectors.Vec n a) => vecCmp n a (RecordProj pa "scmp") x y SAWCoreScaffolding.true) (RecordCons "slt" (fun (x : var__0) (y : SAWCoreVectorsAsCoqVectors.Vec n a) => vecCmp n a (RecordProj pa "scmp") x y SAWCoreScaffolding.false) RecordNil))). Definition PSignedCmpSeq : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PSignedCmp a -> PSignedCmp (seq n a) := - fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PSignedCmp a -> PSignedCmp (seq n1 a)) (fun (n1 : SAWCoreScaffolding.Nat) => PSignedCmpVec n1) (fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) => SAWCoreScaffolding.error (PSignedCmp (SAWCorePrelude.Stream a)) "invalid SignedCmp instance"%string) n. + fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PSignedCmp a -> PSignedCmp (seq n1 a)) (fun (n1 : SAWCoreScaffolding.Nat) => PSignedCmpVec n1) (fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "sle" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "slt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => SAWCoreScaffolding.error (PSignedCmp (SAWCorePrelude.Stream a)) "invalid SignedCmp instance"%string) n. Definition PSignedCmpWord : forall (n : SAWCoreScaffolding.Nat), PSignedCmp (SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) := - fun (n : SAWCoreScaffolding.Nat) => RecordCons "scmp" (bvSCmp n) (RecordCons "signedCmpEq" (PEqWord n) RecordNil). + fun (n : SAWCoreScaffolding.Nat) => RecordCons "scmp" (bvSCmp n) (RecordCons "signedCmpEq" (PEqWord n) (RecordCons "sle" (SAWCoreVectorsAsCoqVectors.bvsle n) (RecordCons "slt" (SAWCoreVectorsAsCoqVectors.bvslt n) RecordNil))). Definition PSignedCmpSeqBool : forall (n : Num), PSignedCmp (seq n SAWCoreScaffolding.Bool) := fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => PSignedCmp (seq n1 SAWCoreScaffolding.Bool)) (fun (n1 : SAWCoreScaffolding.Nat) => PSignedCmpWord n1) (SAWCoreScaffolding.error (PSignedCmp (SAWCorePrelude.Stream SAWCoreScaffolding.Bool)) "invalid SignedCmp instance"%string) n. Definition PSignedCmpUnit : PSignedCmp (unit : Type) := - RecordCons "scmp" unitCmp (RecordCons "signedCmpEq" PEqUnit RecordNil). + RecordCons "scmp" unitCmp (RecordCons "signedCmpEq" PEqUnit (RecordCons "sle" unitLe (RecordCons "slt" unitLt RecordNil))). Definition PSignedCmpPair : forall (a : Type), forall (b : Type), PSignedCmp a -> PSignedCmp b -> PSignedCmp (prod a b) := - fun (a : Type) (b : Type) (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (pb : RecordTypeCons "scmp" (b -> b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) => RecordCons "scmp" (pairCmp a b (RecordProj pa "scmp") (RecordProj pb "scmp")) (RecordCons "signedCmpEq" (PEqPair a b (RecordProj pa "signedCmpEq") (RecordProj pb "signedCmpEq")) RecordNil). + fun (a : Type) (b : Type) (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "sle" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "slt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (pb : RecordTypeCons "scmp" (b -> b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "sle" (b -> b -> SAWCoreScaffolding.Bool) (RecordTypeCons "slt" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => let var__0 := RecordProj pa "scmp" in + RecordCons "scmp" (pairCmp a b var__0 (RecordProj pb "scmp")) (RecordCons "signedCmpEq" (PEqPair a b (RecordProj pa "signedCmpEq") (RecordProj pb "signedCmpEq")) (RecordCons "sle" (pairLt a b var__0 (RecordProj pb "sle")) (RecordCons "slt" (pairLt a b var__0 (RecordProj pb "slt")) RecordNil))). Definition PZero : Type -> Type := fun (a : Type) => a. @@ -523,19 +548,19 @@ Definition ecFieldDiv : forall (a : Type), PField a -> a -> a -> a := fun (a : Type) (pf : RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) => RecordProj pf "fieldDiv". Definition ecCeiling : forall (a : Type), PRound a -> a -> SAWCoreScaffolding.Integer := - fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "ceiling". + fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "ceiling". Definition ecFloor : forall (a : Type), PRound a -> a -> SAWCoreScaffolding.Integer := - fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "floor". + fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "floor". Definition ecTruncate : forall (a : Type), PRound a -> a -> SAWCoreScaffolding.Integer := - fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "trunc". + fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "trunc". Definition ecRoundAway : forall (a : Type), PRound a -> a -> SAWCoreScaffolding.Integer := - fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "roundAway". + fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "roundAway". Definition ecRoundToEven : forall (a : Type), PRound a -> a -> SAWCoreScaffolding.Integer := - fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "roundToEven". + fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "roundToEven". Definition ecLg2 : forall (n : Num), seq n SAWCoreScaffolding.Bool -> seq n SAWCoreScaffolding.Bool := fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => seq n1 SAWCoreScaffolding.Bool -> seq n1 SAWCoreScaffolding.Bool) SAWCoreVectorsAsCoqVectors.bvLg2 (SAWCoreScaffolding.error (SAWCorePrelude.Stream SAWCoreScaffolding.Bool -> SAWCorePrelude.Stream SAWCoreScaffolding.Bool) "ecLg2: expected finite word"%string) n. @@ -556,19 +581,19 @@ Definition ecNotEq : forall (a : Type), PEq a -> a -> a -> SAWCoreScaffolding.Bo fun (a : Type) (pa : RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (x : a) (y : a) => SAWCoreScaffolding.not (ecEq a pa x y). Definition ecLt : forall (a : Type), PCmp a -> a -> a -> SAWCoreScaffolding.Bool := - fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (x : a) (y : a) => RecordProj pa "cmp" x y SAWCoreScaffolding.false. + fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => RecordProj pa "lt". Definition ecGt : forall (a : Type), PCmp a -> a -> a -> SAWCoreScaffolding.Bool := - fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (x : a) (y : a) => ecLt a pa y x. + fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (x : a) (y : a) => ecLt a pa y x. Definition ecLtEq : forall (a : Type), PCmp a -> a -> a -> SAWCoreScaffolding.Bool := - fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (x : a) (y : a) => SAWCoreScaffolding.not (ecLt a pa y x). + fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => RecordProj pa "le". Definition ecGtEq : forall (a : Type), PCmp a -> a -> a -> SAWCoreScaffolding.Bool := - fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (x : a) (y : a) => SAWCoreScaffolding.not (ecLt a pa x y). + fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (x : a) (y : a) => ecLtEq a pa y x. Definition ecSLt : forall (a : Type), PSignedCmp a -> a -> a -> SAWCoreScaffolding.Bool := - fun (a : Type) (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (x : a) (y : a) => RecordProj pa "scmp" x y SAWCoreScaffolding.false. + fun (a : Type) (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "sle" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "slt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => RecordProj pa "slt". Definition ecAnd : forall (a : Type), PLogic a -> a -> a -> a := fun (a : Type) (pa : RecordTypeCons "and" (a -> a -> a) (RecordTypeCons "logicZero" a (RecordTypeCons "not" (a -> a) (RecordTypeCons "or" (a -> a -> a) (RecordTypeCons "xor" (a -> a -> a) RecordTypeNil))))) => RecordProj pa "and". @@ -694,7 +719,8 @@ Definition PEqFloat : forall (e : Num), forall (p : Num), PEq (TCFloat e p) := fun (e : Num) (p : Num) => RecordCons "eq" (fun (x : unit : Type) (y : unit : Type) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: (==) Float"%string) RecordNil. Definition PCmpFloat : forall (e : Num), forall (p : Num), PCmp (TCFloat e p) := - fun (e : Num) (p : Num) => RecordCons "cmp" (fun (x : unit : Type) (y : unit : Type) (k : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: Cmp Float"%string) (RecordCons "cmpEq" (PEqFloat e p) RecordNil). + fun (e : Num) (p : Num) => let var__0 := fun (x : unit : Type) (y : unit : Type) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: Cmp Float"%string in + RecordCons "cmp" (fun (x : unit : Type) (y : unit : Type) (k : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: Cmp Float"%string) (RecordCons "cmpEq" (PEqFloat e p) (RecordCons "le" var__0 (RecordCons "lt" var__0 RecordNil))). Definition PZeroFloat : forall (e : Num), forall (p : Num), PZero (TCFloat e p) := fun (e : Num) (p : Num) => SAWCoreScaffolding.error (TCFloat e p) "Unimplemented: Zero Float"%string. diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v index 792b54e6e9..8ea02a2411 100644 --- a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v +++ b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v @@ -377,12 +377,12 @@ Definition and_triv2 : forall (x : SAWCoreScaffolding.Bool), SAWCoreScaffolding. fun (x : SAWCoreScaffolding.Bool) => let var__0 := SAWCoreScaffolding.not SAWCoreScaffolding.true in SAWCoreScaffolding.iteDep (fun (b : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool (SAWCoreScaffolding.and (SAWCoreScaffolding.not b) b) SAWCoreScaffolding.false) x (trans SAWCoreScaffolding.Bool (SAWCoreScaffolding.and var__0 SAWCoreScaffolding.true) var__0 SAWCoreScaffolding.false (and_True2 var__0) not_True) (and_False2 (SAWCoreScaffolding.not SAWCoreScaffolding.false)). -Definition FalseProp : Prop := - SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false. - Definition EqTrue : SAWCoreScaffolding.Bool -> Prop := fun (x : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool x SAWCoreScaffolding.true. +Definition TrueProp : Prop := + EqTrue SAWCoreScaffolding.true. + Definition TrueI : EqTrue SAWCoreScaffolding.true := SAWCoreScaffolding.Refl SAWCoreScaffolding.Bool SAWCoreScaffolding.true. @@ -534,6 +534,9 @@ Axiom head : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), SAWCoreVect Axiom tail : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), SAWCoreVectorsAsCoqVectors.Vec (SAWCoreScaffolding.Succ n) a -> SAWCoreVectorsAsCoqVectors.Vec n a . +Definition atWithDefault' : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), a -> SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Nat -> a := + fun (n_top : SAWCoreScaffolding.Nat) (a : Type) (d : a) => Nat__rec (fun (n : SAWCoreScaffolding.Nat) => SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Nat -> a) (fun (_1 : SAWCoreVectorsAsCoqVectors.Vec 0 a) (_2 : SAWCoreScaffolding.Nat) => d) (fun (n : SAWCoreScaffolding.Nat) (rec_f : SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Nat -> a) (v : SAWCoreVectorsAsCoqVectors.Vec (SAWCoreScaffolding.Succ n) a) (i : SAWCoreScaffolding.Nat) => Nat_cases a (head n a v) (fun (i_prev : SAWCoreScaffolding.Nat) (_1 : a) => rec_f (tail n a v) i_prev) i) n_top. + (* Prelude.atWithDefault was skipped *) Definition sawAt : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Nat -> a := @@ -1009,10 +1012,16 @@ Definition genBVVec : forall (n : SAWCoreScaffolding.Nat), forall (len : SAWCore Definition genBVVecFromVec : forall (m : SAWCoreScaffolding.Nat), forall (a : Type), SAWCoreVectorsAsCoqVectors.Vec m a -> a -> forall (n : SAWCoreScaffolding.Nat), forall (len : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool), BVVec n len a := fun (m : SAWCoreScaffolding.Nat) (a : Type) (v : SAWCoreVectorsAsCoqVectors.Vec m a) (def : a) (n : SAWCoreScaffolding.Nat) (len : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) => genBVVec n len a (fun (i : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) (_1 : SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool (SAWCoreVectorsAsCoqVectors.bvult n i len) SAWCoreScaffolding.true) => SAWCoreVectorsAsCoqVectors.atWithDefault m a def v (SAWCoreVectorsAsCoqVectors.bvToNat n i)). -Definition efq : forall (a : Type), SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false -> a := +Definition FalseProp : Prop := + SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false. + +Definition efq : forall (a : Type), FalseProp -> a := fun (a : Type) (contra : SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false) => let var__0 := if SAWCoreScaffolding.true then unit : Type else a in SAWCoreScaffolding.coerce (unit : Type) a (trans Type (unit : Type) var__0 a (sym Type var__0 (unit : Type) (ite_true Type (unit : Type) a)) (trans Type var__0 (if SAWCoreScaffolding.false then unit : Type else a) a (eq_cong SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false contra Type (fun (b : SAWCoreScaffolding.Bool) => if b then unit : Type else a)) (ite_false Type (unit : Type) a))) tt. +Definition efq1 : forall (a : Type), SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false -> a := + fun (a : Type) (contra : SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false) => SAWCoreScaffolding.Eq__rec Bit Bit1 (fun (b : Bit) (_1 : SAWCoreScaffolding.Eq Bit Bit1 b) => SAWCorePrelude.Bit_rect (fun (_2 : Bit) => Type) (unit : Type) a b) tt Bit0 (efq (SAWCoreScaffolding.Eq Bit Bit1 Bit0) contra). + Definition emptyBVVec : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), BVVec n (SAWCoreVectorsAsCoqVectors.bvNat n 0) a := fun (n : SAWCoreScaffolding.Nat) (a : Type) => genBVVec n (SAWCoreVectorsAsCoqVectors.bvNat n 0) a (fun (i : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) (pf : SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool (SAWCoreVectorsAsCoqVectors.bvult n i (SAWCoreVectorsAsCoqVectors.bvNat n 0)) SAWCoreScaffolding.true) => let var__0 := SAWCoreVectorsAsCoqVectors.bvult n i (SAWCoreVectorsAsCoqVectors.bvNat n 0) in efq a (trans SAWCoreScaffolding.Bool SAWCoreScaffolding.true var__0 SAWCoreScaffolding.false (sym SAWCoreScaffolding.Bool var__0 SAWCoreScaffolding.true pf) (not_bvult_zero n i))). @@ -1130,8 +1139,6 @@ Definition foldIRT : forall (As : ListSort), forall (Ds : IRTSubsts As), forall (* Prelude.bindM was skipped *) -(* Prelude.existsM was skipped *) - (* Prelude.errorM was skipped *) Definition fmapM : forall (a : Type), forall (b : Type), (a -> b) -> CompM a -> CompM b := @@ -1147,6 +1154,21 @@ Definition fmapM2 : forall (a : Type), forall (b : Type), forall (c : Type), (a Definition fmapM3 : forall (a : Type), forall (b : Type), forall (c : Type), forall (d : Type), (a -> b -> c -> d) -> CompM a -> CompM b -> CompM c -> CompM d := fun (a : Type) (b : Type) (c : Type) (d : Type) (f : a -> b -> c -> d) (m1 : CompM a) (m2 : CompM b) (m3 : CompM c) => applyM c d (fmapM2 a b (c -> d) f m1 m2) m3. +Definition bindM2 : forall (a : Type), forall (b : Type), forall (c : Type), CompM a -> CompM b -> (a -> b -> CompM c) -> CompM c := + fun (a : Type) (b : Type) (c : Type) (m1 : CompM a) (m2 : CompM b) (f : a -> b -> CompM c) => @bindM CompM _ a c m1 (fun (x : a) => @bindM CompM _ b c m2 (f x)). + +Definition bindM3 : forall (a : Type), forall (b : Type), forall (c : Type), forall (d : Type), CompM a -> CompM b -> CompM c -> (a -> b -> c -> CompM d) -> CompM d := + fun (a : Type) (b : Type) (c : Type) (d : Type) (m1 : CompM a) (m2 : CompM b) (m3 : CompM c) (f : a -> b -> c -> CompM d) => @bindM CompM _ a d m1 (fun (x : a) => bindM2 b c d m2 m3 (f x)). + +Definition bindApplyM : forall (a : Type), forall (b : Type), (a -> CompM b) -> CompM a -> CompM b := + fun (a : Type) (b : Type) (f : a -> CompM b) (m : CompM a) => @bindM CompM _ a b m f. + +Definition bindApplyM2 : forall (a : Type), forall (b : Type), forall (c : Type), (a -> b -> CompM c) -> CompM a -> CompM b -> CompM c := + fun (a : Type) (b : Type) (c : Type) (f : a -> b -> CompM c) (m1 : CompM a) (m2 : CompM b) => @bindM CompM _ a c m1 (fun (x : a) => @bindM CompM _ b c m2 (f x)). + +Definition bindApplyM3 : forall (a : Type), forall (b : Type), forall (c : Type), forall (d : Type), (a -> b -> c -> CompM d) -> CompM a -> CompM b -> CompM c -> CompM d := + fun (a : Type) (b : Type) (c : Type) (d : Type) (f : a -> b -> c -> CompM d) (m1 : CompM a) (m2 : CompM b) (m3 : CompM c) => bindM3 a b c d m1 m2 m3 f. + Definition composeM : forall (a : Type), forall (b : Type), forall (c : Type), (a -> CompM b) -> (b -> CompM c) -> a -> CompM c := fun (a : Type) (b : Type) (c : Type) (f : a -> CompM b) (g : b -> CompM c) (x : a) => @bindM CompM _ b c (f x) g. @@ -1171,7 +1193,14 @@ Definition appendCastBVVecM : forall (n : SAWCoreScaffolding.Nat), forall (len1 let var__5 := BVVec n len3 a in @returnM CompM _ var__5 (SAWCoreScaffolding.coerce (BVVec n var__4 a) var__5 (eq_cong var__3 var__4 len3 pf Type (fun (l : var__3) => BVVec n l a)) (appendBVVec n len1 len2 a v1 v2))) (bvEqWithProof n var__0 len3). -(* Prelude.fixM was skipped *) +(* Prelude.existsM was skipped *) + +(* Prelude.orM was skipped *) + +(* Prelude.forallM was skipped *) + +Definition precondHint : forall (a : Type), SAWCoreScaffolding.Bool -> a -> a := + fun (_1 : Type) (_2 : SAWCoreScaffolding.Bool) (a : _1) => a. (* Prelude.LetRecType was skipped *) @@ -1183,14 +1212,19 @@ Definition appendCastBVVecM : forall (n : SAWCoreScaffolding.Nat), forall (len1 (* Prelude.lrtTupleType was skipped *) -(* Prelude.multiFixM was skipped *) - (* Prelude.letRecM was skipped *) Definition letRecM1 : forall (a : Type), forall (b : Type), forall (c : Type), ((a -> CompM b) -> a -> CompM b) -> ((a -> CompM b) -> CompM c) -> CompM c := fun (a : Type) (b : Type) (c : Type) (fn : (a -> CompM b) -> a -> CompM b) (body : (a -> CompM b) -> CompM c) => let var__0 := a -> CompM b in @CompM.letRecM (CompM.LRT_Cons (CompM.LRT_Fun a (fun (_1 : a) => CompM.LRT_Ret b)) CompM.LRT_Nil) c (fun (f : var__0) => pair (fn f) tt) (fun (f : var__0) => body f). +(* Prelude.fixM was skipped *) + +(* Prelude.multiFixM was skipped *) + +Definition multiArgFixM : forall (lrt : CompM.LetRecType), (CompM.lrtToType lrt -> CompM.lrtToType lrt) -> CompM.lrtToType lrt := + fun (lrt : CompM.LetRecType) (F : CompM.LetRecType_rect (fun (lrt1 : CompM.LetRecType) => Type) (fun (b : Type) => CompM b) (fun (a : Type) (_1 : a -> CompM.LetRecType) (b : a -> Type) => forall (x : a), b x) lrt -> CompM.LetRecType_rect (fun (lrt1 : CompM.LetRecType) => Type) (fun (b : Type) => CompM b) (fun (a : Type) (_2 : a -> CompM.LetRecType) (b : a -> Type) => forall (x : a), b x) lrt) => SAWCoreScaffolding.fst (@CompM.multiFixM (CompM.LRT_Cons lrt CompM.LRT_Nil) (fun (f : CompM.LetRecType_rect (fun (lrt1 : CompM.LetRecType) => Type) (fun (b : Type) => CompM b) (fun (a : Type) (_1 : a -> CompM.LetRecType) (b : a -> Type) => forall (x : a), b x) lrt) => pair (F f) tt)). + (* Prelude.test_fun0 was skipped *) (* Prelude.test_fun1 was skipped *) diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs index c772b7d01d..d8e61537de 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs +++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs @@ -451,11 +451,11 @@ sawCorePreludeSpecialTreatmentMap configuration = , ("errorM", replace (Coq.App (Coq.ExplVar "errorM") [Coq.Var "CompM", Coq.Var "_"])) , ("catchM", skip) - , ("existsM", mapsTo compMModule "existsM") - , ("forallM", mapsTo compMModule "forallM") + , ("existsM", mapsToExpl compMModule "existsM") + , ("forallM", mapsToExpl compMModule "forallM") + , ("orM", mapsToExpl compMModule "orM") , ("fixM", replace (Coq.App (Coq.ExplVar "fixM") [Coq.Var "CompM", Coq.Var "_"])) - , ("existsM", mapsToExpl compMModule "existsM") , ("LetRecType", mapsTo compMModule "LetRecType") , ("LRT_Ret", mapsTo compMModule "LRT_Ret") , ("LRT_Fun", mapsTo compMModule "LRT_Fun") diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index 7b0676ff67..8eeaaf033b 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/saw-core/prelude/Prelude.sawcore @@ -1718,9 +1718,9 @@ efq a contra = -- Ex Falso Quodlibet at sort 1 efq1 : (a : sort 1) -> Eq Bool True False -> a; efq1 a contra = - Eq#rec Bit Bit1 - (\ (b:Bit) (_:Eq Bit Bit1 b) -> Bit#rec (\ (_:Bit) -> sort 1) #() a b) - () Bit0 (efq (Eq Bit Bit1 Bit0) contra); + Eq__rec Bit Bit1 + (\ (b:Bit) (_:Eq Bit Bit1 b) -> Bit#rec (\ (_:Bit) -> sort 1) #() a b) + () Bit0 (efq (Eq Bit Bit1 Bit0) contra); -- Generate an empty BVVec emptyBVVec : (n : Nat) -> (a : sort 0) -> BVVec n (bvNat n 0) a; @@ -2158,6 +2158,10 @@ orM a m1 m2 = existsM Bool a (\ (b:Bool) -> ite (CompM a) b m1 m2); -- those computations diverge from each other. primitive forallM : (a b:sort 0) -> (a -> CompM b) -> CompM b; +-- A hint to Mr Solver that a recursive function has the given precondition +precondHint : (a : sort 0) -> Bool -> a -> a; +precondHint _ _ a = a; + -- NOTE: for the simplicity and efficiency of MR solver, we define all -- fixed-point computations in CompM via a primitive multiFixM, defined below. -- Thus, even though fixM is really the primitive operation, we write this file @@ -2262,27 +2266,6 @@ lrtPi lrts b = (\ (lrt:LetRecType) (_:LetRecTypes) (rest:sort 0) -> lrtToType lrt -> rest) lrts; --- Apply a function the the body of a multi-arity lrtPi function -lrtPiMap : (a b : sort 0) -> (f : a -> b) -> (lrts : LetRecTypes) -> - lrtPi lrts a -> lrtPi lrts b; -lrtPiMap a b f lrts_top = - LetRecTypes#rec - (\ (lrts:LetRecTypes) -> lrtPi lrts a -> lrtPi lrts b) - (\ (x:a) -> f x) - (\ (lrt:LetRecType) (lrts:LetRecTypes) (rec:lrtPi lrts a -> lrtPi lrts b) - (f:lrtToType lrt -> lrtPi lrts a) (g:lrtToType lrt) -> - rec (f g)) - lrts_top; - --- Convert a multi-arity lrtPi that returns a pair to a pair of lrtPi functions --- that return the individual arguments -lrtPiPair : (a b:sort 0) -> (lrts : LetRecTypes) -> lrtPi lrts #(a,b) -> - #(lrtPi lrts a, lrtPi lrts b); -lrtPiPair a b lrts f = - (lrtPiMap #(a,b) a (\ (tup:#(a,b)) -> tup.(1)) lrts f, - lrtPiMap #(a,b) b (\ (tup:#(a,b)) -> tup.(2)) lrts f); - - -- Build the product type (lrtToType lrt1, ..., lrtToType lrtn) from the -- LetRecTypes list [lrt1, ..., lrtn] lrtTupleType : LetRecTypes -> sort 0; @@ -2387,6 +2370,32 @@ fixM a b f x = (\ (g: (y:a) -> CompM (b y)) -> (f g, ())) (\ (g: (y:a) -> CompM (b y)) -> g x); + +-- The following commented block allows multiFixM to be defined in terms of and +-- to reduce to letRecM, which is useful if we want to define all our automated +-- reasoning in terms of letRecM instead of multiFixM + +-- Apply a function the the body of a multi-arity lrtPi function +{- +lrtPiMap : (a b : sort 0) -> (f : a -> b) -> (lrts : LetRecTypes) -> + lrtPi lrts a -> lrtPi lrts b; +lrtPiMap a b f lrts_top = + LetRecTypes#rec + (\ (lrts:LetRecTypes) -> lrtPi lrts a -> lrtPi lrts b) + (\ (x:a) -> f x) + (\ (lrt:LetRecType) (lrts:LetRecTypes) (rec:lrtPi lrts a -> lrtPi lrts b) + (f:lrtToType lrt -> lrtPi lrts a) (g:lrtToType lrt) -> + rec (f g)) + lrts_top; + +-- Convert a multi-arity lrtPi that returns a pair to a pair of lrtPi functions +-- that return the individual arguments +lrtPiPair : (a b:sort 0) -> (lrts : LetRecTypes) -> lrtPi lrts #(a,b) -> + #(lrtPi lrts a, lrtPi lrts b); +lrtPiPair a b lrts f = + (lrtPiMap #(a,b) a (\ (tup:#(a,b)) -> tup.(1)) lrts f, + lrtPiMap #(a,b) b (\ (tup:#(a,b)) -> tup.(2)) lrts f); + -- Build a monadic function that takes in its arguments and then calls letRecM. -- That is, build a function -- @@ -2439,6 +2448,21 @@ multiFixM lrts_top F_top = rec (lrtPiPair (lrtToType lrt) (lrtTupleType lrts) lrts_top F).(2))) lrts_top F_top; +-} + +-- Construct a fixed-point for a tuple of mutually-recursive functions +-- +-- NOTE: Currently, Mr Solver actually works better with a primitive multiFixM, +-- so that's what we are going to do for now... +primitive +multiFixM : (lrts:LetRecTypes) -> lrtPi lrts (lrtTupleType lrts) -> + lrtTupleType lrts; + +-- Build a multi-argument fixed-point of type A1 -> ... -> An -> CompM B +multiArgFixM : (lrt:LetRecType) -> (lrtToType lrt -> lrtToType lrt) -> + lrtToType lrt; +multiArgFixM lrt F = + (multiFixM (LRT_Cons lrt LRT_Nil) (\ (f:lrtToType lrt) -> (F f, ()))).(1); -- Test computations diff --git a/saw-core/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs index fb7ae57fef..59c3e3276d 100644 --- a/saw-core/src/Verifier/SAW/Term/Functor.hs +++ b/saw-core/src/Verifier/SAW/Term/Functor.hs @@ -58,6 +58,7 @@ module Verifier.SAW.Term.Functor -- * Sets of free variables , BitSet, emptyBitSet, inBitSet, unionBitSets, intersectBitSets , decrBitSet, multiDecrBitSet, completeBitSet, singletonBitSet, bitSetElems + , smallestBitSetElem , looseVars, smallestFreeVar ) where @@ -485,7 +486,7 @@ bitSetElems = go 0 where go shft bs = case smallestBitSetElem bs of Nothing -> [] Just i -> - shft + i : go (shft + i + 1) (multiDecrBitSet (shft + i + 1) bs) + shft + i : go (shft + i + 1) (multiDecrBitSet (i + 1) bs) -- | Compute the free variables of a term given free variables for its immediate -- subterms diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 776abea42e..b6ac03c7f6 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -59,6 +59,7 @@ import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW import Verifier.SAW.CryptolEnv (initCryptolEnv, bindTypedTerm) import qualified Cryptol.Utils.Ident as Cryptol import Verifier.SAW.Cryptol.Monadify (defaultMonEnv) +import SAWScript.Prover.MRSolver (emptyMREnv) import qualified Argo --import qualified CryptolServer (validateServerState, ServerState(..)) @@ -219,6 +220,7 @@ initialState readFileFn = , rwDocs = mempty , rwCryptol = cenv , rwMonadify = defaultMonEnv + , rwMRSolverEnv = emptyMREnv , rwPPOpts = defaultPPOpts , rwJVMTrans = jvmTrans , rwPrimsAvail = mempty diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 9454f86a72..1765ce785b 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -1560,14 +1560,18 @@ ensureMonadicTerm sc t False -> monadifyTypedTerm sc t ensureMonadicTerm sc t = monadifyTypedTerm sc t +-- | Run Mr Solver with the given debug level to prove that the first term +-- refines the second mrSolver :: SharedContext -> Int -> TypedTerm -> TypedTerm -> TopLevel Bool mrSolver sc dlvl t1 t2 = - do m1 <- ttTerm <$> ensureMonadicTerm sc t1 + do rw <- get + m1 <- ttTerm <$> ensureMonadicTerm sc t1 m2 <- ttTerm <$> ensureMonadicTerm sc t2 - res <- liftIO $ Prover.askMRSolver sc dlvl Nothing m1 m2 + let env = rwMRSolverEnv rw + res <- liftIO $ Prover.askMRSolver sc dlvl env Nothing m1 m2 case res of - Just err -> io (putStrLn $ Prover.showMRFailure err) >> return False - Nothing -> return True + Left err -> io (putStrLn $ Prover.showMRFailure err) >> return False + Right env' -> put (rw { rwMRSolverEnv = env' }) >> return True setMonadification :: SharedContext -> String -> String -> TopLevel () setMonadification sc cry_str saw_str = diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index e53db153db..4a4b2c8f10 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -67,6 +67,7 @@ import SAWScript.Value import SAWScript.Proof (newTheoremDB) import SAWScript.Prover.Rewrite(basic_ss) import SAWScript.Prover.Exporter +import SAWScript.Prover.MRSolver (emptyMREnv) import Verifier.SAW.Conversion --import Verifier.SAW.PrettySExp import Verifier.SAW.Prim (rethrowEvalError) @@ -474,6 +475,7 @@ buildTopLevelEnv proxy opts = , rwDocs = primDocEnv primsAvail , rwCryptol = ce0 , rwMonadify = Monadify.defaultMonEnv + , rwMRSolverEnv = emptyMREnv , rwProofs = [] , rwPPOpts = SAWScript.Value.defaultPPOpts , rwJVMTrans = jvmTrans diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs index 856f94a5a7..759116dedf 100644 --- a/src/SAWScript/Prover/MRSolver.hs +++ b/src/SAWScript/Prover/MRSolver.hs @@ -9,7 +9,8 @@ Portability : non-portable (language extensions) -} module SAWScript.Prover.MRSolver - (askMRSolver, MRFailure(..), showMRFailure, isCompFunType) where + (askMRSolver, MRFailure(..), showMRFailure, isCompFunType, + MREnv(..), emptyMREnv) where import SAWScript.Prover.MRSolver.Term import SAWScript.Prover.MRSolver.Monad diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index b5e4526a3c..433a4a382f 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -73,6 +73,7 @@ data MRFailure | MalformedDefsFun Term | MalformedComp Term | NotCompFunType Term + | PrecondNotProvable FunName FunName Term -- | A local variable binding | MRFailureLocalVar LocalName MRFailure -- | Information about the context of the failure @@ -129,6 +130,10 @@ instance PrettyInCtx MRFailure where ppWithPrefix "Could not handle computation:" t prettyInCtx (NotCompFunType tp) = ppWithPrefix "Not a computation or computational function type:" tp + prettyInCtx (PrecondNotProvable f g pre) = + prettyAppList [return "Could not prove precondition for functions", + prettyInCtx f, return "and", prettyInCtx g, + return ":", prettyInCtx pre] prettyInCtx (MRFailureLocalVar x err) = local (x:) $ prettyInCtx err prettyInCtx (MRFailureCtx ctx err) = @@ -189,50 +194,39 @@ data CoIndHyp = CoIndHyp { -- | The LHS argument expressions @y1, ..., ym@ over the 'coIndHypCtx' uvars coIndHypLHS :: [Term], -- | The RHS argument expressions @y1, ..., ym@ over the 'coIndHypCtx' uvars - coIndHypRHS :: [Term] + coIndHypRHS :: [Term], + -- | The precondition for the left-hand arguments, as a closed function from + -- the left-hand arguments to @Bool@ + coIndHypPrecondLHS :: Maybe Term, + -- | The precondition for the right-hand arguments, as a closed function from + -- the left-hand arguments to @Bool@ + coIndHypPrecondRHS :: Maybe Term } deriving Show -- | Extract the @i@th argument on either the left- or right-hand side of a -- coinductive hypothesis coIndHypArg :: CoIndHyp -> Either Int Int -> Term -coIndHypArg (CoIndHyp _ _ _ args1 _) (Left i) = args1 !! i -coIndHypArg (CoIndHyp _ _ _ _ args2) (Right i) = args2 !! i +coIndHypArg hyp (Left i) = (coIndHypLHS hyp) !! i +coIndHypArg hyp (Right i) = (coIndHypRHS hyp) !! i -- | A map from pairs of function names to co-inductive hypotheses over those -- names type CoIndHyps = Map (FunName, FunName) CoIndHyp instance PrettyInCtx CoIndHyp where - prettyInCtx (CoIndHyp ctx f1 f2 args1 args2) = + prettyInCtx (CoIndHyp ctx f1 f2 args1 args2 pre1 pre2) = local (const $ map fst $ reverse ctx) $ prettyAppList [return (ppCtx ctx <> "."), + (case pre1 of + Just f -> prettyTermApp f args1 + Nothing -> return "True"), return "=>", + (case pre2 of + Just f -> prettyTermApp f args2 + Nothing -> return "True"), return "=>", prettyInCtx (FunBind f1 args1 CompFunReturn), return "|=", prettyInCtx (FunBind f2 args2 CompFunReturn)] --- | An assumption that a named function refines some specificaiton. This has --- the form --- --- > forall x1, ..., xn. F e1 ... ek |= m --- --- for some universal context @x1:T1, .., xn:Tn@, some list of argument --- expressions @ei@ over the universal @xj@ variables, and some right-hand side --- computation expression @m@. -data FunAssump = FunAssump { - -- | The uvars that were in scope when this assmption was created, in order - -- from outermost to innermost; that is, the uvars as "seen from outside their - -- scope", which is the reverse of the order of 'mrUVars', below - fassumpCtx :: [(LocalName,Term)], - -- | The argument expressions @e1, ..., en@ over the 'fassumpCtx' uvars - fassumpArgs :: [Term], - -- | The right-hand side upper bound @m@ over the 'fassumpCtx' uvars - fassumpRHS :: NormComp -} - --- | A map from function names to function refinement assumptions over that --- name -type FunAssumps = Map FunName FunAssump - -- | An assumption that something is equal to one of the constructors of a -- datatype, e.g. equal to @Left@ of some 'Term' or @Right@ of some 'Term' data DataTypeAssump = IsLeft Term | IsRight Term @@ -262,8 +256,8 @@ data MRInfo = MRInfo { -- variables, in order from innermost to outermost, i.e., where element @0@ -- corresponds to deBruijn index @0@ mriUVars :: [(LocalName,Type)], - -- | The set of function refinements to be assumed by to Mr. Solver - mriFunAssumps :: FunAssumps, + -- | The top-level Mr Solver environment + mriEnv :: MREnv, -- | The current set of co-inductive hypotheses mriCoIndHyps :: CoIndHyps, -- | The current assumptions, which are conjoined into a single Boolean term; @@ -314,9 +308,9 @@ mrSMTTimeout = mriSMTTimeout <$> ask mrUVars :: MRM [(LocalName,Type)] mrUVars = mriUVars <$> ask --- | Get the current value of 'mriFunAssumps' +-- | Get the current function assumptions mrFunAssumps :: MRM FunAssumps -mrFunAssumps = mriFunAssumps <$> ask +mrFunAssumps = mreFunAssumps <$> mriEnv <$> ask -- | Get the current value of 'mriCoIndHyps' mrCoIndHyps :: MRM CoIndHyps @@ -339,12 +333,12 @@ mrVars :: MRM MRVarMap mrVars = mrsVars <$> get -- | Run an 'MRM' computation and return a result or an error -runMRM :: SharedContext -> Maybe Integer -> Int -> FunAssumps -> +runMRM :: SharedContext -> Maybe Integer -> Int -> MREnv -> MRM a -> IO (Either MRFailure a) -runMRM sc timeout debug assumps m = +runMRM sc timeout debug env m = do true_tm <- scBool sc True let init_info = MRInfo { mriSC = sc, mriSMTTimeout = timeout, - mriDebugLevel = debug, mriFunAssumps = assumps, + mriDebugLevel = debug, mriEnv = env, mriUVars = [], mriCoIndHyps = Map.empty, mriAssumptions = true_tm, mriDataTypeAssumps = HashMap.empty } @@ -473,6 +467,7 @@ mrTypeOf :: Term -> MRM Term mrTypeOf t = -- NOTE: scTypeOf' wants the type context in the most recently bound var -- first, i.e., in the mrUVarCtxRev order + mrDebugPPPrefix 2 "mrTypeOf:" t >> mrUVarCtxRev >>= \ctx -> liftSC2 scTypeOf' (map snd ctx) t -- | Check if two 'Term's are convertible in the 'MRM' monad @@ -702,7 +697,15 @@ mrSetEVarClosed var val = -- following subtyping check will succeed var_tp <- mrSubstEVars $ mrVarType var -- FIXME: catch subtyping errors and report them as being evar failures - liftSC3 scCheckSubtype Nothing (TypedTerm val val_tp) var_tp + eith_err <- + liftSC2 (runTCM $ checkSubtype (TypedTerm val val_tp) var_tp) Nothing [] + case eith_err of + Left _ -> + error ("mrSetEVarClosed: incorrect instantiation for evar " ++ + showMRVar var ++ + "\nexpected type:\n" ++ showTerm var_tp ++ + "\nactual type:\n" ++ showTerm val_tp) + Right _ -> return () modify $ \st -> st { mrsVars = Map.alter @@ -734,15 +737,19 @@ mrTrySetAppliedEVar evar args t = -- Build a list of the input vars x1 ... xn as terms, noting that the -- first variable is the least recently bound and so has the highest -- deBruijn index - let arg_ixs = [length args - 1, length args - 2 .. 0] + let arg_ixs = reverse [0 .. length args - 1] arg_vars <- mapM (liftSC1 scLocalVar) arg_ixs - -- For free variable of t, we substitute the corresponding variable - -- xi, substituting error terms for the variables that are not free - -- (since we have nothing else to substitute for them) + -- For each free variable of t, we substitute the corresponding + -- variable xi, substituting error terms for the variables that are + -- not free (since we have nothing else to substitute for them) let var_map = zip free_vars fv_arg_ixs - let subst = flip map [0 .. length args - 1] $ \i -> - maybe (error "mrTrySetAppliedEVar: unexpected free variable") + let subst_vars = if free_vars == [] then [] else + [0 .. maximum free_vars] + let subst = flip map subst_vars $ \i -> + maybe (error + ("mrTrySetAppliedEVar: unexpected free variable " + ++ show i ++ " in term\n" ++ showTerm t)) (arg_vars !!) (lookup i var_map) body <- substTerm 0 subst t @@ -790,9 +797,9 @@ mrGetCoIndHyp :: FunName -> FunName -> MRM (Maybe CoIndHyp) mrGetCoIndHyp nm1 nm2 = Map.lookup (nm1, nm2) <$> mrCoIndHyps -- | Run a compuation under an additional co-inductive assumption -withCoIndHypRaw :: CoIndHyp -> MRM a -> MRM a -withCoIndHypRaw hyp m = - do debugPretty 1 ("withCoIndHyp" <+> ppInEmptyCtx hyp) +withCoIndHyp :: CoIndHyp -> MRM a -> MRM a +withCoIndHyp hyp m = + do debugPretty 2 ("withCoIndHyp" <+> ppInEmptyCtx hyp) hyps' <- Map.insert (coIndHypLHSFun hyp, coIndHypRHSFun hyp) hyp <$> mrCoIndHyps local (\info -> info { mriCoIndHyps = hyps' }) m @@ -806,6 +813,25 @@ instantiateCoIndHyp (CoIndHyp {..}) = rhs <- substTermLike 0 evars coIndHypRHS return (lhs, rhs) +-- | Apply the preconditions of a 'CoIndHyp' to their respective arguments, +-- yielding @Bool@ conditions, using the constant @True@ value when a +-- precondition is absent +applyCoIndHypPreconds :: CoIndHyp -> MRM (Term, Term) +applyCoIndHypPreconds hyp = + let apply_precond :: Maybe Term -> [Term] -> MRM Term + apply_precond (Just (asLambdaList -> (vars, phi))) args + | length vars == length args + -- NOTE: applying to a list of arguments == substituting the reverse + -- of that list, because the first argument corresponds to the + -- greatest deBruijn index + = substTerm 0 (reverse args) phi + apply_precond (Just _) _ = + error "applyCoIndHypPreconds: wrong number of arguments for precondition!" + apply_precond Nothing _ = liftSC1 scBool True in + do pre1 <- apply_precond (coIndHypPrecondLHS hyp) (coIndHypLHS hyp) + pre2 <- apply_precond (coIndHypPrecondRHS hyp) (coIndHypRHS hyp) + return (pre1, pre2) + -- | Look up the 'FunAssump' for a 'FunName', if there is one mrGetFunAssump :: FunName -> MRM (Maybe FunAssump) mrGetFunAssump nm = Map.lookup nm <$> mrFunAssumps @@ -820,7 +846,9 @@ withFunAssump fname args rhs m = ctx <- mrUVarCtx assumps <- mrFunAssumps let assumps' = Map.insert fname (FunAssump ctx args rhs) assumps - local (\info -> info { mriFunAssumps = assumps' }) m + local (\info -> + let env' = (mriEnv info) { mreFunAssumps = assumps' } in + info { mriEnv = env' }) m -- | Generate fresh evars for the context of a 'FunAssump' and substitute them -- into its arguments and right-hand side @@ -831,6 +859,23 @@ instantiateFunAssump fassump = rhs <- substTermLike 0 evars $ fassumpRHS fassump return (args, rhs) +-- | Get the precondition hint associated with a function name, by unfolding the +-- name and checking if its body has the form +-- +-- > \ x1 ... xn -> precondHint a phi m +-- +-- If so, return @\ x1 ... xn -> phi@ as a term with the @xi@ variables free. +-- Otherwise, return 'Nothing'. +mrGetPrecond :: FunName -> MRM (Maybe Term) +mrGetPrecond nm = + mrFunNameBody nm >>= \case + Just (asLambdaList -> + (args, + asApplyAll -> (isGlobalDef "Prelude.precondHint" -> Just (), + [_, phi, _]))) -> + Just <$> liftSC2 scLambdaList args phi + _ -> return Nothing + -- | Add an assumption of type @Bool@ to the current path condition while -- executing a sub-computation withAssumption :: Term -> MRM a -> MRM a @@ -840,6 +885,12 @@ withAssumption phi m = assumps' <- liftSC2 scAnd phi assumps local (\info -> info { mriAssumptions = assumps' }) m +-- | Remove any existing assumptions and replace them with a Boolean term +withOnlyAssumption :: Term -> MRM a -> MRM a +withOnlyAssumption phi m = + do mrDebugPPPrefix 1 "withOnlyAssumption" phi + local (\info -> info { mriAssumptions = phi }) m + -- | Add a 'DataTypeAssump' to the current context while executing a -- sub-computations withDataTypeAssump :: Term -> DataTypeAssump -> MRM a -> MRM a diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index cb49875836..04f85ece7f 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -274,7 +274,7 @@ mrProveEqSimple eqf t1 t2 = mrProveEq :: Term -> Term -> MRM Bool mrProveEq t1 t2 = do mrDebugPPPrefixSep 1 "mrProveEq" t1 "==" t2 - tp <- mrTypeOf t1 + tp <- mrTypeOf t1 >>= mrSubstEVars varmap <- mrVars cond_in_ctx <- mrProveEqH varmap tp t1 t2 res <- withTermInCtx cond_in_ctx mrProvable diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 8f25dc5d72..fbde43b184 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -114,10 +114,12 @@ C |- F e1 ... en >>= k |= F' e1' ... em' >>= k': module SAWScript.Prover.MRSolver.Solver where +import Data.Maybe import Data.Either import Data.List (findIndices, intercalate) import Control.Monad.Except -import qualified Data.Map as Map + +import Prettyprinter import Verifier.SAW.Term.Functor import Verifier.SAW.SharedTerm @@ -226,6 +228,8 @@ normComp (CompTerm t) = return $ ExistsM (Type tp) (CompFunTerm body_tm) (isGlobalDef "Prelude.forallM" -> Just (), [tp, _, body_tm]) -> return $ ForallM (Type tp) (CompFunTerm body_tm) + (isGlobalDef "Prelude.precondHint" -> Just (), [_, _, body_tm]) -> + normCompTerm body_tm (isGlobalDef "Prelude.letRecM" -> Just (), [lrts, _, defs_f, body_f]) -> do -- Bind fresh function vars for the letrec-bound functions @@ -345,31 +349,65 @@ handling the recursive ones -- * Handling Coinductive Hypotheses ---------------------------------------------------------------------- --- | Run a compuation under the additional co-inductive assumption that --- @forall x1, ..., xn. F y1 ... ym |= G z1 ... zl@, where @F@ and @G@ are --- the given 'FunName's, @y1, ..., ym@ and @z1, ..., zl@ are the given --- argument lists, and @x1, ..., xn@ is the current context of uvars. If --- while running the given computation a 'CoIndHypMismatchWidened' error is --- reached with the given names, the state is restored and the computation is --- re-run with the widened hypothesis. -withCoIndHyp :: FunName -> [Term] -> FunName -> [Term] -> MRM a -> MRM a -withCoIndHyp f1 args1 f2 args2 m = +-- | Prove the precondition of a coinductive hypothesis +proveCoIndHypPreCond :: CoIndHyp -> MRM () +proveCoIndHypPreCond hyp = + do (pre1, pre2) <- applyCoIndHypPreconds hyp + pre <- liftSC2 scAnd pre1 pre2 + success <- mrProvable pre + if success then return () else + throwMRFailure $ + PrecondNotProvable (coIndHypLHSFun hyp) (coIndHypRHSFun hyp) pre + +-- | Co-inductively prove the refinement +-- +-- > forall x1, ..., xn. preF y1 ... ym -> preG z1 ... zl -> +-- > F y1 ... ym |= G z1 ... zl@ +-- +-- where @F@ and @G@ are the given 'FunName's, @y1, ..., ym@ and @z1, ..., zl@ +-- are the given argument lists, @x1, ..., xn@ is the current context of uvars, +-- and @preF@ and @preG@ are the preconditions associated with @F@ and @G@, +-- respectively. This proof is performed by coinductively assuming the +-- refinement holds and proving the refinement with the definitions of @F@ and +-- @G@ unfolded to their bodies. Note that this refinement is performed with +-- /only/ the preconditions @preF@ and @preG@ as assumptions; all other +-- assumptions are thrown away. If while running the refinement computation a +-- 'CoIndHypMismatchWidened' error is reached with the given names, the state is +-- restored and the computation is re-run with the widened hypothesis. +mrRefinesCoInd :: FunName -> [Term] -> FunName -> [Term] -> MRM () +mrRefinesCoInd f1 args1 f2 args2 = do ctx <- mrUVarCtx - withCoIndHyp' (CoIndHyp ctx f1 f2 args1 args2) m - --- | The main loop of 'withCoIndHyp' -withCoIndHyp' :: CoIndHyp -> MRM a -> MRM a -withCoIndHyp' hyp m = - withCoIndHypRaw hyp m `catchError` \case - MRExnWiden nm1' nm2' new_vars - | coIndHypLHSFun hyp == nm1' && coIndHypRHSFun hyp == nm2' -> - -- NOTE: the state automatically gets reset here because we defined MRM - -- with ExceptT at a lower level than StateT - do mrDebugPPPrefixSep 1 "Widening recursive assumption for" nm1' "|=" nm2' - debugPrint 2 $ "Widening indices: " ++ intercalate ", " (map show new_vars) - hyp' <- generalizeCoIndHyp hyp new_vars - withCoIndHyp' hyp' m - e -> throwError e + preF1 <- mrGetPrecond f1 + preF2 <- mrGetPrecond f2 + let hyp = CoIndHyp ctx f1 f2 args1 args2 preF1 preF2 + proveCoIndHypPreCond hyp + proveCoIndHyp hyp + +-- | Prove the refinement represented by a 'CoIndHyp' coinductively. This is the +-- main loop implementing 'mrRefinesCoInd'. See that function for documentation. +proveCoIndHyp :: CoIndHyp -> MRM () +proveCoIndHyp hyp = + do let f1 = coIndHypLHSFun hyp + f2 = coIndHypRHSFun hyp + args1 = coIndHypLHS hyp + args2 = coIndHypRHS hyp + debugPretty 1 ("proveCoIndHyp" <+> ppInEmptyCtx hyp) + lhs <- fromMaybe (error "proveCoIndHyp") <$> mrFunBody f1 args1 + rhs <- fromMaybe (error "proveCoIndHyp") <$> mrFunBody f2 args2 + (pre1, pre2) <- applyCoIndHypPreconds hyp + pre <- liftSC2 scAnd pre1 pre2 + (withOnlyUVars (coIndHypCtx hyp) $ withOnlyAssumption pre $ + withCoIndHyp hyp $ mrRefines lhs rhs) `catchError` \case + MRExnWiden nm1' nm2' new_vars + | f1 == nm1' && f2 == nm2' -> + -- NOTE: the state automatically gets reset here because we defined + -- MRM with ExceptT at a lower level than StateT + do mrDebugPPPrefixSep 1 "Widening recursive assumption for" nm1' "|=" nm2' + debugPrint 2 ("Widening indices: " ++ + intercalate ", " (map show new_vars)) + hyp' <- generalizeCoIndHyp hyp new_vars + proveCoIndHyp hyp' + e -> throwError e -- | Test that a coinductive hypothesis for the given function names matches the @@ -382,6 +420,8 @@ matchCoIndHyp hyp args1 args2 = if and (eqs1 ++ eqs2) then return () else throwError $ MRExnWiden (coIndHypLHSFun hyp) (coIndHypRHSFun hyp) (map Left (findIndices not eqs1) ++ map Right (findIndices not eqs2)) + proveCoIndHypPreCond hyp + -- | Generalize some of the arguments of a coinductive hypothesis generalizeCoIndHyp :: CoIndHyp -> [Either Int Int] -> MRM CoIndHyp @@ -399,7 +439,6 @@ generalizeCoIndHyp hyp all_specs@(arg_spec:arg_specs) = do let arg' = coIndHypArg hyp spec' tp' <- mrTypeOf arg' mrDebugPPPrefixSep 2 "generalizeCoIndHyp: the type of" arg' "is" tp' - debugPrint 2 ("arg' = " ++ show arg') tps_eq <- mrConvertible arg_tp tp' args_eq <- if tps_eq then mrProveEq arg arg' else return False return $ if args_eq then Left spec' else Right spec' @@ -412,7 +451,7 @@ generalizeCoIndHyp hyp all_specs@(arg_spec:arg_specs) = -- | Add a new variable of the given type to the context of a coinductive -- hypothesis and set the specified arguments to that new variable generalizeCoIndHypArgs :: CoIndHyp -> Term -> [Either Int Int] -> MRM CoIndHyp -generalizeCoIndHypArgs (CoIndHyp ctx f1 f2 args1 args2) tp specs = +generalizeCoIndHypArgs (CoIndHyp ctx f1 f2 args1 args2 pre1 pre2) tp specs = do let set_arg i args = take i args ++ (Unshared $ LocalVar 0) : drop (i+1) args let (specs1, specs2) = partitionEithers specs @@ -421,7 +460,7 @@ generalizeCoIndHypArgs (CoIndHyp ctx f1 f2 args1 args2) tp specs = args2' <- liftTermLike 0 1 args2 let args1'' = foldr set_arg args1' specs1 args2'' = foldr set_arg args2' specs2 - return $ CoIndHyp (ctx ++ [("z",tp)]) f1 f2 args1'' args2'' + return $ CoIndHyp (ctx ++ [("z",tp)]) f1 f2 args1'' args2'' pre1 pre2 ---------------------------------------------------------------------- @@ -580,7 +619,7 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) = -- * If it is convertible to our goal, continue and prove that k1 |= k2 -- * If it can be widened with our goal, restart the current proof branch -- with the widened hypothesis (done by throwing a - -- 'CoIndHypMismatchWidened' error for 'withCoIndHyp' to catch) + -- 'CoIndHypMismatchWidened' error for 'proveCoIndHyp' to catch) -- * Otherwise, throw a 'CoIndHypMismatchFailure' error. (Just hyp, _) -> matchCoIndHyp hyp args1 args2 >> @@ -608,10 +647,9 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) = -- that f1 args1 |= f2 args2 under the assumption that f1 args1 |= f2 args2, -- and then try to prove that k1 |= k2 _ | tps_eq - , Just (f1_body, _) <- maybe_f1_body - , Just (f2_body, _) <- maybe_f2_body -> - do withCoIndHyp f1 args1 f2 args2 $ mrRefines f1_body f2_body - mrRefinesFun k1 k2 + , Just _ <- maybe_f1_body + , Just _ <- maybe_f2_body -> + mrRefinesCoInd f1 args1 f2 args2 >> mrRefinesFun k1 k2 -- If we cannot line up f1 and f2, then making progress here would require us -- to somehow split either m1 or m2 into some bind m' >>= k' such that m' is @@ -722,20 +760,22 @@ mrRefinesFun _ _ = error "mrRefinesFun: unreachable!" -- * External Entrypoints ---------------------------------------------------------------------- --- | Test two monadic, recursive terms for equivalence +-- | Test two monadic, recursive terms for refinement. On success, if the +-- left-hand term is a named function, add the refinement to the 'MREnv' +-- environment. askMRSolver :: SharedContext -> Int {- ^ The debug level -} -> + MREnv {- ^ The Mr Solver environment -} -> Maybe Integer {- ^ Timeout in milliseconds for each SMT call -} -> - Term -> Term -> IO (Maybe MRFailure) + Term -> Term -> IO (Either MRFailure MREnv) -askMRSolver sc dlvl timeout t1 t2 = +askMRSolver sc dlvl env timeout t1 t2 = do tp1 <- scTypeOf sc t1 >>= scWhnf sc tp2 <- scTypeOf sc t2 >>= scWhnf sc case asPiList tp1 of (uvar_ctx, asCompM -> Just _) -> - fmap (either Just (const Nothing)) $ - runMRM sc timeout dlvl Map.empty $ + runMRM sc timeout dlvl env $ withUVars uvar_ctx $ \vars -> do tps_are_eq <- mrConvertible tp1 tp2 if tps_are_eq then return () else @@ -744,4 +784,12 @@ askMRSolver sc dlvl timeout t1 t2 = m1 <- mrApplyAll t1 vars >>= normCompTerm m2 <- mrApplyAll t2 vars >>= normCompTerm mrRefines m1 m2 - _ -> return $ Just $ NotCompFunType tp1 + -- If t1 is a named function, add forall xs. f1 xs |= m2 to the env + case asGlobalFunName t1 of + Just f1 -> + let fassump = FunAssump { fassumpCtx = uvar_ctx, + fassumpArgs = vars, + fassumpRHS = m2 } in + return $ mrEnvAddFunAssump f1 fassump env + Nothing -> return env + _ -> return $ Left $ NotCompFunType tp1 diff --git a/src/SAWScript/Prover/MRSolver/Term.hs b/src/SAWScript/Prover/MRSolver/Term.hs index fcc88f4639..cd7a10c86d 100644 --- a/src/SAWScript/Prover/MRSolver/Term.hs +++ b/src/SAWScript/Prover/MRSolver/Term.hs @@ -37,6 +37,9 @@ import GHC.Generics import Prettyprinter +import Data.Map (Map) +import qualified Data.Map as Map + import Verifier.SAW.Term.Functor import Verifier.SAW.Term.CtxTerm (MonadTerm(..)) import Verifier.SAW.Term.Pretty @@ -56,6 +59,10 @@ newtype MRVar = MRVar { unMRVar :: ExtCns Term } deriving (Eq, Show, Ord) mrVarType :: MRVar -> Term mrVarType = ecType . unMRVar +-- | Print the string name of an 'MRVar' +showMRVar :: MRVar -> String +showMRVar = show . ppName . ecName . unMRVar + -- | A tuple or record projection of a 'Term' data TermProj = TermProjLeft | TermProjRight | TermProjRecord FieldName deriving (Eq, Ord, Show) @@ -164,6 +171,52 @@ isCompFunType sc t = scWhnf sc t >>= \case _ -> return False +---------------------------------------------------------------------- +-- * Mr Solver Environments +---------------------------------------------------------------------- + +-- | An assumption that a named function refines some specification. This has +-- the form +-- +-- > forall x1, ..., xn. F e1 ... ek |= m +-- +-- for some universal context @x1:T1, .., xn:Tn@, some list of argument +-- expressions @ei@ over the universal @xj@ variables, and some right-hand side +-- computation expression @m@. +data FunAssump = FunAssump { + -- | The uvars that were in scope when this assmption was created, in order + -- from outermost to innermost; that is, the uvars as "seen from outside their + -- scope", which is the reverse of the order of 'mrUVars', below + fassumpCtx :: [(LocalName,Term)], + -- | The argument expressions @e1, ..., en@ over the 'fassumpCtx' uvars + fassumpArgs :: [Term], + -- | The right-hand side upper bound @m@ over the 'fassumpCtx' uvars + fassumpRHS :: NormComp +} + +-- | A map from function names to function refinement assumptions over that +-- name +-- +-- FIXME: this should probably be an 'IntMap' on the 'VarIndex' of globals +type FunAssumps = Map FunName FunAssump + +-- | A global MR Solver environment +data MREnv = MREnv { + -- | The set of function refinements to be assumed by to Mr. Solver (which + -- have hopefully been proved previously...) + mreFunAssumps :: FunAssumps + } + +-- | The empty 'MREnv' +emptyMREnv :: MREnv +emptyMREnv = MREnv { mreFunAssumps = Map.empty } + +-- | Add a 'FunAssump' to a Mr Solver environment +mrEnvAddFunAssump :: FunName -> FunAssump -> MREnv -> MREnv +mrEnvAddFunAssump f fassump env = + env { mreFunAssumps = Map.insert f fassump (mreFunAssumps env) } + + ---------------------------------------------------------------------- -- * Utility Functions for Transforming 'Term's ---------------------------------------------------------------------- @@ -324,6 +377,9 @@ instance PrettyInCtx Type where instance PrettyInCtx MRVar where prettyInCtx (MRVar ec) = return $ ppName $ ecName ec +instance PrettyInCtx [Term] where + prettyInCtx xs = list <$> mapM prettyInCtx xs + instance PrettyInCtx TermProj where prettyInCtx TermProjLeft = return (pretty '.' <> "1") prettyInCtx TermProjRight = return (pretty '.' <> "2") diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index ca1eac5f59..9da3910473 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -76,6 +76,7 @@ import SAWScript.JavaPretty (prettyClass) import SAWScript.Options (Options(printOutFn),printOutLn,Verbosity) import SAWScript.Proof import SAWScript.Prover.SolverStats +import SAWScript.Prover.MRSolver.Term as MRSolver import SAWScript.Crucible.LLVM.Skeleton import SAWScript.X86 (X86Unsupported(..), X86Error(..)) @@ -431,6 +432,7 @@ data TopLevelRW = , rwDocs :: Map SS.Name String , rwCryptol :: CEnv.CryptolEnv , rwMonadify :: Monadify.MonadifyEnv + , rwMRSolverEnv :: MRSolver.MREnv , rwProofs :: [Value] {- ^ Values, generated anywhere, that represent proofs. -} , rwPPOpts :: PPOpts -- , rwCrucibleLLVMCtx :: Crucible.LLVMContext