diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c99f63cfa..fa8b348ea 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -9,7 +9,7 @@ on: workflow_dispatch: env: - SOLVER_PKG_VERSION: "snapshot-20220721" + SOLVER_PKG_VERSION: "snapshot-20220812" # The CACHE_VERSION can be updated to force the use of a new cache if # the current cache contents become corrupted/invalid. This can # sometimes happen when (for example) the OS version is changed but @@ -20,7 +20,7 @@ env: jobs: config: - runs-on: ubuntu-20.04 + runs-on: ubuntu-22.04 outputs: name: ${{ steps.config.outputs.name }} version: ${{ steps.config.outputs.version }} @@ -58,8 +58,8 @@ jobs: strategy: fail-fast: false matrix: - os: [ubuntu-20.04, macos-12, windows-2019] - ghc-version: ["8.8.4", "8.10.7", "9.0.2", "9.2.2"] + os: [ubuntu-22.04, macos-12, windows-2019] + ghc-version: ["8.8.4", "8.10.7", "9.0.2", "9.2.4"] exclude: # https://gitlab.haskell.org/ghc/ghc/-/issues/18550 - os: windows-2019 @@ -67,11 +67,11 @@ jobs: - os: windows-2019 ghc-version: 9.0.2 - os: windows-2019 - ghc-version: 9.2.2 + ghc-version: 9.2.4 include: # We include one job from an older Ubuntu LTS release to increase our # coverage of possible Linux configurations. - - os: ubuntu-18.04 + - os: ubuntu-22.04 ghc-version: 8.8.4 outputs: test-lib-json: ${{ steps.test-lib.outputs.targets-json }} @@ -147,6 +147,8 @@ jobs: cmd="cat \$1.stdout" if ${{ runner.os == 'Windows' }}; then cmd="cat \$1.stdout.mingw32 2>/dev/null || $cmd" + elif ${{ runner.os == 'macOS' }}; then + cmd="cat \$1.stdout.darwin 2>/dev/null || $cmd" fi ./bin/test-runner --ext=.icry -r ./output --exe=$(which bash) -F -c -F "$cmd" -F -- ./tests TARGETS_JSON=$(echo -n "$(ls -1 ./output/tests)" | jq -Rsc 'split("\n")') @@ -158,7 +160,7 @@ jobs: - if: runner.os == 'Windows' run: .github/wix.ps1 - - if: runner.os == 'Windows' + - if: runner.os == 'Windows' && github.event.pull_request.head.repo.fork == false shell: bash env: SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }} @@ -181,7 +183,8 @@ jobs: env: OS_TAG: ${{ matrix.os }} - - shell: bash + - if: github.event.pull_request.head.repo.fork == false + shell: bash env: SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }} SIGNING_KEY: ${{ secrets.SIGNING_KEY }} @@ -231,12 +234,12 @@ jobs: matrix: suite: [test-lib] target: ${{ fromJson(needs.build.outputs.test-lib-json) }} - os: [ubuntu-20.04, macos-12, windows-2019] + os: [ubuntu-22.04, macos-12, windows-2019] continue-on-error: [false] include: - suite: rpc target: '' - os: ubuntu-20.04 + os: ubuntu-22.04 continue-on-error: false #- suite: rpc # target: '' @@ -311,7 +314,7 @@ jobs: cryptol-remote-api/run_rpc_tests.sh build-push-image: - runs-on: ubuntu-20.04 + runs-on: ubuntu-22.04 needs: [config] if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' || needs.config.outputs.release == 'true' strategy: diff --git a/Dockerfile b/Dockerfile index 29a88679b..5e0f67ba0 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,21 +1,36 @@ -FROM haskell:8.8.4 AS build +FROM ubuntu:22.04 AS build -RUN apt-get update && apt-get install -y libncurses-dev unzip +RUN apt-get update && \ + apt-get install -y \ + # ghcup requirements + build-essential curl libffi-dev libffi8 libgmp-dev libgmp10 libncurses-dev libncurses6 libtinfo6 \ + # Cryptol dependencies + zlib1g-dev \ + # Miscellaneous + unzip RUN useradd -m cryptol COPY --chown=cryptol:cryptol . /cryptol USER cryptol WORKDIR /cryptol RUN mkdir -p rootfs/usr/local/bin WORKDIR /cryptol/rootfs/usr/local/bin -RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220114/ubuntu-18.04-bin.zip" +RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220812/ubuntu-22.04-bin.zip" RUN unzip solvers.zip && rm solvers.zip && chmod +x * WORKDIR /cryptol -ENV PATH=/cryptol/rootfs/usr/local/bin:$PATH +ENV PATH=/cryptol/rootfs/usr/local/bin:/home/cryptol/.local/bin:/home/cryptol/.ghcup/bin:$PATH RUN z3 --version ARG CRYPTOLPATH="/cryptol/.cryptol" ENV LANG=C.UTF-8 \ LC_ALL=C.UTF-8 COPY cabal.GHC-8.8.4.config cabal.project.freeze +RUN mkdir -p /home/cryptol/.local/bin && \ + curl -L https://downloads.haskell.org/~ghcup/0.1.17.7/x86_64-linux-ghcup-0.1.17.7 -o /home/cryptol/.local/bin/ghcup && \ + chmod +x /home/cryptol/.local/bin/ghcup +RUN mkdir -p /home/cryptol/.ghcup && \ + ghcup --version && \ + ghcup install cabal 3.6.2.0 && \ + ghcup install ghc 8.8.4 && \ + ghcup set ghc 8.8.4 RUN cabal v2-update && \ cabal v2-build -j cryptol:exe:cryptol && \ cp $(cabal v2-exec which cryptol) rootfs/usr/local/bin && \ @@ -33,9 +48,9 @@ RUN mkdir -p rootfs/"${CRYPTOLPATH}" \ USER root RUN chown -R root:root /cryptol/rootfs -FROM debian:buster-20210511-slim +FROM ubuntu:22.04 RUN apt-get update \ - && apt-get install -y libgmp10 libgomp1 libffi6 libncurses6 libtinfo6 libreadline7 \ + && apt-get install -y libgmp10 libgomp1 libffi8 libncurses6 libtinfo6 libreadline8 \ && apt-get clean && rm -rf /var/lib/apt/lists/* RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol COPY --from=build /cryptol/rootfs / diff --git a/README.md b/README.md index 88f183c61..4e996fce6 100644 --- a/README.md +++ b/README.md @@ -46,7 +46,7 @@ Cryptol currently uses Microsoft Research's [Z3 SMT solver](https://github.com/Z3Prover/z3) by default to solve constraints during type checking, and as the default solver for the `:sat` and `:prove` commands. Cryptol generally requires the most recent version -of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20220721). +of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20220812). You can download Z3 binaries for a variety of platforms from their [releases page](https://github.com/Z3Prover/z3/releases). If you @@ -75,15 +75,15 @@ Cryptol builds and runs on various flavors of Linux, Mac OS X, and Windows. We regularly build and test it in the following environments: - macOS 12, 64-bit -- Ubuntu 18.04, 64-bit - Ubuntu 20.04, 64-bit +- Ubuntu 22.04, 64-bit - Windows Server 2019, 64-bit ## Prerequisites Cryptol is regularly built and tested with the three most recent versions of GHC, which at the time of this writing are 8.10.7, 9.0.2, and -9.2.2. The easiest way to install an approporiate version of GHC is +9.2.4. The easiest way to install an approporiate version of GHC is with [ghcup](https://www.haskell.org/ghcup/). Some supporting non-Haskell libraries are required to build diff --git a/cabal.GHC-8.10.7.config b/cabal.GHC-8.10.7.config index 47f6fa6e5..02a6a053f 100644 --- a/cabal.GHC-8.10.7.config +++ b/cabal.GHC-8.10.7.config @@ -11,10 +11,7 @@ constraints: any.Cabal ==3.2.1.0, any.QuickCheck ==2.14.2, QuickCheck -old-random +templatehaskell, any.StateVar ==1.2.2, - any.abstract-deque ==0.3, - abstract-deque -usecas, - any.abstract-par ==0.3.3, - any.adjunctions ==4.4, + any.adjunctions ==4.4.1, any.aeson ==2.0.3.0, aeson -cffi +ordered-keymap, any.alex ==3.2.7.1, @@ -23,7 +20,7 @@ constraints: any.Cabal ==3.2.1.0, any.ansi-wl-pprint ==0.6.9, ansi-wl-pprint -example, any.appar ==0.1.8, - any.arithmoi ==0.12.0.1, + any.arithmoi ==0.12.0.2, any.array ==0.5.4.0, any.asn1-encoding ==0.9.6, any.asn1-parse ==0.9.5, @@ -35,16 +32,18 @@ constraints: any.Cabal ==3.2.1.0, attoparsec -developer, any.auto-update ==0.1.6, any.base ==4.14.3.0, - any.base-compat ==0.12.1, - any.base-compat-batteries ==0.12.1, - any.base-orphans ==0.8.6, + any.base-compat ==0.12.2, + any.base-compat-batteries ==0.12.2, + any.base-orphans ==0.8.7, any.base64-bytestring ==1.2.1.0, any.basement ==0.0.14, - any.bifunctors ==5.5.11, + any.bifunctors ==5.5.12, bifunctors +semigroups +tagged, - any.bimap ==0.4.0, + any.bimap ==0.5.0, any.binary ==0.8.8.0, - any.binary-orphans ==1.0.2, + any.binary-orphans ==1.0.3, + any.bitvec ==1.1.3.0, + bitvec -libgmp, any.bitwise ==1.0.0.1, any.blaze-builder ==0.4.2.2, any.blaze-html ==0.9.1.2, @@ -56,9 +55,9 @@ constraints: any.Cabal ==3.2.1.0, any.cabal-doctest ==1.0.9, any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, - any.cassava ==0.5.2.0, + any.cassava ==0.5.3.0, cassava -bytestring--lt-0_10_4, - any.cereal ==0.5.8.2, + any.cereal ==0.5.8.3, cereal -bytestring-builder, any.chimera ==0.3.2.0, chimera +representable, @@ -69,15 +68,15 @@ constraints: any.Cabal ==3.2.1.0, any.comonad ==5.0.8, comonad +containers +distributive +indexed-traversable, any.concurrent-extra ==0.7.0.12, - any.config-value ==0.8.2.1, - any.constraints ==0.13.3, + any.config-value ==0.8.3, + any.constraints ==0.13.4, any.containers ==0.6.5.1, any.contravariant ==1.5.5, contravariant +semigroups +statevar +tagged, any.cookie ==0.4.5, - any.criterion ==1.5.13.0, + any.criterion ==1.6.0.0, criterion -embed-data-files -fast, - any.criterion-measurement ==0.1.3.0, + any.criterion-measurement ==0.2.0.0, criterion-measurement -fast, any.cryptohash-md5 ==0.11.101.0, any.cryptohash-sha1 ==0.11.101.0, @@ -91,7 +90,7 @@ constraints: any.Cabal ==3.2.1.0, any.data-fix ==0.3.2, any.deepseq ==1.4.4.0, any.dense-linear-algebra ==0.1.0.0, - any.deriving-compat ==0.6, + any.deriving-compat ==0.6.1, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.directory ==1.3.6.0, any.distributive ==0.6.2.1, @@ -110,7 +109,7 @@ constraints: any.Cabal ==3.2.1.0, any.filelock ==0.1.1.5, any.filepath ==1.4.2.1, any.fingertree ==0.1.5.0, - any.free ==5.1.7, + any.free ==5.1.9, any.ghc-boot-th ==8.10.7, any.ghc-prim ==0.6.1, any.gitrev ==1.3.1, @@ -130,34 +129,33 @@ constraints: any.Cabal ==3.2.1.0, any.http2 ==3.0.3, http2 -devel -doc -h2spec, any.indexed-traversable ==0.1.2, - any.indexed-traversable-instances ==0.1.1, + any.indexed-traversable-instances ==0.1.1.1, any.integer-gmp ==1.0.3.0, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, any.integer-roots ==1.0.2.0, - any.invariant ==0.5.5, + any.invariant ==0.6, any.io-streams ==1.5.2.1, io-streams +network -nointeractivetests +zlib, any.iproute ==1.7.12, any.js-chart ==2.9.4.1, - any.kan-extensions ==5.2.3, - any.lens ==5.1, + any.kan-extensions ==5.2.5, + any.lens ==5.1.1, lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.3, + any.libBF ==0.6.4, libBF -system-libbf, + any.libffi ==0.2, + libffi +ghc-bundled-libffi, any.math-functions ==0.3.4.2, math-functions +system-erf +system-expm1, - any.megaparsec ==9.2.0, + any.megaparsec ==9.2.1, megaparsec -dev, any.memory ==0.17.0, memory +support_bytestring +support_deepseq, - any.microstache ==1.0.2, + any.microstache ==1.0.2.2, any.mod ==0.1.2.2, mod +semirings +vector, any.monad-control ==1.0.3.1, - any.monad-par ==0.3.5, - monad-par -chaselev -newgeneric, - any.monad-par-extras ==0.3.3, any.monadLib ==3.10.1, any.mtl ==2.2.2, any.mwc-random ==0.15.0.2, @@ -167,7 +165,7 @@ constraints: any.Cabal ==3.2.1.0, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.1, - any.newtype-generics ==0.6.1, + any.newtype-generics ==0.6.2, any.numtype-dk ==0.5.0.3, any.old-locale ==1.0.0.7, any.old-time ==1.1.0.3, @@ -184,20 +182,20 @@ constraints: any.Cabal ==3.2.1.0, any.pretty ==1.1.3.6, any.prettyprinter ==1.7.1, prettyprinter -buildreadme +text, - any.primitive ==0.7.3.0, + any.primitive ==0.7.4.0, any.process ==1.6.13.2, any.profunctors ==5.6.2, any.psqueues ==0.2.7.3, - any.quickcheck-instances ==0.3.27, + any.quickcheck-instances ==0.3.28, quickcheck-instances -bytestring-builder, - any.random ==1.2.1, + any.random ==1.2.1.1, any.reflection ==2.1.6, reflection -slow +template-haskell, any.regex-base ==0.94.0.2, any.regex-compat ==0.95.2.1, any.regex-posix ==0.96.0.1, regex-posix -_regex-posix-clib, - any.resourcet ==1.2.4.3, + any.resourcet ==1.2.6, any.rts ==1.0.1, any.safe ==0.3.19, any.sbv ==9.0, @@ -219,7 +217,7 @@ constraints: any.Cabal ==3.2.1.0, any.simple-smt ==0.9.7, any.splitmix ==0.1.0.4, splitmix -optimised-mixer, - any.statistics ==0.16.0.2, + any.statistics ==0.16.1.0, any.stm ==2.5.0.1, any.streaming-commons ==0.2.2.4, streaming-commons -use-bytestring-builder, @@ -228,7 +226,7 @@ constraints: any.Cabal ==3.2.1.0, any.syb ==0.7.2.1, any.tagged ==0.8.6.1, tagged +deepseq +transformers, - any.tasty ==1.4.2.1, + any.tasty ==1.4.2.3, tasty +clock +unix, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.2, @@ -243,7 +241,7 @@ constraints: any.Cabal ==3.2.1.0, any.text-short ==0.1.5, text-short -asserts, any.tf-random ==0.5, - any.th-abstraction ==0.4.3.0, + any.th-abstraction ==0.4.4.0, any.th-lift ==0.8.2, any.th-lift-instances ==0.1.19, any.these ==1.1.1.1, @@ -252,19 +250,19 @@ constraints: any.Cabal ==3.2.1.0, any.time-compat ==1.9.6.1, time-compat -old-locale, any.time-manager ==0.0.0, - any.tls ==1.5.7, + any.tls ==1.6.0, tls +compat -hans +network, any.tls-session-manager ==0.0.4, any.transformers ==0.5.6.2, any.transformers-base ==0.4.6, transformers-base +orphaninstances, - any.transformers-compat ==0.7.1, + any.transformers-compat ==0.7.2, transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, any.type-equality ==1, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.7.2.2, - any.unix-compat ==0.5.4, + any.unix-compat ==0.6, unix-compat -old-time, any.unix-time ==0.4.7, any.unliftio ==0.2.22.0, @@ -278,7 +276,7 @@ constraints: any.Cabal ==3.2.1.0, vault +useghc, any.vector ==0.12.3.1, vector +boundschecks -internalchecks -unsafechecks -wall, - any.vector-algorithms ==0.8.0.4, + any.vector-algorithms ==0.9.0.1, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, any.vector-binary-instances ==0.2.5.2, any.vector-th-unbox ==0.2.2, @@ -286,19 +284,19 @@ constraints: any.Cabal ==3.2.1.0, any.void ==0.7.3, void -safe, any.wai ==3.2.3, - any.wai-extra ==3.1.10, + any.wai-extra ==3.1.12.1, wai-extra -build-example, any.wai-logger ==2.4.0, - any.warp ==3.3.20, + any.warp ==3.3.22, warp +allow-sendfilefd -network-bytestring -warp-debug +x509, - any.warp-tls ==3.3.2, + any.warp-tls ==3.3.3, any.wcwidth ==0.0.2, wcwidth -cli +split-base, any.what4 ==1.3, what4 -drealtestdisable -solvertests -stptestdisable, any.witherable ==0.4.2, any.word8 ==0.1.3, - any.x509 ==1.7.6, + any.x509 ==1.7.7, any.x509-store ==1.6.9, any.x509-validation ==1.6.12, any.xml ==1.3.14, @@ -306,4 +304,4 @@ constraints: any.Cabal ==3.2.1.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2022-05-04T18:13:54Z +index-state: hackage.haskell.org 2022-08-12T18:38:07Z diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config index eef2cd6fe..45b9816e1 100644 --- a/cabal.GHC-8.8.4.config +++ b/cabal.GHC-8.8.4.config @@ -11,10 +11,7 @@ constraints: any.Cabal ==3.0.1.0, any.QuickCheck ==2.14.2, QuickCheck -old-random +templatehaskell, any.StateVar ==1.2.2, - any.abstract-deque ==0.3, - abstract-deque -usecas, - any.abstract-par ==0.3.3, - any.adjunctions ==4.4, + any.adjunctions ==4.4.1, any.aeson ==2.0.3.0, aeson -cffi +ordered-keymap, any.alex ==3.2.7.1, @@ -23,7 +20,7 @@ constraints: any.Cabal ==3.0.1.0, any.ansi-wl-pprint ==0.6.9, ansi-wl-pprint -example, any.appar ==0.1.8, - any.arithmoi ==0.12.0.1, + any.arithmoi ==0.12.0.2, any.array ==0.5.4.0, any.asn1-encoding ==0.9.6, any.asn1-parse ==0.9.5, @@ -35,16 +32,18 @@ constraints: any.Cabal ==3.0.1.0, attoparsec -developer, any.auto-update ==0.1.6, any.base ==4.13.0.0, - any.base-compat ==0.12.1, - any.base-compat-batteries ==0.12.1, - any.base-orphans ==0.8.6, + any.base-compat ==0.12.2, + any.base-compat-batteries ==0.12.2, + any.base-orphans ==0.8.7, any.base64-bytestring ==1.2.1.0, any.basement ==0.0.14, - any.bifunctors ==5.5.11, + any.bifunctors ==5.5.12, bifunctors +semigroups +tagged, - any.bimap ==0.4.0, + any.bimap ==0.5.0, any.binary ==0.8.7.0, - any.binary-orphans ==1.0.2, + any.binary-orphans ==1.0.3, + any.bitvec ==1.1.3.0, + bitvec -libgmp, any.bitwise ==1.0.0.1, any.blaze-builder ==0.4.2.2, any.blaze-html ==0.9.1.2, @@ -56,9 +55,9 @@ constraints: any.Cabal ==3.0.1.0, any.cabal-doctest ==1.0.9, any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, - any.cassava ==0.5.2.0, + any.cassava ==0.5.3.0, cassava -bytestring--lt-0_10_4, - any.cereal ==0.5.8.2, + any.cereal ==0.5.8.3, cereal -bytestring-builder, any.chimera ==0.3.2.0, chimera +representable, @@ -69,15 +68,15 @@ constraints: any.Cabal ==3.0.1.0, any.comonad ==5.0.8, comonad +containers +distributive +indexed-traversable, any.concurrent-extra ==0.7.0.12, - any.config-value ==0.8.2.1, - any.constraints ==0.13.3, + any.config-value ==0.8.3, + any.constraints ==0.13.4, any.containers ==0.6.2.1, any.contravariant ==1.5.5, contravariant +semigroups +statevar +tagged, any.cookie ==0.4.5, - any.criterion ==1.5.13.0, + any.criterion ==1.6.0.0, criterion -embed-data-files -fast, - any.criterion-measurement ==0.1.3.0, + any.criterion-measurement ==0.2.0.0, criterion-measurement -fast, any.cryptohash-md5 ==0.11.101.0, any.cryptohash-sha1 ==0.11.101.0, @@ -91,7 +90,7 @@ constraints: any.Cabal ==3.0.1.0, any.data-fix ==0.3.2, any.deepseq ==1.4.4.0, any.dense-linear-algebra ==0.1.0.0, - any.deriving-compat ==0.6, + any.deriving-compat ==0.6.1, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.directory ==1.3.6.0, any.distributive ==0.6.2.1, @@ -102,7 +101,7 @@ constraints: any.Cabal ==3.0.1.0, any.entropy ==0.4.1.7, entropy -halvm, any.exact-pi ==0.5.0.2, - any.exceptions ==0.10.4, + any.exceptions ==0.10.5, exceptions +transformers-0-4, any.extensible-exceptions ==0.1.1.4, any.extra ==1.7.10, @@ -111,7 +110,7 @@ constraints: any.Cabal ==3.0.1.0, any.filelock ==0.1.1.5, any.filepath ==1.4.2.1, any.fingertree ==0.1.5.0, - any.free ==5.1.7, + any.free ==5.1.9, any.ghc-boot-th ==8.8.4, any.ghc-prim ==0.5.3, any.gitrev ==1.3.1, @@ -131,34 +130,33 @@ constraints: any.Cabal ==3.0.1.0, any.http2 ==3.0.3, http2 -devel -doc -h2spec, any.indexed-traversable ==0.1.2, - any.indexed-traversable-instances ==0.1.1, + any.indexed-traversable-instances ==0.1.1.1, any.integer-gmp ==1.0.2.0, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, any.integer-roots ==1.0.2.0, - any.invariant ==0.5.5, + any.invariant ==0.6, any.io-streams ==1.5.2.1, io-streams +network -nointeractivetests +zlib, any.iproute ==1.7.12, any.js-chart ==2.9.4.1, - any.kan-extensions ==5.2.3, - any.lens ==5.1, + any.kan-extensions ==5.2.5, + any.lens ==5.1.1, lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.3, + any.libBF ==0.6.4, libBF -system-libbf, + any.libffi ==0.2, + libffi +ghc-bundled-libffi, any.math-functions ==0.3.4.2, math-functions +system-erf +system-expm1, - any.megaparsec ==9.2.0, + any.megaparsec ==9.2.1, megaparsec -dev, any.memory ==0.17.0, memory +support_bytestring +support_deepseq, - any.microstache ==1.0.2, + any.microstache ==1.0.2.2, any.mod ==0.1.2.2, mod +semirings +vector, any.monad-control ==1.0.3.1, - any.monad-par ==0.3.5, - monad-par -chaselev -newgeneric, - any.monad-par-extras ==0.3.3, any.monadLib ==3.10.1, any.mtl ==2.2.2, any.mwc-random ==0.15.0.2, @@ -168,7 +166,7 @@ constraints: any.Cabal ==3.0.1.0, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.1, - any.newtype-generics ==0.6.1, + any.newtype-generics ==0.6.2, any.numtype-dk ==0.5.0.3, any.old-locale ==1.0.0.7, any.old-time ==1.1.0.3, @@ -185,20 +183,20 @@ constraints: any.Cabal ==3.0.1.0, any.pretty ==1.1.3.6, any.prettyprinter ==1.7.1, prettyprinter -buildreadme +text, - any.primitive ==0.7.3.0, + any.primitive ==0.7.4.0, any.process ==1.6.9.0, any.profunctors ==5.6.2, any.psqueues ==0.2.7.3, - any.quickcheck-instances ==0.3.27, + any.quickcheck-instances ==0.3.28, quickcheck-instances -bytestring-builder, - any.random ==1.2.1, + any.random ==1.2.1.1, any.reflection ==2.1.6, reflection -slow +template-haskell, any.regex-base ==0.94.0.2, any.regex-compat ==0.95.2.1, any.regex-posix ==0.96.0.1, regex-posix -_regex-posix-clib, - any.resourcet ==1.2.4.3, + any.resourcet ==1.2.6, any.rts ==1.0, any.safe ==0.3.19, any.sbv ==9.0, @@ -220,7 +218,7 @@ constraints: any.Cabal ==3.0.1.0, any.simple-smt ==0.9.7, any.splitmix ==0.1.0.4, splitmix -optimised-mixer, - any.statistics ==0.16.0.2, + any.statistics ==0.16.1.0, any.stm ==2.5.0.0, any.streaming-commons ==0.2.2.4, streaming-commons -use-bytestring-builder, @@ -229,7 +227,7 @@ constraints: any.Cabal ==3.0.1.0, any.syb ==0.7.2.1, any.tagged ==0.8.6.1, tagged +deepseq +transformers, - any.tasty ==1.4.2.1, + any.tasty ==1.4.2.3, tasty +clock +unix, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.2, @@ -244,7 +242,7 @@ constraints: any.Cabal ==3.0.1.0, any.text-short ==0.1.5, text-short -asserts, any.tf-random ==0.5, - any.th-abstraction ==0.4.3.0, + any.th-abstraction ==0.4.4.0, any.th-lift ==0.8.2, any.th-lift-instances ==0.1.19, any.these ==1.1.1.1, @@ -253,19 +251,19 @@ constraints: any.Cabal ==3.0.1.0, any.time-compat ==1.9.6.1, time-compat -old-locale, any.time-manager ==0.0.0, - any.tls ==1.5.7, + any.tls ==1.6.0, tls +compat -hans +network, any.tls-session-manager ==0.0.4, any.transformers ==0.5.6.2, any.transformers-base ==0.4.6, transformers-base +orphaninstances, - any.transformers-compat ==0.7.1, + any.transformers-compat ==0.7.2, transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, any.type-equality ==1, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.7.2.2, - any.unix-compat ==0.5.4, + any.unix-compat ==0.6, unix-compat -old-time, any.unix-time ==0.4.7, any.unliftio ==0.2.22.0, @@ -279,7 +277,7 @@ constraints: any.Cabal ==3.0.1.0, vault +useghc, any.vector ==0.12.3.1, vector +boundschecks -internalchecks -unsafechecks -wall, - any.vector-algorithms ==0.8.0.4, + any.vector-algorithms ==0.9.0.1, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, any.vector-binary-instances ==0.2.5.2, any.vector-th-unbox ==0.2.2, @@ -287,19 +285,19 @@ constraints: any.Cabal ==3.0.1.0, any.void ==0.7.3, void -safe, any.wai ==3.2.3, - any.wai-extra ==3.1.10, + any.wai-extra ==3.1.12.1, wai-extra -build-example, any.wai-logger ==2.4.0, - any.warp ==3.3.20, + any.warp ==3.3.22, warp +allow-sendfilefd -network-bytestring -warp-debug +x509, - any.warp-tls ==3.3.2, + any.warp-tls ==3.3.3, any.wcwidth ==0.0.2, wcwidth -cli +split-base, any.what4 ==1.3, what4 -drealtestdisable -solvertests -stptestdisable, any.witherable ==0.4.2, any.word8 ==0.1.3, - any.x509 ==1.7.6, + any.x509 ==1.7.7, any.x509-store ==1.6.9, any.x509-validation ==1.6.12, any.xml ==1.3.14, @@ -307,4 +305,4 @@ constraints: any.Cabal ==3.0.1.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2022-05-04T18:13:54Z +index-state: hackage.haskell.org 2022-08-12T18:38:07Z diff --git a/cabal.GHC-9.0.2.config b/cabal.GHC-9.0.2.config index 7e5d18e2c..6b6fc31c5 100644 --- a/cabal.GHC-9.0.2.config +++ b/cabal.GHC-9.0.2.config @@ -11,10 +11,7 @@ constraints: any.Cabal ==3.4.1.0, any.QuickCheck ==2.14.2, QuickCheck -old-random +templatehaskell, any.StateVar ==1.2.2, - any.abstract-deque ==0.3, - abstract-deque -usecas, - any.abstract-par ==0.3.3, - any.adjunctions ==4.4, + any.adjunctions ==4.4.1, any.aeson ==2.0.3.0, aeson -cffi +ordered-keymap, any.alex ==3.2.7.1, @@ -23,7 +20,7 @@ constraints: any.Cabal ==3.4.1.0, any.ansi-wl-pprint ==0.6.9, ansi-wl-pprint -example, any.appar ==0.1.8, - any.arithmoi ==0.12.0.1, + any.arithmoi ==0.12.0.2, any.array ==0.5.4.0, any.asn1-encoding ==0.9.6, any.asn1-parse ==0.9.5, @@ -35,16 +32,18 @@ constraints: any.Cabal ==3.4.1.0, attoparsec -developer, any.auto-update ==0.1.6, any.base ==4.15.1.0, - any.base-compat ==0.12.1, - any.base-compat-batteries ==0.12.1, - any.base-orphans ==0.8.6, + any.base-compat ==0.12.2, + any.base-compat-batteries ==0.12.2, + any.base-orphans ==0.8.7, any.base64-bytestring ==1.2.1.0, any.basement ==0.0.14, - any.bifunctors ==5.5.11, + any.bifunctors ==5.5.12, bifunctors +semigroups +tagged, - any.bimap ==0.4.0, + any.bimap ==0.5.0, any.binary ==0.8.8.0, - any.binary-orphans ==1.0.2, + any.binary-orphans ==1.0.3, + any.bitvec ==1.1.3.0, + bitvec -libgmp, any.bitwise ==1.0.0.1, any.blaze-builder ==0.4.2.2, any.blaze-html ==0.9.1.2, @@ -56,9 +55,9 @@ constraints: any.Cabal ==3.4.1.0, any.cabal-doctest ==1.0.9, any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, - any.cassava ==0.5.2.0, + any.cassava ==0.5.3.0, cassava -bytestring--lt-0_10_4, - any.cereal ==0.5.8.2, + any.cereal ==0.5.8.3, cereal -bytestring-builder, any.chimera ==0.3.2.0, chimera +representable, @@ -69,15 +68,15 @@ constraints: any.Cabal ==3.4.1.0, any.comonad ==5.0.8, comonad +containers +distributive +indexed-traversable, any.concurrent-extra ==0.7.0.12, - any.config-value ==0.8.2.1, - any.constraints ==0.13.3, + any.config-value ==0.8.3, + any.constraints ==0.13.4, any.containers ==0.6.4.1, any.contravariant ==1.5.5, contravariant +semigroups +statevar +tagged, any.cookie ==0.4.5, - any.criterion ==1.5.13.0, + any.criterion ==1.6.0.0, criterion -embed-data-files -fast, - any.criterion-measurement ==0.1.3.0, + any.criterion-measurement ==0.2.0.0, criterion-measurement -fast, any.cryptohash-md5 ==0.11.101.0, any.cryptohash-sha1 ==0.11.101.0, @@ -91,7 +90,7 @@ constraints: any.Cabal ==3.4.1.0, any.data-fix ==0.3.2, any.deepseq ==1.4.5.0, any.dense-linear-algebra ==0.1.0.0, - any.deriving-compat ==0.6, + any.deriving-compat ==0.6.1, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.directory ==1.3.6.2, any.distributive ==0.6.2.1, @@ -110,7 +109,7 @@ constraints: any.Cabal ==3.4.1.0, any.filelock ==0.1.1.5, any.filepath ==1.4.2.1, any.fingertree ==0.1.5.0, - any.free ==5.1.7, + any.free ==5.1.9, any.ghc-bignum ==1.1, any.ghc-boot-th ==9.0.2, any.ghc-prim ==0.7.0, @@ -131,34 +130,33 @@ constraints: any.Cabal ==3.4.1.0, any.http2 ==3.0.3, http2 -devel -doc -h2spec, any.indexed-traversable ==0.1.2, - any.indexed-traversable-instances ==0.1.1, + any.indexed-traversable-instances ==0.1.1.1, any.integer-gmp ==1.1, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, any.integer-roots ==1.0.2.0, - any.invariant ==0.5.5, + any.invariant ==0.6, any.io-streams ==1.5.2.1, io-streams +network -nointeractivetests +zlib, any.iproute ==1.7.12, any.js-chart ==2.9.4.1, - any.kan-extensions ==5.2.3, - any.lens ==5.1, + any.kan-extensions ==5.2.5, + any.lens ==5.1.1, lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.3, + any.libBF ==0.6.4, libBF -system-libbf, + any.libffi ==0.2, + libffi +ghc-bundled-libffi, any.math-functions ==0.3.4.2, math-functions +system-erf +system-expm1, - any.megaparsec ==9.2.0, + any.megaparsec ==9.2.1, megaparsec -dev, any.memory ==0.17.0, memory +support_bytestring +support_deepseq, - any.microstache ==1.0.2, + any.microstache ==1.0.2.2, any.mod ==0.1.2.2, mod +semirings +vector, any.monad-control ==1.0.3.1, - any.monad-par ==0.3.5, - monad-par -chaselev -newgeneric, - any.monad-par-extras ==0.3.3, any.monadLib ==3.10.1, any.mtl ==2.2.2, any.mwc-random ==0.15.0.2, @@ -168,7 +166,7 @@ constraints: any.Cabal ==3.4.1.0, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.1, - any.newtype-generics ==0.6.1, + any.newtype-generics ==0.6.2, any.numtype-dk ==0.5.0.3, any.old-locale ==1.0.0.7, any.old-time ==1.1.0.3, @@ -185,20 +183,20 @@ constraints: any.Cabal ==3.4.1.0, any.pretty ==1.1.3.6, any.prettyprinter ==1.7.1, prettyprinter -buildreadme +text, - any.primitive ==0.7.3.0, + any.primitive ==0.7.4.0, any.process ==1.6.13.2, any.profunctors ==5.6.2, any.psqueues ==0.2.7.3, - any.quickcheck-instances ==0.3.27, + any.quickcheck-instances ==0.3.28, quickcheck-instances -bytestring-builder, - any.random ==1.2.1, + any.random ==1.2.1.1, any.reflection ==2.1.6, reflection -slow +template-haskell, any.regex-base ==0.94.0.2, any.regex-compat ==0.95.2.1, any.regex-posix ==0.96.0.1, regex-posix -_regex-posix-clib, - any.resourcet ==1.2.4.3, + any.resourcet ==1.2.6, any.rts ==1.0.2, any.safe ==0.3.19, any.sbv ==9.0, @@ -220,7 +218,7 @@ constraints: any.Cabal ==3.4.1.0, any.simple-smt ==0.9.7, any.splitmix ==0.1.0.4, splitmix -optimised-mixer, - any.statistics ==0.16.0.2, + any.statistics ==0.16.1.0, any.stm ==2.5.0.0, any.streaming-commons ==0.2.2.4, streaming-commons -use-bytestring-builder, @@ -229,7 +227,7 @@ constraints: any.Cabal ==3.4.1.0, any.syb ==0.7.2.1, any.tagged ==0.8.6.1, tagged +deepseq +transformers, - any.tasty ==1.4.2.1, + any.tasty ==1.4.2.3, tasty +clock +unix, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.2, @@ -244,7 +242,7 @@ constraints: any.Cabal ==3.4.1.0, any.text-short ==0.1.5, text-short -asserts, any.tf-random ==0.5, - any.th-abstraction ==0.4.3.0, + any.th-abstraction ==0.4.4.0, any.th-lift ==0.8.2, any.th-lift-instances ==0.1.19, any.these ==1.1.1.1, @@ -253,19 +251,19 @@ constraints: any.Cabal ==3.4.1.0, any.time-compat ==1.9.6.1, time-compat -old-locale, any.time-manager ==0.0.0, - any.tls ==1.5.7, + any.tls ==1.6.0, tls +compat -hans +network, any.tls-session-manager ==0.0.4, any.transformers ==0.5.6.2, any.transformers-base ==0.4.6, transformers-base +orphaninstances, - any.transformers-compat ==0.7.1, + any.transformers-compat ==0.7.2, transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, any.type-equality ==1, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.7.2.2, - any.unix-compat ==0.5.4, + any.unix-compat ==0.6, unix-compat -old-time, any.unix-time ==0.4.7, any.unliftio ==0.2.22.0, @@ -279,7 +277,7 @@ constraints: any.Cabal ==3.4.1.0, vault +useghc, any.vector ==0.12.3.1, vector +boundschecks -internalchecks -unsafechecks -wall, - any.vector-algorithms ==0.8.0.4, + any.vector-algorithms ==0.9.0.1, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, any.vector-binary-instances ==0.2.5.2, any.vector-th-unbox ==0.2.2, @@ -287,19 +285,19 @@ constraints: any.Cabal ==3.4.1.0, any.void ==0.7.3, void -safe, any.wai ==3.2.3, - any.wai-extra ==3.1.10, + any.wai-extra ==3.1.12.1, wai-extra -build-example, any.wai-logger ==2.4.0, - any.warp ==3.3.20, + any.warp ==3.3.22, warp +allow-sendfilefd -network-bytestring -warp-debug +x509, - any.warp-tls ==3.3.2, + any.warp-tls ==3.3.3, any.wcwidth ==0.0.2, wcwidth -cli +split-base, any.what4 ==1.3, what4 -drealtestdisable -solvertests -stptestdisable, any.witherable ==0.4.2, any.word8 ==0.1.3, - any.x509 ==1.7.6, + any.x509 ==1.7.7, any.x509-store ==1.6.9, any.x509-validation ==1.6.12, any.xml ==1.3.14, @@ -307,4 +305,4 @@ constraints: any.Cabal ==3.4.1.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2022-05-04T18:13:54Z +index-state: hackage.haskell.org 2022-08-12T18:38:07Z diff --git a/cabal.GHC-9.2.2.config b/cabal.GHC-9.2.4.config similarity index 85% rename from cabal.GHC-9.2.2.config rename to cabal.GHC-9.2.4.config index db68aade8..ca38427df 100644 --- a/cabal.GHC-9.2.2.config +++ b/cabal.GHC-9.2.4.config @@ -11,10 +11,7 @@ constraints: any.Cabal ==3.6.3.0, any.QuickCheck ==2.14.2, QuickCheck -old-random +templatehaskell, any.StateVar ==1.2.2, - any.abstract-deque ==0.3, - abstract-deque -usecas, - any.abstract-par ==0.3.3, - any.adjunctions ==4.4, + any.adjunctions ==4.4.1, any.aeson ==2.0.3.0, aeson -cffi +ordered-keymap, any.alex ==3.2.7.1, @@ -23,7 +20,7 @@ constraints: any.Cabal ==3.6.3.0, any.ansi-wl-pprint ==0.6.9, ansi-wl-pprint -example, any.appar ==0.1.8, - any.arithmoi ==0.12.0.1, + any.arithmoi ==0.12.0.2, any.array ==0.5.4.0, any.asn1-encoding ==0.9.6, any.asn1-parse ==0.9.5, @@ -34,17 +31,19 @@ constraints: any.Cabal ==3.6.3.0, any.attoparsec ==0.14.4, attoparsec -developer, any.auto-update ==0.1.6, - any.base ==4.16.1.0, - any.base-compat ==0.12.1, - any.base-compat-batteries ==0.12.1, - any.base-orphans ==0.8.6, + any.base ==4.16.3.0, + any.base-compat ==0.12.2, + any.base-compat-batteries ==0.12.2, + any.base-orphans ==0.8.7, any.base64-bytestring ==1.2.1.0, any.basement ==0.0.14, - any.bifunctors ==5.5.11, + any.bifunctors ==5.5.12, bifunctors +semigroups +tagged, - any.bimap ==0.4.0, + any.bimap ==0.5.0, any.binary ==0.8.9.0, - any.binary-orphans ==1.0.2, + any.binary-orphans ==1.0.3, + any.bitvec ==1.1.3.0, + bitvec -libgmp, any.bitwise ==1.0.0.1, any.blaze-builder ==0.4.2.2, any.blaze-html ==0.9.1.2, @@ -56,9 +55,9 @@ constraints: any.Cabal ==3.6.3.0, any.cabal-doctest ==1.0.9, any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, - any.cassava ==0.5.2.0, + any.cassava ==0.5.3.0, cassava -bytestring--lt-0_10_4, - any.cereal ==0.5.8.2, + any.cereal ==0.5.8.3, cereal -bytestring-builder, any.chimera ==0.3.2.0, chimera +representable, @@ -69,15 +68,15 @@ constraints: any.Cabal ==3.6.3.0, any.comonad ==5.0.8, comonad +containers +distributive +indexed-traversable, any.concurrent-extra ==0.7.0.12, - any.config-value ==0.8.2.1, - any.constraints ==0.13.3, + any.config-value ==0.8.3, + any.constraints ==0.13.4, any.containers ==0.6.5.1, any.contravariant ==1.5.5, contravariant +semigroups +statevar +tagged, any.cookie ==0.4.5, - any.criterion ==1.5.13.0, + any.criterion ==1.6.0.0, criterion -embed-data-files -fast, - any.criterion-measurement ==0.1.3.0, + any.criterion-measurement ==0.2.0.0, criterion-measurement -fast, any.cryptohash-md5 ==0.11.101.0, any.cryptohash-sha1 ==0.11.101.0, @@ -91,7 +90,7 @@ constraints: any.Cabal ==3.6.3.0, any.data-fix ==0.3.2, any.deepseq ==1.4.6.1, any.dense-linear-algebra ==0.1.0.0, - any.deriving-compat ==0.6, + any.deriving-compat ==0.6.1, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.directory ==1.3.6.2, any.distributive ==0.6.2.1, @@ -110,9 +109,9 @@ constraints: any.Cabal ==3.6.3.0, any.filelock ==0.1.1.5, any.filepath ==1.4.2.2, any.fingertree ==0.1.5.0, - any.free ==5.1.7, + any.free ==5.1.9, any.ghc-bignum ==1.2, - any.ghc-boot-th ==9.2.2, + any.ghc-boot-th ==9.2.4, any.ghc-prim ==0.8.0, any.gitrev ==1.3.1, any.happy ==1.20.0, @@ -131,34 +130,33 @@ constraints: any.Cabal ==3.6.3.0, any.http2 ==3.0.3, http2 -devel -doc -h2spec, any.indexed-traversable ==0.1.2, - any.indexed-traversable-instances ==0.1.1, + any.indexed-traversable-instances ==0.1.1.1, any.integer-gmp ==1.1, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, any.integer-roots ==1.0.2.0, - any.invariant ==0.5.5, + any.invariant ==0.6, any.io-streams ==1.5.2.1, io-streams +network -nointeractivetests +zlib, any.iproute ==1.7.12, any.js-chart ==2.9.4.1, - any.kan-extensions ==5.2.3, - any.lens ==5.1, + any.kan-extensions ==5.2.5, + any.lens ==5.1.1, lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.3, + any.libBF ==0.6.4, libBF -system-libbf, + any.libffi ==0.2, + libffi +ghc-bundled-libffi, any.math-functions ==0.3.4.2, math-functions +system-erf +system-expm1, - any.megaparsec ==9.2.0, + any.megaparsec ==9.2.1, megaparsec -dev, any.memory ==0.17.0, memory +support_bytestring +support_deepseq, - any.microstache ==1.0.2, + any.microstache ==1.0.2.2, any.mod ==0.1.2.2, mod +semirings +vector, any.monad-control ==1.0.3.1, - any.monad-par ==0.3.5, - monad-par -chaselev -newgeneric, - any.monad-par-extras ==0.3.3, any.monadLib ==3.10.1, any.mtl ==2.2.2, any.mwc-random ==0.15.0.2, @@ -168,7 +166,7 @@ constraints: any.Cabal ==3.6.3.0, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.1, - any.newtype-generics ==0.6.1, + any.newtype-generics ==0.6.2, any.numtype-dk ==0.5.0.3, any.old-locale ==1.0.0.7, any.old-time ==1.1.0.3, @@ -185,20 +183,20 @@ constraints: any.Cabal ==3.6.3.0, any.pretty ==1.1.3.6, any.prettyprinter ==1.7.1, prettyprinter -buildreadme +text, - any.primitive ==0.7.3.0, + any.primitive ==0.7.4.0, any.process ==1.6.13.2, any.profunctors ==5.6.2, any.psqueues ==0.2.7.3, - any.quickcheck-instances ==0.3.27, + any.quickcheck-instances ==0.3.28, quickcheck-instances -bytestring-builder, - any.random ==1.2.1, + any.random ==1.2.1.1, any.reflection ==2.1.6, reflection -slow +template-haskell, any.regex-base ==0.94.0.2, any.regex-compat ==0.95.2.1, any.regex-posix ==0.96.0.1, regex-posix -_regex-posix-clib, - any.resourcet ==1.2.4.3, + any.resourcet ==1.2.6, any.rts ==1.0.2, any.safe ==0.3.19, any.sbv ==9.0, @@ -220,7 +218,7 @@ constraints: any.Cabal ==3.6.3.0, any.simple-smt ==0.9.7, any.splitmix ==0.1.0.4, splitmix -optimised-mixer, - any.statistics ==0.16.0.2, + any.statistics ==0.16.1.0, any.stm ==2.5.0.2, any.streaming-commons ==0.2.2.4, streaming-commons -use-bytestring-builder, @@ -229,7 +227,7 @@ constraints: any.Cabal ==3.6.3.0, any.syb ==0.7.2.1, any.tagged ==0.8.6.1, tagged +deepseq +transformers, - any.tasty ==1.4.2.1, + any.tasty ==1.4.2.3, tasty +clock +unix, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.2, @@ -244,7 +242,7 @@ constraints: any.Cabal ==3.6.3.0, any.text-short ==0.1.5, text-short -asserts, any.tf-random ==0.5, - any.th-abstraction ==0.4.3.0, + any.th-abstraction ==0.4.4.0, any.th-lift ==0.8.2, any.th-lift-instances ==0.1.19, any.these ==1.1.1.1, @@ -253,19 +251,19 @@ constraints: any.Cabal ==3.6.3.0, any.time-compat ==1.9.6.1, time-compat -old-locale, any.time-manager ==0.0.0, - any.tls ==1.5.7, + any.tls ==1.6.0, tls +compat -hans +network, any.tls-session-manager ==0.0.4, any.transformers ==0.5.6.2, any.transformers-base ==0.4.6, transformers-base +orphaninstances, - any.transformers-compat ==0.7.1, + any.transformers-compat ==0.7.2, transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, any.type-equality ==1, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.7.2.2, - any.unix-compat ==0.5.4, + any.unix-compat ==0.6, unix-compat -old-time, any.unix-time ==0.4.7, any.unliftio ==0.2.22.0, @@ -279,7 +277,7 @@ constraints: any.Cabal ==3.6.3.0, vault +useghc, any.vector ==0.12.3.1, vector +boundschecks -internalchecks -unsafechecks -wall, - any.vector-algorithms ==0.8.0.4, + any.vector-algorithms ==0.9.0.1, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, any.vector-binary-instances ==0.2.5.2, any.vector-th-unbox ==0.2.2, @@ -287,19 +285,19 @@ constraints: any.Cabal ==3.6.3.0, any.void ==0.7.3, void -safe, any.wai ==3.2.3, - any.wai-extra ==3.1.10, + any.wai-extra ==3.1.12.1, wai-extra -build-example, any.wai-logger ==2.4.0, - any.warp ==3.3.20, + any.warp ==3.3.22, warp +allow-sendfilefd -network-bytestring -warp-debug +x509, - any.warp-tls ==3.3.2, + any.warp-tls ==3.3.3, any.wcwidth ==0.0.2, wcwidth -cli +split-base, any.what4 ==1.3, what4 -drealtestdisable -solvertests -stptestdisable, any.witherable ==0.4.2, any.word8 ==0.1.3, - any.x509 ==1.7.6, + any.x509 ==1.7.7, any.x509-store ==1.6.9, any.x509-validation ==1.6.12, any.xml ==1.3.14, @@ -307,4 +305,4 @@ constraints: any.Cabal ==3.6.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2022-05-04T18:13:54Z +index-state: hackage.haskell.org 2022-08-12T18:38:07Z diff --git a/cryptol-remote-api/Dockerfile b/cryptol-remote-api/Dockerfile index 225f64dd0..0cb6c870e 100644 --- a/cryptol-remote-api/Dockerfile +++ b/cryptol-remote-api/Dockerfile @@ -1,10 +1,17 @@ ARG GHCVER="8.10.7" ARG GHCVER_BOOTSTRAP="8.10.2" -FROM debian:buster-20210511 AS toolchain +FROM ubuntu:22.04 AS toolchain ARG PORTABILITY=false -RUN apt-get update && apt-get install -y libncurses-dev libz-dev unzip \ - build-essential curl libffi-dev libffi6 libgmp-dev libgmp10 libncurses-dev libncurses5 libtinfo5 libnuma-dev \ - $(if ${PORTABILITY}; then echo git autoconf python3; fi) +RUN apt-get update && \ + apt-get install -y \ + # ghcup requirements + build-essential curl libffi-dev libffi8 libgmp-dev libgmp10 libncurses-dev libncurses6 libtinfo6 \ + # Cryptol dependencies + zlib1g-dev \ + # GHC build dependencies + $(if ${PORTABILITY}; then echo git autoconf python3 libnuma-dev; fi) \ + # Miscellaneous + unzip ENV GHCUP_INSTALL_BASE_PREFIX=/opt \ PATH=/opt/.ghcup/bin:$PATH RUN curl -o /usr/local/bin/ghcup "https://downloads.haskell.org/~ghcup/0.1.17.7/x86_64-linux-ghcup-0.1.17.7" && \ @@ -57,14 +64,14 @@ ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH RUN mkdir -p rootfs/"${CRYPTOLPATH}" \ && cp -r lib/* rootfs/"${CRYPTOLPATH}" WORKDIR /cryptol/rootfs/usr/local/bin -RUN curl -sL -o solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220114/ubuntu-18.04-bin.zip" && \ +RUN curl -sL -o solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220812/ubuntu-22.04-bin.zip" && \ unzip solvers.zip && rm solvers.zip && chmod +x * USER root RUN chown -R root:root /cryptol/rootfs -FROM debian:buster-20210511-slim +FROM ubuntu:22.04 RUN apt-get update \ - && apt-get install -y libgmp10 libgomp1 libffi6 libncurses6 libtinfo6 libreadline7 libnuma-dev openssl \ + && apt-get install -y libgmp10 libgomp1 libffi8 libncurses6 libtinfo6 libreadline8 libnuma-dev openssl \ && apt-get clean && rm -rf /var/lib/apt/lists/* RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol COPY --from=build /cryptol/rootfs / diff --git a/docs/RefMan/FFI.rst b/docs/RefMan/FFI.rst index 6ef7ecbd9..84eba5320 100644 --- a/docs/RefMan/FFI.rst +++ b/docs/RefMan/FFI.rst @@ -188,20 +188,23 @@ Other sizes of floating points are not supported. Sequences ~~~~~~~~~ -Let ``n : #`` be a Cryptol type, possibly containing type variables, that -satisfies ``fin n``, and ``T`` be one of the above Cryptol *integral types* or -*floating point types*. Let ``U`` be the C type that ``T`` corresponds to. - -============ =========== -Cryptol type C type -============ =========== -``[n]T`` ``U*`` -============ =========== - -The C pointer points to an array of ``n`` elements of type ``U``. Note that, -while the length of the array itself is not explicitly passed along with the -pointer, any type arguments contained in the size are passed as C ``size_t``'s -earlier, so the C code can always know the length of the array. +Let ``n1, n2, ..., nk : #`` be Cryptol types (with ``k >= 1``), possibly +containing type variables, that satisfy ``fin n1, fin n2, ..., fin nk``, and +``T`` be one of the above Cryptol *integral types* or *floating point types*. +Let ``U`` be the C type that ``T`` corresponds to. + +==================== =========== +Cryptol type C type +==================== =========== +``[n1][n2]...[nk]T`` ``U*`` +==================== =========== + +The C pointer points to an array of ``n1 * n2 * ... * nk`` elements of type +``U``. If the sequence is multidimensional, it is flattened and stored +contiguously, similar to the representation of multidimensional arrays in C. +Note that, while the dimensions of the array itself are not explicitly passed +along with the pointer, any type arguments contained in the size are passed as C +``size_t``'s earlier, so the C code can always know the dimensions of the array. Tuples and records ~~~~~~~~~~~~~~~~~~ @@ -258,12 +261,12 @@ Cryptol type (or kind) C argument type(s) C return type C output ``[K]Bit`` where ``32 < K <= 64`` ``uint64_t`` ``uint64_t`` ``uint64_t*`` ``Float32`` ``float`` ``float`` ``float*`` ``Float64`` ``double`` ``double`` ``double*`` -``[n]T`` ``U*`` N/A ``U*`` +``[n1][n2]...[nk]T`` ``U*`` N/A ``U*`` ``(T1, T2, ..., Tn)`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn`` ``{f1: T1, f2: T2, ..., fn: Tn}`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn`` ================================== =================== ============= ========================= -where ``K`` is a constant number, ``n`` is a variable number, ``Ti`` is a type, +where ``K`` is a constant number, ``ni`` are variable numbers, ``Ti`` is a type, ``Ui`` is its C argument type, and ``Vi`` is its C output argument type. Memory diff --git a/docs/RefMan/_build/doctrees/FFI.doctree b/docs/RefMan/_build/doctrees/FFI.doctree index 11ab91157..8b44e1ef0 100644 Binary files a/docs/RefMan/_build/doctrees/FFI.doctree and b/docs/RefMan/_build/doctrees/FFI.doctree differ diff --git a/docs/RefMan/_build/doctrees/environment.pickle b/docs/RefMan/_build/doctrees/environment.pickle index dbda8b1dc..1e4de8bee 100644 Binary files a/docs/RefMan/_build/doctrees/environment.pickle and b/docs/RefMan/_build/doctrees/environment.pickle differ diff --git a/docs/RefMan/_build/html/FFI.html b/docs/RefMan/_build/html/FFI.html index 918a0aeec..98e8b9ced 100644 --- a/docs/RefMan/_build/html/FFI.html +++ b/docs/RefMan/_build/html/FFI.html @@ -303,13 +303,14 @@

Floating point types

Sequences

-

Let n : # be a Cryptol type, possibly containing type variables, that -satisfies fin n, and T be one of the above Cryptol integral types or -floating point types. Let U be the C type that T corresponds to.

+

Let n1, n2, ..., nk : # be Cryptol types (with k >= 1), possibly +containing type variables, that satisfy fin n1, fin n2, ..., fin nk, and +T be one of the above Cryptol integral types or floating point types. +Let U be the C type that T corresponds to.

--++ @@ -317,15 +318,17 @@

Sequences

+

Cryptol type

[n]T

[n1][n2]...[nk]T

U*
-

The C pointer points to an array of n elements of type U. Note that, -while the length of the array itself is not explicitly passed along with the -pointer, any type arguments contained in the size are passed as C size_t’s -earlier, so the C code can always know the length of the array.

+

The C pointer points to an array of n1 * n2 * ... * nk elements of type +U. If the sequence is multidimensional, it is flattened and stored +contiguously, similar to the representation of multidimensional arrays in C. +Note that, while the dimensions of the array itself are not explicitly passed +along with the pointer, any type arguments contained in the size are passed as C +size_t’s earlier, so the C code can always know the dimensions of the array.

Tuples and records

@@ -432,7 +435,7 @@

Quick referencedouble

double*

-

[n]T

+

[n1][n2]...[nk]T

U*

N/A

U*

@@ -449,7 +452,7 @@

Quick referenceK is a constant number, n is a variable number, Ti is a type, +

where K is a constant number, ni are variable numbers, Ti is a type, Ui is its C argument type, and Vi is its C output argument type.

diff --git a/docs/RefMan/_build/html/_sources/FFI.rst.txt b/docs/RefMan/_build/html/_sources/FFI.rst.txt index 6ef7ecbd9..84eba5320 100644 --- a/docs/RefMan/_build/html/_sources/FFI.rst.txt +++ b/docs/RefMan/_build/html/_sources/FFI.rst.txt @@ -188,20 +188,23 @@ Other sizes of floating points are not supported. Sequences ~~~~~~~~~ -Let ``n : #`` be a Cryptol type, possibly containing type variables, that -satisfies ``fin n``, and ``T`` be one of the above Cryptol *integral types* or -*floating point types*. Let ``U`` be the C type that ``T`` corresponds to. - -============ =========== -Cryptol type C type -============ =========== -``[n]T`` ``U*`` -============ =========== - -The C pointer points to an array of ``n`` elements of type ``U``. Note that, -while the length of the array itself is not explicitly passed along with the -pointer, any type arguments contained in the size are passed as C ``size_t``'s -earlier, so the C code can always know the length of the array. +Let ``n1, n2, ..., nk : #`` be Cryptol types (with ``k >= 1``), possibly +containing type variables, that satisfy ``fin n1, fin n2, ..., fin nk``, and +``T`` be one of the above Cryptol *integral types* or *floating point types*. +Let ``U`` be the C type that ``T`` corresponds to. + +==================== =========== +Cryptol type C type +==================== =========== +``[n1][n2]...[nk]T`` ``U*`` +==================== =========== + +The C pointer points to an array of ``n1 * n2 * ... * nk`` elements of type +``U``. If the sequence is multidimensional, it is flattened and stored +contiguously, similar to the representation of multidimensional arrays in C. +Note that, while the dimensions of the array itself are not explicitly passed +along with the pointer, any type arguments contained in the size are passed as C +``size_t``'s earlier, so the C code can always know the dimensions of the array. Tuples and records ~~~~~~~~~~~~~~~~~~ @@ -258,12 +261,12 @@ Cryptol type (or kind) C argument type(s) C return type C output ``[K]Bit`` where ``32 < K <= 64`` ``uint64_t`` ``uint64_t`` ``uint64_t*`` ``Float32`` ``float`` ``float`` ``float*`` ``Float64`` ``double`` ``double`` ``double*`` -``[n]T`` ``U*`` N/A ``U*`` +``[n1][n2]...[nk]T`` ``U*`` N/A ``U*`` ``(T1, T2, ..., Tn)`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn`` ``{f1: T1, f2: T2, ..., fn: Tn}`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn`` ================================== =================== ============= ========================= -where ``K`` is a constant number, ``n`` is a variable number, ``Ti`` is a type, +where ``K`` is a constant number, ``ni`` are variable numbers, ``Ti`` is a type, ``Ui`` is its C argument type, and ``Vi`` is its C output argument type. Memory diff --git a/docs/RefMan/_build/html/searchindex.js b/docs/RefMan/_build/html/searchindex.js index 5bf45ee7c..3d37d72c7 100644 --- a/docs/RefMan/_build/html/searchindex.js +++ b/docs/RefMan/_build/html/searchindex.js @@ -1 +1 @@ -Search.setIndex({"docnames": ["BasicSyntax", "BasicTypes", "Expressions", "FFI", "Modules", "OverloadedOperations", "RefMan", "TypeDeclarations"], "filenames": ["BasicSyntax.rst", "BasicTypes.rst", "Expressions.rst", "FFI.rst", "Modules.rst", "OverloadedOperations.rst", "RefMan.rst", "TypeDeclarations.rst"], "titles": ["Basic Syntax", "Basic Types", "Expressions", "Foreign Function Interface", "Modules", "Overloaded Operations", "Cryptol Reference Manual", "Type Declarations"], "terms": {"f": [0, 1, 2, 3, 4], "x": [0, 1, 2, 3, 4, 7], "y": [0, 1, 2, 3, 4], "z": [0, 2, 4], "g": [0, 2, 4], "b": [0, 3, 4, 5, 7], "fin": [0, 3, 4], "group": [0, 4, 7], "ar": [0, 1, 2, 3, 4, 7], "organ": 0, "base": [0, 2], "indent": [0, 4], "same": [0, 1, 3, 4, 7], "belong": 0, "line": [0, 4, 7], "text": 0, "more": [0, 4], "than": [0, 3, 4], "begin": 0, "while": [0, 1, 3], "less": 0, "termin": 0, "consid": [0, 4, 7], "exampl": [0, 1, 2, 4, 6], "follow": [0, 1, 2, 3, 4], "cryptol": [0, 2, 4], "where": [0, 1, 2, 3, 4], "thi": [0, 1, 2, 3, 4], "ha": [0, 1, 2, 3], "two": [0, 1, 2, 4, 7], "one": [0, 2, 3, 4], "all": [0, 2, 3, 4, 7], "between": [0, 6], "The": [0, 1, 2, 3, 4], "principl": 0, "appli": [0, 3], "block": [0, 6], "which": [0, 2, 3, 4, 7], "defin": [0, 1, 3, 4, 7], "local": [0, 4, 6], "name": [0, 1, 3, 6, 7], "support": [0, 4, 6], "start": [0, 1], "end": [0, 4], "mai": [0, 1, 2, 3, 4, 7], "nest": [0, 1, 3, 6], "arbitrarili": 0, "i": [0, 1, 2, 3, 4, 7], "document": [0, 4], "consist": 0, "charact": 0, "first": [0, 1, 3, 4], "must": [0, 3, 4], "either": [0, 3, 4], "an": [0, 1, 2, 3, 6], "english": 0, "letter": 0, "underscor": 0, "_": [0, 1], "decim": 0, "digit": 0, "prime": 0, "some": [0, 4], "have": [0, 1, 2, 3, 4, 7], "special": 0, "mean": [0, 3], "languag": [0, 3], "so": [0, 1, 2, 3, 4], "thei": [0, 1, 3, 4, 7], "us": [0, 1, 2, 3, 4, 7], "programm": 0, "see": [0, 4], "name1": 0, "longer_nam": 0, "name2": 0, "longernam": 0, "extern": 0, "includ": 0, "interfac": [0, 6], "paramet": [0, 2, 6], "properti": 0, "hide": [0, 6], "infix": [0, 6], "let": [0, 3], "pragma": 0, "submodul": [0, 4], "els": [0, 2, 4], "constraint": [0, 6], "infixl": 0, "modul": [0, 3, 6], "primit": 0, "down": [0, 1], "import": [0, 1, 2, 6], "infixr": 0, "newtyp": [0, 4, 6], "privat": [0, 6], "tabl": [0, 3], "contain": [0, 1, 3, 4], "": [0, 2, 3, 4], "associ": 0, "lowest": 0, "highest": 0, "last": [0, 2, 3], "right": [0, 1], "left": [0, 1], "unari": [0, 2], "varieti": 0, "allow": [0, 3, 4, 7], "comput": [0, 1], "specifi": [0, 2, 4], "size": [0, 1, 3], "sequenc": [0, 6], "addit": [0, 4], "subtract": 0, "multipl": [0, 1, 2, 3, 4], "divis": [0, 6], "ceil": [0, 5], "round": [0, 6], "up": [0, 3], "modulu": 0, "pad": [0, 3], "exponenti": 0, "lg2": 0, "logarithm": 0, "2": [0, 1, 2, 3, 4, 7], "width": [0, 4], "bit": [0, 1, 2, 4, 5, 6], "equal": [0, 1, 6, 7], "n": [0, 1, 3, 4], "1": [0, 1, 2, 3, 4, 7], "max": [0, 5], "maximum": 0, "min": [0, 5], "minimum": 0, "written": [0, 1, 2, 3, 7], "binari": [0, 3], "octal": 0, "hexadecim": 0, "notat": [0, 1, 2, 4], "determin": [0, 1], "its": [0, 3, 4], "prefix": [0, 4, 6], "0b": 0, "0o": 0, "0x": 0, "254": 0, "0254": 0, "0b11111110": 0, "0o376": 0, "0xfe": 0, "result": [0, 1, 2, 4], "fix": [0, 1, 3], "length": [0, 1, 3], "e": [0, 1, 4, 5], "number": [0, 1, 2, 3], "overload": [0, 6], "infer": [0, 2], "from": [0, 1, 2, 3, 4], "context": [0, 2], "0b1010": 0, "4": [0, 3], "0o1234": 0, "12": [0, 4], "3": [0, 1, 2, 4, 7], "0x1234": 0, "16": [0, 3], "10": [0, 1, 3, 4], "integ": [0, 2, 5, 7], "also": [0, 1, 3, 4], "polynomi": 0, "write": [0, 1, 3], "express": [0, 1, 4, 6, 7], "term": 0, "open": 0, "close": 0, "degre": 0, "6": [0, 7], "7": [0, 2, 4], "0b1010111": 0, "5": [0, 1, 2, 4], "0b11010": 0, "fraction": 0, "ox": 0, "A": [0, 1, 3, 4, 7], "option": [0, 7], "expon": 0, "mark": 0, "symbol": [0, 3, 4], "p": [0, 1, 4], "2e3": 0, "0x30": 0, "64": [0, 3], "1p4": 0, "ration": 0, "float": [0, 6], "famili": 0, "cannot": [0, 2], "repres": 0, "precis": 0, "Such": [0, 4], "reject": 0, "static": [0, 3], "when": [0, 1, 2, 3, 4], "closest": 0, "represent": 0, "even": [0, 7], "effect": 0, "valu": [0, 1, 4, 6, 7], "improv": [0, 3], "readabl": [0, 3], "here": [0, 2, 4], "0b_0000_0010": 0, "0x_ffff_ffea": 0, "packag": 1, "togeth": [1, 4], "enclos": [1, 4], "parenthes": 1, "curli": 1, "brace": 1, "compon": [1, 3], "both": [1, 4], "separ": [1, 4], "comma": 1, "label": 1, "sign": [1, 6], "identifi": [1, 4, 6], "posit": 1, "order": [1, 3, 4], "most": [1, 4], "purpos": [1, 7], "true": [1, 3], "fals": [1, 3], "lexicograph": 1, "compar": 1, "appear": [1, 7], "wherea": 1, "alphabet": 1, "wai": [1, 3, 4], "via": 1, "pattern": [1, 2], "match": [1, 3], "explicit": [1, 4, 6], "selector": 1, "15": 1, "20": [1, 3], "0": [1, 2, 3], "onli": [1, 3, 4, 7], "program": 1, "suffici": [1, 2], "inform": 1, "shape": 1, "For": [1, 2, 3, 4, 7], "t": [1, 2, 3, 4, 7], "valid": 1, "definit": [1, 2, 4], "known": 1, "isposit": 1, "invalid": 1, "insuffici": 1, "baddef": 1, "mirror": 1, "syntax": [1, 2, 6], "construct": [1, 2, 4], "getfst": 1, "distance2": 1, "xpo": 1, "ypo": 1, "lift": 1, "through": [1, 6], "point": [1, 6], "wise": 1, "equat": 1, "should": [1, 2, 3], "hold": [1, 3], "l": [1, 3], "thu": [1, 4], "we": [1, 3, 4], "can": [1, 2, 3, 4, 7], "quickli": 1, "obtain": [1, 3, 4], "similarli": 1, "get": 1, "entri": 1, "behavior": [1, 3], "quit": [1, 4], "handi": 1, "examin": 1, "complex": 1, "data": 1, "repl": 1, "r": 1, "pt": 1, "100": 1, "set": [1, 3], "30": [1, 4], "rel": 1, "old": 1, "25": 1, "collect": [1, 7], "element": [1, 2, 3], "finit": [1, 2], "often": 1, "call": [1, 3, 4, 6], "word": [1, 3], "abbrevi": 1, "infinit": 1, "inf": [1, 5], "stream": 1, "e1": 1, "e2": 1, "e3": 1, "three": 1, "t1": [1, 3], "t2": [1, 3], "enumer": 1, "exclus": 1, "bound": [1, 3], "stride": 1, "ex": 1, "downward": 1, "t3": 1, "step": [1, 4], "p11": 1, "e11": 1, "p12": 1, "e12": 1, "comprehens": 1, "p21": 1, "e21": 1, "p22": 1, "e22": 1, "gener": [1, 3], "index": 1, "bind": [1, 3], "arr": 1, "j": [1, 4], "dimension": 1, "note": [1, 3, 4], "those": [1, 4], "descript": 1, "concaten": 1, "shift": 1, "rotat": 1, "arithmet": [1, 6], "bitvector": 1, "front": 1, "back": 1, "sub": [1, 4], "updateend": 1, "locat": [1, 4], "updatesend": 1, "There": 1, "pointwis": 1, "p1": 1, "p2": 1, "p3": 1, "p4": 1, "split": [1, 3], "lambda": [1, 2], "section": [2, 3, 4], "provid": [2, 4], "overview": 2, "h": [2, 4], "pair": 2, "paren": 2, "ad": [2, 3, 4], "8": [2, 3, 4], "whole": [2, 3, 4], "9": 2, "variabl": [2, 3], "If": [2, 3, 4], "polymorph": [2, 3], "typaram": 2, "zero": [2, 3, 6], "you": [2, 3, 4], "evalu": [2, 6], "pass": [2, 3, 6], "13": 2, "weakest": 2, "preced": [2, 4], "scope": [2, 4, 7], "defint": 2, "do": [2, 3, 4, 7], "need": [2, 3, 4], "branch": 2, "22": 2, "33": 2, "correspond": [2, 3], "access": [2, 3, 6], "kind": [2, 3], "larg": [2, 3], "accommod": 2, "liter": [2, 6], "backtick": 2, "sugar": [2, 4], "applic": 2, "primtiv": 2, "abov": [2, 3, 4], "suitabl": 2, "automat": [2, 3], "chosen": 2, "possibl": [2, 4], "usual": 2, "ffi": 3, "other": [3, 4, 7], "convent": 3, "current": 3, "window": 3, "work": [3, 4], "unix": 3, "like": [3, 4, 7], "system": [3, 4], "maco": 3, "linux": 3, "suppos": 3, "want": [3, 4], "uint32_t": 3, "add": [3, 4], "In": [3, 4], "our": 3, "file": [3, 4], "declar": [3, 4, 6], "bodi": [3, 7], "32": [3, 4], "dynam": 3, "load": 3, "share": 3, "librari": 3, "look": [3, 4], "directori": [3, 4], "differ": [3, 4], "extens": 3, "exact": 3, "specif": 3, "On": 3, "dylib": 3, "your": 3, "foo": 3, "cry": [3, 4], "Then": [3, 4], "each": [3, 4, 7], "case": [3, 4], "onc": [3, 4], "ani": [3, 4, 7], "sinc": [3, 4], "sourc": [3, 4], "check": 3, "actual": 3, "It": [3, 4], "respons": 3, "make": [3, 4], "sure": [3, 4], "undefin": 3, "doe": 3, "handl": 3, "simpl": [3, 4], "manual": 3, "command": 3, "cc": 3, "fpic": 3, "o": 3, "dynamiclib": 3, "describ": [3, 4], "how": 3, "given": 3, "signatur": [3, 6], "map": 3, "prototyp": 3, "limit": 3, "clear": 3, "translat": 3, "These": 3, "curri": 3, "argument": [3, 6, 7], "certain": 3, "befor": [3, 4], "That": 3, "could": 3, "mani": [3, 4], "after": 3, "directli": [3, 7], "output": 3, "depend": 3, "pointer": 3, "modifi": 3, "store": 3, "list": [3, 6], "size_t": 3, "numer": [3, 4, 6], "furthermor": 3, "satisfi": 3, "explicitli": 3, "fit": 3, "runtim": 3, "error": [3, 4], "requir": [3, 4], "instead": [3, 4, 7], "just": [3, 4, 7], "practic": [3, 4], "would": [3, 4, 7], "too": 3, "cumbersom": [3, 4], "uint8_t": 3, "nonzero": 3, "k": 3, "uint16_t": 3, "uint64_t": 3, "smaller": 3, "extra": 3, "ignor": 3, "instanc": 3, "0xf": 3, "0x0f": 3, "0xaf": 3, "larger": 3, "standard": 3, "convers": 3, "arrai": 3, "float32": 3, "float64": 3, "doubl": 3, "built": [3, 6], "possibli": 3, "u": 3, "itself": [3, 4], "along": 3, "earlier": 3, "alwai": 3, "know": 3, "tn": 3, "mention": [3, 7], "themselv": 3, "u1": 3, "u2": 3, "un": 3, "respect": 3, "f1": 3, "f2": 3, "fn": 3, "arbitrari": 3, "field": [3, 5, 6, 7], "flatten": 3, "out": 3, "behav": 3, "individu": 3, "recurs": [3, 4, 7], "empti": 3, "don": 3, "void": 3, "treat": [3, 4, 7], "except": [3, 4], "input": 3, "version": 3, "becaus": [3, 4], "alreadi": 3, "involv": 3, "alloc": 3, "dealloc": 3, "manag": [3, 6], "non": 3, "piec": 3, "enough": 3, "try": [3, 4], "adjac": 3, "uniniti": 3, "read": 3, "relat": 4, "top": 4, "level": [4, 6], "m": 4, "type": [4, 6], "glu": 4, "ordinari": 4, "hash": 4, "sha256": 4, "structur": [4, 6], "implement": 4, "search": 4, "cryptolpath": 4, "To": 4, "anoth": 4, "wa": 4, "sometim": 4, "0x02": 4, "0x03": 4, "0x04": 4, "help": 4, "reduc": 4, "collis": 4, "tend": 4, "code": [4, 6], "easier": 4, "understand": 4, "easi": 4, "them": 4, "few": 4, "clash": 4, "situat": 4, "conveni": 4, "everyth": 4, "avoid": 4, "happen": 4, "combin": 4, "claus": 4, "introduc": 4, "might": 4, "helper": 4, "function": [4, 6, 7], "intend": 4, "outsid": 4, "good": 4, "place": 4, "0x01": 4, "helper1": 4, "helper2": 4, "public": 4, "remain": 4, "extend": 4, "keyword": [4, 6], "new": [4, 7], "layout": [4, 6], "singl": 4, "equival": 4, "previou": 4, "withing": 4, "keword": 4, "refer": 4, "shadow": 4, "outer": 4, "submdul": 4, "across": 4, "submould": 4, "bring": [4, 7], "upcom": 4, "variant": 4, "featur": 4, "yet": 4, "part": 4, "main": [3, 4], "content": 4, "without": 4, "concret": 4, "assumpt": 4, "about": 4, "constant": [3, 4], "desrib": 4, "parmaet": 4, "sumbodul": 4, "mayb": 4, "link": 4, "abl": 4, "impos": 4, "cours": 4, "done": 4, "impl": 4, "26": 4, "myf": 4, "fill": 4, "my": 4, "slight": 4, "variat": 4, "impl1": 4, "impl2": 4, "deriv": 4, "somewher": 4, "presum": 4, "coupl": 4, "straight": 4, "awai": 4, "thing": 4, "notion": 4, "11": 4, "syntact": 4, "functor": 4, "time": 4, "synonym": [4, 6], "noth": 4, "exist": [4, 7], "semant": 4, "occasion": 4, "being": 4, "eq": 5, "cmp": 5, "ab": 5, "ring": 5, "signedcmp": 5, "complement": 5, "frominteg": 5, "negat": 5, "tointeg": 5, "inffrom": 5, "inffromthen": 5, "recip": 5, "floor": 5, "trunc": 5, "roundawai": 5, "roundtoeven": 5, "basic": 6, "comment": 6, "oper": 6, "annot": 6, "instanti": 6, "condit": 6, "demot": 6, "tupl": 6, "record": [6, 7], "updat": 6, "comparison": 6, "logic": 6, "integr": 6, "hierarch": 6, "qualifi": 6, "implicit": 6, "parameter": 6, "anonym": 6, "foreign": 6, "platform": 6, "usag": 6, "compil": 6, "c": 6, "convert": 6, "overal": 6, "return": 6, "memori": 6, "creat": 7, "pre": 7, "transpar": 7, "unfold": 7, "site": 7, "though": 7, "user": 7, "had": 7, "newt": 7, "seq": 7, "unlik": 7, "distinct": 7, "checker": 7, "moreov": 7, "member": 7, "typeclass": 7, "typecheck": 7, "otherwis": 7, "irrelev": 7, "form": 7, "everi": 7, "project": 7, "extract": 7, "sum": 7, "someth": 3, "a1": 3, "ak": 3, "c1": 3, "cn": 3, "tm": 3, "tr": 3, "expand": 3, "rule": 3, "out0": 3, "out1": 3, "in0": 3, "in1": 3, "in2": 3, "fulli": 3, "process": 3, "0x00000003": 3, "v1": 3, "v2": 3, "vn": 3, "ti": 3, "ui": 3, "vi": 3, "quick": 6}, "objects": {}, "objtypes": {}, "objnames": {}, "titleterms": {"basic": [0, 1, 3, 5], "syntax": 0, "declar": [0, 2, 7], "type": [0, 1, 2, 3, 7], "signatur": 0, "layout": 0, "comment": 0, "todo": [0, 2], "identifi": 0, "keyword": 0, "built": 0, "oper": [0, 1, 2, 5], "preced": 0, "level": 0, "numer": [0, 2], "liter": 0, "tupl": [1, 3], "record": [1, 3], "access": 1, "field": 1, "updat": 1, "sequenc": [1, 3], "function": [1, 2, 3], "express": 2, "call": 2, "prefix": 2, "infix": 2, "annot": 2, "explicit": 2, "instanti": [2, 4], "local": 2, "block": [2, 4], "argument": [2, 4], "condit": 2, "demot": 2, "valu": [2, 3], "foreign": 3, "interfac": [3, 4], "platform": 3, "support": 3, "usag": 3, "compil": 3, "c": 3, "code": 3, "convert": 3, "between": 3, "cryptol": [3, 6], "overal": 3, "structur": 3, "paramet": [3, 4], "bit": 3, "integr": [3, 5], "float": 3, "point": 3, "return": 3, "memori": 3, "modul": 4, "hierarch": 4, "name": 4, "import": 4, "list": 4, "hide": 4, "qualifi": 4, "privat": 4, "nest": 4, "implicit": 4, "manag": 4, "parameter": 4, "an": 4, "constraint": 4, "anonym": 4, "pass": 4, "through": 4, "overload": 5, "equal": 5, "comparison": 5, "sign": 5, "zero": 5, "logic": 5, "arithmet": 5, "divis": 5, "round": 5, "refer": [3, 6], "manual": 6, "synonym": [3, 7], "newtyp": 7, "exampl": 3, "evalu": 3, "quick": 3}, "envversion": {"sphinx.domains.c": 2, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 6, "sphinx.domains.index": 1, "sphinx.domains.javascript": 2, "sphinx.domains.math": 2, "sphinx.domains.python": 3, "sphinx.domains.rst": 2, "sphinx.domains.std": 2, "sphinx.ext.todo": 2, "sphinx": 56}}) \ No newline at end of file +Search.setIndex({"docnames": ["BasicSyntax", "BasicTypes", "Expressions", "FFI", "Modules", "OverloadedOperations", "RefMan", "TypeDeclarations"], "filenames": ["BasicSyntax.rst", "BasicTypes.rst", "Expressions.rst", "FFI.rst", "Modules.rst", "OverloadedOperations.rst", "RefMan.rst", "TypeDeclarations.rst"], "titles": ["Basic Syntax", "Basic Types", "Expressions", "Foreign Function Interface", "Modules", "Overloaded Operations", "Cryptol Reference Manual", "Type Declarations"], "terms": {"f": [0, 1, 2, 3, 4], "x": [0, 1, 2, 3, 4, 7], "y": [0, 1, 2, 3, 4], "z": [0, 2, 4], "g": [0, 2, 4], "b": [0, 3, 4, 5, 7], "fin": [0, 3, 4], "group": [0, 4, 7], "ar": [0, 1, 2, 3, 4, 7], "organ": 0, "base": [0, 2], "indent": [0, 4], "same": [0, 1, 3, 4, 7], "belong": 0, "line": [0, 4, 7], "text": 0, "more": [0, 4], "than": [0, 3, 4], "begin": 0, "while": [0, 1, 3], "less": 0, "termin": 0, "consid": [0, 4, 7], "exampl": [0, 1, 2, 4, 6], "follow": [0, 1, 2, 3, 4], "cryptol": [0, 2, 4], "where": [0, 1, 2, 3, 4], "thi": [0, 1, 2, 3, 4], "ha": [0, 1, 2, 3], "two": [0, 1, 2, 4, 7], "one": [0, 2, 3, 4], "all": [0, 2, 3, 4, 7], "between": [0, 6], "The": [0, 1, 2, 3, 4], "principl": 0, "appli": [0, 3], "block": [0, 6], "which": [0, 2, 3, 4, 7], "defin": [0, 1, 3, 4, 7], "local": [0, 4, 6], "name": [0, 1, 3, 6, 7], "support": [0, 4, 6], "start": [0, 1], "end": [0, 4], "mai": [0, 1, 2, 3, 4, 7], "nest": [0, 1, 3, 6], "arbitrarili": 0, "i": [0, 1, 2, 3, 4, 7], "document": [0, 4], "consist": 0, "charact": 0, "first": [0, 1, 3, 4], "must": [0, 3, 4], "either": [0, 3, 4], "an": [0, 1, 2, 3, 6], "english": 0, "letter": 0, "underscor": 0, "_": [0, 1], "decim": 0, "digit": 0, "prime": 0, "some": [0, 4], "have": [0, 1, 2, 3, 4, 7], "special": 0, "mean": [0, 3], "languag": [0, 3], "so": [0, 1, 2, 3, 4], "thei": [0, 1, 3, 4, 7], "us": [0, 1, 2, 3, 4, 7], "programm": 0, "see": [0, 4], "name1": 0, "longer_nam": 0, "name2": 0, "longernam": 0, "extern": 0, "includ": 0, "interfac": [0, 6], "paramet": [0, 2, 6], "properti": 0, "hide": [0, 6], "infix": [0, 6], "let": [0, 3], "pragma": 0, "submodul": [0, 4], "els": [0, 2, 4], "constraint": [0, 6], "infixl": 0, "modul": [0, 3, 6], "primit": 0, "down": [0, 1], "import": [0, 1, 2, 6], "infixr": 0, "newtyp": [0, 4, 6], "privat": [0, 6], "tabl": [0, 3], "contain": [0, 1, 3, 4], "": [0, 2, 3, 4], "associ": 0, "lowest": 0, "highest": 0, "last": [0, 2, 3], "right": [0, 1], "left": [0, 1], "unari": [0, 2], "varieti": 0, "allow": [0, 3, 4, 7], "comput": [0, 1], "specifi": [0, 2, 4], "size": [0, 1, 3], "sequenc": [0, 6], "addit": [0, 4], "subtract": 0, "multipl": [0, 1, 2, 3, 4], "divis": [0, 6], "ceil": [0, 5], "round": [0, 6], "up": [0, 3], "modulu": 0, "pad": [0, 3], "exponenti": 0, "lg2": 0, "logarithm": 0, "2": [0, 1, 2, 3, 4, 7], "width": [0, 4], "bit": [0, 1, 2, 4, 5, 6], "equal": [0, 1, 6, 7], "n": [0, 1, 3, 4], "1": [0, 1, 2, 3, 4, 7], "max": [0, 5], "maximum": 0, "min": [0, 5], "minimum": 0, "written": [0, 1, 2, 3, 7], "binari": [0, 3], "octal": 0, "hexadecim": 0, "notat": [0, 1, 2, 4], "determin": [0, 1], "its": [0, 3, 4], "prefix": [0, 4, 6], "0b": 0, "0o": 0, "0x": 0, "254": 0, "0254": 0, "0b11111110": 0, "0o376": 0, "0xfe": 0, "result": [0, 1, 2, 4], "fix": [0, 1, 3], "length": [0, 1], "e": [0, 1, 4, 5], "number": [0, 1, 2, 3], "overload": [0, 6], "infer": [0, 2], "from": [0, 1, 2, 3, 4], "context": [0, 2], "0b1010": 0, "4": [0, 3], "0o1234": 0, "12": [0, 4], "3": [0, 1, 2, 4, 7], "0x1234": 0, "16": [0, 3], "10": [0, 1, 3, 4], "integ": [0, 2, 5, 7], "also": [0, 1, 3, 4], "polynomi": 0, "write": [0, 1, 3], "express": [0, 1, 4, 6, 7], "term": 0, "open": 0, "close": 0, "degre": 0, "6": [0, 7], "7": [0, 2, 4], "0b1010111": 0, "5": [0, 1, 2, 4], "0b11010": 0, "fraction": 0, "ox": 0, "A": [0, 1, 3, 4, 7], "option": [0, 7], "expon": 0, "mark": 0, "symbol": [0, 3, 4], "p": [0, 1, 4], "2e3": 0, "0x30": 0, "64": [0, 3], "1p4": 0, "ration": 0, "float": [0, 6], "famili": 0, "cannot": [0, 2], "repres": 0, "precis": 0, "Such": [0, 4], "reject": 0, "static": [0, 3], "when": [0, 1, 2, 3, 4], "closest": 0, "represent": [0, 3], "even": [0, 7], "effect": 0, "valu": [0, 1, 4, 6, 7], "improv": [0, 3], "readabl": [0, 3], "here": [0, 2, 4], "0b_0000_0010": 0, "0x_ffff_ffea": 0, "packag": 1, "togeth": [1, 4], "enclos": [1, 4], "parenthes": 1, "curli": 1, "brace": 1, "compon": [1, 3], "both": [1, 4], "separ": [1, 4], "comma": 1, "label": 1, "sign": [1, 6], "identifi": [1, 4, 6], "posit": 1, "order": [1, 3, 4], "most": [1, 4], "purpos": [1, 7], "true": [1, 3], "fals": [1, 3], "lexicograph": 1, "compar": 1, "appear": [1, 7], "wherea": 1, "alphabet": 1, "wai": [1, 3, 4], "via": 1, "pattern": [1, 2], "match": [1, 3], "explicit": [1, 4, 6], "selector": 1, "15": 1, "20": [1, 3], "0": [1, 2, 3], "onli": [1, 3, 4, 7], "program": 1, "suffici": [1, 2], "inform": 1, "shape": 1, "For": [1, 2, 3, 4, 7], "t": [1, 2, 3, 4, 7], "valid": 1, "definit": [1, 2, 4], "known": 1, "isposit": 1, "invalid": 1, "insuffici": 1, "baddef": 1, "mirror": 1, "syntax": [1, 2, 6], "construct": [1, 2, 4], "getfst": 1, "distance2": 1, "xpo": 1, "ypo": 1, "lift": 1, "through": [1, 6], "point": [1, 6], "wise": 1, "equat": 1, "should": [1, 2, 3], "hold": [1, 3], "l": [1, 3], "thu": [1, 4], "we": [1, 3, 4], "can": [1, 2, 3, 4, 7], "quickli": 1, "obtain": [1, 3, 4], "similarli": 1, "get": 1, "entri": 1, "behavior": [1, 3], "quit": [1, 4], "handi": 1, "examin": 1, "complex": 1, "data": 1, "repl": 1, "r": 1, "pt": 1, "100": 1, "set": [1, 3], "30": [1, 4], "rel": 1, "old": 1, "25": 1, "collect": [1, 7], "element": [1, 2, 3], "finit": [1, 2], "often": 1, "call": [1, 3, 4, 6], "word": [1, 3], "abbrevi": 1, "infinit": 1, "inf": [1, 5], "stream": 1, "e1": 1, "e2": 1, "e3": 1, "three": 1, "t1": [1, 3], "t2": [1, 3], "enumer": 1, "exclus": 1, "bound": [1, 3], "stride": 1, "ex": 1, "downward": 1, "t3": 1, "step": [1, 4], "p11": 1, "e11": 1, "p12": 1, "e12": 1, "comprehens": 1, "p21": 1, "e21": 1, "p22": 1, "e22": 1, "gener": [1, 3], "index": 1, "bind": [1, 3], "arr": 1, "j": [1, 4], "dimension": 1, "note": [1, 3, 4], "those": [1, 4], "descript": 1, "concaten": 1, "shift": 1, "rotat": 1, "arithmet": [1, 6], "bitvector": 1, "front": 1, "back": 1, "sub": [1, 4], "updateend": 1, "locat": [1, 4], "updatesend": 1, "There": 1, "pointwis": 1, "p1": 1, "p2": 1, "p3": 1, "p4": 1, "split": [1, 3], "lambda": [1, 2], "section": [2, 3, 4], "provid": [2, 4], "overview": 2, "h": [2, 4], "pair": 2, "paren": 2, "ad": [2, 3, 4], "8": [2, 3, 4], "whole": [2, 3, 4], "9": 2, "variabl": [2, 3], "If": [2, 3, 4], "polymorph": [2, 3], "typaram": 2, "zero": [2, 3, 6], "you": [2, 3, 4], "evalu": [2, 6], "pass": [2, 3, 6], "13": 2, "weakest": 2, "preced": [2, 4], "scope": [2, 4, 7], "defint": 2, "do": [2, 3, 4, 7], "need": [2, 3, 4], "branch": 2, "22": 2, "33": 2, "correspond": [2, 3], "access": [2, 3, 6], "kind": [2, 3], "larg": [2, 3], "accommod": 2, "liter": [2, 6], "backtick": 2, "sugar": [2, 4], "applic": 2, "primtiv": 2, "abov": [2, 3, 4], "suitabl": 2, "automat": [2, 3], "chosen": 2, "possibl": [2, 4], "usual": 2, "ffi": 3, "other": [3, 4, 7], "convent": 3, "current": 3, "window": 3, "work": [3, 4], "unix": 3, "like": [3, 4, 7], "system": [3, 4], "maco": 3, "linux": 3, "suppos": 3, "want": [3, 4], "uint32_t": 3, "add": [3, 4], "In": [3, 4], "our": 3, "file": [3, 4], "declar": [3, 4, 6], "bodi": [3, 7], "32": [3, 4], "dynam": 3, "load": 3, "share": 3, "librari": 3, "look": [3, 4], "directori": [3, 4], "differ": [3, 4], "extens": 3, "exact": 3, "specif": 3, "On": 3, "dylib": 3, "your": 3, "foo": 3, "cry": [3, 4], "Then": [3, 4], "each": [3, 4, 7], "case": [3, 4], "onc": [3, 4], "ani": [3, 4, 7], "sinc": [3, 4], "sourc": [3, 4], "check": 3, "actual": 3, "It": [3, 4], "respons": 3, "make": [3, 4], "sure": [3, 4], "undefin": 3, "doe": 3, "handl": 3, "simpl": [3, 4], "manual": 3, "command": 3, "cc": 3, "fpic": 3, "o": 3, "dynamiclib": 3, "describ": [3, 4], "how": 3, "given": 3, "signatur": [3, 6], "map": 3, "prototyp": 3, "limit": 3, "clear": 3, "translat": 3, "These": 3, "curri": 3, "argument": [3, 6, 7], "certain": 3, "befor": [3, 4], "That": 3, "could": 3, "mani": [3, 4], "after": 3, "directli": [3, 7], "output": 3, "depend": 3, "pointer": 3, "modifi": 3, "store": 3, "list": [3, 6], "size_t": 3, "numer": [3, 4, 6], "furthermor": 3, "satisfi": 3, "explicitli": 3, "fit": 3, "runtim": 3, "error": [3, 4], "requir": [3, 4], "instead": [3, 4, 7], "just": [3, 4, 7], "practic": [3, 4], "would": [3, 4, 7], "too": 3, "cumbersom": [3, 4], "uint8_t": 3, "nonzero": 3, "k": 3, "uint16_t": 3, "uint64_t": 3, "smaller": 3, "extra": 3, "ignor": 3, "instanc": 3, "0xf": 3, "0x0f": 3, "0xaf": 3, "larger": 3, "standard": 3, "convers": 3, "arrai": 3, "float32": 3, "float64": 3, "doubl": 3, "built": [3, 6], "possibli": 3, "u": 3, "itself": [3, 4], "along": 3, "earlier": 3, "alwai": 3, "know": 3, "tn": 3, "mention": [3, 7], "themselv": 3, "u1": 3, "u2": 3, "un": 3, "respect": 3, "f1": 3, "f2": 3, "fn": 3, "arbitrari": 3, "field": [3, 5, 6, 7], "flatten": 3, "out": 3, "behav": 3, "individu": 3, "recurs": [3, 4, 7], "empti": 3, "don": 3, "void": 3, "treat": [3, 4, 7], "except": [3, 4], "input": 3, "version": 3, "becaus": [3, 4], "alreadi": 3, "involv": 3, "alloc": 3, "dealloc": 3, "manag": [3, 6], "non": 3, "piec": 3, "enough": 3, "try": [3, 4], "adjac": 3, "uniniti": 3, "read": 3, "relat": 4, "top": 4, "level": [4, 6], "m": 4, "type": [4, 6], "glu": 4, "ordinari": 4, "hash": 4, "sha256": 4, "structur": [4, 6], "implement": 4, "search": 4, "cryptolpath": 4, "To": 4, "anoth": 4, "wa": 4, "sometim": 4, "0x02": 4, "0x03": 4, "0x04": 4, "help": 4, "reduc": 4, "collis": 4, "tend": 4, "code": [4, 6], "easier": 4, "understand": 4, "easi": 4, "them": 4, "few": 4, "clash": 4, "situat": 4, "conveni": 4, "everyth": 4, "avoid": 4, "happen": 4, "combin": 4, "claus": 4, "introduc": 4, "might": 4, "helper": 4, "function": [4, 6, 7], "intend": 4, "outsid": 4, "good": 4, "place": 4, "0x01": 4, "helper1": 4, "helper2": 4, "public": 4, "remain": 4, "extend": 4, "keyword": [4, 6], "new": [4, 7], "layout": [4, 6], "singl": 4, "equival": 4, "previou": 4, "withing": 4, "keword": 4, "refer": 4, "shadow": 4, "outer": 4, "submdul": 4, "across": 4, "submould": 4, "bring": [4, 7], "upcom": 4, "variant": 4, "featur": 4, "yet": 4, "part": 4, "main": [3, 4], "content": 4, "without": 4, "concret": 4, "assumpt": 4, "about": 4, "constant": [3, 4], "desrib": 4, "parmaet": 4, "sumbodul": 4, "mayb": 4, "link": 4, "abl": 4, "impos": 4, "cours": 4, "done": 4, "impl": 4, "26": 4, "myf": 4, "fill": 4, "my": 4, "slight": 4, "variat": 4, "impl1": 4, "impl2": 4, "deriv": 4, "somewher": 4, "presum": 4, "coupl": 4, "straight": 4, "awai": 4, "thing": 4, "notion": 4, "11": 4, "syntact": 4, "functor": 4, "time": 4, "synonym": [4, 6], "noth": 4, "exist": [4, 7], "semant": 4, "occasion": 4, "being": 4, "eq": 5, "cmp": 5, "ab": 5, "ring": 5, "signedcmp": 5, "complement": 5, "frominteg": 5, "negat": 5, "tointeg": 5, "inffrom": 5, "inffromthen": 5, "recip": 5, "floor": 5, "trunc": 5, "roundawai": 5, "roundtoeven": 5, "basic": 6, "comment": 6, "oper": 6, "annot": 6, "instanti": 6, "condit": 6, "demot": 6, "tupl": 6, "record": [6, 7], "updat": 6, "comparison": 6, "logic": 6, "integr": 6, "hierarch": 6, "qualifi": 6, "implicit": 6, "parameter": 6, "anonym": 6, "foreign": 6, "platform": 6, "usag": 6, "compil": 6, "c": 6, "convert": 6, "overal": 6, "return": 6, "memori": 6, "creat": 7, "pre": 7, "transpar": 7, "unfold": 7, "site": 7, "though": 7, "user": 7, "had": 7, "newt": 7, "seq": 7, "unlik": 7, "distinct": 7, "checker": 7, "moreov": 7, "member": 7, "typeclass": 7, "typecheck": 7, "otherwis": 7, "irrelev": 7, "form": 7, "everi": 7, "project": 7, "extract": 7, "sum": 7, "someth": 3, "a1": 3, "ak": 3, "c1": 3, "cn": 3, "tm": 3, "tr": 3, "expand": 3, "rule": 3, "out0": 3, "out1": 3, "in0": 3, "in1": 3, "in2": 3, "fulli": 3, "process": 3, "0x00000003": 3, "v1": 3, "v2": 3, "vn": 3, "ti": 3, "ui": 3, "vi": 3, "quick": 6, "n1": 3, "n2": 3, "nk": 3, "multidimension": 3, "contigu": 3, "similar": 3, "dimens": 3, "ni": 3}, "objects": {}, "objtypes": {}, "objnames": {}, "titleterms": {"basic": [0, 1, 3, 5], "syntax": 0, "declar": [0, 2, 7], "type": [0, 1, 2, 3, 7], "signatur": 0, "layout": 0, "comment": 0, "todo": [0, 2], "identifi": 0, "keyword": 0, "built": 0, "oper": [0, 1, 2, 5], "preced": 0, "level": 0, "numer": [0, 2], "liter": 0, "tupl": [1, 3], "record": [1, 3], "access": 1, "field": 1, "updat": 1, "sequenc": [1, 3], "function": [1, 2, 3], "express": 2, "call": 2, "prefix": 2, "infix": 2, "annot": 2, "explicit": 2, "instanti": [2, 4], "local": 2, "block": [2, 4], "argument": [2, 4], "condit": 2, "demot": 2, "valu": [2, 3], "foreign": 3, "interfac": [3, 4], "platform": 3, "support": 3, "usag": 3, "compil": 3, "c": 3, "code": 3, "convert": 3, "between": 3, "cryptol": [3, 6], "overal": 3, "structur": 3, "paramet": [3, 4], "bit": 3, "integr": [3, 5], "float": 3, "point": 3, "return": 3, "memori": 3, "modul": 4, "hierarch": 4, "name": 4, "import": 4, "list": 4, "hide": 4, "qualifi": 4, "privat": 4, "nest": 4, "implicit": 4, "manag": 4, "parameter": 4, "an": 4, "constraint": 4, "anonym": 4, "pass": 4, "through": 4, "overload": 5, "equal": 5, "comparison": 5, "sign": 5, "zero": 5, "logic": 5, "arithmet": 5, "divis": 5, "round": 5, "refer": [3, 6], "manual": 6, "synonym": [3, 7], "newtyp": 7, "exampl": 3, "evalu": 3, "quick": 3}, "envversion": {"sphinx.domains.c": 2, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 6, "sphinx.domains.index": 1, "sphinx.domains.javascript": 2, "sphinx.domains.math": 2, "sphinx.domains.python": 3, "sphinx.domains.rst": 2, "sphinx.domains.std": 2, "sphinx.ext.todo": 2, "sphinx": 56}}) \ No newline at end of file diff --git a/src/Cryptol/Backend/FFI.hs b/src/Cryptol/Backend/FFI.hs index 7b13d16be..686c02385 100644 --- a/src/Cryptol/Backend/FFI.hs +++ b/src/Cryptol/Backend/FFI.hs @@ -12,6 +12,7 @@ -- libraries. Currently works on Unix only. module Cryptol.Backend.FFI ( ForeignSrc + , getForeignSrcPath , loadForeignSrc , unloadForeignSrc #ifdef FFI_ENABLED @@ -56,12 +57,14 @@ import GHC.Generics -- | A source from which we can retrieve implementations of foreign functions. data ForeignSrc = ForeignSrc - { -- | The 'ForeignPtr' wraps the pointer returned by 'dlopen', where the + { -- | The file path of the 'ForeignSrc'. + foreignSrcPath :: FilePath + -- | The 'ForeignPtr' wraps the pointer returned by 'dlopen', where the -- finalizer calls 'dlclose' when the library is no longer needed. We keep -- references to the 'ForeignPtr' in each foreign function that is in the -- evaluation environment, so that the shared library will stay open as long -- as there are references to it. - foreignSrcFPtr :: ForeignPtr () + , foreignSrcFPtr :: ForeignPtr () -- | We support explicit unloading of the shared library so we keep track of -- if it has already been unloaded, and if so the finalizer does nothing. -- This is updated atomically when the library is unloaded. @@ -73,16 +76,20 @@ instance Show ForeignSrc where instance NFData ForeignSrc where rnf ForeignSrc {..} = foreignSrcFPtr `seq` foreignSrcLoaded `deepseq` () +-- | Get the file path of the 'ForeignSrc'. +getForeignSrcPath :: ForeignSrc -> Maybe FilePath +getForeignSrcPath = Just . foreignSrcPath + -- | Load a 'ForeignSrc' for the given __Cryptol__ file path. The file path of -- the shared library that we try to load is the same as the Cryptol file path -- except with a platform specific extension. loadForeignSrc :: FilePath -> IO (Either FFILoadError ForeignSrc) -loadForeignSrc = loadForeignLib >=> traverse \ptr -> do +loadForeignSrc = loadForeignLib >=> traverse \(foreignSrcPath, ptr) -> do foreignSrcLoaded <- newMVar True foreignSrcFPtr <- newForeignPtr ptr (unloadForeignSrc' foreignSrcLoaded ptr) pure ForeignSrc {..} -loadForeignLib :: FilePath -> IO (Either FFILoadError (Ptr ())) +loadForeignLib :: FilePath -> IO (Either FFILoadError (FilePath, Ptr ())) #ifdef darwin_HOST_OS -- On Darwin, try loading .dylib first, and if that fails try .so loadForeignLib path = @@ -95,9 +102,12 @@ loadForeignLib path = loadForeignLib path = tryLoad (CantLoadFFISrc path) $ open "so" #endif - where -- RTLD_NOW so we can make sure that the symbols actually exist at - -- module loading time - open ext = undl <$> dlopen (path -<.> ext) [RTLD_NOW] + where open ext = do + let libPath = path -<.> ext + -- RTLD_NOW so we can make sure that the symbols actually exist at + -- module loading time + ptr <- undl <$> dlopen libPath [RTLD_NOW] + pure (libPath, ptr) -- | Explicitly unload a 'ForeignSrc' immediately instead of waiting for the -- garbage collector to do it. This can be useful if you want to immediately @@ -218,6 +228,9 @@ callForeignImpl ForeignImpl {..} xs = withForeignSrc foreignImplSrc \_ -> data ForeignSrc = ForeignSrc deriving (Show, Generic, NFData) +getForeignSrcPath :: ForeignSrc -> Maybe FilePath +getForeignSrcPath _ = Nothing + loadForeignSrc :: FilePath -> IO (Either FFILoadError ForeignSrc) loadForeignSrc _ = pure $ Right ForeignSrc diff --git a/src/Cryptol/Eval/FFI.hs b/src/Cryptol/Eval/FFI.hs index 51b06e247..1ccc25ea7 100644 --- a/src/Cryptol/Eval/FFI.hs +++ b/src/Cryptol/Eval/FFI.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE BangPatterns #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE CPP #-} {-# LANGUAGE LambdaCase #-} @@ -12,29 +13,31 @@ -- | Evaluation of foreign functions. module Cryptol.Eval.FFI - ( evalForeignDecls + ( findForeignDecls + , evalForeignDecls ) where +import Data.Maybe + import Cryptol.Backend.FFI import Cryptol.Backend.FFI.Error import Cryptol.Eval -import Cryptol.ModuleSystem.Env import Cryptol.TypeCheck.AST +import Cryptol.TypeCheck.FFI.FFIType #ifdef FFI_ENABLED import Data.Either +import Data.Foldable import Data.IORef -import Data.Maybe import Data.Proxy import Data.Traversable import Data.Word import Foreign import Foreign.C.Types import GHC.Float -import LibBF (bfFromDouble, bfToDouble, - pattern NearEven) -import System.Directory +import LibBF (bfFromDouble, bfToDouble, + pattern NearEven) import Cryptol.Backend.Concrete import Cryptol.Backend.FloatHelpers @@ -45,42 +48,36 @@ import Cryptol.Eval.Prims import Cryptol.Eval.Type import Cryptol.Eval.Value import Cryptol.ModuleSystem.Name -import Cryptol.TypeCheck.FFI.FFIType import Cryptol.Utils.Ident import Cryptol.Utils.RecordMap --- | Find all the foreign declarations in the module and add them to the --- environment. This is a separate pass from the main evaluation functions in --- "Cryptol.Eval" since it only works for the Concrete backend. --- --- Note: 'Right' is only returned if we successfully loaded some foreign --- functions and the environment was modified. If there were no foreign --- declarations at all then @Left []@ is returned, so 'Left' does not --- necessarily indicate an error. -evalForeignDecls :: ModulePath -> Module -> EvalEnv -> - Eval (Either [FFILoadError] (ForeignSrc, EvalEnv)) -evalForeignDecls path m env = io - case mapMaybe getForeign $ mDecls m of - [] -> pure $ Left [] - foreigns -> - case path of - InFile p -> canonicalizePath p >>= loadForeignSrc >>= - \case - Right fsrc -> collect <$> for foreigns \(name, ffiType) -> - fmap ((name,) . foreignPrimPoly name ffiType) <$> - loadForeignImpl fsrc (unpackIdent $ nameIdent name) - where collect (partitionEithers -> (errs, primMap)) - | null errs = Right - (fsrc, foldr (uncurry bindVarDirect) env primMap) - | otherwise = Left errs - Left err -> pure $ Left [err] - -- We don't handle in-memory modules for now - InMem _ _ -> evalPanic "evalForeignDecls" - ["Can't find foreign source of in-memory module"] +#endif + +-- | Find all the foreign declarations in the module and return their names and +-- FFIFunTypes. +findForeignDecls :: Module -> [(Name, FFIFunType)] +findForeignDecls = mapMaybe getForeign . mDecls where getForeign (NonRecursive Decl { dName, dDefinition = DForeign ffiType }) = Just (dName, ffiType) + -- Recursive DeclGroups can't have foreign decls getForeign _ = Nothing +#ifdef FFI_ENABLED + +-- | Add the given foreign declarations to the environment, loading their +-- implementations from the given 'ForeignSrc'. This is a separate pass from the +-- main evaluation functions in "Cryptol.Eval" since it only works for the +-- Concrete backend. +evalForeignDecls :: ForeignSrc -> [(Name, FFIFunType)] -> EvalEnv -> + Eval (Either [FFILoadError] EvalEnv) +evalForeignDecls fsrc decls env = io do + ePrims <- for decls \(name, ffiType) -> + fmap ((name,) . foreignPrimPoly name ffiType) <$> + loadForeignImpl fsrc (unpackIdent $ nameIdent name) + pure case partitionEithers ePrims of + ([], prims) -> Right $ foldr (uncurry bindVarDirect) env prims + (errs, _) -> Left errs + -- | Generate a 'Prim' value representing the given foreign function, containing -- all the code necessary to marshal arguments and return values and do the -- actual FFI call. @@ -153,13 +150,21 @@ foreignPrim name FFIFunType {..} impl tenv = buildFun ffiArgTypes [] marshalArg (FFIBasic t) val f = getMarshalBasicArg t \m -> do arg <- m val f [SomeFFIArg arg] - marshalArg (FFIArray (evalFinType -> n) t) val f = - getMarshalBasicArg t \m -> do - args <- traverse (>>= m) $ enumerateSeqMap n $ fromVSeq val - -- Since we need to do an Eval action in an IO callback, we need to - -- manually unwrap and wrap the Eval datatype + marshalArg (FFIArray (map evalFinType -> sizes) t) val f = + getMarshalBasicArg t \m -> + -- Since we need to do Eval actions in an IO callback, we need to manually + -- unwrap and wrap the Eval datatype Eval \stk -> - withArray args \ptr -> + allocaArray (fromInteger $ product sizes) \ptr -> do + -- Traverse the nested sequences and write the elements to the array + -- in order + let write (n:ns) !i v = do + vs <- traverse (runEval stk) $ enumerateSeqMap n $ fromVSeq v + foldlM (write ns) i vs + write [] !i v = do + runEval stk (m v) >>= pokeElemOff ptr i + pure (i + 1) + _ <- write sizes 0 val runEval stk $ f [SomeFFIArg ptr] marshalArg (FFITuple types) val f = do vals <- sequence $ fromVTuple val @@ -177,17 +182,26 @@ foreignPrim name FFIFunType {..} impl tenv = buildFun ffiArgTypes [] go ((t, v):tvs) prevArgs = marshalArg t v \currArgs -> go tvs (prevArgs ++ currArgs) - -- Given a FFIType and a GetRet, obtain a return value and convert it to a + -- Given an FFIType and a GetRet, obtain a return value and convert it to a -- Cryptol value. The return value is obtained differently depending on the -- FFIType. marshalRet :: FFIType -> GetRet -> Eval (GenValue Concrete) marshalRet FFIBool gr = VBit . toBool <$> io (getRetAsValue gr @Word8) marshalRet (FFIBasic t) gr = getMarshalBasicRet t (io (getRetAsValue gr) >>=) - marshalRet (FFIArray (evalFinType -> n) t) gr = getMarshalBasicRet t \m -> - fmap (VSeq n . finiteSeqMap Concrete . map m) $ - io $ allocaArray (fromInteger n) \ptr -> do - getRetAsOutArgs gr [SomeFFIArg ptr] - peekArray (fromInteger n) ptr + marshalRet (FFIArray (map evalFinType -> sizes) t) gr = + getMarshalBasicRet t \m -> + Eval \stk -> + allocaArray (fromInteger $ product sizes) \ptr -> do + getRetAsOutArgs gr [SomeFFIArg ptr] + let build (n:ns) !i = do + -- We need to be careful to actually run this here and not just + -- stick the IO action into the sequence with io, or else we + -- will read from the array after it is deallocated. + vs <- for [0 .. fromInteger n - 1] \j -> + build ns (i * fromInteger n + j) + pure $ VSeq n $ finiteSeqMap Concrete $ map pure vs + build [] !i = peekElemOff ptr i >>= runEval stk . m + build sizes 0 marshalRet (FFITuple types) gr = VTuple <$> marshalMultiRet types gr marshalRet (FFIRecord typeMap) gr = VRecord . recordFromFields . zip (displayOrder typeMap) <$> @@ -274,8 +288,8 @@ withWordType FFIWord64 f = f $ Proxy @Word64 -- | Dummy implementation for when FFI is disabled. Does not add anything to -- the environment. -evalForeignDecls :: ModulePath -> Module -> EvalEnv -> - Eval (Either [FFILoadError] (ForeignSrc, EvalEnv)) -evalForeignDecls _ _ _ = pure $ Left [] +evalForeignDecls :: ForeignSrc -> [(Name, FFIFunType)] -> EvalEnv -> + Eval (Either [FFILoadError] EvalEnv) +evalForeignDecls _ _ env = pure $ Right env #endif diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index e17384e75..7113a488c 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -19,7 +19,6 @@ module Cryptol.ModuleSystem.Base where import qualified Control.Exception as X import Control.Monad (unless,when) -import Data.Functor.Compose import Data.Maybe (fromMaybe) import Data.Monoid ((<>)) import Data.Text.Encoding (decodeUtf8') @@ -51,6 +50,7 @@ import Cryptol.ModuleSystem.Env (lookupModule , meCoreLint, CoreLint(..) , ModContext(..) , ModulePath(..), modulePathLabel) +import Cryptol.Backend.FFI import qualified Cryptol.Eval as E import qualified Cryptol.Eval.Concrete as Concrete import Cryptol.Eval.Concrete (Concrete(..)) @@ -240,16 +240,11 @@ doLoadModule quiet isrc path fp pm0 = let ?evalPrim = \i -> Right <$> Map.lookup i tbl callStacks <- getCallStacks let ?callStacks = callStacks - foreignSrc <- - if T.isParametrizedModule tcm - then pure Nothing - else (getCompose - <$> modifyEvalEnvM (fmap Compose . evalForeignDecls path tcm) - >>= \case - Left [] -> pure Nothing - Left errs -> ffiLoadErrors (T.mName tcm) errs - Right (foreignSrc, ()) -> pure (Just foreignSrc)) - <* modifyEvalEnv (E.moduleEnv Concrete tcm) + foreignSrc <- if T.isParametrizedModule tcm + then pure Nothing + else evalForeign tcm + unless (T.isParametrizedModule tcm) $ + modifyEvalEnv (E.moduleEnv Concrete tcm) loadedModule path fp nameEnv foreignSrc tcm return tcm @@ -263,7 +258,25 @@ doLoadModule quiet isrc path fp pm0 = else notAParameterizedModule (T.mName tcm) | otherwise = return tcm - + evalForeign tcm + | null foreigns = pure Nothing + | otherwise = case path of + InFile p -> io (canonicalizePath p >>= loadForeignSrc) >>= + \case + Right fsrc -> do + unless quiet $ + case getForeignSrcPath fsrc of + Just fpath -> withLogger logPutStrLn $ + "Loading dynamic library " ++ takeFileName fpath + Nothing -> pure () + modifyEvalEnvM (evalForeignDecls fsrc foreigns) >>= + \case + Right () -> pure $ Just fsrc + Left errs -> ffiLoadErrors (T.mName tcm) errs + Left err -> ffiLoadErrors (T.mName tcm) [err] + InMem m _ -> panic "doLoadModule" + ["Can't find foreign source of in-memory module", m] + where foreigns = findForeignDecls tcm diff --git a/src/Cryptol/TypeCheck/FFI.hs b/src/Cryptol/TypeCheck/FFI.hs index b4c97b198..3a845cb06 100644 --- a/src/Cryptol/TypeCheck/FFI.hs +++ b/src/Cryptol/TypeCheck/FFI.hs @@ -7,6 +7,7 @@ module Cryptol.TypeCheck.FFI ( toFFIFunType ) where +import Data.Bifunctor import Data.Containers.ListUtils import Data.Either @@ -61,11 +62,14 @@ toFFIType t = case t of TCon (TC TCBit) [] -> Right ([], FFIBool) (toFFIBasicType -> Just r) -> (\fbt -> ([], FFIBasic fbt)) <$> r - TCon (TC TCSeq) [sz, bt] -> - case toFFIBasicType bt of - Just (Right fbt) -> Right ([fin sz], FFIArray sz fbt) - Just (Left err) -> Left $ FFITypeError t $ FFIBadComponentTypes [err] - Nothing -> Left $ FFITypeError t FFIBadArrayType + TCon (TC TCSeq) _ -> + (\(szs, fbt) -> (map fin szs, FFIArray szs fbt)) <$> go t + where go (toFFIBasicType -> Just r) = + case r of + Right fbt -> Right ([], fbt) + Left err -> Left $ FFITypeError t $ FFIBadComponentTypes [err] + go (TCon (TC TCSeq) [sz, ty]) = first (sz:) <$> go ty + go _ = Left $ FFITypeError t FFIBadArrayType TCon (TC (TCTuple _)) ts -> case partitionEithers $ map toFFIType ts of ([], unzip -> (pss, fts)) -> Right (concat pss, FFITuple fts) diff --git a/src/Cryptol/TypeCheck/FFI/Error.hs b/src/Cryptol/TypeCheck/FFI/Error.hs index 23f942bb8..ea9513b3d 100644 --- a/src/Cryptol/TypeCheck/FFI/Error.hs +++ b/src/Cryptol/TypeCheck/FFI/Error.hs @@ -70,12 +70,12 @@ instance PP (WithNames FFITypeErrorReason) where , "Only Float32 and Float64 are supported" ] FFIBadArrayType -> vcat [ "Unsupported sequence element type" - , "Only words or floats are supported as the element type of sequences" + , "Only words or floats are supported as the element type of" + , "(possibly multidimensional) sequences" ] FFIBadComponentTypes errs -> indent 2 $ vcat $ map (ppWithNames names) errs FFIBadType -> vcat - [ "Only Bit, words, floats, sequences of words or floats," - , "or structs or tuples of the above are supported as FFI" - , "argument or return types"] + [ "Only Bit, words, floats, sequences, or structs or tuples" + , "of the above are supported as FFI argument or return types" ] FFINotFunction -> "FFI binding must be a function" diff --git a/src/Cryptol/TypeCheck/FFI/FFIType.hs b/src/Cryptol/TypeCheck/FFI/FFIType.hs index dfd8ef502..a19fcbff0 100644 --- a/src/Cryptol/TypeCheck/FFI/FFIType.hs +++ b/src/Cryptol/TypeCheck/FFI/FFIType.hs @@ -26,21 +26,20 @@ data FFIFunType = FFIFunType data FFIType = FFIBool | FFIBasic FFIBasicType - | FFIArray - Type -- ^ Size (should be of kind @\#@) - FFIBasicType -- ^ Element type + -- | [n][m][p]T --> FFIArray [n, m, p] T + | FFIArray [Type] FFIBasicType | FFITuple [FFIType] | FFIRecord (RecordMap Ident FFIType) deriving (Show, Generic, NFData) --- | Types which can be elements of FFI sequences. +-- | Types which can be elements of FFI arrays. data FFIBasicType = FFIWord - Integer -- ^ The size of the Cryptol type + Integer -- ^ The size of the Cryptol type FFIWordSize -- ^ The machine word size that it corresponds to | FFIFloat - Integer -- ^ Exponent - Integer -- ^ Precision + Integer -- ^ Exponent + Integer -- ^ Precision FFIFloatSize -- ^ The machine float size that it corresponds to deriving (Show, Generic, NFData) diff --git a/tests/ffi/ffi-reload.icry.stdout b/tests/ffi/ffi-reload.icry.stdout index 441a89a75..ed065cd07 100644 --- a/tests/ffi/ffi-reload.icry.stdout +++ b/tests/ffi/ffi-reload.icry.stdout @@ -1,7 +1,9 @@ Loading module Cryptol Loading module Cryptol Loading module Main +Loading dynamic library ffi-reload.so False Loading module Cryptol Loading module Main +Loading dynamic library ffi-reload.so True diff --git a/tests/ffi/ffi-reload.icry.stdout.darwin b/tests/ffi/ffi-reload.icry.stdout.darwin new file mode 100644 index 000000000..28ace0847 --- /dev/null +++ b/tests/ffi/ffi-reload.icry.stdout.darwin @@ -0,0 +1,9 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main +Loading dynamic library ffi-reload.dylib +False +Loading module Cryptol +Loading module Main +Loading dynamic library ffi-reload.dylib +True diff --git a/tests/ffi/ffi-runtime-errors.icry.stdout b/tests/ffi/ffi-runtime-errors.icry.stdout index 1bf3c9006..19f17e108 100644 --- a/tests/ffi/ffi-runtime-errors.icry.stdout +++ b/tests/ffi/ffi-runtime-errors.icry.stdout @@ -1,6 +1,7 @@ Loading module Cryptol Loading module Cryptol Loading module Main +Loading dynamic library ffi-runtime-errors.so numeric type argument to foreign function is too large: 18446744073709551616 in type parameter n`899 of function Main::f diff --git a/tests/ffi/ffi-runtime-errors.icry.stdout.darwin b/tests/ffi/ffi-runtime-errors.icry.stdout.darwin new file mode 100644 index 000000000..105b5ba54 --- /dev/null +++ b/tests/ffi/ffi-runtime-errors.icry.stdout.darwin @@ -0,0 +1,29 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main +Loading dynamic library ffi-runtime-errors.dylib + +numeric type argument to foreign function is too large: 18446744073709551616 +in type parameter n`899 of function Main::f +type arguments must fit in a C `size_t` +-- Backtrace -- +Main::f called at ffi-runtime-errors.icry:4:1--4:2 + +cannot call foreign function Main::g +FFI calls are not supported in this context +If you are trying to evaluate an expression, try rebuilding + Cryptol with FFI support enabled. + +cannot call foreign function Main::g +FFI calls are not supported in this context +If you are trying to evaluate an expression, try rebuilding + Cryptol with FFI support enabled. + +cannot call foreign function Main::g +FFI calls are not supported in this context +If you are trying to evaluate an expression, try rebuilding + Cryptol with FFI support enabled. +cannot call foreign function Main::g +FFI calls are not supported in this context +If you are trying to evaluate an expression, try rebuilding + Cryptol with FFI support enabled. diff --git a/tests/ffi/ffi-type-errors.cry b/tests/ffi/ffi-type-errors.cry index 4c13c57ee..822feaa15 100644 --- a/tests/ffi/ffi-type-errors.cry +++ b/tests/ffi/ffi-type-errors.cry @@ -2,7 +2,8 @@ import Float foreign badWordSizes : [65] -> [128] foreign badFloatSizes : Float16 -> Float128 -foreign badArrayTypes : {n} (fin n) => [n]Bit -> [n]([16], [16]) -> [n][4][8] +foreign badArrayTypes : {n} (fin n) => + [n]Bit -> [n]([16], [16]) -> [n][4][8]{a : [n], b : [2]} foreign badTypes : Integer -> Z 3 foreign notFunction : [32] foreign badKind : {t} t -> [32] diff --git a/tests/ffi/ffi-type-errors.icry.stdout b/tests/ffi/ffi-type-errors.icry.stdout index e13efa913..871e683dc 100644 --- a/tests/ffi/ffi-type-errors.icry.stdout +++ b/tests/ffi/ffi-type-errors.icry.stdout @@ -33,70 +33,72 @@ Loading module Main Unsupported Float format Only Float32 and Float64 are supported When checking the type of 'Main::badFloatSizes' -[error] at ffi-type-errors.cry:5:9--5:78: +[error] at ffi-type-errors.cry:5:9--6:59: Type unsupported for FFI: - [n`969] -> [n`969]([16], [16]) -> [n`969][4][8] + [n`969] -> [n`969]([16], [16]) -> [n`969][4][8]{a : [n`969], + b : [2]} Due to: Type unsupported for FFI: [n`969] Due to: Unsupported sequence element type - Only words or floats are supported as the element type of sequences + Only words or floats are supported as the element type of + (possibly multidimensional) sequences Type unsupported for FFI: [n`969]([16], [16]) Due to: Unsupported sequence element type - Only words or floats are supported as the element type of sequences + Only words or floats are supported as the element type of + (possibly multidimensional) sequences Type unsupported for FFI: - [n`969][4][8] + [n`969][4][8]{a : [n`969], b : [2]} Due to: Unsupported sequence element type - Only words or floats are supported as the element type of sequences + Only words or floats are supported as the element type of + (possibly multidimensional) sequences When checking the type of 'Main::badArrayTypes' -[error] at ffi-type-errors.cry:6:9--6:34: +[error] at ffi-type-errors.cry:7:9--7:34: Type unsupported for FFI: Integer -> Z 3 Due to: Type unsupported for FFI: Integer Due to: - Only Bit, words, floats, sequences of words or floats, - or structs or tuples of the above are supported as FFI - argument or return types + Only Bit, words, floats, sequences, or structs or tuples + of the above are supported as FFI argument or return types Type unsupported for FFI: Z 3 Due to: - Only Bit, words, floats, sequences of words or floats, - or structs or tuples of the above are supported as FFI - argument or return types + Only Bit, words, floats, sequences, or structs or tuples + of the above are supported as FFI argument or return types When checking the type of 'Main::badTypes' -[error] at ffi-type-errors.cry:7:9--7:27: +[error] at ffi-type-errors.cry:8:9--8:27: Type unsupported for FFI: [32] Due to: FFI binding must be a function When checking the type of 'Main::notFunction' -[error] at ffi-type-errors.cry:8:9--8:32: +[error] at ffi-type-errors.cry:9:9--9:32: Kind of type variable unsupported for FFI: t`970 : * Only type variables of kind # are supported When checking the type of 'Main::badKind' -[error] at ffi-type-errors.cry:9:9--9:43: +[error] at ffi-type-errors.cry:10:9--10:43: Failed to validate user-specified signature. - in the definition of 'Main::noFin', at ffi-type-errors.cry:9:9--9:14, + in the definition of 'Main::noFin', at ffi-type-errors.cry:10:9--10:14, we need to show that for any type n the following constraints hold: • fin n arising from declaration of foreign function Main::noFin - at ffi-type-errors.cry:9:9--9:43 -[error] at ffi-type-errors.cry:10:9--10:34: + at ffi-type-errors.cry:10:9--10:43 +[error] at ffi-type-errors.cry:11:9--11:34: • Unsolvable constraint: fin inf arising from declaration of foreign function Main::infSeq - at ffi-type-errors.cry:10:9--10:34 -[error] at ffi-type-errors.cry:11:48--11:49: + at ffi-type-errors.cry:11:9--11:34 +[error] at ffi-type-errors.cry:12:48--12:49: Wild card types are not allowed in this context (e.g., they cannot be used in type synonyms or FFI declarations). diff --git a/tests/ffi/test-ffi.c b/tests/ffi/test-ffi.c index 6a88c9a61..ed8e220b0 100644 --- a/tests/ffi/test-ffi.c +++ b/tests/ffi/test-ffi.c @@ -116,3 +116,9 @@ void zipMul3(size_t n, size_t m, size_t p, float *xs, float *ys, float *zs, out[i] = xs[i] * ys[i] * zs[i]; } } + +void nestedSeq(size_t n, size_t m, size_t p, uint8_t *in, uint8_t *out) { + for (unsigned i = 0; i < n * m * p; ++i) { + out[i] = in[i]; + } +} diff --git a/tests/ffi/test-ffi.cry b/tests/ffi/test-ffi.cry index 2be07c795..eeef0de35 100644 --- a/tests/ffi/test-ffi.cry +++ b/tests/ffi/test-ffi.cry @@ -38,3 +38,7 @@ foreign sumPoly : {n} (fin n) => [n]Word32 -> Word32 foreign inits : {n} (fin n) => [n][8] -> [n * (n + 1) / 2][8] foreign zipMul3 : {n, m, p} (fin n, fin m, fin p) => [n]Float32 -> [m]Float32 -> [p]Float32 -> [min n (min m p)]Float32 + +// Nested sequences +foreign nestedSeq : {n, m, p} (fin n, fin m, fin p, n * m * p == 4 * 3 * 2) => + [n][m][p][8] -> [4][3][2][8] diff --git a/tests/ffi/test-ffi.icry b/tests/ffi/test-ffi.icry index 93f2771e5..f1699e81e 100644 --- a/tests/ffi/test-ffi.icry +++ b/tests/ffi/test-ffi.icry @@ -32,3 +32,5 @@ sumPoly [1..10] sumPoly [1..10000] inits [1..5] zipMul3 [1, 2, 3] [3, 4, 5, 6] [6, 7, 8, 9, 10] + +nestedSeq [split`{4} x | x <- split`{2} [1..24]] diff --git a/tests/ffi/test-ffi.icry.stdout b/tests/ffi/test-ffi.icry.stdout index 72db4b2e8..3405573ab 100644 --- a/tests/ffi/test-ffi.icry.stdout +++ b/tests/ffi/test-ffi.icry.stdout @@ -2,6 +2,7 @@ Loading module Cryptol Loading module Cryptol Loading module Float Loading module Main +Loading dynamic library test-ffi.so 0x03 0x15b4 0x3a0f1880 @@ -31,3 +32,7 @@ True [0x01, 0x01, 0x02, 0x01, 0x02, 0x03, 0x01, 0x02, 0x03, 0x04, 0x01, 0x02, 0x03, 0x04, 0x05] [0x12.0, 0x38.0, 0x78.0] +[[[0x01, 0x02], [0x03, 0x04], [0x05, 0x06]], + [[0x07, 0x08], [0x09, 0x0a], [0x0b, 0x0c]], + [[0x0d, 0x0e], [0x0f, 0x10], [0x11, 0x12]], + [[0x13, 0x14], [0x15, 0x16], [0x17, 0x18]]] diff --git a/tests/ffi/test-ffi.icry.stdout.darwin b/tests/ffi/test-ffi.icry.stdout.darwin new file mode 100644 index 000000000..6d148394c --- /dev/null +++ b/tests/ffi/test-ffi.icry.stdout.darwin @@ -0,0 +1,38 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Float +Loading module Main +Loading dynamic library test-ffi.dylib +0x03 +0x15b4 +0x3a0f1880 +0x00000002e90edc8f +0x07 +0x7 +0x0 +False +0x45.1eb8 +-0x1e61.c71de69ad5 +fpPosInf +fpNegInf +fpNaN +-0.0 +True +0x00000037 +[0xb.cd, -0x9.0a, 0x6.78, -0x3.45, 0x1.23] +{a = (0x1234, 0x5678), + b = {c = [0x0000a, 0x00014, 0x0001e, 0x00028, 0x00032, 0x0003c, + 0x00046, 0x00050], + d = 0x09, + e = 0x0c}} +0x12345678deadbeef +0x00000000 +0x00000037 +0x02fb0408 +[0x01, 0x01, 0x02, 0x01, 0x02, 0x03, 0x01, 0x02, 0x03, 0x04, 0x01, + 0x02, 0x03, 0x04, 0x05] +[0x12.0, 0x38.0, 0x78.0] +[[[0x01, 0x02], [0x03, 0x04], [0x05, 0x06]], + [[0x07, 0x08], [0x09, 0x0a], [0x0b, 0x0c]], + [[0x0d, 0x0e], [0x0f, 0x10], [0x11, 0x12]], + [[0x13, 0x14], [0x15, 0x16], [0x17, 0x18]]]