Date: Thursday, February 25, 2021 @ 06:58:24 Author: felixonmars Revision: 873089
archrelease: copy trunk to community-staging-x86_64 Added: cryptol/repos/community-staging-x86_64/ cryptol/repos/community-staging-x86_64/PKGBUILD (from rev 873088, cryptol/trunk/PKGBUILD) cryptol/repos/community-staging-x86_64/libbf-0.6.patch (from rev 873088, cryptol/trunk/libbf-0.6.patch) cryptol/repos/community-staging-x86_64/sbv-8.8.patch (from rev 873088, cryptol/trunk/sbv-8.8.patch) -----------------+ PKGBUILD | 52 ++++++++++++++++++ libbf-0.6.patch | 156 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ sbv-8.8.patch | 101 ++++++++++++++++++++++++++++++++++ 3 files changed, 309 insertions(+) Copied: cryptol/repos/community-staging-x86_64/PKGBUILD (from rev 873088, cryptol/trunk/PKGBUILD) =================================================================== --- community-staging-x86_64/PKGBUILD (rev 0) +++ community-staging-x86_64/PKGBUILD 2021-02-25 06:58:24 UTC (rev 873089) @@ -0,0 +1,52 @@ +# Maintainer: Felix Yan <felixonm...@archlinux.org> + +pkgname=cryptol +pkgver=2.10.0 +pkgrel=82 +pkgdesc="The Language of Cryptography" +url="https://www.cryptol.net" +license=("BSD") +arch=('x86_64') +depends=('ghc-libs' 'z3' 'haskell-async' 'haskell-base-compat' 'haskell-bv-sized' + 'haskell-cryptohash-sha1' 'haskell-exceptions' 'haskell-gitrev' 'haskell-graphscc' + 'haskell-heredoc' 'haskell-libbf' 'haskell-memotrie' 'haskell-monad-control' + 'haskell-monadlib' 'haskell-parameterized-utils' 'haskell-panic' 'haskell-random' + 'haskell-sbv' 'haskell-simple-smt' 'haskell-strict' 'haskell-tf-random' + 'haskell-transformers-base' 'haskell-what4' 'haskell-ansi-terminal' 'haskell-blaze-html') +makedepends=('ghc' 'uusi' 'alex' 'happy') +source=("$pkgname-$pkgver.tar.gz::https://github.com/GaloisInc/cryptol/archive/$pkgver.tar.gz" + sbv-8.8.patch + libbf-0.6.patch) +sha512sums=('efb5f048a23de2040716d210b3d59071744d97989920266206590320585850a84de989851ed94687995874d74a3e6986d2e735e636aaa9f70f8949604ab62904' + 'da4ac99c538a935eed9efd98dd6c57f24ad12d8effe328a814661ed02395445d28c8b4f43b48492171dc0bd65c6568fe7641de94e32765d51ab208a38f09d2d2' + 'b26cef81b4412b7d655376ee01a67bb531b69b2a134b08d6ee592618dee87bc70f8f1acb38db42d5b49f0e70934670f3118e07887958a262924faf469d41eb47') + +prepare() { + patch -d $pkgname-$pkgver -p1 < sbv-8.8.patch + patch -d $pkgname-$pkgver -p1 < libbf-0.6.patch + uusi -u sbv $pkgname-$pkgver/$pkgname.cabal +} + +build() { + cd "${srcdir}/${pkgname}-${pkgver}" + + runhaskell Setup configure -O --enable-shared --enable-executable-dynamic --disable-library-vanilla \ + --prefix=/usr --docdir="/usr/share/doc/${pkgname}" --datasubdir="$pkgname" \ + --dynlibdir=/usr/lib --libsubdir=\$compiler/site-local/\$pkgid \ + -f-static -f-relocatable --ghc-option='-pie' + runhaskell Setup build $MAKEFLAGS + runhaskell Setup register --gen-script + runhaskell Setup unregister --gen-script + sed -i -r -e "s|ghc-pkg.*update[^ ]* |&'--force' |" register.sh + sed -i -r -e "s|ghc-pkg.*unregister[^ ]* |&'--force' |" unregister.sh +} + +package() { + cd "${srcdir}/${pkgname}-${pkgver}" + + install -D -m744 register.sh "${pkgdir}/usr/share/haskell/register/${pkgname}.sh" + install -D -m744 unregister.sh "${pkgdir}/usr/share/haskell/unregister/${pkgname}.sh" + runhaskell Setup copy --destdir="${pkgdir}" + install -D -m644 LICENSE "$pkgdir"/usr/share/licenses/$pkgname/LICENSE + rm -f "$pkgdir"/usr/share/doc/$pkgname/LICENSE +} Copied: cryptol/repos/community-staging-x86_64/libbf-0.6.patch (from rev 873088, cryptol/trunk/libbf-0.6.patch) =================================================================== --- community-staging-x86_64/libbf-0.6.patch (rev 0) +++ community-staging-x86_64/libbf-0.6.patch 2021-02-25 06:58:24 UTC (rev 873089) @@ -0,0 +1,156 @@ +From 78855e796720cf6b96f4ccc9435d871b9474f05c Mon Sep 17 00:00:00 2001 +From: Rob Dockins <rdock...@galois.com> +Date: Thu, 28 Jan 2021 15:24:15 -0800 +Subject: [PATCH] Update to use `libBF` version 0.6, which has some bugfixes + and additional operations. + +--- + cryptol.cabal | 2 +- + src/Cryptol/Backend/Concrete.hs | 4 +- + src/Cryptol/Backend/FloatHelpers.hs | 86 +---------------------------- + 3 files changed, 5 insertions(+), 87 deletions(-) + +diff --git a/cryptol.cabal b/cryptol.cabal +index a737c0d3..dfd30a26 100644 +--- a/cryptol.cabal ++++ b/cryptol.cabal +@@ -57,7 +57,7 @@ library + GraphSCC >= 1.0.4, + heredoc >= 0.2, + integer-gmp >= 1.0 && < 1.1, +- libBF >= 0.5.1, ++ libBF >= 0.6 && < 0.7, + MemoTrie >= 0.6 && < 0.7, + monad-control >= 1.0, + monadLib >= 3.7.2, +diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs +index 129c9a11..cb043b17 100644 +--- a/src/Cryptol/Backend/Concrete.hs ++++ b/src/Cryptol/Backend/Concrete.hs +@@ -338,11 +338,11 @@ instance Backend Concrete where + fpDiv = fpBinArith FP.bfDiv + fpNeg _ x = pure x { FP.bfValue = FP.bfNeg (FP.bfValue x) } + fpFromInteger sym e p r x = +- do opts <- FP.fpOpts e p <$> fpRoundMode sym r ++ do r' <- fpRoundMode sym r + pure FP.BF { FP.bfExpWidth = e + , FP.bfPrecWidth = p + , FP.bfValue = FP.fpCheckStatus $ +- FP.bfRoundInt opts (FP.bfFromInteger x) ++ FP.bfRoundInt r' (FP.bfFromInteger x) + } + fpToInteger = fpCvtToInteger + +diff --git a/src/Cryptol/Backend/FloatHelpers.hs b/src/Cryptol/Backend/FloatHelpers.hs +index 07c5113f..a622b668 100644 +--- a/src/Cryptol/Backend/FloatHelpers.hs ++++ b/src/Cryptol/Backend/FloatHelpers.hs +@@ -3,8 +3,6 @@ + module Cryptol.Backend.FloatHelpers where + + import Data.Ratio(numerator,denominator) +-import Data.Int(Int64) +-import Data.Bits(testBit,setBit,shiftL,shiftR,(.&.),(.|.)) + import LibBF + + import Cryptol.Utils.PP +@@ -150,97 +148,17 @@ floatToInteger fun r fp = + ["Unexpected rounding mode", show r] + + +- +- + floatFromBits :: + Integer {- ^ Exponent width -} -> + Integer {- ^ Precision widht -} -> + Integer {- ^ Raw bits -} -> + BF +-floatFromBits e p bv = BF { bfValue = floatFromBits' e p bv ++floatFromBits e p bv = BF { bfValue = bfFromBits (fpOpts e p NearEven) bv + , bfExpWidth = e, bfPrecWidth = p } + + +- +--- | Make a float using "raw" bits. +-floatFromBits' :: +- Integer {- ^ Exponent width -} -> +- Integer {- ^ Precision widht -} -> +- Integer {- ^ Raw bits -} -> +- BigFloat +- +-floatFromBits' e p bits +- | expoBiased == 0 && mant == 0 = -- zero +- if isNeg then bfNegZero else bfPosZero +- +- | expoBiased == eMask && mant == 0 = -- infinity +- if isNeg then bfNegInf else bfPosInf +- +- | expoBiased == eMask = bfNaN -- NaN +- +- | expoBiased == 0 = -- Subnormal +- case bfMul2Exp opts (bfFromInteger mant) (expoVal + 1) of +- (num,Ok) -> if isNeg then bfNeg num else num +- (_,s) -> panic "floatFromBits" [ "Unexpected status: " ++ show s ] +- +- | otherwise = -- Normal +- case bfMul2Exp opts (bfFromInteger mantVal) expoVal of +- (num,Ok) -> if isNeg then bfNeg num else num +- (_,s) -> panic "floatFromBits" [ "Unexpected status: " ++ show s ] +- +- where +- opts = expBits e' <> precBits (p' + 1) <> allowSubnormal +- +- e' = fromInteger e :: Int +- p' = fromInteger p - 1 :: Int +- eMask = (1 `shiftL` e') - 1 :: Int64 +- pMask = (1 `shiftL` p') - 1 :: Integer +- +- isNeg = testBit bits (e' + p') +- +- mant = pMask .&. bits :: Integer +- mantVal = mant `setBit` p' :: Integer +- -- accounts for the implicit 1 bit +- +- expoBiased = eMask .&. fromInteger (bits `shiftR` p') :: Int64 +- bias = eMask `shiftR` 1 :: Int64 +- expoVal = expoBiased - bias - fromIntegral p' :: Int64 +- +- + -- | Turn a float into raw bits. + -- @NaN@ is represented as a positive "quiet" @NaN@ + -- (most significant bit in the significand is set, the rest of it is 0) + floatToBits :: Integer -> Integer -> BigFloat -> Integer +-floatToBits e p bf = (isNeg `shiftL` (e' + p')) +- .|. (expBiased `shiftL` p') +- .|. (mant `shiftL` 0) +- where +- e' = fromInteger e :: Int +- p' = fromInteger p - 1 :: Int +- +- eMask = (1 `shiftL` e') - 1 :: Integer +- pMask = (1 `shiftL` p') - 1 :: Integer +- +- (isNeg, expBiased, mant) = +- case bfToRep bf of +- BFNaN -> (0, eMask, 1 `shiftL` (p' - 1)) +- BFRep s num -> (sign, be, ma) +- where +- sign = case s of +- Neg -> 1 +- Pos -> 0 +- +- (be,ma) = +- case num of +- Zero -> (0,0) +- Num i ev +- | ex == 0 -> (0, i `shiftL` (p' - m -1)) +- | otherwise -> (ex, (i `shiftL` (p' - m)) .&. pMask) +- where +- m = msb 0 i - 1 +- bias = eMask `shiftR` 1 +- ex = toInteger ev + bias + toInteger m +- +- Inf -> (eMask,0) +- +- msb !n j = if j == 0 then n else msb (n+1) (j `shiftR` 1) ++floatToBits e p bf = bfToBits (fpOpts e p NearEven) bf Copied: cryptol/repos/community-staging-x86_64/sbv-8.8.patch (from rev 873088, cryptol/trunk/sbv-8.8.patch) =================================================================== --- community-staging-x86_64/sbv-8.8.patch (rev 0) +++ community-staging-x86_64/sbv-8.8.patch 2021-02-25 06:58:24 UTC (rev 873089) @@ -0,0 +1,101 @@ +diff --git a/cryptol.cabal b/cryptol.cabal +index 24eb2929..e65d3ed7 100644 +--- a/cryptol.cabal ++++ b/cryptol.cabal +@@ -65,7 +65,7 @@ library + pretty >= 1.1, + process >= 1.2, + random >= 1.0.1, +- sbv >= 8.6 && < 8.8, ++ sbv >= 8.6 && < 8.10, + simple-smt >= 0.7.1, + stm >= 2.4, + strict, +diff --git a/src/Cryptol/Backend/SBV.hs b/src/Cryptol/Backend/SBV.hs +index 6a4d8b00..50e4e087 100644 +--- a/src/Cryptol/Backend/SBV.hs ++++ b/src/Cryptol/Backend/SBV.hs +@@ -6,6 +6,7 @@ + -- Stability : provisional + -- Portability : portable + ++{-# LANGUAGE CPP #-} + {-# LANGUAGE DeriveFunctor #-} + {-# LANGUAGE FlexibleInstances #-} + {-# LANGUAGE GeneralizedNewtypeDeriving #-} +@@ -73,17 +74,24 @@ unpackSBV x = [ svTestBit x i | i <- reverse [0 .. intSizeOf x - 1] ] + literalSWord :: Int -> Integer -> SWord SBV + literalSWord w i = svInteger (KBounded False w) i + ++svMkSymVar_ :: Maybe Quantifier -> Kind -> Maybe String -> SBV.State -> IO SVal ++#if MIN_VERSION_sbv(8,8,0) ++svMkSymVar_ a b c = svMkSymVar (SBV.NonQueryVar a) b c ++#else ++svMkSymVar_ a b c = svMkSymVar a b c ++#endif ++ + freshBV_ :: SBV -> Int -> IO (SWord SBV) + freshBV_ (SBV stateVar _) w = +- withMVar stateVar (svMkSymVar Nothing (KBounded False w) Nothing) ++ withMVar stateVar (svMkSymVar_ Nothing (KBounded False w) Nothing) + + freshSBool_ :: SBV -> IO (SBit SBV) + freshSBool_ (SBV stateVar _) = +- withMVar stateVar (svMkSymVar Nothing KBool Nothing) ++ withMVar stateVar (svMkSymVar_ Nothing KBool Nothing) + + freshSInteger_ :: SBV -> IO (SInteger SBV) + freshSInteger_ (SBV stateVar _) = +- withMVar stateVar (svMkSymVar Nothing KUnbounded Nothing) ++ withMVar stateVar (svMkSymVar_ Nothing KUnbounded Nothing) + + + -- SBV Evaluation monad ------------------------------------------------------- +diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs +index 2f97100e..7421db91 100644 +--- a/src/Cryptol/Symbolic/SBV.hs ++++ b/src/Cryptol/Symbolic/SBV.hs +@@ -6,6 +6,7 @@ + -- Stability : provisional + -- Portability : portable + ++{-# LANGUAGE CPP #-} + {-# LANGUAGE FlexibleContexts #-} + {-# LANGUAGE ImplicitParams #-} + {-# LANGUAGE LambdaCase #-} +@@ -124,7 +125,11 @@ proverNames = map fst proverConfigs + setupProver :: String -> IO (Either String ([String], SBVProverConfig)) + setupProver nm + | nm `elem` ["any","sbv-any"] = ++#if MIN_VERSION_sbv(8,9,0) ++ do ps <- SBV.getAvailableSolvers ++#else + do ps <- SBV.sbvAvailableSolvers ++#endif + case ps of + [] -> pure (Left "SBV could not find any provers") + _ -> let msg = "SBV found the following solvers: " ++ show (map (SBV.name . SBV.solver) ps) in +@@ -155,7 +160,11 @@ satSMTResults :: SBV.SatResult -> [SBV.SMTResult] + satSMTResults (SBV.SatResult r) = [r] + + allSatSMTResults :: SBV.AllSatResult -> [SBV.SMTResult] ++#if MIN_VERSION_sbv(8,8,0) ++allSatSMTResults (SBV.AllSatResult {allSatResults = rs}) = rs ++#else + allSatSMTResults (SBV.AllSatResult (_, _, _, rs)) = rs ++#endif + + thmSMTResults :: SBV.ThmResult -> [SBV.SMTResult] + thmSMTResults (SBV.ThmResult r) = [r] +@@ -389,7 +398,11 @@ processResults ProverCommand{..} ts results = + + -- otherwise something is wrong + _ -> return $ ProverError (rshow results) ++#if MIN_VERSION_sbv(8,8,0) ++ where rshow | isSat = show . (SBV.AllSatResult False False False False) ++#else + where rshow | isSat = show . SBV.AllSatResult . (False,False,False,) ++#endif + | otherwise = show . SBV.ThmResult . head + + where