[arch-commits] Commit in cryptol/repos (4 files)
Felix Yan
felixonmars at archlinux.org
Tue Mar 2 22:17:10 UTC 2021
Date: Tuesday, March 2, 2021 @ 22:17:10
Author: felixonmars
Revision: 878544
archrelease: copy trunk to community-staging-x86_64
Added:
cryptol/repos/community-staging-x86_64/
cryptol/repos/community-staging-x86_64/PKGBUILD
(from rev 878543, cryptol/trunk/PKGBUILD)
cryptol/repos/community-staging-x86_64/libbf-0.6.patch
(from rev 878543, cryptol/trunk/libbf-0.6.patch)
cryptol/repos/community-staging-x86_64/sbv-8.8.patch
(from rev 878543, 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 878543, cryptol/trunk/PKGBUILD)
===================================================================
--- community-staging-x86_64/PKGBUILD (rev 0)
+++ community-staging-x86_64/PKGBUILD 2021-03-02 22:17:10 UTC (rev 878544)
@@ -0,0 +1,52 @@
+# Maintainer: Felix Yan <felixonmars at archlinux.org>
+
+pkgname=cryptol
+pkgver=2.10.0
+pkgrel=88
+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 878543, 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-03-02 22:17:10 UTC (rev 878544)
@@ -0,0 +1,156 @@
+From 78855e796720cf6b96f4ccc9435d871b9474f05c Mon Sep 17 00:00:00 2001
+From: Rob Dockins <rdockins at 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 878543, 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-03-02 22:17:10 UTC (rev 878544)
@@ -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
More information about the arch-commits
mailing list