diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index f8dcc82988..6dda297619 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -328,8 +328,43 @@ cryptolRun name (CryFunArgs (CryFunArgs' tpArgs ctrs normArgs)) retShp funcTerm toListFC getConst <$> Ctx.zipWithM getNormArg normArgs (Ctx.drop tpArgsSize normArgsSize argsCtx) - - let allTerms = tpTerms ++ argTerms + let + -- We have already checked that all numeric type constraints + -- concretely evaluate to true; thus we should be able to + -- discharge the constraints in SAWCore by reflexivity. + proveProp :: Cry.Prop -> IO SAW.Term + proveProp p = + case p of + (Cry.pIsEqual -> Just (m, _)) -> + -- Constraint `m == n` is translated as `Eq Num m n` + case Cry.tIsNum (Cry.apSubst su m) of + Just i -> + do t <- SAW.scGlobalDef sc "Cryptol.Num" + i' <- SAW.scNat sc (fromIntegral i) + x <- SAW.scGlobalApply sc "Prelude.TCNum" [i'] + SAW.scGlobalApply sc "Prelude.Refl" [t, x] + Nothing -> fail "Invalid size parameter" + (Cry.pIsNeq -> Just _) -> + -- `PNeq m n` is defined as `Eq Bool (tcEqual m n) False` + do t <- SAW.scBoolType sc + x <- SAW.scBool sc False + SAW.scGlobalApply sc "Prelude.Refl" [t, x] + (Cry.pIsGeq -> Just _) -> + -- `PGeq m n` is defined as `Eq Bool (tcLt m n) False` + do t <- SAW.scBoolType sc + x <- SAW.scBool sc False + SAW.scGlobalApply sc "Prelude.Refl" [t, x] + (Cry.pIsFin -> Just _) -> + -- `PFin n` is defined as `Eq Bool (tcFin n) True` + do t <- SAW.scBoolType sc + x <- SAW.scBool sc True + SAW.scGlobalApply sc "Prelude.Refl" [t, x] + _ -> + fail $ "Unsupported constraint form: " ++ show (pp p) + + proofTerms <- liftIO $ traverse proveProp ctrs + + let allTerms = tpTerms ++ proofTerms ++ argTerms appTerm <- liftIO (SAW.scApplyAll sc funcTerm allTerms) liftIO $ termToReg sym appTerm retShp diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore index 1e2e56c61e..7713417c5d 100644 --- a/cryptol-saw-core/saw/Cryptol.sawcore +++ b/cryptol-saw-core/saw/Cryptol.sawcore @@ -53,27 +53,37 @@ Num_rec p f1 f2 n = Num#rec1 p f1 f2 n; tcFin : Num -> Bool; tcFin n = Num#rec (\ (n:Num) -> Bool) (\ (n:Nat) -> True) False n; --- Helper function: take a Num that we expect to be finite, and extract its Nat, --- raising an error if that Num is not finite -getFinNat : (n:Num) -> Nat; -getFinNat n = - Num#rec (\ (n:Num) -> Nat) (\ (n:Nat) -> n) - (error Nat "Unexpected Fin constraint violation!") n; +-- | Cryptol `fin` constraint for finite numeric types. +PFin : Num -> Prop; +PFin n = Eq Bool (tcFin n) True; + +PFin_TCNum : (n : Nat) -> PFin (TCNum n); +PFin_TCNum n = Refl Bool True; + +PFin_TCInf : PFin TCInf -> FalseProp; +PFin_TCInf pf = sym Bool False True pf; + +FalseProp_elim : (a : sort 1) -> FalseProp -> a; +FalseProp_elim a = + Eq__rec Bool True + (\ (y : Bool) (_ : Eq Bool True y) -> + Bool#rec2 (\ (_ : Bool) -> sort 1) TrueProp a y) + TrueI + False; -- Helper function: destruct a Num that we expect to be finite -finNumRec : (p: Num -> isort 1) -> ((n:Nat) -> p (TCNum n)) -> - (n:Num) -> p n; -finNumRec p f n = - Num#rec1 p f (error (p TCInf) "Unexpected Fin constraint violation!") n; - --- Helper function: destruct two Nums that we expect to be finite -finNumRec2 : (p: Num -> Num -> isort 1) -> - ((m n:Nat) -> p (TCNum m) (TCNum n)) -> - (m n:Num) -> p m n; -finNumRec2 p f = - finNumRec - (\ (m:Num) -> (n:Num) -> p m n) - (\ (m:Nat) -> finNumRec (p (TCNum m)) (f m)); +PFinNumRec : + (n : Num) -> + PFin n -> + (p : Num -> sort 1) -> + ((n : Nat) -> p (TCNum n)) -> + p n; +PFinNumRec n fn p f = + Num#rec1 + (\ (n : Num) -> PFin n -> p n) + (\ (n : Nat) (_ : PFin (TCNum n)) -> f n) + (\ (c : PFin TCInf) -> FalseProp_elim (p TCInf) (PFin_TCInf c)) + n fn; -- Build a binary function on Nums by lifting a binary function on Nats (the -- first argument) and using additional cases for: when the first argument is a @@ -234,6 +244,98 @@ tcEqual = tcLt : Num -> Num -> Bool; tcLt = binaryNumPred ltNat (\ (x:Nat) -> True) (\ (y:Nat) -> False) True; +-- The Cryptol numeric type constraint m != n. +PNeq : Num -> Num -> Prop; +PNeq m n = Eq Bool (tcEqual m n) False; + +-- The Cryptol numeric type constraint m >= n. +PGeq : Num -> Num -> Prop; +PGeq m n = Eq Bool (tcLt m n) False; + +PGeq_0 : (n : Num) -> PGeq n (TCNum 0); +PGeq_0 = + Num#ind (\ (n : Num) -> PGeq n (TCNum 0)) + ltNat_0_right + (Refl Bool False); + +PFin_tcAdd : (m n : Num) -> PFin m -> PFin n -> PFin (tcAdd m n); +PFin_tcAdd m n pm pn = + PFinNumRec m pm (\ (m : Num) -> PFin (tcAdd m n)) + (\ (m : Nat) -> + PFinNumRec n pn (\ (n : Num) -> PFin (tcAdd (TCNum m) n)) + (\ (n : Nat) -> PFin_TCNum (addNat m n))); + +PFin_tcMul : (m n : Num) -> PFin m -> PFin n -> PFin (tcMul m n); +PFin_tcMul m n pm pn = + PFinNumRec m pm (\ (m : Num) -> PFin (tcMul m n)) + (\ (m : Nat) -> + PFinNumRec n pn (\ (n : Num) -> PFin (tcMul (TCNum m) n)) + (\ (n : Nat) -> PFin_TCNum (mulNat m n))); + +PFin_tcSub : (m n : Num) -> PFin m -> PFin (tcSub m n); +PFin_tcSub m n pm = + PFinNumRec m pm (\ (m : Num) -> PFin (tcSub m n)) + (\ (m : Nat) -> + Num#ind (\ (n : Num) -> PFin (tcSub (TCNum m) n)) + (\ (n : Nat) -> PFin_TCNum (subNat m n)) + (PFin_TCNum 0) + n); + +PFin_tcDiv : (m n : Num) -> PFin m -> PFin (tcDiv m n); +PFin_tcDiv m n pm = + PFinNumRec m pm (\ (m : Num) -> PFin (tcDiv m n)) + (\ (m : Nat) -> + Num#ind (\ (n : Num) -> PFin (tcDiv (TCNum m) n)) + (\ (n : Nat) -> PFin_TCNum (divNat m n)) + (PFin_TCNum 0) + n); + +PFin_tcCeilDiv : (m n : Num) -> PFin m -> PFin (tcCeilDiv m n); +PFin_tcCeilDiv m n pm = + PFinNumRec m pm (\ (m : Num) -> PFin (tcCeilDiv m n)) + (\ (m : Nat) -> + Num#ind (\ (n : Num) -> PFin (tcCeilDiv (TCNum m) n)) + (\ (n : Nat) -> PFin_TCNum (ceilDivNat m n)) + (PFin_TCNum 0) + n); + +PFin_downward_closed : (m n : Num) -> PGeq m n -> PFin m -> PFin n; +PFin_downward_closed m n = + Num#rec + (\ (m : Num) -> PGeq m n -> PFin m -> PFin n) + (\ (m : Nat) -> + Num#rec + (\ (n : Num) -> PGeq (TCNum m) n -> PFin (TCNum m) -> PFin n) + (\ (n : Nat) (_ : PGeq (TCNum m) (TCNum n)) (_ : PFin (TCNum m)) -> Refl Bool True) + (\ (c1 : PGeq (TCNum m) TCInf) (_ : PFin (TCNum m)) -> sym Bool True False c1) + n) + (Num#rec + (\ (n : Num) -> PGeq TCInf n -> PFin TCInf -> PFin n) + (\ (n : Nat) (_ : PGeq TCInf (TCNum n)) (_ : PFin TCInf) -> Refl Bool True) + (\ (_ : PGeq TCInf TCInf) (c2 : PFin TCInf) -> c2) + n) + m; + +-- Assuming `fin` constraints proved by the Cryptol type checker. +unsafeAssumePFin : (n : Num) -> PFin n; +unsafeAssumePFin = Num#ind PFin PFin_TCNum (unsafeAssert Bool False True); + +-- Assuming `>=` constraints proved by the Cryptol type checker. +unsafeAssumePGeq : (m n : Num) -> PGeq m n; +unsafeAssumePGeq m n = + Bool#ind (\ (x : Bool) -> Eq Bool x False) + (unsafeAssert Bool True False) + (Refl Bool False) + (tcLt m n); + +-- Assuming `!=` constraints proved by the Cryptol type checker. +unsafeAssumePNeq : (m n : Num) -> PNeq m n; +unsafeAssumePNeq m n = + Bool#ind (\ (x : Bool) -> Eq Bool x False) + (unsafeAssert Bool True False) + (Refl Bool False) + (tcEqual m n); + -------------------------------------------------------------------------------- -- Possibly infinite sequences @@ -1370,12 +1472,10 @@ ecNumber val a pa = Num#rec (\ (_ : Num) -> a) pa (pa 0) val; -- Dummy case: treat `inf as `0 (this never happens anyway) -ecFromZ : (n : Num) -> IntModNum n -> Integer; -ecFromZ n = - Num#rec (\ (n : Num) -> IntModNum n -> Integer) - fromIntMod - (\ (x : Integer) -> x) - n; +-- primitive fromZ : {n} (fin n, n >= 1) => Z n -> Integer +ecFromZ : (n : Num) -> PFin n -> PGeq n (TCNum 1) -> IntModNum n -> Integer; +ecFromZ n pn _ = + PFinNumRec n pn (\ (n : Num) -> IntModNum n -> Integer) fromIntMod; -- Ring ecFromInteger : (a : sort 0) -> PRing a -> Integer -> a; @@ -1437,37 +1537,31 @@ ecRoundToEven a pr = pr.roundToEven; -- Bitvector ops -ecLg2 : (n : Num) -> seq n Bool -> seq n Bool; -ecLg2 n = - Num#rec (\ (n:Num) -> seq n Bool -> seq n Bool) - bvLg2 - (error (Stream Bool -> Stream Bool) "ecLg2: expected finite word") - n; +-- primitive lg2 : {n} (fin n) => [n] -> [n] +ecLg2 : (n : Num) -> PFin n -> seq n Bool -> seq n Bool; +ecLg2 n pn = + PFinNumRec n pn (\ (n:Num) -> seq n Bool -> seq n Bool) bvLg2; -ecSDiv : (n : Num) -> seq n Bool -> seq n Bool -> seq n Bool; -ecSDiv n = - Num#rec (\ (n:Num) -> seq n Bool -> seq n Bool -> seq n Bool) +-- primitive (/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] +ecSDiv : (n : Num) -> PFin n -> PGeq n (TCNum 1) -> seq n Bool -> seq n Bool -> seq n Bool; +ecSDiv n pn _pgeq = + PFinNumRec n pn (\ (n:Num) -> seq n Bool -> seq n Bool -> seq n Bool) (Nat__rec (\ (n:Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool) (error (Vec 0 Bool -> Vec 0 Bool -> Vec 0 Bool) "ecSDiv: illegal 0-width word") - (\ (n':Nat) -> \ (_:Vec n' Bool -> Vec n' Bool -> Vec n' Bool) -> bvSDiv n')) - (error (Stream Bool -> Stream Bool -> Stream Bool) "ecSDiv: expected finite word") - n; + (\ (n' : Nat) -> \ (_ : Vec n' Bool -> Vec n' Bool -> Vec n' Bool) -> bvSDiv n')); -ecSMod : (n : Num) -> seq n Bool -> seq n Bool -> seq n Bool; -ecSMod n = - Num#rec (\ (n:Num) -> seq n Bool -> seq n Bool -> seq n Bool) +-- primitive (%$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] +ecSMod : (n : Num) -> PFin n -> PGeq n (TCNum 1) -> seq n Bool -> seq n Bool -> seq n Bool; +ecSMod n pn _pgeq = + PFinNumRec n pn (\ (n:Num) -> seq n Bool -> seq n Bool -> seq n Bool) (Nat__rec (\ (n:Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool) (error (Vec 0 Bool -> Vec 0 Bool -> Vec 0 Bool) "ecSMod: illegal 0-width word") - (\ (n':Nat) -> \ (_:Vec n' Bool -> Vec n' Bool -> Vec n' Bool) -> bvSRem n')) - (error (Stream Bool -> Stream Bool -> Stream Bool) "ecSMod: expected finite word") - n; + (\ (n' : Nat) -> \ (_ : Vec n' Bool -> Vec n' Bool -> Vec n' Bool) -> bvSRem n')); -toSignedInteger : (n : Num) -> seq n Bool -> Integer; -toSignedInteger n = - Num#rec (\ (n:Num) -> seq n Bool -> Integer) - sbvToInt - (error (Stream Bool -> Integer) "toSignedInteger: expected finite word") - n; +-- primitive toSignedInteger : {n} (fin n, n >= 1) => [n] -> Integer +toSignedInteger : (n : Num) -> PFin n -> PGeq n (TCNum 1) -> seq n Bool -> Integer; +toSignedInteger n pn _pgeq = + PFinNumRec n pn (\ (n : Num) -> seq n Bool -> Integer) sbvToInt; -- Eq ecEq : (a : sort 0) -> PEq a -> a -> a -> Bool; @@ -1570,52 +1664,58 @@ ecShiftR m = (streamShiftL a xs)) m; -ecSShiftR : (n : Num) -> (ix : sort 0) -> PIntegral ix -> seq n Bool -> ix -> seq n Bool; -ecSShiftR = - finNumRec - (\ (n:Num) -> (ix : sort 0) -> PIntegral ix -> seq n Bool -> ix -> seq n Bool) - (\ (n:Nat) -> - (\ (ix : sort 0) -> \ (pix : PIntegral ix) -> - natCase - (\ (w : Nat) -> Vec w Bool -> ix -> Vec w Bool) - (\ (xs : Vec 0 Bool) -> \ (_ : ix) -> xs) - (\ (w : Nat) -> \ (xs : Vec (Succ w) Bool) -> - posNegCases ix pix (Vec (Succ w) Bool) - (bvSShr w xs) - (bvShl (Succ w) xs)) - n)); - -ecRotL : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m a; -ecRotL = - finNumRec - (\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m a) - (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec m a) -> +-- primitive (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n] +ecSShiftR : + (n : Num) -> (ix : sort 0) -> + PFin n -> PGeq n (TCNum 1) -> PIntegral ix -> + seq n Bool -> ix -> seq n Bool; +ecSShiftR n ix pn _pgeq pix = + PFinNumRec n pn (\ (n : Num) -> seq n Bool -> ix -> seq n Bool) + (natCase + (\ (w : Nat) -> Vec w Bool -> ix -> Vec w Bool) + (\ (xs : Vec 0 Bool) -> \ (_ : ix) -> xs) + (\ (w : Nat) -> \ (xs : Vec (Succ w) Bool) -> + posNegCases ix pix (Vec (Succ w) Bool) + (bvSShr w xs) + (bvShl (Succ w) xs))); + +-- primitive (<<<) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a +ecRotL : + (m : Num) -> (ix a : sort 0) -> + PFin m -> PIntegral ix -> seq m a -> ix -> seq m a; +ecRotL m ix a pm = + PFinNumRec m pm + (\ (m : Num) -> PIntegral ix -> seq m a -> ix -> seq m a) + (\ (m : Nat) -> \ (pix:PIntegral ix) -> \ (xs:Vec m a) -> posNegCases ix pix (Vec m a) (rotateL m a xs) (rotateR m a xs)); -ecRotR : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m a; -ecRotR = - finNumRec - (\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m a) - (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec m a) -> +-- primitive (>>>) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a +ecRotR : + (m : Num) -> (ix a : sort 0) -> + PFin m -> PIntegral ix -> seq m a -> ix -> seq m a; +ecRotR m ix a pm = + PFinNumRec m pm + (\ (m:Num) -> PIntegral ix -> seq m a -> ix -> seq m a) + (\ (m:Nat) -> \ (pix:PIntegral ix) -> \ (xs:Vec m a) -> posNegCases ix pix (Vec m a) (rotateR m a xs) (rotateL m a xs)); -ecCat : (m n : Num) -> (a : isort 0) -> seq m a -> seq n a -> seq (tcAdd m n) a; -ecCat = - finNumRec - (\ (m:Num) -> (n:Num) -> (a:isort 0) -> seq m a -> seq n a -> - seq (tcAdd m n) a) - (\ (m:Nat) -> +-- primitive (#) : {front, back, a} (fin front) => [front]a -> [back]a -> [front + back]a +ecCat : (m n : Num) -> (a : isort 0) -> PFin m -> seq m a -> seq n a -> seq (tcAdd m n) a; +ecCat m n a pm = + PFinNumRec m pm + (\ (m : Num) -> seq m a -> seq n a -> seq (tcAdd m n) a) + (\ (m : Nat) -> Num_rec - (\ (n:Num) -> (a:isort 0) -> Vec m a -> seq n a -> - seq (tcAdd (TCNum m) n) a) + (\ (n : Num) -> Vec m a -> seq n a -> seq (tcAdd (TCNum m) n) a) -- Case for (TCNum m, TCNum n) - (\ (n:Nat) -> \ (a:isort 0) -> append m n a) + (\ (n : Nat) -> append m n a) -- Case for (TCNum m, TCInf) - (\ (a:isort 0) -> streamAppend a m)); + (streamAppend a m) + n); ecTake : (m n : Num) -> (a : isort 0) -> seq (tcAdd m n) a -> seq m a; ecTake = @@ -1637,77 +1737,59 @@ ecTake = -- The case (TCInf, TCInf) (\ (a:isort 0) -> \ (xs:Stream a) -> xs)); -ecDrop : (m n : Num) -> (a : isort 0) -> seq (tcAdd m n) a -> seq n a; -ecDrop = - finNumRec - (\ (m:Num) -> (n:Num) -> (a:isort 0) -> seq (tcAdd m n) a -> seq n a) - (\ (m:Nat) -> +ecDrop : (m n : Num) -> (a : isort 0) -> PFin m -> seq (tcAdd m n) a -> seq n a; +ecDrop m n a pm = + PFinNumRec m pm + (\ (m : Num) -> seq (tcAdd m n) a -> seq n a) + (\ (m : Nat) -> Num_rec - (\ (n:Num) -> (a:isort 0) -> seq (tcAdd (TCNum m) n) a -> seq n a) + (\ (n : Num) -> seq (tcAdd (TCNum m) n) a -> seq n a) -- The case (TCNum n, TCNum m) - (\ (n:Nat) -> \ (a:isort 0) -> \ (xs: Vec (addNat m n) a) -> drop a m n xs) + (drop a m) -- The case (TCNum m, infinity) - (\ (a:isort 0) -> \ (xs: Stream a) -> streamDrop a m xs)); + (streamDrop a m) + n); -ecJoin : (m n : Num) -> (a : isort 0) -> seq m (seq n a) -> seq (tcMul m n) a; -ecJoin m = - Num#rec1 - (\ (m:Num) -> (n:Num) -> (a:isort 0) -> seq m (seq n a) -> - seq (tcMul m n) a) - (\ (m:Nat) -> - finNumRec - (\ (n:Num) -> (a:isort 0) -> Vec m (seq n a) -> - seq (tcMul (TCNum m) n) a) - -- Case for (TCNum m, TCNum n) - (\ (n:Nat) -> \ (a:isort 0) -> join m n a)) - -- No case for (TCNum m, TCInf), shoudn't happen - (finNumRec - (\ (n:Num) -> (a:isort 0) -> Stream (seq n a) -> - seq (tcMul TCInf n) a) - -- Case for (TCInf, TCNum n) - (\ (n:Nat) -> \ (a:isort 0) -> - natCase - (\ (n':Nat) -> Stream (Vec n' a) -> +ecJoin : (m n : Num) -> (a : isort 0) -> PFin n -> seq m (seq n a) -> seq (tcMul m n) a; +ecJoin m n a pn = + PFinNumRec n pn + (\ (n : Num) -> seq m (seq n a) -> seq (tcMul m n) a) + (\ (n : Nat) -> + Num#rec1 + (\ (m : Num) -> seq m (Vec n a) -> seq (tcMul m (TCNum n)) a) + (\ (m : Nat) -> join m n a) + (natCase + (\ (n' : Nat) -> Stream (Vec n' a) -> seq (if0Nat Num n' (TCNum 0) TCInf) a) - (\ (s:Stream (Vec 0 a)) -> EmptyVec a) - (\ (n':Nat) -> \ (s:Stream (Vec (Succ n') a)) -> - streamJoin a n' s) - n)) - -- No case for (TCInf, TCInf), shouldn't happen - m; - -ecSplit : (m n : Num) -> (a : isort 0) -> seq (tcMul m n) a -> - seq m (seq n a); -ecSplit m = - Num#rec1 - (\ (m:Num) -> (n:Num) -> (a:isort 0) -> seq (tcMul m n) a -> - seq m (seq n a)) - (\ (m:Nat) -> - finNumRec - (\ (n:Num) -> (a:isort 0) -> seq (tcMul (TCNum m) n) a -> - Vec m (seq n a)) - -- Case for (TCNum m, TCNum n) - (\ (n:Nat) -> \ (a:isort 0) -> split m n a)) - -- No case for (TCNum m, TCInf), shouldn't happen - - (finNumRec - (\ (n:Num) -> (a:isort 0) -> seq (tcMul TCInf n) a -> Stream (seq n a)) - -- Case for (TCInf, TCNum n) - (\ (n:Nat) -> \ (a:isort 0) -> - natCase - (\ (n':Nat) -> - seq (if0Nat Num n' (TCNum 0) TCInf) a -> - Stream (Vec n' a)) - (streamConst (Vec 0 a)) - (\ (n':Nat) -> streamSplit a (Succ n')) - n)) - -- No case for (TCInf, TCInf), shouldn't happen - m; + (\ (s : Stream (Vec 0 a)) -> EmptyVec a) + (streamJoin a) + n) + m); + +ecSplit : + (m n : Num) -> (a : isort 0) -> PFin n -> + seq (tcMul m n) a -> seq m (seq n a); +ecSplit m n a pn = + PFinNumRec n pn + (\ (n : Num) -> seq (tcMul m n) a -> seq m (seq n a)) + (\ (n : Nat) -> + Num#rec + (\ (m : Num) -> seq (tcMul m (TCNum n)) a -> seq m (Vec n a)) + (\ (m : Nat) -> split m n a) + (natCase + (\ (n' : Nat) -> + seq (if0Nat Num n' (TCNum 0) TCInf) a -> + Stream (Vec n' a)) + (streamConst (Vec 0 a)) + (\ (n' : Nat) -> streamSplit a (Succ n')) + n) + m); -ecReverse : (n : Num) -> (a : isort 0) -> seq n a -> seq n a; -ecReverse = - finNumRec - (\ (n:Num) -> (a:isort 0) -> seq n a -> seq n a) reverse; +ecReverse : (n : Num) -> (a : isort 0) -> PFin n -> seq n a -> seq n a; +ecReverse n a pn = + PFinNumRec n pn + (\ (n : Num) -> seq n a -> seq n a) + (\ (n : Nat) -> reverse n a); ecTranspose : (m n : Num) -> (a : isort 0) -> seq m (seq n a) -> seq n (seq m a); @@ -1754,27 +1836,47 @@ ecAt n = -- (error (Nat -> a) "ecAt : negative index")) n; -ecAtBack : (n : Num) -> (a : isort 0) -> (ix : sort 0) -> PIntegral ix -> seq n a -> ix -> a; -ecAtBack n a ix pix xs = ecAt n a ix pix (ecReverse n a xs); +ecAtBack : + (n : Num) -> (a : isort 0) -> (ix : sort 0) -> + PFin n -> PIntegral ix -> seq n a -> ix -> a; +ecAtBack n a ix pn pix xs = ecAt n a ix pix (ecReverse n a pn xs); -ecFromTo : (first last : Num) -> (a : isort 0) -> PLiteral a -> - seq (tcAdd (TCNum 1) (tcSub last first)) a; -ecFromTo = - finNumRec - (\ (first:Num) -> (last:Num) -> (a : isort 0) -> PLiteral a -> - seq (tcAdd (TCNum 1) (tcSub last first)) a) - (\ (first:Nat) -> - finNumRec - (\ (last:Num) -> (a : isort 0) -> PLiteral a -> - seq (tcAdd (TCNum 1) (tcSub last (TCNum first))) a) - (\ (last:Nat) -> \ (a : isort 0) -> \ (pa : PLiteral a) -> +-- | The Cryptol primitive `fromTo`, +-- which represents the Cryptol syntax `[x .. y]`. +-- +-- primitive fromTo : {first, last, a} +-- (fin last, last >= first, Literal last a) => +-- [1 + (last - first)]a +ecFromTo : + (first last : Num) -> (a : isort 0) -> + PFin last -> + PGeq last first -> + PLiteral a -> + seq (tcAdd (TCNum 1) (tcSub last first)) a; +ecFromTo first last a plast pgeq pa = + PFinNumRec first (PFin_downward_closed last first pgeq plast) + (\ (first : Num) -> seq (tcAdd (TCNum 1) (tcSub last first)) a) + (\ (first : Nat) -> + PFinNumRec last plast + (\ (last : Num) -> seq (tcAdd (TCNum 1) (tcSub last (TCNum first))) a) + (\ (last : Nat) -> gen (addNat 1 (subNat last first)) a (\ (i : Nat) -> pa (addNat i first)))); +-- | The Cryptol primitive `fromToLessThan`, +-- which represents the Cryptol syntax `[x ..< y]`. +-- +-- primitive fromToLessThan : +-- {first, bound, a} (fin first, bound >= first, LiteralLessThan bound a) => +-- [bound - first]a ecFromToLessThan : - (first bound : Num) -> (a : isort 0) -> PLiteralLessThan a -> seq (tcSub bound first) a; -ecFromToLessThan first bound a = - finNumRec + (first bound : Num) -> (a : isort 0) -> + PFin first -> + PGeq bound first -> + PLiteralLessThan a -> + seq (tcSub bound first) a; +ecFromToLessThan first bound a pfirst _pgeq = + PFinNumRec first pfirst (\ (first:Num) -> PLiteralLessThan a -> seq (tcSub bound first) a) (\ (first:Nat) -> @@ -1786,113 +1888,153 @@ ecFromToLessThan first bound a = (\ (i : Nat) -> pa (addNat i first))) (\ (pa : PLiteralLessThan a) -> MkStream a (\ (i : Nat) -> pa (addNat i first))) - bound) - first; + bound); +-- | The Cryptol primitive `fromThenTo`, +-- which represents the Cryptol syntax `[x, y .. z]`. +-- +-- primitive fromThenTo : {first, next, last, a, len} +-- ( fin first, fin next, fin last +-- , Literal first a, Literal next a, Literal last a +-- , first != next +-- , lengthFromThenTo first next last == len) => [len]a ecFromThenTo : (first next last : Num) -> (a : isort 0) -> (len : Num) -> - PLiteral a -> PLiteral a -> PLiteral a -> seq len a; -ecFromThenTo first next _ a = - finNumRec - (\ (len:Num) -> PLiteral a -> PLiteral a -> PLiteral a -> seq len a) - (\ (len:Nat) -> \ (pa : PLiteral a) -> \ (_ : PLiteral a) -> \ (_ : PLiteral a) -> - gen len a - (\ (i : Nat) -> - pa (subNat (addNat (getFinNat first) - (mulNat i (getFinNat next))) - (mulNat i (getFinNat first))))); - + PFin first -> PFin next -> PFin last -> + PLiteral a -> PLiteral a -> PLiteral a -> + PNeq first next -> + Eq Num (tcLenFromThenTo first next last) len -> + seq len a; +ecFromThenTo first next last a len pf pn pl pa _ _ _pneq = + PFinNumRec first pf + (\ (first : Num) -> Eq Num (tcLenFromThenTo first next last) len -> seq len a) + (\ (first : Nat) -> + PFinNumRec next pn + (\ (next : Num) -> Eq Num (tcLenFromThenTo (TCNum first) next last) len -> seq len a) + (\ (next : Nat) -> + PFinNumRec last pl + (\ (last : Num) -> Eq Num (tcLenFromThenTo (TCNum first) (TCNum next) last) len -> seq len a) + (\ (last : Nat) -> \ (eq : Eq Num (TCNum (tcLenFromThenTo_Nat first next last)) len) -> + coerce (Vec (tcLenFromThenTo_Nat first next last) a) (seq len a) + (seq_cong1 (TCNum (tcLenFromThenTo_Nat first next last)) len a eq) + (gen (tcLenFromThenTo_Nat first next last) a + (\ (i : Nat) -> + pa (subNat (addNat first (mulNat i next)) (mulNat i first))))))); + +-- | The Cryptol primitive `fromToBy`, +-- which represents the Cryptol syntax `[x .. y by n]`. +-- +-- primitive fromToBy : {first, last, stride, a} +-- (fin last, fin stride, stride >= 1, last >= first, Literal last a) => +-- [1 + (last - first)/stride]a ecFromToBy : - (first last stride : Num) -> (a : isort 0) -> PLiteral a -> + (first last stride : Num) -> (a : isort 0) -> + PFin last -> PFin stride -> + PGeq stride (TCNum 1) -> PGeq last first -> + PLiteral a -> seq (tcAdd (TCNum 1) (tcDiv (tcSub last first) stride)) a; -ecFromToBy = - finNumRec - (\ (first:Num) -> (last:Num) -> (stride : Num) -> (a : isort 0) -> PLiteral a -> - seq (tcAdd (TCNum 1) (tcDiv (tcSub last first) stride)) a) - (\ (first:Nat) -> - finNumRec - (\ (last:Num) -> (stride : Num) -> (a : isort 0) -> PLiteral a -> - seq (tcAdd (TCNum 1) (tcDiv (tcSub last (TCNum first)) stride)) a) - (\ (last:Nat) -> - finNumRec - (\ (stride:Num) -> (a : isort 0) -> PLiteral a -> - seq (tcAdd (TCNum 1) (tcDiv (TCNum (subNat last first)) stride)) a) - (\ (stride:Nat) -> \ (a : isort 0) -> \ (pa : PLiteral a) -> - gen (addNat 1 (divNat (subNat last first) stride)) a - (\ (i : Nat) -> pa (addNat first (mulNat i stride)))))); - +ecFromToBy first last stride a plast pstride _ pgeqlf pa = + PFinNumRec first (PFin_downward_closed last first pgeqlf plast) + (\ (first : Num) -> seq (tcAdd (TCNum 1) (tcDiv (tcSub last first) stride)) a) + (\ (first : Nat) -> + PFinNumRec last plast + (\ (last : Num) -> seq (tcAdd (TCNum 1) (tcDiv (tcSub last (TCNum first)) stride)) a) + (\ (last : Nat) -> + PFinNumRec stride pstride + (\ (stride : Num) -> seq (tcAdd (TCNum 1) (tcDiv (TCNum (subNat last first)) stride)) a) + (\ (stride : Nat) -> + gen (addNat 1 (divNat (subNat last first) stride)) a + (\ (i : Nat) -> pa (addNat first (mulNat i stride)))))); + +-- | The Cryptol primitive `fromToByLessThan`, +-- which represents the Cryptol syntax `[x ..< y by n]`. +-- +-- primitive fromToByLessThan : {first, bound, stride, a} +-- (fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) => +-- [(bound - first)/^stride]a ecFromToByLessThan : - (first bound stride : Num) -> (a : isort 0) -> PLiteralLessThan a -> + (first bound stride : Num) -> (a : isort 0) -> + PFin first -> PFin stride -> + PGeq stride (TCNum 1) -> PGeq bound first -> + PLiteralLessThan a -> seq (tcCeilDiv (tcSub bound first) stride) a; -ecFromToByLessThan = - finNumRec - (\ (first:Num) -> (bound:Num) -> (stride:Num) -> (a : isort 0) -> PLiteralLessThan a -> - seq (tcCeilDiv (tcSub bound first) stride) a) - (\ (first:Nat) -> +ecFromToByLessThan first bound stride a pfirst pstride _ _ pa = + PFinNumRec first pfirst + (\ (first : Num) -> seq (tcCeilDiv (tcSub bound first) stride) a) + (\ (first : Nat) -> + PFinNumRec stride pstride + (\ (stride : Num) -> seq (tcCeilDiv (tcSub bound (TCNum first)) stride) a) + (\ (stride : Nat) -> Num_rec - (\ (bound:Num) -> (stride:Num) -> (a : isort 0) -> PLiteralLessThan a -> - seq (tcCeilDiv (tcSub bound (TCNum first)) stride) a) + (\ (bound : Num) -> seq (tcCeilDiv (tcSub bound (TCNum first)) (TCNum stride)) a) -- bound is finite case - (\ (bound:Nat) -> - finNumRec - (\ (stride:Num) -> (a : isort 0) -> PLiteralLessThan a -> - seq (tcCeilDiv (TCNum (subNat bound first)) stride) a) - (\ (stride:Nat) -> \ (a:isort 0) -> \ (pa:PLiteralLessThan a) -> - gen (ceilDivNat (subNat bound first) stride) a - (\ (i:Nat) -> pa (addNat first (mulNat i stride))))) + (\ (bound : Nat) -> + gen (ceilDivNat (subNat bound first) stride) a + (\ (i : Nat) -> pa (addNat first (mulNat i stride)))) -- bound is infinite case - (finNumRec - (\ (stride:Num) -> (a : isort 0) -> PLiteralLessThan a -> - seq (tcCeilDiv TCInf stride) a) - (\ (stride:Nat) -> \ (a : isort 0) -> \ (pa:PLiteralLessThan a) -> - MkStream a (\ (i:Nat) -> pa (addNat first (mulNat i stride)))))); + (MkStream a (\ (i : Nat) -> pa (addNat first (mulNat i stride)))) + bound)); +-- | The Cryptol primitive `fromToDownBy`, +-- which represents the Cryptol syntax `[x .. y down by n]`. +-- +-- primitive fromToDownBy : {first, last, stride, a} +-- (fin first, fin stride, stride >= 1, first >= last, Literal first a) => +-- [1 + (first - last)/stride]a ecFromToDownBy : - (first last stride : Num) -> (a : isort 0) -> PLiteral a -> + (first last stride : Num) -> (a : isort 0) -> + PFin first -> PFin stride -> + PGeq stride (TCNum 1) -> PGeq first last -> + PLiteral a -> seq (tcAdd (TCNum 1) (tcDiv (tcSub first last) stride)) a; -ecFromToDownBy = - finNumRec - (\ (first:Num) -> (last:Num) -> (stride:Num) -> (a : isort 0) -> PLiteral a -> - seq (tcAdd (TCNum 1) (tcDiv (tcSub first last) stride)) a) - (\ (first:Nat) -> - finNumRec - (\ (last:Num) -> (stride:Num) -> (a : isort 0) -> PLiteral a -> - seq (tcAdd (TCNum 1) (tcDiv (tcSub (TCNum first) last) stride)) a) - (\ (last:Nat) -> - finNumRec - (\ (stride:Num) -> (a : isort 0) -> PLiteral a -> - seq (tcAdd (TCNum 1) (tcDiv (TCNum (subNat first last)) stride)) a) - (\ (stride:Nat) -> \ (a : isort 0) -> \ (pa : PLiteral a) -> - gen (addNat 1 (divNat (subNat first last) stride)) a - (\ (i:Nat) -> pa (subNat first (mulNat i stride)))))); - - +ecFromToDownBy first last stride a pfirst pstride _ pgeqfl pa = + PFinNumRec last (PFin_downward_closed first last pgeqfl pfirst) + (\ (last : Num) -> seq (tcAdd (TCNum 1) (tcDiv (tcSub first last) stride)) a) + (\ (last : Nat) -> + PFinNumRec first pfirst + (\ (first : Num) -> seq (tcAdd (TCNum 1) (tcDiv (tcSub first (TCNum last)) stride)) a) + (\ (first : Nat) -> + PFinNumRec stride pstride + (\ (stride : Num) -> seq (tcAdd (TCNum 1) (tcDiv (TCNum (subNat first last)) stride)) a) + (\ (stride : Nat) -> + gen (addNat 1 (divNat (subNat first last) stride)) a + (\ (i : Nat) -> pa (subNat first (mulNat i stride)))))); + +-- | The Cryptol primitive `fromToDownByGreaterThan`, +-- which represents the Cryptol syntax `[x ..> y down by n]`. +-- +-- primitive fromToDownByGreaterThan : {first, bound, stride, a} +-- (fin first, fin stride, stride >= 1, first >= bound, Literal first a) => +-- [(first - bound)/^stride]a ecFromToDownByGreaterThan : - (first bound stride : Num) -> (a : isort 0) -> PLiteral a -> + (first bound stride : Num) -> (a : isort 0) -> + PFin first -> PFin stride -> + PGeq stride (TCNum 1) -> PGeq first bound -> + PLiteral a -> seq (tcCeilDiv (tcSub first bound) stride) a; -ecFromToDownByGreaterThan = - finNumRec - (\ (first:Num) -> (bound:Num) -> (stride:Num) -> (a : isort 0) -> PLiteral a -> - seq (tcCeilDiv (tcSub first bound) stride) a) - (\ (first:Nat) -> - finNumRec - (\ (bound:Num) -> (stride:Num) -> (a : isort 0) -> PLiteral a -> - seq (tcCeilDiv (tcSub (TCNum first) bound) stride) a) - (\ (bound:Nat) -> - finNumRec - (\ (stride:Num) -> (a : isort 0) -> PLiteral a -> - seq (tcCeilDiv (TCNum (subNat first bound)) stride) a) - (\ (stride:Nat) -> \ (a : isort 0) -> \ (pa:PLiteral a) -> - gen (ceilDivNat (subNat first bound) stride) a - (\ (i:Nat) -> pa (subNat first (mulNat i stride)))))); +ecFromToDownByGreaterThan first bound stride a pfirst pstride _ pgeqfb pa = + PFinNumRec bound (PFin_downward_closed first bound pgeqfb pfirst) + (\ (bound : Num) -> seq (tcCeilDiv (tcSub first bound) stride) a) + (\ (bound : Nat) -> + PFinNumRec first pfirst + (\ (first : Num) -> seq (tcCeilDiv (tcSub first (TCNum bound)) stride) a) + (\ (first : Nat) -> + PFinNumRec stride pstride + (\ (stride : Num) -> seq (tcCeilDiv (TCNum (subNat first bound)) stride) a) + (\ (stride : Nat) -> + gen (ceilDivNat (subNat first bound) stride) a + (\ (i : Nat) -> pa (subNat first (mulNat i stride)))))); -- Infinite word sequences +-- +-- primitive infFrom : {a} (Integral a) => a -> [inf]a ecInfFrom : (a : sort 0) -> PIntegral a -> a -> seq TCInf a; ecInfFrom a pa x = MkStream a (\ (i : Nat) -> pa.integralRing.add x (pa.integralRing.int (natToInt i))); +-- primitive infFromThen : {a} (Integral a) => a -> a -> [inf]a ecInfFromThen : (a : sort 0) -> PIntegral a -> a -> a -> seq TCInf a; ecInfFromThen a pa x y = MkStream a (\ (i : Nat) -> @@ -1900,9 +2042,9 @@ ecInfFromThen a pa x y = -- Run-time error -ecError : (a : isort 0) -> (len : Num) -> seq len (Vec 8 Bool) -> a; -ecError a = - finNumRec +ecError : (a : isort 0) -> (len : Num) -> PFin len -> seq len (Vec 8 Bool) -> a; +ecError a len plen = + PFinNumRec len plen (\ (len:Num) -> seq len (Vec 8 Bool) -> a) (\ (len:Nat) (msg:Vec len (Vec 8 Bool)) -> error a (appendString "encountered call to the Cryptol 'error' function: " @@ -1914,8 +2056,8 @@ ecRandom : (a : isort 0) -> Vec 256 Bool -> a; ecRandom a _ = error a "Cryptol.random"; -- Trace function; simply return the final argument -ecTrace : (n : Num) -> (a b : sort 0) -> seq n (Vec 8 Bool) -> a -> b -> b; -ecTrace _ _ _ _ _ x = x; +ecTrace : (n : Num) -> (a b : sort 0) -> PFin n -> seq n (Vec 8 Bool) -> a -> b -> b; +ecTrace _ _ _ _ _ _ x = x; -------------------------------------------------------------------------------- @@ -1937,17 +2079,19 @@ ecParmap a b n pb = n; -- foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a -ecFoldl : (n : Num) -> (a : sort 0) -> (b : isort 0) -> (a -> b -> a) -> a -> seq n b -> a; -ecFoldl n a b f z = - Num#rec (\ (n : Num) -> seq n b -> a) - (\ (n : Nat) -> \ (xs : Vec n b) -> foldl b a n f z xs) - (\ (xs : Stream b) -> error a "Unexpected infinite stream in foldl" ) - n; +ecFoldl : + (n : Num) -> (a : sort 0) -> (b : isort 0) -> + PFin n -> (a -> b -> a) -> a -> seq n b -> a; +ecFoldl n a b pn f z = + PFinNumRec n pn + (\ (n : Num) -> seq n b -> a) + (\ (n : Nat) -> foldl b a n f z); -- foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a ecFoldlPrime : - (n : Num) -> (a : sort 0) -> (b : isort 0) -> PEq a -> (a -> b -> a) -> a -> seq n b -> a; -ecFoldlPrime n a b pa = ecFoldl n a b; + (n : Num) -> (a : sort 0) -> (b : isort 0) -> + PFin n -> PEq a -> (a -> b -> a) -> a -> seq n b -> a; +ecFoldlPrime n a b pn pa = ecFoldl n a b pn; -- scanl : {n, a, b} (a -> b -> a) -> a -> [n]b -> [1+n]a ecScanl : @@ -2097,84 +2241,133 @@ ecUpdate n = n; -ecUpdateEnd : (n : Num) -> (a:isort 0) -> (ix: sort 0) -> PIntegral ix -> seq n a -> ix -> a -> seq n a; -ecUpdateEnd = - finNumRec - (\ (n:Num) -> (a:isort 0) -> (ix: sort 0) -> PIntegral ix -> seq n a -> ix -> a -> seq n a) - (\ (n:Nat) -> \ (a:isort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec n a) -> +ecUpdateEnd : + (n : Num) -> (a : isort 0) -> (ix : sort 0) -> + PFin n -> PIntegral ix -> seq n a -> ix -> a -> seq n a; +ecUpdateEnd n a ix pn pix = + PFinNumRec n pn + (\ (n : Num) -> seq n a -> ix -> a -> seq n a) + (\ (n : Nat) -> \ (xs : Vec n a) -> posNegCases ix pix (a -> Vec n a) (\ (i:Nat) -> upd n a xs (subNat (subNat n 1) i)) (\ (_:Nat) -> \ (_:a) -> xs)); - -- (error (Nat -> a -> Vec n a) "ecUpdateEnd: negative index")) - -- No TCInf case, shouldn't happen - -- Bitvector truncation -ecTrunc : (m n : Num) -> seq (tcAdd m n) Bool -> seq n Bool; -ecTrunc = - finNumRec2 - (\ (m:Num) -> \ (n:Num) -> seq (tcAdd m n) Bool -> seq n Bool) - bvTrunc; +-- primitive trunc : {m, n} (fin m, fin n) => [m+n] -> [n] +ecTrunc : (m n : Num) -> PFin m -> PFin n -> seq (tcAdd m n) Bool -> seq n Bool; +ecTrunc m n pm pn = + PFinNumRec m pm + (\ (m : Num) -> seq (tcAdd m n) Bool -> seq n Bool) + (\ (m : Nat) -> + PFinNumRec n pn + (\ (n : Num) -> seq (tcAdd (TCNum m) n) Bool -> seq n Bool) + (\ (n : Nat) -> bvTrunc m n)); -- Zero extension -ecUExt : (m n : Num) -> seq n Bool -> seq (tcAdd m n) Bool; -ecUExt = - finNumRec2 (\ (m:Num) -> \ (n:Num) -> seq n Bool -> seq (tcAdd m n) Bool) - bvUExt; - -ecSExt : (m n : Num) -> seq n Bool -> seq (tcAdd m n) Bool; -ecSExt = - finNumRec2 - (\ (m n : Num) -> seq n Bool -> seq (tcAdd m n) Bool) - (\ (m n : Nat) -> - natCase - (\ (n' : Nat) -> Vec n' Bool -> Vec (addNat m n') Bool) - (\ (_ : Vec 0 Bool) -> bvNat (addNat m 0) 0) - (bvSExt m) - n); +-- primitive uext : {m, n} (fin m, fin n) => [n] -> [m+n] +ecUExt : (m n : Num) -> PFin m -> PFin n -> seq n Bool -> seq (tcAdd m n) Bool; +ecUExt m n pm pn = + PFinNumRec m pm + (\ (m : Num) -> seq n Bool -> seq (tcAdd m n) Bool) + (\ (m : Nat) -> + PFinNumRec n pn + (\ (n : Num) -> seq n Bool -> seq (tcAdd (TCNum m) n) Bool) + (\ (n : Nat) -> bvUExt m n)); + +-- primitive sext : {m, n} (fin m, fin n, n >= 1) => [n] -> [m+n] +ecSExt : + (m n : Num) -> PFin m -> PFin n -> PGeq n (TCNum 1) -> + seq n Bool -> seq (tcAdd m n) Bool; +ecSExt m n pm pn _pgeq = + PFinNumRec m pm + (\ (m : Num) -> seq n Bool -> seq (tcAdd m n) Bool) + (\ (m : Nat) -> + PFinNumRec n pn + (\ (n : Num) -> seq n Bool -> seq (tcAdd (TCNum m) n) Bool) + (\ (n : Nat) -> + natCase + (\ (n' : Nat) -> Vec n' Bool -> Vec (addNat m n') Bool) + (\ (_ : Vec 0 Bool) -> bvNat (addNat m 0) 0) + (bvSExt m) + n)); -- Signed greater-than -ecSgt : (n : Num) -> seq n Bool -> seq n Bool -> Bool; -ecSgt = - finNumRec (\ (n : Num) -> seq n Bool -> seq n Bool -> Bool) bvsgt; +-- primitive sgt : {n} (fin n) => [n] -> [n] -> Bit +ecSgt : (n : Num) -> PFin n -> seq n Bool -> seq n Bool -> Bool; +ecSgt n pn = + PFinNumRec n pn (\ (n : Num) -> seq n Bool -> seq n Bool -> Bool) bvsgt; -- Signed greater-or-equal -ecSge : (n : Num) -> seq n Bool -> seq n Bool -> Bool; -ecSge = - finNumRec (\ (n : Num) -> seq n Bool -> seq n Bool -> Bool) bvsge; +-- primitive sge : {n} (fin n) => [n] -> [n] -> Bit +ecSge : (n : Num) -> PFin n -> seq n Bool -> seq n Bool -> Bool; +ecSge n pn = + PFinNumRec n pn (\ (n : Num) -> seq n Bool -> seq n Bool -> Bool) bvsge; -- Signed less-than -ecSlt : (n : Num) -> seq n Bool -> seq n Bool -> Bool; -ecSlt = - finNumRec (\ (n : Num) -> seq n Bool -> seq n Bool -> Bool) bvslt; +-- primitive slt : {n} (fin n) => [n] -> [n] -> Bit +ecSlt : (n : Num) -> PFin n -> seq n Bool -> seq n Bool -> Bool; +ecSlt n pn = + PFinNumRec n pn (\ (n : Num) -> seq n Bool -> seq n Bool -> Bool) bvslt; -- Signed less-or-equal -ecSle : (n : Num) -> seq n Bool -> seq n Bool -> Bool; -ecSle = - finNumRec (\ (n : Num) -> seq n Bool -> seq n Bool -> Bool) bvsle; +-- primitive sle : {n} (fin n) => [n] -> [n] -> Bit +ecSle : (n : Num) -> PFin n -> seq n Bool -> seq n Bool -> Bool; +ecSle n pn = + PFinNumRec n pn (\ (n : Num) -> seq n Bool -> seq n Bool -> Bool) bvsle; +-------------------------------------------------------------------------------- -- Array operations + +-- primitive arrayConstant : {a, b} b -> (Array a b) ecArrayConstant : (a b : sort 0) -> b -> Array a b; ecArrayConstant = arrayConstant; +-- primitive arrayLookup : {a, b} (Array a b) -> a -> b ecArrayLookup : (a b : sort 0) -> (Array a b) -> a -> b; ecArrayLookup = arrayLookup; +-- primitive arrayUpdate : {a, b} (Array a b) -> a -> b -> (Array a b) ecArrayUpdate : (a b : sort 0) -> (Array a b) -> a -> b -> (Array a b); ecArrayUpdate = arrayUpdate; -ecArrayCopy : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Array (seq n Bool) a; -ecArrayCopy = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Array (seq n Bool) a) arrayCopy; - -ecArrayEq : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> Array (seq n Bool) a -> Bool; -ecArrayEq = finNumRec (\ (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> Array (seq n Bool) a -> Bool) (\ (n:Nat) -> arrayEq (Vec n Bool)); - -ecArraySet : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> a -> seq n Bool -> Array (seq n Bool) a; -ecArraySet = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> a -> seq n Bool -> Array (seq n Bool) a) arraySet; - -ecArrayRangeEq : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Bool; -ecArrayRangeEq = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Bool) arrayRangeEq; +-- primitive arrayCopy : {n, a} (fin n) => Array [n] a -> [n] -> Array [n] a -> [n] -> [n] -> Array [n] a +ecArrayCopy : + (n : Num) -> (a : sort 0) -> PFin n -> + Array (seq n Bool) a -> seq n Bool -> + Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Array (seq n Bool) a; +ecArrayCopy n a pn = + PFinNumRec n pn + (\ (n : Num) -> + Array (seq n Bool) a -> seq n Bool -> + Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Array (seq n Bool) a) + (\ (n : Nat) -> arrayCopy n a); + +-- primitive arrayEq : {n, a} Array [n] a -> Array [n] a -> Bool +ecArrayEq : + (n : Num) -> (a : sort 0) -> + Array (seq n Bool) a -> Array (seq n Bool) a -> Bool; +ecArrayEq n a = arrayEq (seq n Bool) a; + +-- primitive arraySet : {n, a} (fin n) => (Array [n] a) -> [n] -> a -> [n] -> (Array [n] a) +ecArraySet : + (n : Num) -> (a : sort 0) -> PFin n -> + Array (seq n Bool) a -> seq n Bool -> a -> seq n Bool -> Array (seq n Bool) a; +ecArraySet n a pn = + PFinNumRec n pn + (\ (n : Num) -> + Array (seq n Bool) a -> seq n Bool -> a -> seq n Bool -> Array (seq n Bool) a) + (\ (n : Nat) -> arraySet n a); + +-- primitive arrayRangeEqual : {n, a} (fin n) => (Array [n] a) -> [n] -> (Array [n] a) -> [n] -> [n] -> Bool +ecArrayRangeEq : + (n : Num) -> (a : sort 0) -> PFin n -> + Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Bool; +ecArrayRangeEq n a pn = + PFinNumRec n pn + (\ (n : Num) -> + Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Bool) + (\ (n : Nat) -> arrayRangeEq n a); -------------------------------------------------------------------------------- -- GF2 Polynomial Primitives @@ -2189,46 +2382,50 @@ addNat_1 = (eqNatAddS 1 n) (eqNatSucc (addNat 1 n) (Succ n) ih) ); +-- primitive pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v] ecPmult : - (u v : Num) -> + (u v : Num) -> PFin u -> PFin v -> seq (tcAdd (TCNum 1) u) Bool -> seq (tcAdd (TCNum 1) v) Bool -> seq (tcAdd (TCNum 1) (tcAdd u v)) Bool; -ecPmult = - finNumRec2 - (\ (u v : Num) -> - seq (tcAdd (TCNum 1) u) Bool -> - seq (tcAdd (TCNum 1) v) Bool -> - seq (tcAdd (TCNum 1) (tcAdd u v)) Bool - ) - (\ (u v : Nat) -> - \ (x : Vec (addNat 1 u) Bool) -> - \ (y : Vec (addNat 1 v) Bool) -> - coerceVec Bool (Succ (addNat u v)) (addNat 1 (addNat u v)) - (sym Nat (addNat 1 (addNat u v)) (Succ (addNat u v)) (addNat_1 (addNat u v))) - (polyMul u v - (coerceVec Bool (addNat 1 u) (Succ u) (addNat_1 u) x) - (coerceVec Bool (addNat 1 v) (Succ v) (addNat_1 v) y) - ) - ); - +ecPmult u v pu pv = + PFinNumRec u pu + (\ (u : Num) -> + seq (tcAdd (TCNum 1) u) Bool -> + seq (tcAdd (TCNum 1) v) Bool -> + seq (tcAdd (TCNum 1) (tcAdd u v)) Bool) + (\ (u : Nat) -> + PFinNumRec v pv + (\ (v : Num) -> + seq (tcAdd (TCNum 1) (TCNum u)) Bool -> + seq (tcAdd (TCNum 1) v) Bool -> + seq (tcAdd (TCNum 1) (tcAdd (TCNum u) v)) Bool) + (\ (v : Nat) -> + \ (x : Vec (addNat 1 u) Bool) -> + \ (y : Vec (addNat 1 v) Bool) -> + coerceVec Bool (Succ (addNat u v)) (addNat 1 (addNat u v)) + (sym Nat (addNat 1 (addNat u v)) (Succ (addNat u v)) (addNat_1 (addNat u v))) + (polyMul u v + (coerceVec Bool (addNat 1 u) (Succ u) (addNat_1 u) x) + (coerceVec Bool (addNat 1 v) (Succ v) (addNat_1 v) y) + ))); + +-- primitive pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v] ecPmod : - (u v : Num) -> + (u v : Num) -> PFin u -> PFin v -> seq u Bool -> seq (tcAdd (TCNum 1) v) Bool -> seq v Bool; -ecPmod = - finNumRec2 - (\ (u v : Num) -> - seq u Bool -> - seq (tcAdd (TCNum 1) v) Bool -> - seq v Bool - ) - (\ (u v : Nat) -> - \ (x : Vec u Bool) -> - \ (y : Vec (addNat 1 v) Bool) -> - polyMod u v x (coerceVec Bool (addNat 1 v) (Succ v) (addNat_1 v) y) - ); +ecPmod u v pu pv = + PFinNumRec u pu + (\ (u : Num) -> seq u Bool -> seq (tcAdd (TCNum 1) v) Bool -> seq v Bool) + (\ (u : Nat) -> + PFinNumRec v pv + (\ (v : Num) -> Vec u Bool -> seq (tcAdd (TCNum 1) v) Bool -> seq v Bool) + (\ (v : Nat) -> + \ (x : Vec u Bool) -> + \ (y : Vec (addNat 1 v) Bool) -> + polyMod u v x (coerceVec Bool (addNat 1 v) (Succ v) (addNat_1 v) y))); -------------------------------------------------------------------------------- -- Suite-B Primitives @@ -2253,28 +2450,32 @@ AESInvMixColumns : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool); AESInvMixColumns x = error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESInvMixColumns"; +-- primitive AESKeyExpand : {k} (fin k, k >= 4, 8 >= k) => [k][32] -> [4*(k+7)][32] AESKeyExpand : (k : Num) -> + PFin k -> + PGeq k (TCNum 4) -> + PGeq (TCNum 8) k -> seq k (Vec 32 Bool) -> seq (tcMul (TCNum 4) (tcAdd (TCNum 7) k)) (Vec 32 Bool); -AESKeyExpand k x = +AESKeyExpand k _ _ _ x = error (seq (tcMul (TCNum 4) (tcAdd (TCNum 7) k)) (Vec 32 Bool)) "Unimplemented: AESKeyExpand"; -processSHA2_224 : (n : Num) -> seq n (Vec 16 (Vec 32 Bool)) -> Vec 7 (Vec 32 Bool); -processSHA2_224 n x = +processSHA2_224 : (n : Num) -> PFin n -> seq n (Vec 16 (Vec 32 Bool)) -> Vec 7 (Vec 32 Bool); +processSHA2_224 n _ x = error (Vec 7 (Vec 32 Bool)) "Unimplemented: processSHA2_224"; -processSHA2_256 : (n : Num) -> seq n (Vec 16 (Vec 32 Bool)) -> Vec 8 (Vec 32 Bool); -processSHA2_256 n x = +processSHA2_256 : (n : Num) -> PFin n -> seq n (Vec 16 (Vec 32 Bool)) -> Vec 8 (Vec 32 Bool); +processSHA2_256 n _ x = error (Vec 8 (Vec 32 Bool)) "Unimplemented: processSHA2_256"; -processSHA2_384 : (n : Num) -> seq n (Vec 16 (Vec 64 Bool)) -> Vec 6 (Vec 64 Bool); -processSHA2_384 n x = +processSHA2_384 : (n : Num) -> PFin n -> seq n (Vec 16 (Vec 64 Bool)) -> Vec 6 (Vec 64 Bool); +processSHA2_384 n _ x = error (Vec 6 (Vec 64 Bool)) "Unimplemented: processSHA2_384"; -processSHA2_512 : (n : Num) -> seq n (Vec 16 (Vec 64 Bool)) -> Vec 8 (Vec 64 Bool); -processSHA2_512 n x = +processSHA2_512 : (n : Num) -> PFin n -> seq n (Vec 16 (Vec 64 Bool)) -> Vec 8 (Vec 64 Bool); +processSHA2_512 n _ x = error (Vec 8 (Vec 64 Bool)) "Unimplemented: processSHA2_512"; -------------------------------------------------------------------------------- @@ -2284,24 +2485,28 @@ ProjectivePoint : Num -> sort 0; ProjectivePoint p = #{x : IntModNum p, y : IntModNum p, z : IntModNum p}; ec_double : - (p : Num) -> ProjectivePoint p -> ProjectivePoint p; -ec_double p x = + (p : Num) -> PGeq p (TCNum 4) -> + ProjectivePoint p -> ProjectivePoint p; +ec_double p _ x = error (ProjectivePoint p) "Unimplemented: ec_double"; ec_add_nonzero : - (p : Num) -> ProjectivePoint p -> ProjectivePoint p -> ProjectivePoint p; -ec_add_nonzero p x y = + (p : Num) -> PGeq p (TCNum 4) -> + ProjectivePoint p -> ProjectivePoint p -> ProjectivePoint p; +ec_add_nonzero p _ x y = error (ProjectivePoint p) "Unimplemented: ec_add_nonzero"; ec_mult : - (p : Num) -> IntModNum p -> ProjectivePoint p -> ProjectivePoint p; -ec_mult p x y = + (p : Num) -> PGeq p (TCNum 4) -> + IntModNum p -> ProjectivePoint p -> ProjectivePoint p; +ec_mult p _ x y = error (ProjectivePoint p) "Unimplemented: ec_mult"; ec_twin_mult : - (p : Num) -> IntModNum p -> + (p : Num) -> PGeq p (TCNum 4) -> + IntModNum p -> ProjectivePoint p -> ProjectivePoint p -> ProjectivePoint p; -ec_twin_mult p x y z = +ec_twin_mult p _ x y z = error (ProjectivePoint p) "Unimplemented: ec_twin_mult"; -------------------------------------------------------------------------------- diff --git a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs index 9dbdbdea87..6408ca0cd9 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs @@ -238,10 +238,12 @@ importTFun sc tf = importPC :: SharedContext -> C.PC -> IO Term importPC sc pc = case pc of - C.PEqual -> panic "importPC" ["found PEqual"] - C.PNeq -> panic "importPC" ["found PNeq"] - C.PGeq -> panic "importPC" ["found PGeq"] - C.PFin -> panic "importPC" ["found PFin"] + C.PEqual -> do eq <- scGlobalDef sc "Prelude.Eq" + num <- scGlobalDef sc "Cryptol.Num" + scApply sc eq num + C.PNeq -> scGlobalDef sc "Cryptol.PNeq" + C.PGeq -> scGlobalDef sc "Cryptol.PGeq" + C.PFin -> scGlobalDef sc "Cryptol.PFin" C.PHas _ -> panic "importPC" ["found PHas"] C.PPrime -> panic "importPC" ["found PPrime"] C.PNotPrime -> panic "importPC" ["found PNotPrime"] @@ -258,7 +260,7 @@ importPC sc pc = C.PLiteralLessThan -> scGlobalDef sc "Cryptol.PLiteralLessThan" C.PFLiteral -> scGlobalDef sc "Cryptol.PFLiteral" C.PAnd -> panic "importPC" ["found PAnd"] - C.PTrue -> panic "importPC" ["found PTrue"] + C.PTrue -> scGlobalDef sc "Prelude.TrueProp" C.PValidFloat -> panic "importPC" ["found PValidFloat"] -- | Import a Cryptol `C.Type` as a SAWCore term. @@ -369,10 +371,10 @@ importType sc ty = do isErasedPC :: C.PC -> Bool isErasedPC pc = case pc of - C.PEqual -> True - C.PNeq -> True - C.PGeq -> True - C.PFin -> True + C.PEqual -> False + C.PNeq -> False + C.PGeq -> False + C.PFin -> False C.PPrime -> True C.PNotPrime -> True C.PHas _ -> True @@ -390,7 +392,7 @@ isErasedPC pc = C.PFLiteral -> False C.PValidFloat -> True C.PAnd -> True - C.PTrue -> True + C.PTrue -> False isErasedTCon :: C.TCon -> Bool isErasedTCon tcon = @@ -872,6 +874,88 @@ provePropRec sc prop0 prop = do p' <- importType sc p scGlobalApply sc "Cryptol.PFLiteralFloat" [e', p'] + -- instance fin + (C.pIsFin -> Just (C.tIsNum -> Just n)) + -> do a <- scNat sc (fromInteger n) + scGlobalApply sc "Cryptol.PFin_TCNum" [a] + -- instance (fin m, fin n) => fin (m + n) + (C.pIsFin -> Just (C.tIsBinFun C.TCAdd -> Just (m, n))) + -> do a <- importType sc m + b <- importType sc n + pa <- provePropRec sc prop0 (pFin m) + pb <- provePropRec sc prop0 (pFin n) + scGlobalApply sc "Cryptol.PFin_tcAdd" [a, b, pa, pb] + -- instance (fin m, fin n) => fin (m * n) + -- NOTE: It is possible to have `fin (m * n)` without both + -- `fin m` and `fin n` if one of the multiplicands is 0. Yet + -- it should be safe to apply this rule in practice, because + -- Cryptol would have simplified `m * n` to 0 if one of them + -- was 0. + (C.pIsFin -> Just (C.tIsBinFun C.TCMul -> Just (m, n))) + -> do a <- importType sc m + b <- importType sc n + pa <- provePropRec sc prop0 (pFin m) + pb <- provePropRec sc prop0 (pFin n) + scGlobalApply sc "Cryptol.PFin_tcMul" [a, b, pa, pb] + -- instance fin m => fin (m - n) + (C.pIsFin -> Just (C.tIsBinFun C.TCSub -> Just (m, n))) + -> do a <- importType sc m + b <- importType sc n + pa <- provePropRec sc prop0 (pFin m) + scGlobalApply sc "Cryptol.PFin_tcSub" [a, b, pa] + -- instance fin m => fin (m / n) + (C.pIsFin -> Just (C.tIsBinFun C.TCDiv -> Just (m, n))) + -> do a <- importType sc m + b <- importType sc n + pa <- provePropRec sc prop0 (pFin m) + scGlobalApply sc "Cryptol.PFin_tcDiv" [a, b, pa] + -- instance fin m => fin (m /^ n) + (C.pIsFin -> Just (C.tIsBinFun C.TCCeilDiv -> Just (m, n))) + -> do a <- importType sc m + b <- importType sc n + pa <- provePropRec sc prop0 (pFin m) + scGlobalApply sc "Cryptol.PFin_tcCeilDiv" [a, b, pa] + -- instance fin n (fallback case, trusting Cryptol type checker) + (C.pIsFin -> Just n) + -> do n' <- importType sc n + scGlobalApply sc "Cryptol.unsafeAssumePFin" [n'] + + -- instance (n == n) + (C.pIsEqual -> Just (m, n)) + -> do num <- scGlobalDef sc "Cryptol.Num" + m' <- importType sc m + n' <- importType sc n + conv <- scConvertible sc m' n' + if conv + then scGlobalApply sc "Prelude.Refl" [num, m'] + else scGlobalApply sc "Prelude.unsafeAssert" [num, m', n'] + -- instance (n >= 0) + (C.pIsGeq -> Just (n, C.tIsNum -> Just 0)) + -> do n' <- importType sc n + scGlobalApply sc "Cryptol.PGeq_0" [n'] + -- instance (m >= n) (fallback case, trusting Cryptol type checker) + (C.pIsGeq -> Just (m, n)) + -> do m' <- importType sc m + n' <- importType sc n + scGlobalApply sc "Cryptol.unsafeAssumePGeq" [m', n'] + + -- instance ( != ) + (C.pIsNeq -> Just (C.tIsNum -> Just m, C.tIsNum -> Just n)) | m /= n + -> do bool <- scBoolType sc + false <- scBool sc False + scGlobalApply sc "Prelude.Refl" [bool, false] + -- instance (m != n) (fallback case, trusting Cryptol type checker) + (C.pIsNeq -> Just (m, n)) + -> do m' <- importType sc m + n' <- importType sc n + scGlobalApply sc "Cryptol.unsafeAssumePNeq" [m', n'] + + -- instance True + (C.pIsTrue -> True) + -> do ty <- scGlobalDef sc "Prelude.Bool" + t <- scGlobalDef sc "Prelude.True" + scGlobalApply sc "Prelude.Refl" [ty, t] + _ -> do let prop0' = " " <> CryPP.pp prop0 prop' = " " <> CryPP.pp prop @@ -886,6 +970,10 @@ provePropRec sc prop0 prop = do ] ++ env' panic "proveProp" message where + -- | NOTE: C.pFin does extra simplifications we don't want. + pFin :: C.Type -> C.Prop + pFin ty = C.TCon (C.PC C.PFin) [ty] + -- Construct a record value. This is used to import Zero instances for -- record types and newtypes. buildRecord :: (C.Type -> C.Type) -> C.RecordMap C.Ident C.Type -> IO Term @@ -1177,9 +1265,9 @@ prelPrims = -- -- Enumerations , ("fromTo", flip scGlobalDef "Cryptol.ecFromTo") - -- fromTo : {first, last, bits, a} - -- ( fin last, fin bits, last >== first, - -- Literal first a, Literal last a) + -- fromTo : {first, last, a} + -- ( fin last, last >= first, + -- Literal last a) -- => [1 + (last - first)]a , ("fromToLessThan", flip scGlobalDef "Cryptol.ecFromToLessThan") -- fromToLessThan : {first, bound, a} @@ -1221,7 +1309,7 @@ prelPrims = , ("scanl", flip scGlobalDef "Cryptol.ecScanl") -- {n, a, b} (a -> b -> a) -> a -> [n]b -> [1+n]a , ("error", flip scGlobalDef "Cryptol.ecError") -- {at,len} (fin len) => [len][8] -> at -- Run-time error , ("random", flip scGlobalDef "Cryptol.ecRandom") -- {a} => [32] -> a -- Random values - , ("trace", flip scGlobalDef "Cryptol.ecTrace") -- {n,a,b} [n][8] -> a -> b -> b + , ("trace", flip scGlobalDef "Cryptol.ecTrace") -- {n,a,b} (fin n) => [n][8] -> a -> b -> b ] arrayPrims :: Map C.PrimIdent (SharedContext -> IO Term) diff --git a/intTests/test_cryptol_fromto/test.saw b/intTests/test_cryptol_fromto/test.saw new file mode 100644 index 0000000000..039237b0fa --- /dev/null +++ b/intTests/test_cryptol_fromto/test.saw @@ -0,0 +1,9 @@ +// Test Cryptol translation of all enumerated-sequence primitives. +print {{ [3 .. 10] : [_]Integer }}; +print {{ [3 ..< 10] : [_]Integer }}; +print {{ [3, 5 .. 19] : [_]Integer }}; +print {{ [99, 89 .. 9] : [_]Integer }}; +print {{ [3 .. 13 by 2] : [_]Integer }}; +print {{ [3 ..< 20 by 2] : [_]Integer }}; +print {{ [21 .. 9 down by 3] : [_]Integer }}; +print {{ [21 ..> 10 down by 3] : [_]Integer }}; diff --git a/intTests/test_cryptol_fromto/test.sh b/intTests/test_cryptol_fromto/test.sh new file mode 100755 index 0000000000..0b864017cd --- /dev/null +++ b/intTests/test_cryptol_fromto/test.sh @@ -0,0 +1 @@ +$SAW test.saw diff --git a/otherTests/saw-core-rocq/test_arithmetic.log.good b/otherTests/saw-core-rocq/test_arithmetic.log.good index 96da67c1bc..4a258eefff 100644 --- a/otherTests/saw-core-rocq/test_arithmetic.log.good +++ b/otherTests/saw-core-rocq/test_arithmetic.log.good @@ -303,7 +303,7 @@ Definition head (n : CryptolPrimitivesForSAWCore.Num) (a : Type) {Inh_a : SAWCor -Definition sext (m : CryptolPrimitivesForSAWCore.Num) (n : CryptolPrimitivesForSAWCore.Num) (x : CryptolPrimitivesForSAWCore.seq n Init.Datatypes.bool) : CryptolPrimitivesForSAWCore.seq m Init.Datatypes.bool := +Definition sext (m : CryptolPrimitivesForSAWCore.Num) (n : CryptolPrimitivesForSAWCore.Num) (_P : CryptolPrimitivesForSAWCore.PFin m) (_P1 : CryptolPrimitivesForSAWCore.PGeq m n) (_P2 : CryptolPrimitivesForSAWCore.PGeq n (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))) (x : CryptolPrimitivesForSAWCore.seq n Init.Datatypes.bool) : CryptolPrimitivesForSAWCore.seq m Init.Datatypes.bool := let var__0 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) in let var__1 := CryptolPrimitivesForSAWCore.tcSub m n in let var__2 := CryptolPrimitivesForSAWCore.seq var__1 Init.Datatypes.bool in @@ -311,13 +311,14 @@ Definition sext (m : CryptolPrimitivesForSAWCore.Num) (n : CryptolPrimitivesForS let var__4 := CryptolPrimitivesForSAWCore.tcAdd var__0 var__3 in let var__5 := CryptolPrimitivesForSAWCore.ecZero var__2 (CryptolPrimitivesForSAWCore.PZeroSeqBool var__1) in let var__6 := CryptolPrimitivesForSAWCore.tcAdd var__1 n in - SAWCoreScaffolding.coerce (CryptolPrimitivesForSAWCore.seq var__6 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.seq m Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.seq_cong1 var__6 m Init.Datatypes.bool ltac:(solveUnsafeAssert)) (CryptolPrimitivesForSAWCore.ecCat var__1 n Init.Datatypes.bool (if head var__3 Init.Datatypes.bool (SAWCoreScaffolding.coerce (CryptolPrimitivesForSAWCore.seq n Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.seq var__4 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.seq_cong1 n var__4 Init.Datatypes.bool ltac:(solveUnsafeAssert)) x) then CryptolPrimitivesForSAWCore.ecCompl var__2 (CryptolPrimitivesForSAWCore.PLogicSeqBool var__1) var__5 else var__5) x). + SAWCoreScaffolding.coerce (CryptolPrimitivesForSAWCore.seq var__6 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.seq m Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.seq_cong1 var__6 m Init.Datatypes.bool ltac:(solveUnsafeAssert)) (CryptolPrimitivesForSAWCore.ecCat var__1 n Init.Datatypes.bool (CryptolPrimitivesForSAWCore.PFin_tcSub m n _P) (if head var__3 Init.Datatypes.bool (SAWCoreScaffolding.coerce (CryptolPrimitivesForSAWCore.seq n Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.seq var__4 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.seq_cong1 n var__4 Init.Datatypes.bool ltac:(solveUnsafeAssert)) x) then CryptolPrimitivesForSAWCore.ecCompl var__2 (CryptolPrimitivesForSAWCore.PLogicSeqBool var__1) var__5 else var__5) x). Definition TestArith_SignExtend : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool := let var__0 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in - sext (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) var__0 (CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0)). + let var__1 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) in + sext var__1 var__0 (CryptolPrimitivesForSAWCore.PFin_TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) ltac:(solveUnsafeAssumePGeq) ltac:(solveUnsafeAssumePGeq) (CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0)). (** Mandatory imports from saw-core-rocq *) @@ -339,14 +340,15 @@ From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) -Definition zext (m : CryptolPrimitivesForSAWCore.Num) (n : CryptolPrimitivesForSAWCore.Num) (x : CryptolPrimitivesForSAWCore.seq n Init.Datatypes.bool) : CryptolPrimitivesForSAWCore.seq m Init.Datatypes.bool := +Definition zext (m : CryptolPrimitivesForSAWCore.Num) (n : CryptolPrimitivesForSAWCore.Num) (_P : CryptolPrimitivesForSAWCore.PFin m) (_P1 : CryptolPrimitivesForSAWCore.PGeq m n) (x : CryptolPrimitivesForSAWCore.seq n Init.Datatypes.bool) : CryptolPrimitivesForSAWCore.seq m Init.Datatypes.bool := let var__0 := CryptolPrimitivesForSAWCore.tcSub m n in let var__1 := CryptolPrimitivesForSAWCore.tcAdd var__0 n in - SAWCoreScaffolding.coerce (CryptolPrimitivesForSAWCore.seq var__1 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.seq m Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.seq_cong1 var__1 m Init.Datatypes.bool ltac:(solveUnsafeAssert)) (CryptolPrimitivesForSAWCore.ecCat var__0 n Init.Datatypes.bool (CryptolPrimitivesForSAWCore.ecZero (CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.PZeroSeqBool var__0)) x). + SAWCoreScaffolding.coerce (CryptolPrimitivesForSAWCore.seq var__1 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.seq m Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.seq_cong1 var__1 m Init.Datatypes.bool ltac:(solveUnsafeAssert)) (CryptolPrimitivesForSAWCore.ecCat var__0 n Init.Datatypes.bool (CryptolPrimitivesForSAWCore.PFin_tcSub m n _P) (CryptolPrimitivesForSAWCore.ecZero (CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.PZeroSeqBool var__0)) x). Definition TestArith_ZeroExtend : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool := let var__0 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in - zext (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) var__0 (CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0)). + let var__1 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) in + zext var__1 var__0 (CryptolPrimitivesForSAWCore.PFin_TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) ltac:(solveUnsafeAssumePGeq) (CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0)). diff --git a/otherTests/saw-core-rocq/test_cryptol_module_sha512.log.good b/otherTests/saw-core-rocq/test_cryptol_module_sha512.log.good index 187c63c17b..8357e21356 100644 --- a/otherTests/saw-core-rocq/test_cryptol_module_sha512.log.good +++ b/otherTests/saw-core-rocq/test_cryptol_module_sha512.log.good @@ -11,7 +11,7 @@ Malformed term: let { L@free : Num; } in fix _x`6 (\(hash : _x`6) -> - ecCat _x`1 L@free _x`3 [|:Parameter::H0] + ecCat _x`1 L@free _x`3 (PFin_TCNum 1) [|:Parameter::H0] (coerce (seq _x`7 _x`3) (seq L@free _x`3) (seq_cong1 _x`7 L@free _x`3 (unsafeAssert Num _x`7 L@free)) (seqMap #(_x`3, _x`4) _x`3 _x`7 diff --git a/otherTests/saw-core-rocq/test_cryptol_module_simple.log.good b/otherTests/saw-core-rocq/test_cryptol_module_simple.log.good index e4767f8459..84cb2b9290 100644 --- a/otherTests/saw-core-rocq/test_cryptol_module_simple.log.good +++ b/otherTests/saw-core-rocq/test_cryptol_module_simple.log.good @@ -39,19 +39,19 @@ Section Simple . let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool in if CryptolPrimitivesForSAWCore.ecGt var__1 (CryptolPrimitivesForSAWCore.PCmpSeqBool var__0) x y then x else y. - Definition encrypt (a : CryptolPrimitivesForSAWCore.Num) (key : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) (plaintext : CryptolPrimitivesForSAWCore.seq a (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool)) : CryptolPrimitivesForSAWCore.seq a (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) := + Definition encrypt (a : CryptolPrimitivesForSAWCore.Num) (_P : CryptolPrimitivesForSAWCore.PFin a) (key : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) (plaintext : CryptolPrimitivesForSAWCore.seq a (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool)) : CryptolPrimitivesForSAWCore.seq a (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) := let var__0 := CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool in CryptolPrimitivesForSAWCore.seqMap var__0 var__0 a (fun (pt : var__0) => let var__1 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in CryptolPrimitivesForSAWCore.ecXor var__0 (CryptolPrimitivesForSAWCore.PLogicSeqBool var__1) pt key) plaintext. - Definition decrypt (a : CryptolPrimitivesForSAWCore.Num) (key : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) (ciphertext : CryptolPrimitivesForSAWCore.seq a (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool)) : CryptolPrimitivesForSAWCore.seq a (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) := + Definition decrypt (a : CryptolPrimitivesForSAWCore.Num) (_P : CryptolPrimitivesForSAWCore.PFin a) (key : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) (ciphertext : CryptolPrimitivesForSAWCore.seq a (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool)) : CryptolPrimitivesForSAWCore.seq a (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) := let var__0 := CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool in CryptolPrimitivesForSAWCore.seqMap var__0 var__0 a (fun (ct : var__0) => let var__1 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in CryptolPrimitivesForSAWCore.ecXor var__0 (CryptolPrimitivesForSAWCore.PLogicSeqBool var__1) ct key) ciphertext. - Definition roundtrip (u944 : CryptolPrimitivesForSAWCore.Num) (k : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) (ip : CryptolPrimitivesForSAWCore.seq u944 (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool)) : Init.Datatypes.bool := + Definition roundtrip (u944 : CryptolPrimitivesForSAWCore.Num) (_P : CryptolPrimitivesForSAWCore.PFin u944) (k : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) (ip : CryptolPrimitivesForSAWCore.seq u944 (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool)) : Init.Datatypes.bool := let var__0 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool in - CryptolPrimitivesForSAWCore.ecEq (CryptolPrimitivesForSAWCore.seq u944 var__1) (CryptolPrimitivesForSAWCore.PEqSeq u944 var__1 (CryptolPrimitivesForSAWCore.PEqSeqBool var__0)) (decrypt u944 k (encrypt u944 k ip)) ip. + CryptolPrimitivesForSAWCore.ecEq (CryptolPrimitivesForSAWCore.seq u944 var__1) (CryptolPrimitivesForSAWCore.PEqSeq u944 var__1 (CryptolPrimitivesForSAWCore.PEqSeqBool var__0)) (decrypt u944 _P k (encrypt u944 _P k ip)) ip. End Simple . diff --git a/otherTests/saw-core-rocq/test_cryptol_primitives.log.good b/otherTests/saw-core-rocq/test_cryptol_primitives.log.good index 0a5bc464ee..2fd34b83a6 100644 --- a/otherTests/saw-core-rocq/test_cryptol_primitives.log.good +++ b/otherTests/saw-core-rocq/test_cryptol_primitives.log.good @@ -52,14 +52,20 @@ Definition Num__rec : forall (p : forall (_1 : Num), Type), forall (_1 : forall Definition tcFin : forall (_1 : Num), Init.Datatypes.bool := fun (n : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => Init.Datatypes.bool) (fun (n1 : Init.Datatypes.nat) => Init.Datatypes.true) Init.Datatypes.false n. -Definition getFinNat : forall (n : Num), Init.Datatypes.nat := - fun (n : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => Init.Datatypes.nat) (fun (n1 : Init.Datatypes.nat) => n1) (SAWCoreScaffolding.error Init.Datatypes.nat "Unexpected Fin constraint violation!"%string) n. +Definition PFin : forall (_1 : Num), Prop := + fun (n : Num) => @Init.Logic.eq Init.Datatypes.bool (tcFin n) Init.Datatypes.true. -Definition finNumRec : forall (p : forall (_1 : Num), Type), forall {Inh_p : forall (_1 : Num), SAWCoreScaffolding.Inhabited (p _1)}, forall (_1 : forall (n : Init.Datatypes.nat), p (TCNum n)), forall (n : Num), p n := - fun (p : forall (_1 : Num), Type) (Inh_p : forall (_1 : Num), SAWCoreScaffolding.Inhabited (p _1)) (f : forall (n : Init.Datatypes.nat), p (TCNum n)) (n : Num) => @CryptolPrimitivesForSAWCore.Num_rect p f (SAWCoreScaffolding.error (p TCInf) "Unexpected Fin constraint violation!"%string) n. +Definition PFin_TCNum : forall (n : Init.Datatypes.nat), PFin (TCNum n) := + fun (n : Init.Datatypes.nat) => @Init.Logic.eq_refl Init.Datatypes.bool Init.Datatypes.true. -Definition finNumRec2 : forall (p : forall (_1 : Num), forall (_2 : Num), Type), forall {Inh_p : forall (_1 : Num), forall (_2 : Num), SAWCoreScaffolding.Inhabited (p _1 _2)}, forall (_1 : forall (m : Init.Datatypes.nat), forall (n : Init.Datatypes.nat), p (TCNum m) (TCNum n)), forall (m : Num), forall (n : Num), p m n := - fun (p : forall (_1 : Num), forall (_2 : Num), Type) (Inh_p : forall (_1 : Num), forall (_2 : Num), SAWCoreScaffolding.Inhabited (p _1 _2)) (f : forall (m : Init.Datatypes.nat), forall (n : Init.Datatypes.nat), p (TCNum m) (TCNum n)) => finNumRec (fun (m : Num) => forall (n : Num), p m n) (fun (m : Init.Datatypes.nat) => finNumRec (p (TCNum m)) (f m)). +Definition PFin_TCInf : forall (_1 : PFin TCInf), SAWCorePrelude.FalseProp := + fun (pf : PFin TCInf) => SAWCorePrelude.sym Init.Datatypes.bool Init.Datatypes.false Init.Datatypes.true pf. + +Definition FalseProp_elim : forall (a : Type), forall (_1 : SAWCorePrelude.FalseProp), a := + fun (a : Type) => SAWCoreScaffolding.Eq__rec Init.Datatypes.bool Init.Datatypes.true (fun (y : Init.Datatypes.bool) (_1 : @Init.Logic.eq Init.Datatypes.bool Init.Datatypes.true y) => @Init.Datatypes.bool_rect (fun (_2 : Init.Datatypes.bool) => Type) SAWCorePrelude.TrueProp a y) SAWCorePrelude.TrueI Init.Datatypes.false. + +Definition PFinNumRec : forall (n : Num), forall (_1 : PFin n), forall (p : forall (_2 : Num), Type), forall (_2 : forall (n1 : Init.Datatypes.nat), p (TCNum n1)), p n := + fun (n : Num) (fn : PFin n) (p : forall (_1 : Num), Type) (f : forall (n1 : Init.Datatypes.nat), p (TCNum n1)) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (_1 : PFin n1), p n1) (fun (n1 : Init.Datatypes.nat) (_1 : PFin (TCNum n1)) => f n1) (fun (c : PFin TCInf) => FalseProp_elim (p TCInf) (PFin_TCInf c)) n fn. Definition binaryNumFun : forall (_1 : forall (_1 : Init.Datatypes.nat), forall (_2 : Init.Datatypes.nat), Init.Datatypes.nat), forall (_2 : forall (_2 : Init.Datatypes.nat), Num), forall (_3 : forall (_3 : Init.Datatypes.nat), Num), forall (_4 : Num), forall (_5 : Num), forall (_6 : Num), Num := fun (f1 : forall (_1 : Init.Datatypes.nat), forall (_2 : Init.Datatypes.nat), Init.Datatypes.nat) (f2 : forall (_1 : Init.Datatypes.nat), Num) (f3 : forall (_1 : Init.Datatypes.nat), Num) (f4 : Num) (num1 : Num) (num2 : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (num1' : Num) => Num) (fun (n1 : Init.Datatypes.nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (num2' : Num) => Num) (fun (n2 : Init.Datatypes.nat) => TCNum (f1 n1 n2)) (f2 n1) num2) (@CryptolPrimitivesForSAWCore.Num_rect (fun (num2' : Num) => Num) f3 f4 num2) num1. @@ -121,6 +127,39 @@ Definition tcEqual : forall (_1 : Num), forall (_2 : Num), Init.Datatypes.bool : Definition tcLt : forall (_1 : Num), forall (_2 : Num), Init.Datatypes.bool := binaryNumPred SAWCoreScaffolding.ltNat (fun (x : Init.Datatypes.nat) => Init.Datatypes.true) (fun (y : Init.Datatypes.nat) => Init.Datatypes.false) Init.Datatypes.true. +Definition PNeq : forall (_1 : Num), forall (_2 : Num), Prop := + fun (m : Num) (n : Num) => @Init.Logic.eq Init.Datatypes.bool (tcEqual m n) Init.Datatypes.false. + +Definition PGeq : forall (_1 : Num), forall (_2 : Num), Prop := + fun (m : Num) (n : Num) => @Init.Logic.eq Init.Datatypes.bool (tcLt m n) Init.Datatypes.false. + +Definition PGeq_0 : forall (n : Num), PGeq n (TCNum SAWCoreScaffolding.Zero) := + @CryptolPrimitivesForSAWCore.Num_rect (fun (n : Num) => PGeq n (TCNum SAWCoreScaffolding.Zero)) SAWCoreScaffolding.ltNat_0_right (@Init.Logic.eq_refl Init.Datatypes.bool Init.Datatypes.false). + +Definition PFin_tcAdd : forall (m : Num), forall (n : Num), forall (_1 : PFin m), forall (_2 : PFin n), PFin (tcAdd m n) := + fun (m : Num) (n : Num) (pm : PFin m) (pn : PFin n) => PFinNumRec m pm (fun (m1 : Num) => PFin (tcAdd m1 n)) (fun (m1 : Init.Datatypes.nat) => PFinNumRec n pn (fun (n1 : Num) => PFin (tcAdd (TCNum m1) n1)) (fun (n1 : Init.Datatypes.nat) => PFin_TCNum (SAWCoreScaffolding.addNat m1 n1))). + +Definition PFin_tcMul : forall (m : Num), forall (n : Num), forall (_1 : PFin m), forall (_2 : PFin n), PFin (tcMul m n) := + fun (m : Num) (n : Num) (pm : PFin m) (pn : PFin n) => PFinNumRec m pm (fun (m1 : Num) => PFin (tcMul m1 n)) (fun (m1 : Init.Datatypes.nat) => PFinNumRec n pn (fun (n1 : Num) => PFin (tcMul (TCNum m1) n1)) (fun (n1 : Init.Datatypes.nat) => PFin_TCNum (SAWCoreScaffolding.mulNat m1 n1))). + +Definition PFin_tcSub : forall (m : Num), forall (n : Num), forall (_1 : PFin m), PFin (tcSub m n) := + fun (m : Num) (n : Num) (pm : PFin m) => PFinNumRec m pm (fun (m1 : Num) => PFin (tcSub m1 n)) (fun (m1 : Init.Datatypes.nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => PFin (tcSub (TCNum m1) n1)) (fun (n1 : Init.Datatypes.nat) => PFin_TCNum (SAWCoreScaffolding.subNat m1 n1)) (PFin_TCNum SAWCoreScaffolding.Zero) n). + +Definition PFin_tcDiv : forall (m : Num), forall (n : Num), forall (_1 : PFin m), PFin (tcDiv m n) := + fun (m : Num) (n : Num) (pm : PFin m) => PFinNumRec m pm (fun (m1 : Num) => PFin (tcDiv m1 n)) (fun (m1 : Init.Datatypes.nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => PFin (tcDiv (TCNum m1) n1)) (fun (n1 : Init.Datatypes.nat) => PFin_TCNum (SAWCorePrelude.divNat m1 n1)) (PFin_TCNum SAWCoreScaffolding.Zero) n). + +Definition PFin_tcCeilDiv : forall (m : Num), forall (n : Num), forall (_1 : PFin m), PFin (tcCeilDiv m n) := + fun (m : Num) (n : Num) (pm : PFin m) => PFinNumRec m pm (fun (m1 : Num) => PFin (tcCeilDiv m1 n)) (fun (m1 : Init.Datatypes.nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => PFin (tcCeilDiv (TCNum m1) n1)) (fun (n1 : Init.Datatypes.nat) => PFin_TCNum (ceilDivNat m1 n1)) (PFin_TCNum SAWCoreScaffolding.Zero) n). + +Definition PFin_downward_closed : forall (m : Num), forall (n : Num), forall (_1 : PGeq m n), forall (_2 : PFin m), PFin n := + fun (m : Num) (n : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (m1 : Num) => forall (_1 : PGeq m1 n), forall (_2 : PFin m1), PFin n) (fun (m1 : Init.Datatypes.nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (_1 : PGeq (TCNum m1) n1), forall (_2 : PFin (TCNum m1)), PFin n1) (fun (n1 : Init.Datatypes.nat) (_1 : PGeq (TCNum m1) (TCNum n1)) (_2 : PFin (TCNum m1)) => @Init.Logic.eq_refl Init.Datatypes.bool Init.Datatypes.true) (fun (c1 : PGeq (TCNum m1) TCInf) (_1 : PFin (TCNum m1)) => SAWCorePrelude.sym Init.Datatypes.bool Init.Datatypes.true Init.Datatypes.false c1) n) (@CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (_1 : PGeq TCInf n1), forall (_2 : PFin TCInf), PFin n1) (fun (n1 : Init.Datatypes.nat) (_1 : PGeq TCInf (TCNum n1)) (_2 : PFin TCInf) => @Init.Logic.eq_refl Init.Datatypes.bool Init.Datatypes.true) (fun (_1 : PGeq TCInf TCInf) (c2 : PFin TCInf) => c2) n) m. + +(* "Cryptol::unsafeAssumePFin@core" was skipped *) + +(* "Cryptol::unsafeAssumePGeq@core" was skipped *) + +(* "Cryptol::unsafeAssumePNeq@core" was skipped *) + Definition seq : forall (_1 : Num), forall (_2 : Type), Type := fun (num : Num) (a : Type) => @CryptolPrimitivesForSAWCore.Num_rect (fun (num1 : Num) => Type) (fun (n : Init.Datatypes.nat) => SAWCoreVectorsAsRocqVectors.Vec n a) (SAWCorePrelude.Stream a) num. @@ -594,8 +633,8 @@ Definition PFLiteralRational : PFLiteral SAWCoreScaffolding.Rational := Definition ecNumber : forall (val : Num), forall (a : Type), forall (_1 : PLiteral a), a := fun (val : Num) (a : Type) (pa : PLiteral a) => @CryptolPrimitivesForSAWCore.Num_rect (fun (_1 : Num) => a) pa (pa SAWCoreScaffolding.Zero) val. -Definition ecFromZ : forall (n : Num), forall (_1 : IntModNum n), SAWCoreScaffolding.Integer := - fun (n : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (_1 : IntModNum n1), SAWCoreScaffolding.Integer) SAWCoreScaffolding.fromIntMod (fun (x : SAWCoreScaffolding.Integer) => x) n. +Definition ecFromZ : forall (n : Num), forall (_1 : PFin n), forall (_2 : PGeq n (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))), forall (_3 : IntModNum n), SAWCoreScaffolding.Integer := + fun (n : Num) (pn : PFin n) (_1 : PGeq n (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))) => PFinNumRec n pn (fun (n1 : Num) => forall (_2 : IntModNum n1), SAWCoreScaffolding.Integer) SAWCoreScaffolding.fromIntMod. Definition ecFromInteger : forall (a : Type), forall (_1 : PRing a), forall (_2 : SAWCoreScaffolding.Integer), a := fun (a : Type) (pa : PRing a) => @SAWCoreScaffolding.recordHead "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil (@SAWCoreScaffolding.recordTail "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil) (@SAWCoreScaffolding.recordTail "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil)) (@SAWCoreScaffolding.recordTail "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil))) (@SAWCoreScaffolding.recordTail "add"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil)))) (@SAWCoreScaffolding.recordTail "ringZero"%string (PZero a) (SAWCoreScaffolding.RecordTypeCons "add"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil))))) pa))))). @@ -645,17 +684,17 @@ Definition ecRoundAway : forall (a : Type), forall (_1 : PRound a), forall (_2 : Definition ecRoundToEven : forall (a : Type), forall (_1 : PRound a), forall (_2 : a), SAWCoreScaffolding.Integer := fun (a : Type) (pr : PRound a) => @SAWCoreScaffolding.recordHead "roundToEven"%string (forall (_1 : a), SAWCoreScaffolding.Integer) SAWCoreScaffolding.RecordTypeNil (@SAWCoreScaffolding.recordTail "roundAway"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "roundToEven"%string (forall (_1 : a), SAWCoreScaffolding.Integer) SAWCoreScaffolding.RecordTypeNil) (@SAWCoreScaffolding.recordTail "trunc"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "roundAway"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "roundToEven"%string (forall (_1 : a), SAWCoreScaffolding.Integer) SAWCoreScaffolding.RecordTypeNil)) (@SAWCoreScaffolding.recordTail "ceiling"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "trunc"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "roundAway"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "roundToEven"%string (forall (_1 : a), SAWCoreScaffolding.Integer) SAWCoreScaffolding.RecordTypeNil))) (@SAWCoreScaffolding.recordTail "floor"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "ceiling"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "trunc"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "roundAway"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "roundToEven"%string (forall (_1 : a), SAWCoreScaffolding.Integer) SAWCoreScaffolding.RecordTypeNil)))) (@SAWCoreScaffolding.recordTail "roundCmp"%string (PCmp a) (SAWCoreScaffolding.RecordTypeCons "floor"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "ceiling"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "trunc"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "roundAway"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "roundToEven"%string (forall (_1 : a), SAWCoreScaffolding.Integer) SAWCoreScaffolding.RecordTypeNil))))) (@SAWCoreScaffolding.recordTail "roundField"%string (PField a) (SAWCoreScaffolding.RecordTypeCons "roundCmp"%string (PCmp a) (SAWCoreScaffolding.RecordTypeCons "floor"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "ceiling"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "trunc"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "roundAway"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "roundToEven"%string (forall (_1 : a), SAWCoreScaffolding.Integer) SAWCoreScaffolding.RecordTypeNil)))))) pr)))))). -Definition ecLg2 : forall (n : Num), forall (_1 : seq n Init.Datatypes.bool), seq n Init.Datatypes.bool := - fun (n : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), seq n1 Init.Datatypes.bool) SAWCoreVectorsAsRocqVectors.bvLg2 (SAWCoreScaffolding.error (forall (_1 : SAWCorePrelude.Stream Init.Datatypes.bool), SAWCorePrelude.Stream Init.Datatypes.bool) "ecLg2: expected finite word"%string) n. +Definition ecLg2 : forall (n : Num), forall (_1 : PFin n), forall (_2 : seq n Init.Datatypes.bool), seq n Init.Datatypes.bool := + fun (n : Num) (pn : PFin n) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), seq n1 Init.Datatypes.bool) SAWCoreVectorsAsRocqVectors.bvLg2. -Definition ecSDiv : forall (n : Num), forall (_1 : seq n Init.Datatypes.bool), forall (_2 : seq n Init.Datatypes.bool), seq n Init.Datatypes.bool := - fun (n : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), forall (_2 : seq n1 Init.Datatypes.bool), seq n1 Init.Datatypes.bool) (SAWCoreScaffolding.Nat__rec (fun (n1 : Init.Datatypes.nat) => forall (_1 : SAWCoreVectorsAsRocqVectors.Vec n1 Init.Datatypes.bool), forall (_2 : SAWCoreVectorsAsRocqVectors.Vec n1 Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec n1 Init.Datatypes.bool) (SAWCoreScaffolding.error (forall (_1 : SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool), forall (_2 : SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool) "ecSDiv: illegal 0-width word"%string) (fun (n' : Init.Datatypes.nat) (_1 : forall (_1 : SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool), forall (_2 : SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool) => SAWCoreVectorsAsRocqVectors.bvSDiv n')) (SAWCoreScaffolding.error (forall (_1 : SAWCorePrelude.Stream Init.Datatypes.bool), forall (_2 : SAWCorePrelude.Stream Init.Datatypes.bool), SAWCorePrelude.Stream Init.Datatypes.bool) "ecSDiv: expected finite word"%string) n. +Definition ecSDiv : forall (n : Num), forall (_1 : PFin n), forall (_2 : PGeq n (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))), forall (_3 : seq n Init.Datatypes.bool), forall (_4 : seq n Init.Datatypes.bool), seq n Init.Datatypes.bool := + fun (n : Num) (pn : PFin n) (_pgeq : PGeq n (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), forall (_2 : seq n1 Init.Datatypes.bool), seq n1 Init.Datatypes.bool) (SAWCoreScaffolding.Nat__rec (fun (n1 : Init.Datatypes.nat) => forall (_1 : SAWCoreVectorsAsRocqVectors.Vec n1 Init.Datatypes.bool), forall (_2 : SAWCoreVectorsAsRocqVectors.Vec n1 Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec n1 Init.Datatypes.bool) (SAWCoreScaffolding.error (forall (_1 : SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool), forall (_2 : SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool) "ecSDiv: illegal 0-width word"%string) (fun (n' : Init.Datatypes.nat) (_1 : forall (_1 : SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool), forall (_2 : SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool) => SAWCoreVectorsAsRocqVectors.bvSDiv n')). -Definition ecSMod : forall (n : Num), forall (_1 : seq n Init.Datatypes.bool), forall (_2 : seq n Init.Datatypes.bool), seq n Init.Datatypes.bool := - fun (n : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), forall (_2 : seq n1 Init.Datatypes.bool), seq n1 Init.Datatypes.bool) (SAWCoreScaffolding.Nat__rec (fun (n1 : Init.Datatypes.nat) => forall (_1 : SAWCoreVectorsAsRocqVectors.Vec n1 Init.Datatypes.bool), forall (_2 : SAWCoreVectorsAsRocqVectors.Vec n1 Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec n1 Init.Datatypes.bool) (SAWCoreScaffolding.error (forall (_1 : SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool), forall (_2 : SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool) "ecSMod: illegal 0-width word"%string) (fun (n' : Init.Datatypes.nat) (_1 : forall (_1 : SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool), forall (_2 : SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool) => SAWCoreVectorsAsRocqVectors.bvSRem n')) (SAWCoreScaffolding.error (forall (_1 : SAWCorePrelude.Stream Init.Datatypes.bool), forall (_2 : SAWCorePrelude.Stream Init.Datatypes.bool), SAWCorePrelude.Stream Init.Datatypes.bool) "ecSMod: expected finite word"%string) n. +Definition ecSMod : forall (n : Num), forall (_1 : PFin n), forall (_2 : PGeq n (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))), forall (_3 : seq n Init.Datatypes.bool), forall (_4 : seq n Init.Datatypes.bool), seq n Init.Datatypes.bool := + fun (n : Num) (pn : PFin n) (_pgeq : PGeq n (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), forall (_2 : seq n1 Init.Datatypes.bool), seq n1 Init.Datatypes.bool) (SAWCoreScaffolding.Nat__rec (fun (n1 : Init.Datatypes.nat) => forall (_1 : SAWCoreVectorsAsRocqVectors.Vec n1 Init.Datatypes.bool), forall (_2 : SAWCoreVectorsAsRocqVectors.Vec n1 Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec n1 Init.Datatypes.bool) (SAWCoreScaffolding.error (forall (_1 : SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool), forall (_2 : SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool) "ecSMod: illegal 0-width word"%string) (fun (n' : Init.Datatypes.nat) (_1 : forall (_1 : SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool), forall (_2 : SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool) => SAWCoreVectorsAsRocqVectors.bvSRem n')). -Definition toSignedInteger : forall (n : Num), forall (_1 : seq n Init.Datatypes.bool), SAWCoreScaffolding.Integer := - fun (n : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), SAWCoreScaffolding.Integer) SAWCoreVectorsAsRocqVectors.sbvToInt (SAWCoreScaffolding.error (forall (_1 : SAWCorePrelude.Stream Init.Datatypes.bool), SAWCoreScaffolding.Integer) "toSignedInteger: expected finite word"%string) n. +Definition toSignedInteger : forall (n : Num), forall (_1 : PFin n), forall (_2 : PGeq n (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))), forall (_3 : seq n Init.Datatypes.bool), SAWCoreScaffolding.Integer := + fun (n : Num) (pn : PFin n) (_pgeq : PGeq n (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), SAWCoreScaffolding.Integer) SAWCoreVectorsAsRocqVectors.sbvToInt. Definition ecEq : forall (a : Type), forall (_1 : PEq a), forall (_2 : a), forall (_3 : a), Init.Datatypes.bool := fun (a : Type) (pa : PEq a) => @SAWCoreScaffolding.recordHead "eq"%string (forall (_1 : a), forall (_2 : a), Init.Datatypes.bool) SAWCoreScaffolding.RecordTypeNil pa. @@ -704,33 +743,33 @@ Definition ecShiftR : forall (m : Num), forall (ix : Type), forall (a : Type), f fun (m : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (m1 : Num) => forall (ix : Type), forall (a : Type), forall (_1 : PIntegral ix), forall (_2 : PZero a), forall (_3 : seq m1 a), forall (_4 : ix), seq m1 a) (fun (m1 : Init.Datatypes.nat) (ix : Type) (a : Type) (pix : PIntegral ix) (pz : PZero a) (xs : SAWCoreVectorsAsRocqVectors.Vec m1 a) => let var__0 := ecZero a pz in posNegCases ix pix (SAWCoreVectorsAsRocqVectors.Vec m1 a) (SAWCoreVectorsAsRocqVectors.shiftR m1 a var__0 xs) (SAWCoreVectorsAsRocqVectors.shiftL m1 a var__0 xs)) (fun (ix : Type) (a : Type) (pix : PIntegral ix) (pz : PZero a) (xs : SAWCorePrelude.Stream a) => posNegCases ix pix (SAWCorePrelude.Stream a) (SAWCorePrelude.streamShiftR a pz xs) (SAWCorePrelude.streamShiftL a xs)) m. -Definition ecSShiftR : forall (n : Num), forall (ix : Type), forall (_1 : PIntegral ix), forall (_2 : seq n Init.Datatypes.bool), forall (_3 : ix), seq n Init.Datatypes.bool := - finNumRec (fun (n : Num) => forall (ix : Type), forall (_1 : PIntegral ix), forall (_2 : seq n Init.Datatypes.bool), forall (_3 : ix), seq n Init.Datatypes.bool) (fun (n : Init.Datatypes.nat) (ix : Type) (pix : PIntegral ix) => SAWCorePrelude.natCase (fun (w : Init.Datatypes.nat) => forall (_1 : SAWCoreVectorsAsRocqVectors.Vec w Init.Datatypes.bool), forall (_2 : ix), SAWCoreVectorsAsRocqVectors.Vec w Init.Datatypes.bool) (fun (xs : SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool) (_1 : ix) => xs) (fun (w : Init.Datatypes.nat) (xs : SAWCoreVectorsAsRocqVectors.Vec (SAWCoreScaffolding.Succ w) Init.Datatypes.bool) => let var__0 := SAWCoreScaffolding.Succ w in - posNegCases ix pix (SAWCoreVectorsAsRocqVectors.Vec var__0 Init.Datatypes.bool) (SAWCoreVectorsAsRocqVectors.bvSShr w xs) (SAWCoreVectorsAsRocqVectors.bvShl var__0 xs)) n). +Definition ecSShiftR : forall (n : Num), forall (ix : Type), forall (_1 : PFin n), forall (_2 : PGeq n (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))), forall (_3 : PIntegral ix), forall (_4 : seq n Init.Datatypes.bool), forall (_5 : ix), seq n Init.Datatypes.bool := + fun (n : Num) (ix : Type) (pn : PFin n) (_pgeq : PGeq n (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))) (pix : PIntegral ix) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), forall (_2 : ix), seq n1 Init.Datatypes.bool) (SAWCorePrelude.natCase (fun (w : Init.Datatypes.nat) => forall (_1 : SAWCoreVectorsAsRocqVectors.Vec w Init.Datatypes.bool), forall (_2 : ix), SAWCoreVectorsAsRocqVectors.Vec w Init.Datatypes.bool) (fun (xs : SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool) (_1 : ix) => xs) (fun (w : Init.Datatypes.nat) (xs : SAWCoreVectorsAsRocqVectors.Vec (SAWCoreScaffolding.Succ w) Init.Datatypes.bool) => let var__0 := SAWCoreScaffolding.Succ w in + posNegCases ix pix (SAWCoreVectorsAsRocqVectors.Vec var__0 Init.Datatypes.bool) (SAWCoreVectorsAsRocqVectors.bvSShr w xs) (SAWCoreVectorsAsRocqVectors.bvShl var__0 xs))). -Definition ecRotL : forall (m : Num), forall (ix : Type), forall (a : Type), forall (_1 : PIntegral ix), forall (_2 : seq m a), forall (_3 : ix), seq m a := - finNumRec (fun (m : Num) => forall (ix : Type), forall (a : Type), forall (_1 : PIntegral ix), forall (_2 : seq m a), forall (_3 : ix), seq m a) (fun (m : Init.Datatypes.nat) (ix : Type) (a : Type) (pix : PIntegral ix) (xs : SAWCoreVectorsAsRocqVectors.Vec m a) => posNegCases ix pix (SAWCoreVectorsAsRocqVectors.Vec m a) (SAWCoreVectorsAsRocqVectors.rotateL m a xs) (SAWCoreVectorsAsRocqVectors.rotateR m a xs)). +Definition ecRotL : forall (m : Num), forall (ix : Type), forall (a : Type), forall (_1 : PFin m), forall (_2 : PIntegral ix), forall (_3 : seq m a), forall (_4 : ix), seq m a := + fun (m : Num) (ix : Type) (a : Type) (pm : PFin m) => PFinNumRec m pm (fun (m1 : Num) => forall (_1 : PIntegral ix), forall (_2 : seq m1 a), forall (_3 : ix), seq m1 a) (fun (m1 : Init.Datatypes.nat) (pix : PIntegral ix) (xs : SAWCoreVectorsAsRocqVectors.Vec m1 a) => posNegCases ix pix (SAWCoreVectorsAsRocqVectors.Vec m1 a) (SAWCoreVectorsAsRocqVectors.rotateL m1 a xs) (SAWCoreVectorsAsRocqVectors.rotateR m1 a xs)). -Definition ecRotR : forall (m : Num), forall (ix : Type), forall (a : Type), forall (_1 : PIntegral ix), forall (_2 : seq m a), forall (_3 : ix), seq m a := - finNumRec (fun (m : Num) => forall (ix : Type), forall (a : Type), forall (_1 : PIntegral ix), forall (_2 : seq m a), forall (_3 : ix), seq m a) (fun (m : Init.Datatypes.nat) (ix : Type) (a : Type) (pix : PIntegral ix) (xs : SAWCoreVectorsAsRocqVectors.Vec m a) => posNegCases ix pix (SAWCoreVectorsAsRocqVectors.Vec m a) (SAWCoreVectorsAsRocqVectors.rotateR m a xs) (SAWCoreVectorsAsRocqVectors.rotateL m a xs)). +Definition ecRotR : forall (m : Num), forall (ix : Type), forall (a : Type), forall (_1 : PFin m), forall (_2 : PIntegral ix), forall (_3 : seq m a), forall (_4 : ix), seq m a := + fun (m : Num) (ix : Type) (a : Type) (pm : PFin m) => PFinNumRec m pm (fun (m1 : Num) => forall (_1 : PIntegral ix), forall (_2 : seq m1 a), forall (_3 : ix), seq m1 a) (fun (m1 : Init.Datatypes.nat) (pix : PIntegral ix) (xs : SAWCoreVectorsAsRocqVectors.Vec m1 a) => posNegCases ix pix (SAWCoreVectorsAsRocqVectors.Vec m1 a) (SAWCoreVectorsAsRocqVectors.rotateR m1 a xs) (SAWCoreVectorsAsRocqVectors.rotateL m1 a xs)). -Definition ecCat : forall (m : Num), forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : seq m a), forall (_2 : seq n a), seq (tcAdd m n) a := - finNumRec (fun (m : Num) => forall (n : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : seq m a), forall (_2 : seq n a), seq (tcAdd m n) a) (fun (m : Init.Datatypes.nat) => CryptolPrimitivesForSAWCore.Num__rec (fun (n : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : SAWCoreVectorsAsRocqVectors.Vec m a), forall (_2 : seq n a), seq (tcAdd (TCNum m) n) a) (fun (n : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) => SAWCorePrelude.append m n a) (fun (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) => SAWCorePrelude.streamAppend a m)). +Definition ecCat : forall (m : Num), forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PFin m), forall (_2 : seq m a), forall (_3 : seq n a), seq (tcAdd m n) a := + fun (m : Num) (n : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pm : PFin m) => PFinNumRec m pm (fun (m1 : Num) => forall (_1 : seq m1 a), forall (_2 : seq n a), seq (tcAdd m1 n) a) (fun (m1 : Init.Datatypes.nat) => CryptolPrimitivesForSAWCore.Num__rec (fun (n1 : Num) => forall (_1 : SAWCoreVectorsAsRocqVectors.Vec m1 a), forall (_2 : seq n1 a), seq (tcAdd (TCNum m1) n1) a) (fun (n1 : Init.Datatypes.nat) => SAWCorePrelude.append m1 n1 a) (SAWCorePrelude.streamAppend a m1) n). Definition ecTake : forall (m : Num), forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : seq (tcAdd m n) a), seq m a := CryptolPrimitivesForSAWCore.Num__rec (fun (m : Num) => forall (n : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : seq (tcAdd m n) a), seq m a) (fun (m : Init.Datatypes.nat) => CryptolPrimitivesForSAWCore.Num__rec (fun (n : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : seq (tcAdd (TCNum m) n) a), SAWCoreVectorsAsRocqVectors.Vec m a) (fun (n : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (xs : SAWCoreVectorsAsRocqVectors.Vec (SAWCoreScaffolding.addNat m n) a) => SAWCorePrelude.take a m n xs) (fun (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (xs : SAWCorePrelude.Stream a) => SAWCorePrelude.streamTake a m xs)) (CryptolPrimitivesForSAWCore.Num__rec (fun (n : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : seq (tcAdd TCInf n) a), SAWCorePrelude.Stream a) (fun (n : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (xs : SAWCorePrelude.Stream a) => xs) (fun (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (xs : SAWCorePrelude.Stream a) => xs)). -Definition ecDrop : forall (m : Num), forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : seq (tcAdd m n) a), seq n a := - finNumRec (fun (m : Num) => forall (n : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : seq (tcAdd m n) a), seq n a) (fun (m : Init.Datatypes.nat) => CryptolPrimitivesForSAWCore.Num__rec (fun (n : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : seq (tcAdd (TCNum m) n) a), seq n a) (fun (n : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (xs : SAWCoreVectorsAsRocqVectors.Vec (SAWCoreScaffolding.addNat m n) a) => SAWCorePrelude.drop a m n xs) (fun (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (xs : SAWCorePrelude.Stream a) => SAWCorePrelude.streamDrop a m xs)). +Definition ecDrop : forall (m : Num), forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PFin m), forall (_2 : seq (tcAdd m n) a), seq n a := + fun (m : Num) (n : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pm : PFin m) => PFinNumRec m pm (fun (m1 : Num) => forall (_1 : seq (tcAdd m1 n) a), seq n a) (fun (m1 : Init.Datatypes.nat) => CryptolPrimitivesForSAWCore.Num__rec (fun (n1 : Num) => forall (_1 : seq (tcAdd (TCNum m1) n1) a), seq n1 a) (SAWCorePrelude.drop a m1) (SAWCorePrelude.streamDrop a m1) n). -Definition ecJoin : forall (m : Num), forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : seq m (seq n a)), seq (tcMul m n) a := - fun (m : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (m1 : Num) => forall (n : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : seq m1 (seq n a)), seq (tcMul m1 n) a) (fun (m1 : Init.Datatypes.nat) => finNumRec (fun (n : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : SAWCoreVectorsAsRocqVectors.Vec m1 (seq n a)), seq (tcMul (TCNum m1) n) a) (fun (n : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) => SAWCorePrelude.join m1 n a)) (finNumRec (fun (n : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : SAWCorePrelude.Stream (seq n a)), seq (tcMul TCInf n) a) (fun (n : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) => SAWCorePrelude.natCase (fun (n' : Init.Datatypes.nat) => forall (_1 : SAWCorePrelude.Stream (SAWCoreVectorsAsRocqVectors.Vec n' a)), seq (SAWCoreScaffolding.if0Nat Num n' (TCNum SAWCoreScaffolding.Zero) TCInf) a) (fun (s : SAWCorePrelude.Stream (SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero a)) => SAWCoreVectorsAsRocqVectors.EmptyVec a) (fun (n' : Init.Datatypes.nat) (s : SAWCorePrelude.Stream (SAWCoreVectorsAsRocqVectors.Vec (SAWCoreScaffolding.Succ n') a)) => SAWCorePrelude.streamJoin a n' s) n)) m. +Definition ecJoin : forall (m : Num), forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PFin n), forall (_2 : seq m (seq n a)), seq (tcMul m n) a := + fun (m : Num) (n : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pn : PFin n) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq m (seq n1 a)), seq (tcMul m n1) a) (fun (n1 : Init.Datatypes.nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (m1 : Num) => forall (_1 : seq m1 (SAWCoreVectorsAsRocqVectors.Vec n1 a)), seq (tcMul m1 (TCNum n1)) a) (fun (m1 : Init.Datatypes.nat) => SAWCorePrelude.join m1 n1 a) (SAWCorePrelude.natCase (fun (n' : Init.Datatypes.nat) => forall (_1 : SAWCorePrelude.Stream (SAWCoreVectorsAsRocqVectors.Vec n' a)), seq (SAWCoreScaffolding.if0Nat Num n' (TCNum SAWCoreScaffolding.Zero) TCInf) a) (fun (s : SAWCorePrelude.Stream (SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero a)) => SAWCoreVectorsAsRocqVectors.EmptyVec a) (SAWCorePrelude.streamJoin a) n1) m). -Definition ecSplit : forall (m : Num), forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : seq (tcMul m n) a), seq m (seq n a) := - fun (m : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (m1 : Num) => forall (n : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : seq (tcMul m1 n) a), seq m1 (seq n a)) (fun (m1 : Init.Datatypes.nat) => finNumRec (fun (n : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : seq (tcMul (TCNum m1) n) a), SAWCoreVectorsAsRocqVectors.Vec m1 (seq n a)) (fun (n : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) => SAWCorePrelude.split m1 n a)) (finNumRec (fun (n : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : seq (tcMul TCInf n) a), SAWCorePrelude.Stream (seq n a)) (fun (n : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) => SAWCorePrelude.natCase (fun (n' : Init.Datatypes.nat) => forall (_1 : seq (SAWCoreScaffolding.if0Nat Num n' (TCNum SAWCoreScaffolding.Zero) TCInf) a), SAWCorePrelude.Stream (SAWCoreVectorsAsRocqVectors.Vec n' a)) (SAWCorePrelude.streamConst (SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero a)) (fun (n' : Init.Datatypes.nat) => SAWCorePrelude.streamSplit a (SAWCoreScaffolding.Succ n')) n)) m. +Definition ecSplit : forall (m : Num), forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PFin n), forall (_2 : seq (tcMul m n) a), seq m (seq n a) := + fun (m : Num) (n : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pn : PFin n) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq (tcMul m n1) a), seq m (seq n1 a)) (fun (n1 : Init.Datatypes.nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (m1 : Num) => forall (_1 : seq (tcMul m1 (TCNum n1)) a), seq m1 (SAWCoreVectorsAsRocqVectors.Vec n1 a)) (fun (m1 : Init.Datatypes.nat) => SAWCorePrelude.split m1 n1 a) (SAWCorePrelude.natCase (fun (n' : Init.Datatypes.nat) => forall (_1 : seq (SAWCoreScaffolding.if0Nat Num n' (TCNum SAWCoreScaffolding.Zero) TCInf) a), SAWCorePrelude.Stream (SAWCoreVectorsAsRocqVectors.Vec n' a)) (SAWCorePrelude.streamConst (SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero a)) (fun (n' : Init.Datatypes.nat) => SAWCorePrelude.streamSplit a (SAWCoreScaffolding.Succ n')) n1) m). -Definition ecReverse : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : seq n a), seq n a := - finNumRec (fun (n : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : seq n a), seq n a) SAWCorePrelude.reverse. +Definition ecReverse : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PFin n), forall (_2 : seq n a), seq n a := + fun (n : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pn : PFin n) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 a), seq n1 a) (fun (n1 : Init.Datatypes.nat) => SAWCorePrelude.reverse n1 a). Definition ecTranspose : forall (m : Num), forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : seq m (seq n a)), seq n (seq m a) := fun (m : Num) (n : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) => @CryptolPrimitivesForSAWCore.Num_rect (fun (m1 : Num) => forall (_1 : seq m1 (seq n a)), seq n (seq m1 a)) (fun (m1 : Init.Datatypes.nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (_1 : SAWCoreVectorsAsRocqVectors.Vec m1 (seq n1 a)), seq n1 (SAWCoreVectorsAsRocqVectors.Vec m1 a)) (fun (n1 : Init.Datatypes.nat) => SAWCorePrelude.transpose m1 n1 a) (fun (xss : SAWCoreVectorsAsRocqVectors.Vec m1 (SAWCorePrelude.Stream a)) => SAWCorePrelude.MkStream (SAWCoreVectorsAsRocqVectors.Vec m1 a) (fun (i : Init.Datatypes.nat) => SAWCoreVectorsAsRocqVectors.gen m1 a (fun (j : Init.Datatypes.nat) => SAWCorePrelude.streamGet a (SAWCorePrelude.sawAt m1 (SAWCorePrelude.Stream a) xss j) i))) n) (@CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (_1 : SAWCorePrelude.Stream (seq n1 a)), seq n1 (SAWCorePrelude.Stream a)) (fun (n1 : Init.Datatypes.nat) (xss : SAWCorePrelude.Stream (SAWCoreVectorsAsRocqVectors.Vec n1 a)) => SAWCoreVectorsAsRocqVectors.gen n1 (SAWCorePrelude.Stream a) (fun (i : Init.Datatypes.nat) => SAWCorePrelude.MkStream a (fun (j : Init.Datatypes.nat) => SAWCorePrelude.sawAt n1 a (SAWCorePrelude.streamGet (SAWCoreVectorsAsRocqVectors.Vec n1 a) xss j) i))) (fun (xss : SAWCorePrelude.Stream (SAWCorePrelude.Stream a)) => SAWCorePrelude.MkStream (SAWCorePrelude.Stream a) (fun (i : Init.Datatypes.nat) => SAWCorePrelude.MkStream a (fun (j : Init.Datatypes.nat) => SAWCorePrelude.streamGet a (SAWCorePrelude.streamGet (SAWCorePrelude.Stream a) xss j) i))) n) m. @@ -738,30 +777,30 @@ Definition ecTranspose : forall (m : Num), forall (n : Num), forall (a : Type), Definition ecAt : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (ix : Type), forall (_1 : PIntegral ix), forall (_2 : seq n a), forall (_3 : ix), a := fun (n : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (ix : Type), forall (_1 : PIntegral ix), forall (_2 : seq n1 a), forall (_3 : ix), a) (fun (n1 : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (ix : Type) (pix : PIntegral ix) (xs : SAWCoreVectorsAsRocqVectors.Vec n1 a) => posNegCases ix pix a (SAWCorePrelude.sawAt n1 a xs) (fun (_1 : Init.Datatypes.nat) => SAWCorePrelude.sawAt n1 a xs SAWCoreScaffolding.Zero)) (fun (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (ix : Type) (pix : PIntegral ix) (xs : SAWCorePrelude.Stream a) => posNegCases ix pix a (SAWCorePrelude.streamGet a xs) (fun (_1 : Init.Datatypes.nat) => SAWCorePrelude.streamGet a xs SAWCoreScaffolding.Zero)) n. -Definition ecAtBack : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (ix : Type), forall (_1 : PIntegral ix), forall (_2 : seq n a), forall (_3 : ix), a := - fun (n : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (ix : Type) (pix : PIntegral ix) (xs : seq n a) => ecAt n a ix pix (ecReverse n a xs). +Definition ecAtBack : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (ix : Type), forall (_1 : PFin n), forall (_2 : PIntegral ix), forall (_3 : seq n a), forall (_4 : ix), a := + fun (n : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (ix : Type) (pn : PFin n) (pix : PIntegral ix) (xs : seq n a) => ecAt n a ix pix (ecReverse n a pn xs). -Definition ecFromTo : forall (first : Num), forall (last : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcSub last first)) a := - finNumRec (fun (first : Num) => forall (last : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcSub last first)) a) (fun (first : Init.Datatypes.nat) => finNumRec (fun (last : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcSub last (TCNum first))) a) (fun (last : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pa : PLiteral a) => SAWCoreVectorsAsRocqVectors.gen (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) (SAWCoreScaffolding.subNat last first)) a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.addNat i first)))). +Definition ecFromTo : forall (first : Num), forall (last : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PFin last), forall (_2 : PGeq last first), forall (_3 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcSub last first)) a := + fun (first : Num) (last : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (plast : PFin last) (pgeq : PGeq last first) (pa : PLiteral a) => PFinNumRec first (PFin_downward_closed last first pgeq plast) (fun (first1 : Num) => seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcSub last first1)) a) (fun (first1 : Init.Datatypes.nat) => PFinNumRec last plast (fun (last1 : Num) => seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcSub last1 (TCNum first1))) a) (fun (last1 : Init.Datatypes.nat) => SAWCoreVectorsAsRocqVectors.gen (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) (SAWCoreScaffolding.subNat last1 first1)) a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.addNat i first1)))). -Definition ecFromToLessThan : forall (first : Num), forall (bound : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PLiteralLessThan a), seq (tcSub bound first) a := - fun (first : Num) (bound : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) => finNumRec (fun (first1 : Num) => forall (_1 : PLiteralLessThan a), seq (tcSub bound first1) a) (fun (first1 : Init.Datatypes.nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (bound1 : Num) => forall (_1 : PLiteralLessThan a), seq (tcSub bound1 (TCNum first1)) a) (fun (bound1 : Init.Datatypes.nat) (pa : PLiteralLessThan a) => SAWCoreVectorsAsRocqVectors.gen (SAWCoreScaffolding.subNat bound1 first1) a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.addNat i first1))) (fun (pa : PLiteralLessThan a) => SAWCorePrelude.MkStream a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.addNat i first1))) bound) first. +Definition ecFromToLessThan : forall (first : Num), forall (bound : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PFin first), forall (_2 : PGeq bound first), forall (_3 : PLiteralLessThan a), seq (tcSub bound first) a := + fun (first : Num) (bound : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pfirst : PFin first) (_pgeq : PGeq bound first) => PFinNumRec first pfirst (fun (first1 : Num) => forall (_1 : PLiteralLessThan a), seq (tcSub bound first1) a) (fun (first1 : Init.Datatypes.nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (bound1 : Num) => forall (_1 : PLiteralLessThan a), seq (tcSub bound1 (TCNum first1)) a) (fun (bound1 : Init.Datatypes.nat) (pa : PLiteralLessThan a) => SAWCoreVectorsAsRocqVectors.gen (SAWCoreScaffolding.subNat bound1 first1) a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.addNat i first1))) (fun (pa : PLiteralLessThan a) => SAWCorePrelude.MkStream a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.addNat i first1))) bound). -Definition ecFromThenTo : forall (first : Num), forall (next : Num), forall (last : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (len : Num), forall (_1 : PLiteral a), forall (_2 : PLiteral a), forall (_3 : PLiteral a), seq len a := - fun (first : Num) (next : Num) (_1 : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) => finNumRec (fun (len : Num) => forall (_2 : PLiteral a), forall (_3 : PLiteral a), forall (_4 : PLiteral a), seq len a) (fun (len : Init.Datatypes.nat) (pa : PLiteral a) (_2 : PLiteral a) (_3 : PLiteral a) => SAWCoreVectorsAsRocqVectors.gen len a (fun (i : Init.Datatypes.nat) => let var__0 := getFinNat first in - pa (SAWCoreScaffolding.subNat (SAWCoreScaffolding.addNat var__0 (SAWCoreScaffolding.mulNat i (getFinNat next))) (SAWCoreScaffolding.mulNat i var__0)))). +Definition ecFromThenTo : forall (first : Num), forall (next : Num), forall (last : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (len : Num), forall (_1 : PFin first), forall (_2 : PFin next), forall (_3 : PFin last), forall (_4 : PLiteral a), forall (_5 : PLiteral a), forall (_6 : PLiteral a), forall (_7 : PNeq first next), forall (_8 : @Init.Logic.eq Num (tcLenFromThenTo first next last) len), seq len a := + fun (first : Num) (next : Num) (last : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (len : Num) (pf : PFin first) (pn : PFin next) (pl : PFin last) (pa : PLiteral a) (_1 : PLiteral a) (_2 : PLiteral a) (_pneq : PNeq first next) => PFinNumRec first pf (fun (first1 : Num) => forall (_3 : @Init.Logic.eq Num (tcLenFromThenTo first1 next last) len), seq len a) (fun (first1 : Init.Datatypes.nat) => PFinNumRec next pn (fun (next1 : Num) => forall (_3 : @Init.Logic.eq Num (tcLenFromThenTo (TCNum first1) next1 last) len), seq len a) (fun (next1 : Init.Datatypes.nat) => PFinNumRec last pl (fun (last1 : Num) => forall (_3 : @Init.Logic.eq Num (tcLenFromThenTo (TCNum first1) (TCNum next1) last1) len), seq len a) (fun (last1 : Init.Datatypes.nat) (eq : @Init.Logic.eq Num (TCNum (tcLenFromThenTo_Nat first1 next1 last1)) len) => let var__0 := tcLenFromThenTo_Nat first1 next1 last1 in + SAWCoreScaffolding.coerce (SAWCoreVectorsAsRocqVectors.Vec var__0 a) (seq len a) (seq_cong1 (TCNum var__0) len a eq) (SAWCoreVectorsAsRocqVectors.gen var__0 a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.subNat (SAWCoreScaffolding.addNat first1 (SAWCoreScaffolding.mulNat i next1)) (SAWCoreScaffolding.mulNat i first1))))))). -Definition ecFromToBy : forall (first : Num), forall (last : Num), forall (stride : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (tcSub last first) stride)) a := - finNumRec (fun (first : Num) => forall (last : Num), forall (stride : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (tcSub last first) stride)) a) (fun (first : Init.Datatypes.nat) => finNumRec (fun (last : Num) => forall (stride : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (tcSub last (TCNum first)) stride)) a) (fun (last : Init.Datatypes.nat) => finNumRec (fun (stride : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (TCNum (SAWCoreScaffolding.subNat last first)) stride)) a) (fun (stride : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pa : PLiteral a) => SAWCoreVectorsAsRocqVectors.gen (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) (SAWCorePrelude.divNat (SAWCoreScaffolding.subNat last first) stride)) a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.addNat first (SAWCoreScaffolding.mulNat i stride)))))). +Definition ecFromToBy : forall (first : Num), forall (last : Num), forall (stride : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PFin last), forall (_2 : PFin stride), forall (_3 : PGeq stride (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))), forall (_4 : PGeq last first), forall (_5 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (tcSub last first) stride)) a := + fun (first : Num) (last : Num) (stride : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (plast : PFin last) (pstride : PFin stride) (_1 : PGeq stride (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))) (pgeqlf : PGeq last first) (pa : PLiteral a) => PFinNumRec first (PFin_downward_closed last first pgeqlf plast) (fun (first1 : Num) => seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (tcSub last first1) stride)) a) (fun (first1 : Init.Datatypes.nat) => PFinNumRec last plast (fun (last1 : Num) => seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (tcSub last1 (TCNum first1)) stride)) a) (fun (last1 : Init.Datatypes.nat) => PFinNumRec stride pstride (fun (stride1 : Num) => seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (TCNum (SAWCoreScaffolding.subNat last1 first1)) stride1)) a) (fun (stride1 : Init.Datatypes.nat) => SAWCoreVectorsAsRocqVectors.gen (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) (SAWCorePrelude.divNat (SAWCoreScaffolding.subNat last1 first1) stride1)) a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.addNat first1 (SAWCoreScaffolding.mulNat i stride1)))))). -Definition ecFromToByLessThan : forall (first : Num), forall (bound : Num), forall (stride : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PLiteralLessThan a), seq (tcCeilDiv (tcSub bound first) stride) a := - finNumRec (fun (first : Num) => forall (bound : Num), forall (stride : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteralLessThan a), seq (tcCeilDiv (tcSub bound first) stride) a) (fun (first : Init.Datatypes.nat) => CryptolPrimitivesForSAWCore.Num__rec (fun (bound : Num) => forall (stride : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteralLessThan a), seq (tcCeilDiv (tcSub bound (TCNum first)) stride) a) (fun (bound : Init.Datatypes.nat) => finNumRec (fun (stride : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteralLessThan a), seq (tcCeilDiv (TCNum (SAWCoreScaffolding.subNat bound first)) stride) a) (fun (stride : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pa : PLiteralLessThan a) => SAWCoreVectorsAsRocqVectors.gen (ceilDivNat (SAWCoreScaffolding.subNat bound first) stride) a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.addNat first (SAWCoreScaffolding.mulNat i stride))))) (finNumRec (fun (stride : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteralLessThan a), seq (tcCeilDiv TCInf stride) a) (fun (stride : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pa : PLiteralLessThan a) => SAWCorePrelude.MkStream a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.addNat first (SAWCoreScaffolding.mulNat i stride)))))). +Definition ecFromToByLessThan : forall (first : Num), forall (bound : Num), forall (stride : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PFin first), forall (_2 : PFin stride), forall (_3 : PGeq stride (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))), forall (_4 : PGeq bound first), forall (_5 : PLiteralLessThan a), seq (tcCeilDiv (tcSub bound first) stride) a := + fun (first : Num) (bound : Num) (stride : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pfirst : PFin first) (pstride : PFin stride) (_1 : PGeq stride (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))) (_2 : PGeq bound first) (pa : PLiteralLessThan a) => PFinNumRec first pfirst (fun (first1 : Num) => seq (tcCeilDiv (tcSub bound first1) stride) a) (fun (first1 : Init.Datatypes.nat) => PFinNumRec stride pstride (fun (stride1 : Num) => seq (tcCeilDiv (tcSub bound (TCNum first1)) stride1) a) (fun (stride1 : Init.Datatypes.nat) => CryptolPrimitivesForSAWCore.Num__rec (fun (bound1 : Num) => seq (tcCeilDiv (tcSub bound1 (TCNum first1)) (TCNum stride1)) a) (fun (bound1 : Init.Datatypes.nat) => SAWCoreVectorsAsRocqVectors.gen (ceilDivNat (SAWCoreScaffolding.subNat bound1 first1) stride1) a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.addNat first1 (SAWCoreScaffolding.mulNat i stride1)))) (SAWCorePrelude.MkStream a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.addNat first1 (SAWCoreScaffolding.mulNat i stride1)))) bound)). -Definition ecFromToDownBy : forall (first : Num), forall (last : Num), forall (stride : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (tcSub first last) stride)) a := - finNumRec (fun (first : Num) => forall (last : Num), forall (stride : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (tcSub first last) stride)) a) (fun (first : Init.Datatypes.nat) => finNumRec (fun (last : Num) => forall (stride : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (tcSub (TCNum first) last) stride)) a) (fun (last : Init.Datatypes.nat) => finNumRec (fun (stride : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (TCNum (SAWCoreScaffolding.subNat first last)) stride)) a) (fun (stride : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pa : PLiteral a) => SAWCoreVectorsAsRocqVectors.gen (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) (SAWCorePrelude.divNat (SAWCoreScaffolding.subNat first last) stride)) a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.subNat first (SAWCoreScaffolding.mulNat i stride)))))). +Definition ecFromToDownBy : forall (first : Num), forall (last : Num), forall (stride : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PFin first), forall (_2 : PFin stride), forall (_3 : PGeq stride (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))), forall (_4 : PGeq first last), forall (_5 : PLiteral a), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (tcSub first last) stride)) a := + fun (first : Num) (last : Num) (stride : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pfirst : PFin first) (pstride : PFin stride) (_1 : PGeq stride (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))) (pgeqfl : PGeq first last) (pa : PLiteral a) => PFinNumRec last (PFin_downward_closed first last pgeqfl pfirst) (fun (last1 : Num) => seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (tcSub first last1) stride)) a) (fun (last1 : Init.Datatypes.nat) => PFinNumRec first pfirst (fun (first1 : Num) => seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (tcSub first1 (TCNum last1)) stride)) a) (fun (first1 : Init.Datatypes.nat) => PFinNumRec stride pstride (fun (stride1 : Num) => seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcDiv (TCNum (SAWCoreScaffolding.subNat first1 last1)) stride1)) a) (fun (stride1 : Init.Datatypes.nat) => SAWCoreVectorsAsRocqVectors.gen (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) (SAWCorePrelude.divNat (SAWCoreScaffolding.subNat first1 last1) stride1)) a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.subNat first1 (SAWCoreScaffolding.mulNat i stride1)))))). -Definition ecFromToDownByGreaterThan : forall (first : Num), forall (bound : Num), forall (stride : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PLiteral a), seq (tcCeilDiv (tcSub first bound) stride) a := - finNumRec (fun (first : Num) => forall (bound : Num), forall (stride : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteral a), seq (tcCeilDiv (tcSub first bound) stride) a) (fun (first : Init.Datatypes.nat) => finNumRec (fun (bound : Num) => forall (stride : Num), forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteral a), seq (tcCeilDiv (tcSub (TCNum first) bound) stride) a) (fun (bound : Init.Datatypes.nat) => finNumRec (fun (stride : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (_1 : PLiteral a), seq (tcCeilDiv (TCNum (SAWCoreScaffolding.subNat first bound)) stride) a) (fun (stride : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pa : PLiteral a) => SAWCoreVectorsAsRocqVectors.gen (ceilDivNat (SAWCoreScaffolding.subNat first bound) stride) a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.subNat first (SAWCoreScaffolding.mulNat i stride)))))). +Definition ecFromToDownByGreaterThan : forall (first : Num), forall (bound : Num), forall (stride : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : PFin first), forall (_2 : PFin stride), forall (_3 : PGeq stride (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))), forall (_4 : PGeq first bound), forall (_5 : PLiteral a), seq (tcCeilDiv (tcSub first bound) stride) a := + fun (first : Num) (bound : Num) (stride : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (pfirst : PFin first) (pstride : PFin stride) (_1 : PGeq stride (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))) (pgeqfb : PGeq first bound) (pa : PLiteral a) => PFinNumRec bound (PFin_downward_closed first bound pgeqfb pfirst) (fun (bound1 : Num) => seq (tcCeilDiv (tcSub first bound1) stride) a) (fun (bound1 : Init.Datatypes.nat) => PFinNumRec first pfirst (fun (first1 : Num) => seq (tcCeilDiv (tcSub first1 (TCNum bound1)) stride) a) (fun (first1 : Init.Datatypes.nat) => PFinNumRec stride pstride (fun (stride1 : Num) => seq (tcCeilDiv (TCNum (SAWCoreScaffolding.subNat first1 bound1)) stride1) a) (fun (stride1 : Init.Datatypes.nat) => SAWCoreVectorsAsRocqVectors.gen (ceilDivNat (SAWCoreScaffolding.subNat first1 bound1) stride1) a (fun (i : Init.Datatypes.nat) => pa (SAWCoreScaffolding.subNat first1 (SAWCoreScaffolding.mulNat i stride1)))))). Definition ecInfFrom : forall (a : Type), forall (_1 : PIntegral a), forall (_2 : a), seq TCInf a := fun (a : Type) (pa : PIntegral a) (x : a) => SAWCorePrelude.MkStream a (fun (i : Init.Datatypes.nat) => let var__0 := @SAWCoreScaffolding.recordHead "integralRing"%string (PRing a) (SAWCoreScaffolding.RecordTypeCons "div"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mod"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "toInt"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "posneg"%string (forall (_1 : a), Init.Datatypes.sum Init.Datatypes.nat Init.Datatypes.nat) SAWCoreScaffolding.RecordTypeNil)))) pa in @@ -771,14 +810,14 @@ Definition ecInfFromThen : forall (a : Type), forall (_1 : PIntegral a), forall fun (a : Type) (pa : PIntegral a) (x : a) (y : a) => SAWCorePrelude.MkStream a (fun (i : Init.Datatypes.nat) => let var__0 := @SAWCoreScaffolding.recordHead "integralRing"%string (PRing a) (SAWCoreScaffolding.RecordTypeCons "div"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mod"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "toInt"%string (forall (_1 : a), SAWCoreScaffolding.Integer) (SAWCoreScaffolding.RecordTypeCons "posneg"%string (forall (_1 : a), Init.Datatypes.sum Init.Datatypes.nat Init.Datatypes.nat) SAWCoreScaffolding.RecordTypeNil)))) pa in @SAWCoreScaffolding.recordHead "add"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil)))) (@SAWCoreScaffolding.recordTail "ringZero"%string (PZero a) (SAWCoreScaffolding.RecordTypeCons "add"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil))))) var__0) x (@SAWCoreScaffolding.recordHead "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil)) (@SAWCoreScaffolding.recordTail "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil))) (@SAWCoreScaffolding.recordTail "add"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil)))) (@SAWCoreScaffolding.recordTail "ringZero"%string (PZero a) (SAWCoreScaffolding.RecordTypeCons "add"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil))))) var__0))) (@SAWCoreScaffolding.recordHead "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil))) (@SAWCoreScaffolding.recordTail "add"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil)))) (@SAWCoreScaffolding.recordTail "ringZero"%string (PZero a) (SAWCoreScaffolding.RecordTypeCons "add"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil))))) var__0)) y x) (@SAWCoreScaffolding.recordHead "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil (@SAWCoreScaffolding.recordTail "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil) (@SAWCoreScaffolding.recordTail "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil)) (@SAWCoreScaffolding.recordTail "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil))) (@SAWCoreScaffolding.recordTail "add"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil)))) (@SAWCoreScaffolding.recordTail "ringZero"%string (PZero a) (SAWCoreScaffolding.RecordTypeCons "add"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "sub"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "mul"%string (forall (_1 : a), forall (_2 : a), a) (SAWCoreScaffolding.RecordTypeCons "neg"%string (forall (_1 : a), a) (SAWCoreScaffolding.RecordTypeCons "int"%string (forall (_1 : SAWCoreScaffolding.Integer), a) SAWCoreScaffolding.RecordTypeNil))))) var__0))))) (SAWCoreScaffolding.natToInt i)))). -Definition ecError : forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (len : Num), forall (_1 : seq len (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) Init.Datatypes.bool)), a := - fun (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) => finNumRec (fun (len : Num) => forall (_1 : seq len (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) Init.Datatypes.bool)), a) (fun (len : Init.Datatypes.nat) (msg : SAWCoreVectorsAsRocqVectors.Vec len (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) Init.Datatypes.bool)) => SAWCoreScaffolding.error a (SAWCoreScaffolding.appendString "encountered call to the Cryptol 'error' function: "%string (SAWCorePrelude.bytesToString len msg))). +Definition ecError : forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (len : Num), forall (_1 : PFin len), forall (_2 : seq len (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) Init.Datatypes.bool)), a := + fun (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (len : Num) (plen : PFin len) => PFinNumRec len plen (fun (len1 : Num) => forall (_1 : seq len1 (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) Init.Datatypes.bool)), a) (fun (len1 : Init.Datatypes.nat) (msg : SAWCoreVectorsAsRocqVectors.Vec len1 (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) Init.Datatypes.bool)) => SAWCoreScaffolding.error a (SAWCoreScaffolding.appendString "encountered call to the Cryptol 'error' function: "%string (SAWCorePrelude.bytesToString len1 msg))). Definition ecRandom : forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (_1 : SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))))) Init.Datatypes.bool), a := fun (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (_1 : SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))))) Init.Datatypes.bool) => SAWCoreScaffolding.error a "Cryptol.random"%string. -Definition ecTrace : forall (n : Num), forall (a : Type), forall (b : Type), forall (_1 : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) Init.Datatypes.bool)), forall (_2 : a), forall (_3 : b), b := - fun (n : Num) (a : Type) (b : Type) (_1 : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) Init.Datatypes.bool)) (_2 : a) (x : b) => x. +Definition ecTrace : forall (n : Num), forall (a : Type), forall (b : Type), forall (_1 : PFin n), forall (_2 : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) Init.Datatypes.bool)), forall (_3 : a), forall (_4 : b), b := + fun (n : Num) (a : Type) (b : Type) (_1 : PFin n) (_2 : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) Init.Datatypes.bool)) (_3 : a) (x : b) => x. Definition ecDeepseq : forall (a : Type), forall (b : Type), forall (_1 : PEq a), forall (_2 : a), forall (_3 : b), b := fun (a : Type) (b : Type) (pa : PEq a) (x : a) (y : b) => y. @@ -786,11 +825,11 @@ Definition ecDeepseq : forall (a : Type), forall (b : Type), forall (_1 : PEq a) Definition ecParmap : forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (b : Type), forall {Inh_b : SAWCoreScaffolding.Inhabited b}, forall (n : Num), forall (_1 : PEq b), forall (_2 : forall (_2 : a), b), forall (_3 : seq n a), seq n b := fun (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (b : Type) (Inh_b : SAWCoreScaffolding.Inhabited b) (n : Num) (pb : PEq b) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (_1 : forall (_1 : a), b), forall (_2 : seq n1 a), seq n1 b) (fun (n1 : Init.Datatypes.nat) (f : forall (_1 : a), b) (xs : SAWCoreVectorsAsRocqVectors.Vec n1 a) => SAWCorePrelude.map a b f n1 xs) (fun (f : forall (_1 : a), b) (xs : SAWCorePrelude.Stream a) => SAWCoreScaffolding.error (SAWCorePrelude.Stream b) "Unexpected infinite stream in parmap"%string) n. -Definition ecFoldl : forall (n : Num), forall (a : Type), forall (b : Type), forall {Inh_b : SAWCoreScaffolding.Inhabited b}, forall (_1 : forall (_1 : a), forall (_2 : b), a), forall (_2 : a), forall (_3 : seq n b), a := - fun (n : Num) (a : Type) (b : Type) (Inh_b : SAWCoreScaffolding.Inhabited b) (f : forall (_1 : a), forall (_2 : b), a) (z : a) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (_1 : seq n1 b), a) (fun (n1 : Init.Datatypes.nat) (xs : SAWCoreVectorsAsRocqVectors.Vec n1 b) => SAWCoreVectorsAsRocqVectors.foldl b a n1 f z xs) (fun (xs : SAWCorePrelude.Stream b) => SAWCoreScaffolding.error a "Unexpected infinite stream in foldl"%string) n. +Definition ecFoldl : forall (n : Num), forall (a : Type), forall (b : Type), forall {Inh_b : SAWCoreScaffolding.Inhabited b}, forall (_1 : PFin n), forall (_2 : forall (_2 : a), forall (_3 : b), a), forall (_3 : a), forall (_4 : seq n b), a := + fun (n : Num) (a : Type) (b : Type) (Inh_b : SAWCoreScaffolding.Inhabited b) (pn : PFin n) (f : forall (_1 : a), forall (_2 : b), a) (z : a) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 b), a) (fun (n1 : Init.Datatypes.nat) => SAWCoreVectorsAsRocqVectors.foldl b a n1 f z). -Definition ecFoldlPrime : forall (n : Num), forall (a : Type), forall (b : Type), forall {Inh_b : SAWCoreScaffolding.Inhabited b}, forall (_1 : PEq a), forall (_2 : forall (_2 : a), forall (_3 : b), a), forall (_3 : a), forall (_4 : seq n b), a := - fun (n : Num) (a : Type) (b : Type) (Inh_b : SAWCoreScaffolding.Inhabited b) (pa : PEq a) => ecFoldl n a b. +Definition ecFoldlPrime : forall (n : Num), forall (a : Type), forall (b : Type), forall {Inh_b : SAWCoreScaffolding.Inhabited b}, forall (_1 : PFin n), forall (_2 : PEq a), forall (_3 : forall (_3 : a), forall (_4 : b), a), forall (_4 : a), forall (_5 : seq n b), a := + fun (n : Num) (a : Type) (b : Type) (Inh_b : SAWCoreScaffolding.Inhabited b) (pn : PFin n) (pa : PEq a) => ecFoldl n a b pn. Definition ecScanl : forall (n : Num), forall (a : Type), forall (b : Type), forall (_1 : forall (_1 : a), forall (_2 : b), a), forall (_2 : a), forall (_3 : seq n b), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) n) a := fun (n : Num) (a : Type) (b : Type) (f : forall (_1 : a), forall (_2 : b), a) (z : a) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (_1 : seq n1 b), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) n1) a) (fun (n1 : Init.Datatypes.nat) (xs : SAWCoreVectorsAsRocqVectors.Vec n1 b) => SAWCoreVectorsAsRocqVectors.scanl b a n1 f z xs) (fun (xs : SAWCorePrelude.Stream b) => SAWCorePreludeExtra.streamScanl b a f z xs) n. @@ -889,29 +928,29 @@ Definition fpSqrt : forall (e : Num), forall (p : Num), forall (_1 : SAWCoreVect Definition ecUpdate : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (ix : Type), forall (_1 : PIntegral ix), forall (_2 : seq n a), forall (_3 : ix), forall (_4 : a), seq n a := fun (n : Num) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (ix : Type), forall (_1 : PIntegral ix), forall (_2 : seq n1 a), forall (_3 : ix), forall (_4 : a), seq n1 a) (fun (n1 : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (ix : Type) (pix : PIntegral ix) (xs : SAWCoreVectorsAsRocqVectors.Vec n1 a) => posNegCases ix pix (forall (_1 : a), SAWCoreVectorsAsRocqVectors.Vec n1 a) (SAWCorePrelude.upd n1 a xs) (fun (_1 : Init.Datatypes.nat) (_2 : a) => xs)) (fun (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (ix : Type) (pix : PIntegral ix) (xs : SAWCorePrelude.Stream a) => posNegCases ix pix (forall (_1 : a), SAWCorePrelude.Stream a) (SAWCorePrelude.streamUpd a xs) (fun (_1 : Init.Datatypes.nat) (_2 : a) => xs)) n. -Definition ecUpdateEnd : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (ix : Type), forall (_1 : PIntegral ix), forall (_2 : seq n a), forall (_3 : ix), forall (_4 : a), seq n a := - finNumRec (fun (n : Num) => forall (a : Type), forall (Inh_a : SAWCoreScaffolding.Inhabited a), forall (ix : Type), forall (_1 : PIntegral ix), forall (_2 : seq n a), forall (_3 : ix), forall (_4 : a), seq n a) (fun (n : Init.Datatypes.nat) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (ix : Type) (pix : PIntegral ix) (xs : SAWCoreVectorsAsRocqVectors.Vec n a) => posNegCases ix pix (forall (_1 : a), SAWCoreVectorsAsRocqVectors.Vec n a) (fun (i : Init.Datatypes.nat) => SAWCorePrelude.upd n a xs (SAWCoreScaffolding.subNat (SAWCoreScaffolding.subNat n (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) i)) (fun (_1 : Init.Datatypes.nat) (_2 : a) => xs)). +Definition ecUpdateEnd : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (ix : Type), forall (_1 : PFin n), forall (_2 : PIntegral ix), forall (_3 : seq n a), forall (_4 : ix), forall (_5 : a), seq n a := + fun (n : Num) (a : Type) (Inh_a : SAWCoreScaffolding.Inhabited a) (ix : Type) (pn : PFin n) (pix : PIntegral ix) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 a), forall (_2 : ix), forall (_3 : a), seq n1 a) (fun (n1 : Init.Datatypes.nat) (xs : SAWCoreVectorsAsRocqVectors.Vec n1 a) => posNegCases ix pix (forall (_1 : a), SAWCoreVectorsAsRocqVectors.Vec n1 a) (fun (i : Init.Datatypes.nat) => SAWCorePrelude.upd n1 a xs (SAWCoreScaffolding.subNat (SAWCoreScaffolding.subNat n1 (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) i)) (fun (_1 : Init.Datatypes.nat) (_2 : a) => xs)). -Definition ecTrunc : forall (m : Num), forall (n : Num), forall (_1 : seq (tcAdd m n) Init.Datatypes.bool), seq n Init.Datatypes.bool := - finNumRec2 (fun (m : Num) (n : Num) => forall (_1 : seq (tcAdd m n) Init.Datatypes.bool), seq n Init.Datatypes.bool) SAWCorePrelude.bvTrunc. +Definition ecTrunc : forall (m : Num), forall (n : Num), forall (_1 : PFin m), forall (_2 : PFin n), forall (_3 : seq (tcAdd m n) Init.Datatypes.bool), seq n Init.Datatypes.bool := + fun (m : Num) (n : Num) (pm : PFin m) (pn : PFin n) => PFinNumRec m pm (fun (m1 : Num) => forall (_1 : seq (tcAdd m1 n) Init.Datatypes.bool), seq n Init.Datatypes.bool) (fun (m1 : Init.Datatypes.nat) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq (tcAdd (TCNum m1) n1) Init.Datatypes.bool), seq n1 Init.Datatypes.bool) (fun (n1 : Init.Datatypes.nat) => SAWCorePrelude.bvTrunc m1 n1)). -Definition ecUExt : forall (m : Num), forall (n : Num), forall (_1 : seq n Init.Datatypes.bool), seq (tcAdd m n) Init.Datatypes.bool := - finNumRec2 (fun (m : Num) (n : Num) => forall (_1 : seq n Init.Datatypes.bool), seq (tcAdd m n) Init.Datatypes.bool) SAWCorePrelude.bvUExt. +Definition ecUExt : forall (m : Num), forall (n : Num), forall (_1 : PFin m), forall (_2 : PFin n), forall (_3 : seq n Init.Datatypes.bool), seq (tcAdd m n) Init.Datatypes.bool := + fun (m : Num) (n : Num) (pm : PFin m) (pn : PFin n) => PFinNumRec m pm (fun (m1 : Num) => forall (_1 : seq n Init.Datatypes.bool), seq (tcAdd m1 n) Init.Datatypes.bool) (fun (m1 : Init.Datatypes.nat) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), seq (tcAdd (TCNum m1) n1) Init.Datatypes.bool) (fun (n1 : Init.Datatypes.nat) => SAWCorePrelude.bvUExt m1 n1)). -Definition ecSExt : forall (m : Num), forall (n : Num), forall (_1 : seq n Init.Datatypes.bool), seq (tcAdd m n) Init.Datatypes.bool := - finNumRec2 (fun (m : Num) (n : Num) => forall (_1 : seq n Init.Datatypes.bool), seq (tcAdd m n) Init.Datatypes.bool) (fun (m : Init.Datatypes.nat) (n : Init.Datatypes.nat) => SAWCorePrelude.natCase (fun (n' : Init.Datatypes.nat) => forall (_1 : SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec (SAWCoreScaffolding.addNat m n') Init.Datatypes.bool) (fun (_1 : SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool) => SAWCoreVectorsAsRocqVectors.bvNat (SAWCoreScaffolding.addNat m SAWCoreScaffolding.Zero) SAWCoreScaffolding.Zero) (SAWCorePrelude.bvSExt m) n). +Definition ecSExt : forall (m : Num), forall (n : Num), forall (_1 : PFin m), forall (_2 : PFin n), forall (_3 : PGeq n (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))), forall (_4 : seq n Init.Datatypes.bool), seq (tcAdd m n) Init.Datatypes.bool := + fun (m : Num) (n : Num) (pm : PFin m) (pn : PFin n) (_pgeq : PGeq n (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))) => PFinNumRec m pm (fun (m1 : Num) => forall (_1 : seq n Init.Datatypes.bool), seq (tcAdd m1 n) Init.Datatypes.bool) (fun (m1 : Init.Datatypes.nat) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), seq (tcAdd (TCNum m1) n1) Init.Datatypes.bool) (fun (n1 : Init.Datatypes.nat) => SAWCorePrelude.natCase (fun (n' : Init.Datatypes.nat) => forall (_1 : SAWCoreVectorsAsRocqVectors.Vec n' Init.Datatypes.bool), SAWCoreVectorsAsRocqVectors.Vec (SAWCoreScaffolding.addNat m1 n') Init.Datatypes.bool) (fun (_1 : SAWCoreVectorsAsRocqVectors.Vec SAWCoreScaffolding.Zero Init.Datatypes.bool) => SAWCoreVectorsAsRocqVectors.bvNat (SAWCoreScaffolding.addNat m1 SAWCoreScaffolding.Zero) SAWCoreScaffolding.Zero) (SAWCorePrelude.bvSExt m1) n1)). -Definition ecSgt : forall (n : Num), forall (_1 : seq n Init.Datatypes.bool), forall (_2 : seq n Init.Datatypes.bool), Init.Datatypes.bool := - finNumRec (fun (n : Num) => forall (_1 : seq n Init.Datatypes.bool), forall (_2 : seq n Init.Datatypes.bool), Init.Datatypes.bool) SAWCoreVectorsAsRocqVectors.bvsgt. +Definition ecSgt : forall (n : Num), forall (_1 : PFin n), forall (_2 : seq n Init.Datatypes.bool), forall (_3 : seq n Init.Datatypes.bool), Init.Datatypes.bool := + fun (n : Num) (pn : PFin n) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), forall (_2 : seq n1 Init.Datatypes.bool), Init.Datatypes.bool) SAWCoreVectorsAsRocqVectors.bvsgt. -Definition ecSge : forall (n : Num), forall (_1 : seq n Init.Datatypes.bool), forall (_2 : seq n Init.Datatypes.bool), Init.Datatypes.bool := - finNumRec (fun (n : Num) => forall (_1 : seq n Init.Datatypes.bool), forall (_2 : seq n Init.Datatypes.bool), Init.Datatypes.bool) SAWCoreVectorsAsRocqVectors.bvsge. +Definition ecSge : forall (n : Num), forall (_1 : PFin n), forall (_2 : seq n Init.Datatypes.bool), forall (_3 : seq n Init.Datatypes.bool), Init.Datatypes.bool := + fun (n : Num) (pn : PFin n) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), forall (_2 : seq n1 Init.Datatypes.bool), Init.Datatypes.bool) SAWCoreVectorsAsRocqVectors.bvsge. -Definition ecSlt : forall (n : Num), forall (_1 : seq n Init.Datatypes.bool), forall (_2 : seq n Init.Datatypes.bool), Init.Datatypes.bool := - finNumRec (fun (n : Num) => forall (_1 : seq n Init.Datatypes.bool), forall (_2 : seq n Init.Datatypes.bool), Init.Datatypes.bool) SAWCoreVectorsAsRocqVectors.bvslt. +Definition ecSlt : forall (n : Num), forall (_1 : PFin n), forall (_2 : seq n Init.Datatypes.bool), forall (_3 : seq n Init.Datatypes.bool), Init.Datatypes.bool := + fun (n : Num) (pn : PFin n) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), forall (_2 : seq n1 Init.Datatypes.bool), Init.Datatypes.bool) SAWCoreVectorsAsRocqVectors.bvslt. -Definition ecSle : forall (n : Num), forall (_1 : seq n Init.Datatypes.bool), forall (_2 : seq n Init.Datatypes.bool), Init.Datatypes.bool := - finNumRec (fun (n : Num) => forall (_1 : seq n Init.Datatypes.bool), forall (_2 : seq n Init.Datatypes.bool), Init.Datatypes.bool) SAWCoreVectorsAsRocqVectors.bvsle. +Definition ecSle : forall (n : Num), forall (_1 : PFin n), forall (_2 : seq n Init.Datatypes.bool), forall (_3 : seq n Init.Datatypes.bool), Init.Datatypes.bool := + fun (n : Num) (pn : PFin n) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : seq n1 Init.Datatypes.bool), forall (_2 : seq n1 Init.Datatypes.bool), Init.Datatypes.bool) SAWCoreVectorsAsRocqVectors.bvsle. Definition ecArrayConstant : forall (a : Type), forall (b : Type), forall (_1 : b), SAWCorePrelude.Array a b := SAWCorePrelude.arrayConstant. @@ -922,31 +961,31 @@ Definition ecArrayLookup : forall (a : Type), forall (b : Type), forall (_1 : SA Definition ecArrayUpdate : forall (a : Type), forall (b : Type), forall (_1 : SAWCorePrelude.Array a b), forall (_2 : a), forall (_3 : b), SAWCorePrelude.Array a b := SAWCorePrelude.arrayUpdate. -Definition ecArrayCopy : forall (n : Num), forall (a : Type), forall (_1 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_2 : seq n Init.Datatypes.bool), forall (_3 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_4 : seq n Init.Datatypes.bool), forall (_5 : seq n Init.Datatypes.bool), SAWCorePrelude.Array (seq n Init.Datatypes.bool) a := - finNumRec (fun (n : Num) => forall (a : Type), forall (_1 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_2 : seq n Init.Datatypes.bool), forall (_3 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_4 : seq n Init.Datatypes.bool), forall (_5 : seq n Init.Datatypes.bool), SAWCorePrelude.Array (seq n Init.Datatypes.bool) a) SAWCorePrelude.arrayCopy. +Definition ecArrayCopy : forall (n : Num), forall (a : Type), forall (_1 : PFin n), forall (_2 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_3 : seq n Init.Datatypes.bool), forall (_4 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_5 : seq n Init.Datatypes.bool), forall (_6 : seq n Init.Datatypes.bool), SAWCorePrelude.Array (seq n Init.Datatypes.bool) a := + fun (n : Num) (a : Type) (pn : PFin n) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : SAWCorePrelude.Array (seq n1 Init.Datatypes.bool) a), forall (_2 : seq n1 Init.Datatypes.bool), forall (_3 : SAWCorePrelude.Array (seq n1 Init.Datatypes.bool) a), forall (_4 : seq n1 Init.Datatypes.bool), forall (_5 : seq n1 Init.Datatypes.bool), SAWCorePrelude.Array (seq n1 Init.Datatypes.bool) a) (fun (n1 : Init.Datatypes.nat) => SAWCorePrelude.arrayCopy n1 a). Definition ecArrayEq : forall (n : Num), forall (a : Type), forall (_1 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_2 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), Init.Datatypes.bool := - finNumRec (fun (n : Num) => forall (a : Type), forall (_1 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_2 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), Init.Datatypes.bool) (fun (n : Init.Datatypes.nat) => SAWCorePrelude.arrayEq (SAWCoreVectorsAsRocqVectors.Vec n Init.Datatypes.bool)). + fun (n : Num) (a : Type) => SAWCorePrelude.arrayEq (seq n Init.Datatypes.bool) a. -Definition ecArraySet : forall (n : Num), forall (a : Type), forall (_1 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_2 : seq n Init.Datatypes.bool), forall (_3 : a), forall (_4 : seq n Init.Datatypes.bool), SAWCorePrelude.Array (seq n Init.Datatypes.bool) a := - finNumRec (fun (n : Num) => forall (a : Type), forall (_1 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_2 : seq n Init.Datatypes.bool), forall (_3 : a), forall (_4 : seq n Init.Datatypes.bool), SAWCorePrelude.Array (seq n Init.Datatypes.bool) a) SAWCorePrelude.arraySet. +Definition ecArraySet : forall (n : Num), forall (a : Type), forall (_1 : PFin n), forall (_2 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_3 : seq n Init.Datatypes.bool), forall (_4 : a), forall (_5 : seq n Init.Datatypes.bool), SAWCorePrelude.Array (seq n Init.Datatypes.bool) a := + fun (n : Num) (a : Type) (pn : PFin n) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : SAWCorePrelude.Array (seq n1 Init.Datatypes.bool) a), forall (_2 : seq n1 Init.Datatypes.bool), forall (_3 : a), forall (_4 : seq n1 Init.Datatypes.bool), SAWCorePrelude.Array (seq n1 Init.Datatypes.bool) a) (fun (n1 : Init.Datatypes.nat) => SAWCorePrelude.arraySet n1 a). -Definition ecArrayRangeEq : forall (n : Num), forall (a : Type), forall (_1 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_2 : seq n Init.Datatypes.bool), forall (_3 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_4 : seq n Init.Datatypes.bool), forall (_5 : seq n Init.Datatypes.bool), Init.Datatypes.bool := - finNumRec (fun (n : Num) => forall (a : Type), forall (_1 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_2 : seq n Init.Datatypes.bool), forall (_3 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_4 : seq n Init.Datatypes.bool), forall (_5 : seq n Init.Datatypes.bool), Init.Datatypes.bool) SAWCorePrelude.arrayRangeEq. +Definition ecArrayRangeEq : forall (n : Num), forall (a : Type), forall (_1 : PFin n), forall (_2 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_3 : seq n Init.Datatypes.bool), forall (_4 : SAWCorePrelude.Array (seq n Init.Datatypes.bool) a), forall (_5 : seq n Init.Datatypes.bool), forall (_6 : seq n Init.Datatypes.bool), Init.Datatypes.bool := + fun (n : Num) (a : Type) (pn : PFin n) => PFinNumRec n pn (fun (n1 : Num) => forall (_1 : SAWCorePrelude.Array (seq n1 Init.Datatypes.bool) a), forall (_2 : seq n1 Init.Datatypes.bool), forall (_3 : SAWCorePrelude.Array (seq n1 Init.Datatypes.bool) a), forall (_4 : seq n1 Init.Datatypes.bool), forall (_5 : seq n1 Init.Datatypes.bool), Init.Datatypes.bool) (fun (n1 : Init.Datatypes.nat) => SAWCorePrelude.arrayRangeEq n1 a). Definition addNat_1 : forall (n : Init.Datatypes.nat), @Init.Logic.eq Init.Datatypes.nat (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) n) (SAWCoreScaffolding.Succ n) := SAWCoreScaffolding.Nat__rec (fun (n : Init.Datatypes.nat) => @Init.Logic.eq Init.Datatypes.nat (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) n) (SAWCoreScaffolding.Succ n)) (@Init.Logic.eq_refl Init.Datatypes.nat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (fun (n : Init.Datatypes.nat) (ih : @Init.Logic.eq Init.Datatypes.nat (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) n) (SAWCoreScaffolding.Succ n)) => let var__0 := SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) n in let var__1 := SAWCoreScaffolding.Succ n in SAWCorePrelude.trans Init.Datatypes.nat (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) var__1) (SAWCoreScaffolding.Succ var__0) (SAWCoreScaffolding.Succ var__1) (SAWCoreScaffolding.eqNatAddS (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) n) (SAWCorePrelude.eqNatSucc var__0 var__1 ih)). -Definition ecPmult : forall (u : Num), forall (v : Num), forall (_1 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) u) Init.Datatypes.bool), forall (_2 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) v) Init.Datatypes.bool), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcAdd u v)) Init.Datatypes.bool := - finNumRec2 (fun (u : Num) (v : Num) => forall (_1 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) u) Init.Datatypes.bool), forall (_2 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) v) Init.Datatypes.bool), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcAdd u v)) Init.Datatypes.bool) (fun (u : Init.Datatypes.nat) (v : Init.Datatypes.nat) (x : SAWCoreVectorsAsRocqVectors.Vec (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) u) Init.Datatypes.bool) (y : SAWCoreVectorsAsRocqVectors.Vec (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) v) Init.Datatypes.bool) => let var__0 := SAWCoreScaffolding.addNat u v in +Definition ecPmult : forall (u : Num), forall (v : Num), forall (_1 : PFin u), forall (_2 : PFin v), forall (_3 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) u) Init.Datatypes.bool), forall (_4 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) v) Init.Datatypes.bool), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcAdd u v)) Init.Datatypes.bool := + fun (u : Num) (v : Num) (pu : PFin u) (pv : PFin v) => PFinNumRec u pu (fun (u1 : Num) => forall (_1 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) u1) Init.Datatypes.bool), forall (_2 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) v) Init.Datatypes.bool), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcAdd u1 v)) Init.Datatypes.bool) (fun (u1 : Init.Datatypes.nat) => PFinNumRec v pv (fun (v1 : Num) => forall (_1 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (TCNum u1)) Init.Datatypes.bool), forall (_2 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) v1) Init.Datatypes.bool), seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) (tcAdd (TCNum u1) v1)) Init.Datatypes.bool) (fun (v1 : Init.Datatypes.nat) (x : SAWCoreVectorsAsRocqVectors.Vec (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) u1) Init.Datatypes.bool) (y : SAWCoreVectorsAsRocqVectors.Vec (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) v1) Init.Datatypes.bool) => let var__0 := SAWCoreScaffolding.addNat u1 v1 in let var__1 := SAWCoreScaffolding.Succ var__0 in let var__2 := SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) var__0 in - SAWCoreVectorsAsRocqVectors.coerceVec Init.Datatypes.bool var__1 var__2 (SAWCorePrelude.sym Init.Datatypes.nat var__2 var__1 (addNat_1 var__0)) (SAWCorePrelude.polyMul u v (SAWCoreVectorsAsRocqVectors.coerceVec Init.Datatypes.bool (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) u) (SAWCoreScaffolding.Succ u) (addNat_1 u) x) (SAWCoreVectorsAsRocqVectors.coerceVec Init.Datatypes.bool (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) v) (SAWCoreScaffolding.Succ v) (addNat_1 v) y))). + SAWCoreVectorsAsRocqVectors.coerceVec Init.Datatypes.bool var__1 var__2 (SAWCorePrelude.sym Init.Datatypes.nat var__2 var__1 (addNat_1 var__0)) (SAWCorePrelude.polyMul u1 v1 (SAWCoreVectorsAsRocqVectors.coerceVec Init.Datatypes.bool (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) u1) (SAWCoreScaffolding.Succ u1) (addNat_1 u1) x) (SAWCoreVectorsAsRocqVectors.coerceVec Init.Datatypes.bool (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) v1) (SAWCoreScaffolding.Succ v1) (addNat_1 v1) y)))). -Definition ecPmod : forall (u : Num), forall (v : Num), forall (_1 : seq u Init.Datatypes.bool), forall (_2 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) v) Init.Datatypes.bool), seq v Init.Datatypes.bool := - finNumRec2 (fun (u : Num) (v : Num) => forall (_1 : seq u Init.Datatypes.bool), forall (_2 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) v) Init.Datatypes.bool), seq v Init.Datatypes.bool) (fun (u : Init.Datatypes.nat) (v : Init.Datatypes.nat) (x : SAWCoreVectorsAsRocqVectors.Vec u Init.Datatypes.bool) (y : SAWCoreVectorsAsRocqVectors.Vec (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) v) Init.Datatypes.bool) => SAWCorePrelude.polyMod u v x (SAWCoreVectorsAsRocqVectors.coerceVec Init.Datatypes.bool (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) v) (SAWCoreScaffolding.Succ v) (addNat_1 v) y)). +Definition ecPmod : forall (u : Num), forall (v : Num), forall (_1 : PFin u), forall (_2 : PFin v), forall (_3 : seq u Init.Datatypes.bool), forall (_4 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) v) Init.Datatypes.bool), seq v Init.Datatypes.bool := + fun (u : Num) (v : Num) (pu : PFin u) (pv : PFin v) => PFinNumRec u pu (fun (u1 : Num) => forall (_1 : seq u1 Init.Datatypes.bool), forall (_2 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) v) Init.Datatypes.bool), seq v Init.Datatypes.bool) (fun (u1 : Init.Datatypes.nat) => PFinNumRec v pv (fun (v1 : Num) => forall (_1 : SAWCoreVectorsAsRocqVectors.Vec u1 Init.Datatypes.bool), forall (_2 : seq (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) v1) Init.Datatypes.bool), seq v1 Init.Datatypes.bool) (fun (v1 : Init.Datatypes.nat) (x : SAWCoreVectorsAsRocqVectors.Vec u1 Init.Datatypes.bool) (y : SAWCoreVectorsAsRocqVectors.Vec (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) v1) Init.Datatypes.bool) => SAWCorePrelude.polyMod u1 v1 x (SAWCoreVectorsAsRocqVectors.coerceVec Init.Datatypes.bool (SAWCoreScaffolding.addNat (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH) v1) (SAWCoreScaffolding.Succ v1) (addNat_1 v1) y))). Definition AESEncRound : forall (_1 : SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)), SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool) := fun (x : SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)) => SAWCoreScaffolding.error (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)) "Unimplemented: AESEncRound"%string. @@ -963,36 +1002,36 @@ Definition AESDecFinalRound : forall (_1 : SAWCoreVectorsAsRocqVectors.Vec (Stdl Definition AESInvMixColumns : forall (_1 : SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)), SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool) := fun (x : SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)) => SAWCoreScaffolding.error (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)) "Unimplemented: AESInvMixColumns"%string. -Definition AESKeyExpand : forall (k : Num), forall (_1 : seq k (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)), seq (tcMul (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH)))) k)) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool) := - fun (k : Num) (x : seq k (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)) => SAWCoreScaffolding.error (seq (tcMul (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH)))) k)) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)) "Unimplemented: AESKeyExpand"%string. +Definition AESKeyExpand : forall (k : Num), forall (_1 : PFin k), forall (_2 : PGeq k (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))), forall (_3 : PGeq (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) k), forall (_4 : seq k (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)), seq (tcMul (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH)))) k)) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool) := + fun (k : Num) (_1 : PFin k) (_2 : PGeq k (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (_3 : PGeq (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) k) (x : seq k (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)) => SAWCoreScaffolding.error (seq (tcMul (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (tcAdd (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH)))) k)) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)) "Unimplemented: AESKeyExpand"%string. -Definition processSHA2_224 : forall (n : Num), forall (_1 : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool))), SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool) := - fun (n : Num) (x : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool))) => SAWCoreScaffolding.error (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)) "Unimplemented: processSHA2_224"%string. +Definition processSHA2_224 : forall (n : Num), forall (_1 : PFin n), forall (_2 : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool))), SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool) := + fun (n : Num) (_1 : PFin n) (x : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool))) => SAWCoreScaffolding.error (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)) "Unimplemented: processSHA2_224"%string. -Definition processSHA2_256 : forall (n : Num), forall (_1 : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool))), SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool) := - fun (n : Num) (x : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool))) => SAWCoreScaffolding.error (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)) "Unimplemented: processSHA2_256"%string. +Definition processSHA2_256 : forall (n : Num), forall (_1 : PFin n), forall (_2 : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool))), SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool) := + fun (n : Num) (_1 : PFin n) (x : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool))) => SAWCoreScaffolding.error (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))) Init.Datatypes.bool)) "Unimplemented: processSHA2_256"%string. -Definition processSHA2_384 : forall (n : Num), forall (_1 : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool))), SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool) := - fun (n : Num) (x : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool))) => SAWCoreScaffolding.error (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool)) "Unimplemented: processSHA2_384"%string. +Definition processSHA2_384 : forall (n : Num), forall (_1 : PFin n), forall (_2 : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool))), SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool) := + fun (n : Num) (_1 : PFin n) (x : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool))) => SAWCoreScaffolding.error (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool)) "Unimplemented: processSHA2_384"%string. -Definition processSHA2_512 : forall (n : Num), forall (_1 : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool))), SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool) := - fun (n : Num) (x : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool))) => SAWCoreScaffolding.error (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool)) "Unimplemented: processSHA2_512"%string. +Definition processSHA2_512 : forall (n : Num), forall (_1 : PFin n), forall (_2 : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool))), SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool) := + fun (n : Num) (_1 : PFin n) (x : seq n (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool))) => SAWCoreScaffolding.error (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (SAWCoreVectorsAsRocqVectors.Vec (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))))) Init.Datatypes.bool)) "Unimplemented: processSHA2_512"%string. Definition ProjectivePoint : forall (_1 : Num), Type := fun (p : Num) => let var__0 := IntModNum p in SAWCoreScaffolding.RecordTypeCons "x"%string var__0 (SAWCoreScaffolding.RecordTypeCons "y"%string var__0 (SAWCoreScaffolding.RecordTypeCons "z"%string var__0 SAWCoreScaffolding.RecordTypeNil)). -Definition ec_double : forall (p : Num), forall (_1 : ProjectivePoint p), ProjectivePoint p := - fun (p : Num) (x : ProjectivePoint p) => SAWCoreScaffolding.error (ProjectivePoint p) "Unimplemented: ec_double"%string. +Definition ec_double : forall (p : Num), forall (_1 : PGeq p (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))), forall (_2 : ProjectivePoint p), ProjectivePoint p := + fun (p : Num) (_1 : PGeq p (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (x : ProjectivePoint p) => SAWCoreScaffolding.error (ProjectivePoint p) "Unimplemented: ec_double"%string. -Definition ec_add_nonzero : forall (p : Num), forall (_1 : ProjectivePoint p), forall (_2 : ProjectivePoint p), ProjectivePoint p := - fun (p : Num) (x : ProjectivePoint p) (y : ProjectivePoint p) => SAWCoreScaffolding.error (ProjectivePoint p) "Unimplemented: ec_add_nonzero"%string. +Definition ec_add_nonzero : forall (p : Num), forall (_1 : PGeq p (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))), forall (_2 : ProjectivePoint p), forall (_3 : ProjectivePoint p), ProjectivePoint p := + fun (p : Num) (_1 : PGeq p (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (x : ProjectivePoint p) (y : ProjectivePoint p) => SAWCoreScaffolding.error (ProjectivePoint p) "Unimplemented: ec_add_nonzero"%string. -Definition ec_mult : forall (p : Num), forall (_1 : IntModNum p), forall (_2 : ProjectivePoint p), ProjectivePoint p := - fun (p : Num) (x : IntModNum p) (y : ProjectivePoint p) => SAWCoreScaffolding.error (ProjectivePoint p) "Unimplemented: ec_mult"%string. +Definition ec_mult : forall (p : Num), forall (_1 : PGeq p (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))), forall (_2 : IntModNum p), forall (_3 : ProjectivePoint p), ProjectivePoint p := + fun (p : Num) (_1 : PGeq p (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (x : IntModNum p) (y : ProjectivePoint p) => SAWCoreScaffolding.error (ProjectivePoint p) "Unimplemented: ec_mult"%string. -Definition ec_twin_mult : forall (p : Num), forall (_1 : IntModNum p), forall (_2 : ProjectivePoint p), forall (_3 : ProjectivePoint p), ProjectivePoint p := - fun (p : Num) (x : IntModNum p) (y : ProjectivePoint p) (z : ProjectivePoint p) => SAWCoreScaffolding.error (ProjectivePoint p) "Unimplemented: ec_twin_mult"%string. +Definition ec_twin_mult : forall (p : Num), forall (_1 : PGeq p (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))), forall (_2 : IntModNum p), forall (_3 : ProjectivePoint p), forall (_4 : ProjectivePoint p), ProjectivePoint p := + fun (p : Num) (_1 : PGeq p (TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (x : IntModNum p) (y : ProjectivePoint p) (z : ProjectivePoint p) => SAWCoreScaffolding.error (ProjectivePoint p) "Unimplemented: ec_twin_mult"%string. Axiom replicate_False : forall (n : Init.Datatypes.nat), @Init.Logic.eq (SAWCoreVectorsAsRocqVectors.Vec n Init.Datatypes.bool) (SAWCorePrelude.replicate n Init.Datatypes.bool Init.Datatypes.false) (SAWCoreVectorsAsRocqVectors.bvNat n SAWCoreScaffolding.Zero) . diff --git a/otherTests/saw-core-rocq/test_literals.log.good b/otherTests/saw-core-rocq/test_literals.log.good index 912e120b39..236718d160 100644 --- a/otherTests/saw-core-rocq/test_literals.log.good +++ b/otherTests/saw-core-rocq/test_literals.log.good @@ -372,7 +372,7 @@ From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. -Definition TestLit_Poly1 (u1301 : CryptolPrimitivesForSAWCore.Num) : CryptolPrimitivesForSAWCore.seq u1301 Init.Datatypes.bool := +Definition TestLit_Poly1 (u1301 : CryptolPrimitivesForSAWCore.Num) (_P : CryptolPrimitivesForSAWCore.PGeq u1301 (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))))) (_P1 : CryptolPrimitivesForSAWCore.PFin u1301) : CryptolPrimitivesForSAWCore.seq u1301 Init.Datatypes.bool := CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))))))) (CryptolPrimitivesForSAWCore.seq u1301 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.PLiteralSeqBool u1301). @@ -397,6 +397,6 @@ From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. -Definition TestLit_Poly2 (u1303 : CryptolPrimitivesForSAWCore.Num) : CryptolPrimitivesForSAWCore.seq u1303 Init.Datatypes.bool := +Definition TestLit_Poly2 (u1303 : CryptolPrimitivesForSAWCore.Num) (_P : CryptolPrimitivesForSAWCore.PGeq u1303 (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) (_P1 : CryptolPrimitivesForSAWCore.PFin u1303) : CryptolPrimitivesForSAWCore.seq u1303 Init.Datatypes.bool := CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH)))))) (CryptolPrimitivesForSAWCore.seq u1303 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.PLiteralSeqBool u1303). diff --git a/otherTests/saw-core-rocq/test_offline_rocq.log.good b/otherTests/saw-core-rocq/test_offline_rocq.log.good index 90abf9f6ee..26288358c8 100644 --- a/otherTests/saw-core-rocq/test_offline_rocq.log.good +++ b/otherTests/saw-core-rocq/test_offline_rocq.log.good @@ -142,7 +142,7 @@ Definition goal : Prop := forall (x : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool), forall (y : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool), let var__0 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool in let var__2 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)) in - SAWCorePrelude.EqTrue (CryptolPrimitivesForSAWCore.ecEq (CryptolPrimitivesForSAWCore.seq var__2 var__1) (CryptolPrimitivesForSAWCore.PEqSeq var__2 var__1 (CryptolPrimitivesForSAWCore.PEqSeqBool var__0)) [x; y] (CryptolPrimitivesForSAWCore.ecReverse var__2 var__1 [y; x])). + SAWCorePrelude.EqTrue (CryptolPrimitivesForSAWCore.ecEq (CryptolPrimitivesForSAWCore.seq var__2 var__1) (CryptolPrimitivesForSAWCore.PEqSeq var__2 var__1 (CryptolPrimitivesForSAWCore.PEqSeqBool var__0)) [x; y] (CryptolPrimitivesForSAWCore.ecReverse var__2 var__1 (CryptolPrimitivesForSAWCore.PFin_TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) [y; x])). === test_offline_rocq6_prove0.v === diff --git a/otherTests/saw-core-rocq/test_prelude.log.good b/otherTests/saw-core-rocq/test_prelude.log.good index a5d9f1615e..fdbd245595 100644 --- a/otherTests/saw-core-rocq/test_prelude.log.good +++ b/otherTests/saw-core-rocq/test_prelude.log.good @@ -510,6 +510,8 @@ Definition posLt : forall (_1 : Stdlib.PArith.BinPos.positive), forall (_2 : Std (* "Prelude::widthNat@core" was skipped *) +(* "Prelude::ltNat_0_right@core" was skipped *) + (* Prelude::Z was skipped *) Definition Z_cases : forall (a : Type), forall (_1 : a), forall (_2 : forall (_2 : Stdlib.PArith.BinPos.positive), a), forall (_3 : forall (_3 : Stdlib.PArith.BinPos.positive), a), forall (_4 : Stdlib.ZArith.BinInt.Z), a := diff --git a/otherTests/saw-core-rocq/test_sequences.log.good b/otherTests/saw-core-rocq/test_sequences.log.good index 61d88c4ed5..1d56850165 100644 --- a/otherTests/saw-core-rocq/test_sequences.log.good +++ b/otherTests/saw-core-rocq/test_sequences.log.good @@ -223,7 +223,7 @@ Definition TestSeq_Drop : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForS let var__2 := CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0 in let var__3 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)) in let var__4 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH)) in - CryptolPrimitivesForSAWCore.ecDrop var__3 var__4 var__1 [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber var__3 var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber var__4 var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) var__1 var__2]. + CryptolPrimitivesForSAWCore.ecDrop var__3 var__4 var__1 (CryptolPrimitivesForSAWCore.PFin_TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber var__3 var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber var__4 var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) var__1 var__2]. (** Mandatory imports from saw-core-rocq *) @@ -252,7 +252,7 @@ Definition TestSeq_DropAll : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesF let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool in let var__2 := CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0 in let var__3 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH)) in - CryptolPrimitivesForSAWCore.ecDrop var__3 (CryptolPrimitivesForSAWCore.TCNum SAWCoreScaffolding.Zero) var__1 [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber var__3 var__1 var__2]. + CryptolPrimitivesForSAWCore.ecDrop var__3 (CryptolPrimitivesForSAWCore.TCNum SAWCoreScaffolding.Zero) var__1 (CryptolPrimitivesForSAWCore.PFin_TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber var__3 var__1 var__2]. (** Mandatory imports from saw-core-rocq *) @@ -281,7 +281,7 @@ Definition TestSeq_DropZero : CryptolPrimitivesForSAWCore.seq (CryptolPrimitives let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool in let var__2 := CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0 in let var__3 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH)) in - CryptolPrimitivesForSAWCore.ecDrop (CryptolPrimitivesForSAWCore.TCNum SAWCoreScaffolding.Zero) var__3 var__1 [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber var__3 var__1 var__2]. + CryptolPrimitivesForSAWCore.ecDrop (CryptolPrimitivesForSAWCore.TCNum SAWCoreScaffolding.Zero) var__3 var__1 (CryptolPrimitivesForSAWCore.PFin_TCNum SAWCoreScaffolding.Zero) [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber var__3 var__1 var__2]. (** Mandatory imports from saw-core-rocq *) @@ -312,7 +312,7 @@ Definition TestSeq_TakeDrop : CryptolPrimitivesForSAWCore.seq (CryptolPrimitives let var__3 := CryptolPrimitivesForSAWCore.PLiteralSeqBool var__1 in let var__4 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)) in let var__5 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH)) in - CryptolPrimitivesForSAWCore.ecTake var__4 var__0 var__2 (CryptolPrimitivesForSAWCore.ecDrop var__0 var__5 var__2 [CryptolPrimitivesForSAWCore.ecNumber var__0 var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber var__4 var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber var__5 var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) var__2 var__3]). + CryptolPrimitivesForSAWCore.ecTake var__4 var__0 var__2 (CryptolPrimitivesForSAWCore.ecDrop var__0 var__5 var__2 (CryptolPrimitivesForSAWCore.PFin_TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) [CryptolPrimitivesForSAWCore.ecNumber var__0 var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber var__4 var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber var__5 var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) var__2 var__3]). (** Mandatory imports from saw-core-rocq *) @@ -528,7 +528,7 @@ Definition TestSeq_Fold : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForS let var__1 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) in let var__2 := CryptolPrimitivesForSAWCore.seq var__1 Init.Datatypes.bool in let var__3 := CryptolPrimitivesForSAWCore.PLiteralSeqBool var__1 in - CryptolPrimitivesForSAWCore.ecFoldl var__0 var__2 var__2 (CryptolPrimitivesForSAWCore.ecPlus var__2 (CryptolPrimitivesForSAWCore.PRingSeqBool var__1)) (CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum SAWCoreScaffolding.Zero) var__2 var__3) [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber var__0 var__2 var__3]. + CryptolPrimitivesForSAWCore.ecFoldl var__0 var__2 var__2 (CryptolPrimitivesForSAWCore.PFin_TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) (CryptolPrimitivesForSAWCore.ecPlus var__2 (CryptolPrimitivesForSAWCore.PRingSeqBool var__1)) (CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum SAWCoreScaffolding.Zero) var__2 var__3) [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber var__0 var__2 var__3]. (** Mandatory imports from saw-core-rocq *) @@ -558,7 +558,7 @@ Definition TestSeq_Concat : let var__0 := CryptolPrimitivesForSAWCore.TCNum (S let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool in let var__2 := CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0 in let var__3 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)) in - CryptolPrimitivesForSAWCore.ecCat var__3 var__3 var__1 [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber var__3 var__1 var__2] [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) var__1 var__2]. + CryptolPrimitivesForSAWCore.ecCat var__3 var__3 var__1 (CryptolPrimitivesForSAWCore.PFin_TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber var__3 var__1 var__2] [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) var__1 var__2; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) var__1 var__2]. (** Mandatory imports from saw-core-rocq *) @@ -618,7 +618,7 @@ Definition TestSeq_Reverse : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesF let var__1 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in let var__2 := CryptolPrimitivesForSAWCore.seq var__1 Init.Datatypes.bool in let var__3 := CryptolPrimitivesForSAWCore.PLiteralSeqBool var__1 in - CryptolPrimitivesForSAWCore.ecReverse var__0 var__2 [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber var__0 var__2 var__3]. + CryptolPrimitivesForSAWCore.ecReverse var__0 var__2 (CryptolPrimitivesForSAWCore.PFin_TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) [CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) var__2 var__3; CryptolPrimitivesForSAWCore.ecNumber var__0 var__2 var__3]. (** Mandatory imports from saw-core-rocq *) diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/FFI.hs b/saw-central/src/SAWCentral/Crucible/LLVM/FFI.hs index fc9f745baa..d3d65a2869 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/FFI.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/FFI.hs @@ -80,6 +80,7 @@ import qualified SAWCore.OpenTerm as OT import SAWCore.Prelude import SAWCore.Recognizer import SAWCore.SharedTerm as Term +import SAWCore.Term.Functor (Sort(..)) import CryptolSAWCore.TypedTerm -- | Commonly used things that need to be passed around. @@ -134,13 +135,25 @@ data FFIPostcond (TypedTerm {- ffiLLVMType -} -> OpenTerm {- ffiCryType -} -> LLVMCrucibleSetupM ()) +-- | Return 'True' if the term's type is a proposition in SAWCore sort @Prop@. +isProofTerm :: Term -> Bool +isProofTerm t = + case termSortOrType t of + Left _ -> False + Right ty -> + case termSortOrType ty of + Left s -> s == PropSort + Right _ -> False + -- | Generate a @LLVMSetup@ spec that can be used to verify that the given -- monomorphic Cryptol term, consisting of a Cryptol foreign function fully -- applied to any type arguments, has a correct foreign (LLVM) implementation -- with respect to its Cryptol implementation. llvm_ffi_setup :: TypedTerm -> LLVMCrucibleSetupM () llvm_ffi_setup TypedTerm { ttTerm = appTerm } = do - let (funTerm, tyArgTerms) = asApplyAll appTerm + let (funTerm, allArgTerms) = asApplyAll appTerm + -- filter out proof terms for type constraints + let tyArgTerms = filter (not . isProofTerm) allArgTerms sc <- lll getSharedContext let ?ctx = FFISetupCtx {..} ffiTypes <- lio $ eFFITypes sc diff --git a/saw-core-rocq/rocq/handwritten/CryptolToRocq/CryptolPrimitivesForSAWCoreExtra.v b/saw-core-rocq/rocq/handwritten/CryptolToRocq/CryptolPrimitivesForSAWCoreExtra.v index 12da775d24..5b16534435 100644 --- a/saw-core-rocq/rocq/handwritten/CryptolToRocq/CryptolPrimitivesForSAWCoreExtra.v +++ b/saw-core-rocq/rocq/handwritten/CryptolToRocq/CryptolPrimitivesForSAWCoreExtra.v @@ -75,6 +75,15 @@ Ltac solveUnsafeAssert := repeat (repeat solveUnsafeAssertStep; simpl; try reflexivity; try lia); trivial). +Ltac solveUnsafeAssumePFin := + reflexivity. + +Ltac solveUnsafeAssumePGEq := + reflexivity. + +Ltac solveUnsafeAssumePNeq := + reflexivity. + Fixpoint iterNat {a : Type} (n : nat) (f : a -> a) : a -> a := match n with | O => fun x => x diff --git a/saw-core-rocq/rocq/handwritten/CryptolToRocq/SAWCoreScaffolding.v b/saw-core-rocq/rocq/handwritten/CryptolToRocq/SAWCoreScaffolding.v index 37530c8e7b..ad325f52f7 100644 --- a/saw-core-rocq/rocq/handwritten/CryptolToRocq/SAWCoreScaffolding.v +++ b/saw-core-rocq/rocq/handwritten/CryptolToRocq/SAWCoreScaffolding.v @@ -276,6 +276,8 @@ Definition minNat := Nat.min. Definition maxNat := Nat.max. Definition Nat__rec := nat_rect. +Definition ltNat_0_right (n : nat) : ltNat n Zero = false := eq_refl. + Fixpoint expNat b n : nat := match n with | 0 => S 0 diff --git a/saw-core-rocq/src/SAWCoreRocq/SpecialTreatment.hs b/saw-core-rocq/src/SAWCoreRocq/SpecialTreatment.hs index 1ad2b48dc7..327b344a12 100644 --- a/saw-core-rocq/src/SAWCoreRocq/SpecialTreatment.hs +++ b/saw-core-rocq/src/SAWCoreRocq/SpecialTreatment.hs @@ -220,6 +220,9 @@ cryptolPreludeSpecialTreatmentMap = Map.fromList $ [] ++ [ ("Num_rec", rename "Num__rec") , ("unsafeAssert_same_Num", skip) -- unsafe and unused + , ("unsafeAssumePFin", replaceDropArgs 1 $ Rocq.Ltac "solveUnsafeAssumePFin") + , ("unsafeAssumePGeq", replaceDropArgs 2 $ Rocq.Ltac "solveUnsafeAssumePGeq") + , ("unsafeAssumePNeq", replaceDropArgs 2 $ Rocq.Ltac "solveUnsafeAssertPNeq") ] -- NOTE: while I initially did the mapping from SAW core names to the @@ -361,6 +364,7 @@ sawCorePreludeSpecialTreatmentMap configuration = , ("Nat__rec", mapsTo sawDefinitionsModule "Nat__rec") , ("if0Nat", mapsTo sawDefinitionsModule "if0Nat") , ("doubleNat", skip) + , ("ltNat_0_right", mapsTo sawDefinitionsModule "ltNat_0_right") ] -- Binary numerals diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index 2054ad3ac9..52b341cd0c 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/saw-core/prelude/Prelude.sawcore @@ -1165,6 +1165,12 @@ widthNat = (\ (_ : Pos) -> Succ) ); +ltNat_0_right : (n : Nat) -> Eq Bool (ltNat n 0) False; +ltNat_0_right = + Nat#ind (\ (n : Nat) -> Eq Bool (ltNat n 0) False) + (Refl Bool False) + (\ (_ : Pos) -> Refl Bool False); + -------------------------------------------------------------------------------- -- Subtraction on Nat