cardano-wallet-agda

KO | EN

gitlite — search

#javascript #python #react #typescript #golang #go #android #linux #macos #nodejs #java #awesome-list #openai #open-source

cardano-wallet-agda

(★ 14)

Formally verified wallet implementation

cardano-wallet-agda Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

🚧 WORK IN PROGRESS 🚧

[![Build status](https://badge.buildkite.com/307068367b3a4746737164e239dca22dd6b5288eb54c71ee0c.svg?branch=main)](https://buildkite.com/cardano-foundation/cardano-wallet-agda)

## Overview

This repository contains wallet implementations for the Cardano blockchain that are formally verified to some degree. The implementations are [Haskell][] packages, but generated using [agda2hs][], with proofs in [Agda][].

[agda]: https://github.com/agda/agda
  [agda2hs]: https://github.com/agda/agda2hs
  [haskell]: https://haskell.org

## Contents

This repository is strucured as follows:

* `flake.nix` — Nix flake for a development shell with relevant Haskell and Agda tools in scope.
* `lib/`
    * `customer-deposit-wallet-pure/` — Specification and implementation of a pure Deposit Wallet.
    * `cardano-wallet-read/` — Data types that correspond to the Cardano Ledger specification, implemented via the [cardano-ledger][] packages.
    * `containers` — Axiomatization of (a subset of)
    the [containers package](https://hackage.haskell.org/package/containers).

Each of the packages in the `lib/` directory may contain the following subdirectories:

* `agda/` — Haskell-in-Agda code with some proofs.
* `haskell/` — Haskell code that corresponds to the code in `agda/`. Most source code files are autogenerated from the `agda/` directory using `agda2hs`, but not all. This code is checked into the repository, so that downstream projects do *not* need the Agda compiler.

[cardano-ledger]: https://github.com/IntersectMBO/cardano-ledger

## QuickStart

Prerequisites:

* [Nix package manager][nix].  
  As some dependencies, such as [agda2hs][], are still under development, we use [nix][] to ensure a working build environment.

How to build:

```console
nix develop
just haskell
just build
```

How to run tests:

* There are no unit tests for `customer-deposit-wallet-pure` — only compiler-checked proofs. 😏
* To run the unit tests for `cardano-wallet-read`, use `just test`.

How to run:

* N/A. This project is a [Haskell package][hackage]. For an exectuable wallet, see the [cardano-wallet][] project.

## Contributors

See [CONTRIBUTING.md](CONTRIBUTING.md).

## Roadmap

* Completion of implementation.
* Completion of proofs.

[cardano-wallet]: https://github.com/cardano-foundation/cardano-wallet
  [hackage]: https://hackage.haskell.org
  [nix]: https://nixos.org/download/

cardano-wallet-agda

cardano-wallet-agda Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

cardano-wallet-agda

cardano-wallet-agda Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README