A domain specific language in coq used to write low-level cryptographic primitives.
We recommend the use of opam2 for working with coq. To know which versions are supported refer to the [CI status page][github-actions].
We assume that you are using opam-2 in which case you need to
initialise it with the --disable-sandboxing option. Otherwise the
package coq-color used by verse will not compile.
opam init --disable-sandboxing --compiler "$OCAML_VER"
opam repo add coq-released https://coq.inria.fr/opam/released
opam updateYou will now need to get a version of coq. Select one of the coq versions using which verse [is tested on our CI system][github-actions].
opam install coq."$COQ_VER"
opam pin add coq "$COQ_VER"
opam install coq-color
Finally prepare the opam environment, configure, and then make.
eval $(opam config env) # set up opam environment if needed.
./configure.sh
make
Verse is an Embedded Domain Specific Language (EDSL) where the
target code is represented as an inductive type in Coq. This EDSL is
use to implement actual primitives, the source of which are available
in the directory src/Verse/CryptoLib. The extracted low level code
is distributed as a separate library called libverse, a library that
can be embedded in other high level libraries. A snapshot of
libverse is built from the coq source using the helper scripts
present in the directory crypto-lib.
Copyright 2018, Piyush P Kurur
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.
SPDX-License-Identifier: Apache-2.0