Home
Softono
i

intersectmbo

Professional software vendor delivering innovative solutions on the Softono platform. Specialized in both open-source and proprietary software development.

Visit Website
Total Products
2

Software by intersectmbo

cardano-ledger
Open Source

cardano-ledger

<h1 align="center">Cardano Ledger</h1> <p align="center"> <a href="https://input-output-hk.github.io/cardano-engineering-handbook"><img alt="CEH" src="https://img.shields.io/badge/policy-Cardano%20Engineering%20Handbook-informational?style=for-the-badge"/></a> <a href="https://github.com/intersectmbo/cardano-ledger/actions/workflows/haskell.yml"><img alt="GitHub Workflow Status (master)" src="https://img.shields.io/github/actions/workflow/status/intersectmbo/cardano-ledger/haskell.yml?branch=master&style=for-the-badge"/></a> <a href="https://cardano-ledger.cardano.intersectmbo.org/"><img alt="Haddock (master)" src="https://img.shields.io/badge/documentation-Haddock-yellow?style=for-the-badge"/></a> </p> This repository contains the formal specifications, executable models, and implementations of the Cardano Ledger. The documents can be accessed using the following links: Era | Design Documents | Formal Specification | CDDL ----|------------------|----------------------|----- Byron | | [Chain Spec](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/byron-blockchain.pdf "Specification of the Blockchain Layer"), [Ledger Spec](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/byron-ledger.pdf "A Formal Specification of the Cardano Ledger") | [CDDL](https://github.com/intersectmbo/cardano-ledger/tree/master/eras/byron/ledger/impl/cddl-spec/byron.cddl), [PDF](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/byron-binary.pdf) Shelley | [Design](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-delegation.pdf "Design Specification for Delegation and Incentives in Cardano") | [Spec](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf "A Formal Specification of the Cardano Ledger") | [CDDL](https://github.com/intersectmbo/cardano-ledger/tree/master/eras/shelley/impl/cddl/data) Allegra | Same as Mary era below | Same as Mary era below | [CDDL](https://github.com/intersectmbo/cardano-ledger/tree/master/eras/allegra/impl/cddl/data) Mary | [Multi-Currency](https://eprint.iacr.org/2020/895 "Multi-Currency Ledgers"), [UTXOma](https://iohk.io/en/research/library/papers/utxoma-utxo-with-multi-asset-support/ "UTXOma:UTXO with Multi-Asset Support") | [Spec](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/mary-ledger.pdf "A Formal Specification of the Cardano Ledger with a Native Multi-Asset Implementation") | [CDDL](https://github.com/intersectmbo/cardano-ledger/tree/master/eras/mary/impl/cddl/data) Alonzo | [eUTXO](https://iohk.io/en/research/library/papers/the-extended-utxo-model/ "The Extended UTXO Model")| [Spec](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/alonzo-ledger.pdf "A Formal Specification of the Cardano Ledger integrating Plutus Core") | [CDDL](https://github.com/intersectmbo/cardano-ledger/tree/master/eras/alonzo/impl/cddl/data) Babbage | [batch-verification](https://iohk.io/en/research/library/papers/on-uc-secure-range-extension-and-batch-verification-for-ecvrf/ "On UC-Secure Range Extension and Batch Verification for ECVRF"), [CIP-31](https://github.com/cardano-foundation/CIPs/pull/159 "Reference inputs"), [CIP-32](https://github.com/cardano-foundation/CIPs/pull/160 "Inline datums"), [CIP-33](https://github.com/cardano-foundation/CIPs/pull/161 "Reference scripts") | [Spec](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/babbage-ledger.pdf "Formal Specification of the Cardano Ledger for the Babbage era") | [CDDL](https://github.com/intersectmbo/cardano-ledger/tree/master/eras/babbage/impl/cddl/data) Conway | [CIP-1694](https://github.com/cardano-foundation/CIPs/tree/master/CIP-1694) | [Spec](https://intersectmbo.github.io/formal-ledger-specifications/site/Ledger.Conway.Specification.html) | [CDDL](https://github.com/intersectmbo/cardano-ledger/tree/master/eras/conway/impl/cddl/data) Note that the formal specification documents present the specification in a diff-style manner. That is, each document shows specification changes with respect to documents of previous eras. There is an ongoing effort to provide a full [machine-verified formal specification of the Cardano Ledger](https://intersectmbo.github.io/formal-ledger-specifications/site) that will subsume the (formal specification) documents listed above. This effort is *complete for Conway* but partially complete for previous eras. Other Documents: - [Non-integer calculations specification](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/non-integer-calculations.pdf): details on the parts of the Shelley specification that use real numbers. - [Stake pool ranking specification](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/pool-ranking.pdf): details for a robust stake pool ranking mechanism. - [Explanation of the small-step-semantics framework](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/small-step-semantics.pdf): a guide to the notation and style used by our ledger rules. In addition, there is a formalization of the Ledger Specification in Isabelle/HOL which can be found [here](https://github.com/input-output-hk/fm-ledger-formalization). Some user documentation is published on [Read the Docs](https://cardano-ledger.readthedocs.io/en/latest) Haddock code documentation of the latest master branch is available [here](https://cardano-ledger.cardano.intersectmbo.org/). # Repository structure The directory structure of this repository is as follows: - [Byron](./eras/byron) - [ledger](./eras/byron/ledger) - [formal-spec](./eras/byron/ledger/formal-spec) - [executable-spec](./eras/byron/ledger/executable-spec) - [implementation](./eras/byron/ledger/impl) - [cddl](./eras/byron/ledger/impl/cddl-spec) - [chain](./eras/byron/chain) - [formal-spec](./eras/byron/chain/formal-spec) - [executable-spec](./eras/byron/chain/executable-spec) - [Shelley](./eras/shelley) - [design-spec](./eras/shelley/design-spec) - [formal-spec](./eras/shelley/formal-spec) - [implementation](./eras/shelley/impl) - [tests](./eras/shelley/test-suite) - [cddl](./eras/shelley/impl/cddl/data) - [Allegra - Timelocks](./eras/allegra) - [formal-spec](./eras/shelley-ma/formal-spec) - [implementation](./eras/allegra/impl) - [tests](./eras/shelley-ma/test-suite) - [Mary - Multi-Assets](./eras/allegra) - [formal-spec](./eras/shelley-ma/formal-spec) - [implementation](./eras/allegra/impl) - [tests](./eras/shelley-ma/test-suite) - [Alonzo - Smart Contracts](./eras/alonzo) - [formal-spec](./eras/alonzo/formal-spec) - [implementation](./eras/alonzo/impl) - [cddl](./eras/alonzo/impl/cddl/data) - [tests](./eras/alonzo/test-suite) - [Babbage](./eras/babbage) - [formal-spec](./eras/babbage/formal-spec) - [implementation](./eras/babbage/impl) - [cddl](./eras/babbage/impl/cddl/data) - [tests](./eras/babbage/impl/test) - [Conway - Governance](./eras/conway) - [formal-spec](./eras/conway/formal-spec) - [implementation](./eras/conway/impl) - [cddl](./eras/conway/impl/cddl/data) - [tests](./eras/conway/impl/test) - [Libraries](./libs) # Building It is recommended to use [`nix`](https://nixos.org/download.html) for building everything in this repository. Make sure you have a recent version of `nix` by following this [guide](https://nixos.org/manual/nix/stable/installation/upgrading.html). Haskell files can be built with [`cabal`](https://www.haskell.org/cabal/) inside of a nix shell, which can be entered by invoking `nix develop` from the root directory. ## Nix Cache When using `nix` it is recommended that you setup the cache, so that it can reuse built artifacts, reducing the compilation times dramatically: If you are using [NixOS](https://nixos.org/) add the snippet below to your `/etc/nixos/configuration.nix`: ``` nix.settings = { experimental-features = [ "nix-command" "flakes" ]; substituters = [ "https://cache.nixos.org" "https://cache.iog.io" ]; trusted-public-keys = [ "hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=" ]; }; ``` If you are using the `nix` package manager next to another operating system put the following in `/etc/nix/nix.conf`: ``` experimental-features = nix-command flakes substituters = https://cache.iog.io https://cache.nixos.org/ trusted-public-keys = hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= ``` ## Building the LaTeX documents and executable specifications When using `nix` the documents and Haskell code can be readily built by running: ```shell nix build .#specs ``` The LaTeX documents will be placed inside a directory named `result`, e.g.: ```shell result/byron-ledger.pdf result/shelley-delegation.pdf result/non-integer-calculations.pdf result/small-step-semantics.pdf result/shelley-ledger.pdf result/byron-blockchain.pdf ``` ## Building individual LaTeX documents Change to the latex directory where the latex document is (e.g. `eras/shelley/formal-spec` for the ledger specification corresponding to the Shelley release, or `eras/byron/ledger/formal-spec` for the ledger specification corresponding to the Byron release). Then, build the latex document by running: ```shell cd <myLaTexDir> nix develop --command make ``` For a continuous compilation of the `LaTeX` file run: ```shell cd <myLaTexDir> nix develop --command make watch ``` # Testing From the root directory invoke `nix develop` to enter a nix shell, then run `cabal test all` to run all tests or `cabal test <package>` to run the tests for a specific package. Note: The `CARDANO_MAINNET_MIRROR` environment variable can be overridden in `flake.nix` if one desires to run the Byron tests with a different version of the [mainnet epochs](https://github.com/input-output-hk/cardano-mainnet-mirror/tree/master/epochs). # Submitting an issue Issues can be filed in the [GitHub Issue tracker](https://github.com/intersectmbo/cardano-ledger/issues). However, note that this is pre-release software, so we will not usually be providing support. # Contributing See [CONTRIBUTING](https://github.com/intersectmbo/cardano-ledger/blob/master/CONTRIBUTING.md). # Using `git fsck` There's some ancient history in the repo that causes `git fsck` version `2.44.0` or later to report errors when running semantic checks on an old version of the `.gitmodules` file. This can be overcome by running `git config fsck.skipList .git-fsck-skiplist` once, sometime after cloning. However, the problem prevents cloning if you have `transfer.fsckObjects` enabled in your global git configuration. You can overcome this by downloading the skiplist file before you clone and then specifying it in a config option to the `clone` command: ```shell $ curl -sSLO https://raw.githubusercontent.com/IntersectMBO/cardano-ledger/refs/heads/master/.git-fsck-skiplist $ git clone -c fetch.fsck.skipList=.git-fsck-skiplist ... ... $ rm .git-fsck-skiplist ```

Crypto & Blockchain
287 Github Stars
plutus
Open Source

plutus

= https://github.com/IntersectMBO/plutus[Plutus Core] :email: [email protected] :author: Input Output HK Limited :toc: left :reproducible: == Introduction Plutus Core is the scripting language embedded in the Cardano ledger and forms the basis of the Plutus Platform, an application development platform for developing distributed applications using the Cardano blockchain. For more information about the projects, see the <<user-documentation>>. This repository contains: * The implementation, specification, and mechanized metatheory of Plutus Core * Plutus Tx, the compiler from Haskell to Plutus Core. For people who want to *use* the project, please consult the <<user-documentation>>. == Development [[how-to-develop]] === How to develop and contribute to the project Run `nix develop` to enter the development shell and you will be presented with a list of available commands. **Please see link:CONTRIBUTING{outfilesuffix}[CONTRIBUTING] for comprehensive documentation on how to contribute to the project, including development and submitting changes* === How to submit an issue Issues can be filed in the https://github.com/IntersectMBO/plutus/issues[GitHub Issue tracker]. === How to depend on the project from another Haskell project The `plutus` libraries are published via https://input-output-hk.github.io/cardano-haskell-packages/[CHaP]. See the information there for how to use CHaP. After setting it up you should just be able to depend on the `plutus` packages as normal and cabal will find them. == Documentation === User documentation The main documentation is located https://plutus.cardano.intersectmbo.org/docs/[here]. The haddock documentation is located https://plutus.cardano.intersectmbo.org/haddock/latest[here]. The documentation for the metatheory can be found https://plutus.cardano.intersectmbo.org/metatheory/latest[here]. === Talks - https://www.youtube.com/watch?v=MpWeg6Fg0t8[Functional Smart Contracts on Cardano (2020)]: an overview of the ideas behind the Plutus Platform. - https://www.youtube.com/watch?v=usMPt8KpBeI[The Plutus Platform (2020)]: an overview of the Platform as a whole (including the Application Framework) at the time. === Specifications and design - https://plutus.cardano.intersectmbo.org/resources/plutus-report.pdf[Plutus Technical Report (draft)]: a technical report and design document for the project. - https://plutus.cardano.intersectmbo.org/resources/plutus-core-spec.pdf[Plutus Core Specification]: the formal specification of the core language. - https://plutus.cardano.intersectmbo.org/resources/extended-utxo-spec.pdf[Extended UTXO Model]: a design document for the core changes to the Cardano ledger. === Academic papers - https://plutus.cardano.intersectmbo.org/resources/unraveling-recursion-paper.pdf[Unraveling Recursion]: a description of some of the compilation strategies used in Plutus IR (https://doi.org/10.1007/978-3-030-33636-3_15[published version]). - https://plutus.cardano.intersectmbo.org/resources/system-f-in-agda-paper.pdf[System F in Agda]: a formal model of System F in Agda (https://doi.org/10.1007/978-3-030-33636-3_10[published version]). - https://plutus.cardano.intersectmbo.org/resources/eutxo-paper.pdf[The Extended UTXO Model]: a full presentation of the EUTXO ledger extension (https://doi.org/10.1007/978-3-030-54455-3_37[published version]). - https://plutus.cardano.intersectmbo.org/resources/utxoma-paper.pdf[UTXOma: UTXO with Multi-Asset Support]: a full presentation of the multi-asset ledger extension (https://doi.org/10.1007/978-3-030-61467-6_8[published version]). - https://plutus.cardano.intersectmbo.org/resources/eutxoma-paper.pdf[Native Custom Tokens in the Extended UTXO Model]: a discussion of the interaction of the multi-asset support with EUTXO (https://doi.org/10.1007/978-3-030-61467-6_7[published version]). - https://arxiv.org/abs/2201.04919[Translation Certification for Smart Contracts]: a certifier of Plutus IR compiler passes written in Coq. == Licensing You are free to copy, modify, and distribute this software under the terms of the Apache 2.0 license. See the link:./LICENSE.md[LICENSE] and link:./NOTICE.md[NOTICE] files for details.

Developer Tools Crypto & Blockchain
1.6K Github Stars