Library ConCert.Embedding.Misc

• Some facts not found in the standard library

Library ConCert.Embedding.SimpleBlockchain

• A simply-typed version of the blockchain execution environment

Library ConCert.Embedding.Notations

• Notations for the deep embedding

Library ConCert.Embedding.Prelude

• Prelude -- definitions of basic of data types

Library ConCert.Embedding.Tests

• Various examples of using notations and conversion to the shallow embedding

Library ConCert.Embedding.EvalE

• Interpreter for the λsmart language

Library ConCert.Embedding.Ast

• λsmart language definition
  • λsmart AST
  • Conversion from named representation to De Bruijn indices
  • Merging type and term De Bruijn indices

Library ConCert.Embedding.EnvSubst

• Conversion from values back to expressions through the environment substitution
  • Substitution for the nameless representation
    • Notations for the environment substitution
  • Substitution for the named representation

Library ConCert.Embedding.Utils

Library ConCert.Embedding.TranslationUtils

Library ConCert.Embedding.CertifyingTranslate

• Certifying translation
  • Negation on booleans

Library ConCert.Embedding.pcuic.PCUICCorrectnessAux

• Auxiliary lemmas for the soundness proof.
  • Environment substitution commutes with PCUIC substitution (In the paper: Lemma 1.)
  • Evaluation gives well-formed values (In the paper: Lemma 2)

Library ConCert.Embedding.pcuic.PCUICtoTemplate

• Almost one-to-one translation of PCUIC to Template Coq kernel AST

Library ConCert.Embedding.pcuic.PCUICFacts

• Lemmas about the environment substitutions, closedness, etc. on expressions

Library ConCert.Embedding.pcuic.PCUICTranslate

• Translation from λsmart expressions to PCUIC terms
  • Translation of types
  • Translation of expressions
• Translation of inductives

Library ConCert.Embedding.pcuic.PCUICCorrectness

• • Soundness for closed expressions (In the paper: Corollary 2)
  • Adequacy for terminating programs (In the paper: Theorem 3)

Library ConCert.Embedding.Wf

• Well-formedness conditions
  • Well-formed global environment (In the paper: (WF.i))
  • Well-formedness condition on evaluation environments wrt.

Library ConCert.Embedding.Examples.AcornExamples

• Examples of library code and contracts originating
  • Bool module from the standard library of Acorn
  • Maybe module from the standard library of Acorn
  • Acorn pairs
  • Acorn List module
  • Acorn blockchain-related data types
  • A simple Counter contract

Library ConCert.Embedding.Examples.Demo

• Simple examples on how to use our framework

Library ConCert.Embedding.Examples.FinMap

• Finite maps
  • The deep embedding of data structures for finite maps
  • Functions on finite maps
  • Correctness
• Computing with the interpreter

Library ConCert.Embedding.Extraction.PreludeExt

• Extensions for Prelude from Embedding
  • Wrappers for some primitive types

Library ConCert.Embedding.Extraction.Liquidity

Library ConCert.Embedding.Extraction.SimpleBlockchainExt

• A simply-typed version of the blockchain execution environment

Library ConCert.Utils.StringExtra

Library ConCert.Utils.Automation

• This file implements various helper tactics

Library ConCert.Utils.Extras

Library ConCert.Utils.RecordSet

Library ConCert.Utils.Env

• Evaluation environments

Library ConCert.Utils.RecordUpdate

Library ConCert.Examples.PiggyBank.PiggyBank

• Piggy Bank Contract
• Types
• Error codes
• Implementation

Library ConCert.Examples.PiggyBank.PiggyBankExtractRust

Library ConCert.Examples.PiggyBank.PiggyBankExtractLiquidity

Library ConCert.Examples.PiggyBank.PiggyBankCorrect

• Piggybank contract
  • Functional properties
  • Safety properties

Library ConCert.Examples.PiggyBank.PiggyBankExtractLIGO

Library ConCert.Examples.EIP20.EIP20TokenPrinters

Library ConCert.Examples.EIP20.EIP20TokenCorrect

• EIP20 Token Implementation
• Properties
  • EIP20 functions not payable
  • EIP20 functions produce no acts
  • Expected behaviour of EIP20 functions
  • Transfer correct
  • Transfer_from correct
  • Approve correct
  • EIP20 functions preserve sum of balances
  • Contract never produces any actions
  • Total supply always equals initial supply
  • Sum of balances always equals total supply

Library ConCert.Examples.EIP20.EIP20TokenGens

Library ConCert.Examples.EIP20.EIP20LiquidityExtraction

• Extraction of a simple counter contract

Library ConCert.Examples.EIP20.EIP20CameLIGOExtraction

• Extraction of various contracts to CameLIGO

Library ConCert.Examples.EIP20.EIP20TokenTests

Library ConCert.Examples.EIP20.EIP20Token

• EIP20 Token Implementation
• Contract types
• Contract functions
  • init
  • transfer
  • transfer_from
  • approve
  • receive

Library ConCert.Examples.iTokenBuggy.iTokenBuggyTests

Library ConCert.Examples.iTokenBuggy.iTokenBuggy

Library ConCert.Examples.iTokenBuggy.iTokenBuggyPrinters

Library ConCert.Examples.iTokenBuggy.iTokenBuggyGens

Library ConCert.Examples.Counter.embedding.CounterEmbed

• • Definitions of data structures for the contract

Library ConCert.Examples.Counter.Counter

• Counter
  • Definition
  • Functional properties
    • Specification
  • Safety properties

Library ConCert.Examples.Counter.extraction.CounterSubsetTypesLIGO

• Extraction of a counter contract with subset types to Liquidity and CameLIGO

Library ConCert.Examples.Counter.extraction.CounterRust

Library ConCert.Examples.Counter.extraction.CounterRefTypesMidlang

• Extraction of a counter contract with refinement types to Midlang

Library ConCert.Examples.Counter.extraction.CounterLIGO

• Extraction of various contracts to CameLIGO

Library ConCert.Examples.Counter.extraction.CounterCertifiedLiquidity

• Extraction of a simple counter contract

Library ConCert.Examples.Counter.extraction.CounterSubsetTypesLiquidity

• Extraction of a counter contract with subset types to Liquidity and CameLIGO

Library ConCert.Examples.Counter.extraction.CounterDepCertifiedLiquidity

• Extraction of a counter contract with dependent types (propositions)

Library ConCert.Examples.FA2.FA2Interface

Library ConCert.Examples.FA2.FA2LegacyInterface

Library ConCert.Examples.FA2.TestContracts

Library ConCert.Examples.FA2.FA2Gens

Library ConCert.Examples.FA2.FA2TokenTests

Library ConCert.Examples.FA2.FA2Printers

Library ConCert.Examples.FA2.FA2Token

Library ConCert.Examples.CIS1.CIS1Utils

Library ConCert.Examples.CIS1.Cis1wccd

• Entry points
• Contract's state
• Transfer
• balanceOf
• updateOperator
• WCCD receive
• WCCD complies with CIS1
  • Receive specification

Library ConCert.Examples.CIS1.CIS1Spec

• Concordium's CIS1
• General types
• Views
• Contract functions
  • Transfer
    • Parameter
    • Requirements
  • updateOperator
    • Parameter
    • Requirements
  • balanceOf
    • Parameter
    • Requirements
  • Full specification of receive
• CIS1 properties
  • Operator updates
  • Balances
    • Main result

Library ConCert.Examples.Crowdfunding.CrowdfundingCameLIGO

• Extraction of various contracts to CameLIGO

Library ConCert.Examples.Crowdfunding.Crowdfunding

• The crowdfunding contract
  • AST of the init function
  • AST of the receive function

Library ConCert.Examples.Crowdfunding.ExecFrameworkIntegration

• Integration with the execution framework, properties of crowdfunding
  • Wrappers
  • Contract balance in the local state consistent with the sum of individual contributions
  • The actual contract balance is consistent with the local state
  • The actual contract balance is consistent with the sum of individual contributions

Library ConCert.Examples.Crowdfunding.CrowdfundingDataExt

• Data types for the crowdfunding contract tailored for extraction
  • Definitions of data structures for the contract
  • Custom notations for projections from the state type
  • State "updates"
  • Custom notations for projections from the call context and global state

Library ConCert.Examples.Crowdfunding.CrowdfundingCorrect

• Properties of the crowdfunding contract

Library ConCert.Examples.Crowdfunding.CrowdfundingData

• Data types for the crowdfunding contract
  • Definitions of data structures for the contract

Library ConCert.Examples.Crowdfunding.CrowdfundingExt

• The crowdfunding contract
  • AST of the validation function
  • AST of the init function
  • AST of the receive function

Library ConCert.Examples.Crowdfunding.CrowdfundingLiquidity

• Extraction of a crowdfunding contract

Library ConCert.Examples.Escrow.tests.EscrowPrinters

Library ConCert.Examples.Escrow.tests.EscrowGens

Library ConCert.Examples.Escrow.tests.EscrowTests

Library ConCert.Examples.Escrow.Escrow

Library ConCert.Examples.Escrow.extraction.EscrowLiquidity

• Extraction of Escrow to CameLIGO and liquidity

Library ConCert.Examples.Escrow.extraction.EscrowMidlang

Library ConCert.Examples.Escrow.extraction.EscrowLIGO

• Extraction of Escrow to CameLIGO and liquidity

Library ConCert.Examples.Escrow.extraction.EscrowRust

Library ConCert.Examples.Escrow.EscrowCorrect

Library ConCert.Examples.Dexter.DexterGens

Library ConCert.Examples.Dexter.DexterTests

Library ConCert.Examples.Dexter.Dexter

Library ConCert.Examples.Dexter.DexterPrinters

Library ConCert.Examples.FA1_2.FA1_2Correct

• FA1.2 token contract
• Properties
  • Contract rejects money
  • Default entrypoint correct
  • Transfer correct
  • Approve correct
  • Get allowance correct
  • Get balance correct
  • Get total supply correct
  • Init correct
  • Outgoing acts facts
  • Contract balance facts
  • Total supply / token balance facts
  • Empty map entries removed
  • Total supply correct

Library ConCert.Examples.FA1_2.FA1_2

• FA1.2 token contract
• Contract types
• Contract functions
  • Transfer
  • Approve
  • Get allowance
  • Get balance
  • Get total supply
  • Init
  • Receive

Library ConCert.Examples.BAT.BATAltFixCorrect

• Basic Attention Token contract
• Contract properties
  • Transfer correct
  • Transfer_from correct
  • Approve correct
  • EIP20 functions only changes token_state
  • EIP20 functions not payable
  • EIP20 functions produces no acts
  • Create_tokens correct
  • Finalize correct
  • Refund correct
  • Init correct
  • EIP20 functions preserve sum of balances
  • Init validation
  • Sum of balances always equals total supply
  • Total supply can only grow before funding fails
  • Constants are constant
  • Finalize cannot be undone
  • Cannot finalize if goal not hit
  • It is always possible to finalize
  • BAToken outgoing acts facts
  • No outgoing acts produces while funding
  • Contract balance bound
  • Outgoing acts are valid

Library ConCert.Examples.BAT.BATCorrect

• Basic Attention Token contract
• Contract properties
  • Transfer correct
  • Transfer_from correct
  • Approve correct
  • EIP20 functions only changes token_state
  • EIP20 functions not payable
  • EIP20 functions produces no acts
  • Create_tokens correct
  • Finalize correct
  • Refund correct
  • Init correct
  • Functions preserve sum of balances
  • Sum of balances always equals total supply
  • Total supply can only grow before funding fails
  • Constants are constant
  • Finalize cannot be undone
  • Cannot finalize if goal not hit
  • It is always possible to finalize
  • Refund guarantee

Library ConCert.Examples.BAT.BATFixed

• Basic Attention Token contract
• Contract functions
  • Init
  • Create Tokens
  • Refund
  • Finalize
  • Receive

Library ConCert.Examples.BAT.BAT

• Basic Attention Token contract
• Contract functions
  • Init
  • Create Tokens
  • Refund
  • Finalize
  • Receive

Library ConCert.Examples.BAT.BATFixedCorrect

• Basic Attention Token contract
• Contract properties
  • Transfer correct
  • Transfer_from correct
  • Approve correct
  • EIP20 functions only changes token_state
  • EIP20 functions not payable
  • EIP20 functions produces no acts
  • Create_tokens correct
  • Finalize correct
  • Refund correct
  • Init correct
  • EIP20 functions preserve sum of balances
  • Init validation
  • Sum of balances always equals total supply
  • Total supply can only grow before funding fails
  • Constants are constant
  • Finalize cannot be undone
  • Cannot finalize if goal not hit
  • It is always possible to finalize
  • BAToken outgoing acts facts
  • batFundDeposit cannot refund
  • Total balance lower bound
  • No outgoing acts produces while funding
  • Token balances divisible by exchange rate
  • Contract balance bound
  • outgoing acts are valid

Library ConCert.Examples.BAT.BATPrinters

Library ConCert.Examples.BAT.BATFixedTests

Library ConCert.Examples.BAT.BATAltFixTests

Library ConCert.Examples.BAT.BATCommon

• Basic Attention Token

Library ConCert.Examples.BAT.BATGens

Library ConCert.Examples.BAT.BATAltFix

• Basic Attention Token contract
• Contract functions
  • Init
  • Create Tokens
  • Refund
  • Finalize
  • Receive

Library ConCert.Examples.BAT.BATTests

Library ConCert.Examples.BAT.BATTestCommon

Library ConCert.Examples.Dexter2.Dexter2FA12Correct

• Dexter 2 FA1.2 Liquidity token contract
• Properties
  • Contract rejects money
  • Default entrypoint correct
  • Transfer correct
  • Approve correct
  • Mint or burn correct
  • Get allowance correct
  • Get balance correct
  • Get total supply correct
  • Init correct
  • Outgoing acts facts
  • Contract balance facts
  • Total supply / token balance facts
  • Empty map entries removed
  • Total supply correct

Library ConCert.Examples.Dexter2.Dexter2CommonExtract

• Common extraction setup

Library ConCert.Examples.Dexter2.Dexter2CPMMExtractLIGO

• Extracting the Main Contract

Library ConCert.Examples.Dexter2.Dexter2FA12

• Dexter 2 FA1.2 Liquidity token contract
• Contract types
• Contract functions
  • Transfer
  • Approve
  • Mint or burn
  • Get allowance
  • Get balance
  • Get total supply
  • Init
  • Receive

Library ConCert.Examples.Dexter2.Dexter2CPMMCorrect

• Dexter 2 CPMM contract
• Properties
  • Set baker correct
  • Set manager correct
  • Set liquidity address correct
  • Default entrypoint correct
  • Update token pool correct
  • Update token pool internal correct
  • Add liquidity correct
  • Remove liquidity correct
  • XTZ to token correct
  • Token to xtz correct
  • Token to token correct
  • Init correct
  • Outgoing acts facts
  • Contract balance facts
  • Total supply correct
  • lqtTotal/total_supply invariant

Library ConCert.Examples.Dexter2.Dexter2FA12ExtractLIGO

• Extracting Liquidity Token

Library ConCert.Examples.Dexter2.Dexter2Tests

• Test setup
  • Setup parameters
  • Setup actions
• Tests

Library ConCert.Examples.Dexter2.Dexter2CPMM

• Dexter 2 CPMM contract
• Contract types
  • Type synonyms
  • Entrypoint types
  • Storage types
• Contract functions
  • Helper functions
  • Add liquidity
  • Remove liquidity
  • XTZ to tokens
  • Tokes to XTZ
  • Default entrypoint
  • Set baker
  • Set manager
  • Set liquidity address
  • Update token pool
  • Update token pool internal
  • Tokens to tokens
  • Receive
  • Init

Library ConCert.Examples.Dexter2.Dexter2Gens

• Dexter2 CPMM generators
• FA2 generators
• Combined generators

Library ConCert.Examples.Dexter2.Dexter2Printers

• Dexter2 CPMM printers
• Dexter2 Lqt Token printers
• Combined message printer

Library ConCert.Examples.BoardroomVoting.BoardroomMath

Library ConCert.Examples.BoardroomVoting.Egcd

Library ConCert.Examples.BoardroomVoting.BoardroomVoting

Library ConCert.Examples.BoardroomVoting.BoardroomVotingTest

Library ConCert.Examples.BoardroomVoting.BoardroomVotingExtractionCameLIGO

• Extraction of the Boardroom voting contract CameLIGO

Library ConCert.Examples.BoardroomVoting.BoardroomVotingZ

Library ConCert.Examples.BoardroomVoting.Euler

Library ConCert.Examples.BoardroomVoting.BoardroomVotingExtractionLiquidity

• Extraction of the Boardroom voting contract Liquidity

Library ConCert.Examples.StackInterpreter.StackInterpreterRustExtract

Library ConCert.Examples.StackInterpreter.StackInterpreterExtract

• Extraction of an interpreter for a stack based DSL

Library ConCert.Examples.StackInterpreter.StackInterpreterLIGOExtract

• Extraction of an interpreter for a stack based DSL

Library ConCert.Examples.StackInterpreter.StackInterpreterLiquidityExtract

• Extraction of an interpreter for a stack based DSL

Library ConCert.Examples.StackInterpreter.StackInterpreter

Library ConCert.Examples.Congress.Congress_Buggy

Library ConCert.Examples.Congress.CongressCorrect

Library ConCert.Examples.Congress.tests.CongressTests

Library ConCert.Examples.Congress.tests.Congress_BuggyTests

Library ConCert.Examples.Congress.tests.CongressGens

Library ConCert.Examples.Congress.tests.CongressPrinters

Library ConCert.Examples.Congress.tests.Congress_BuggyPrinters

Library ConCert.Examples.Congress.tests.Congress_BuggyGens

Library ConCert.Examples.Congress.Congress

Library ConCert.Examples.Congress.LocalBlockchainTests

Library ConCert.Examples.ExchangeBuggy.ExchangeBuggy

Library ConCert.Examples.ExchangeBuggy.ExchangeBuggyPrinters

Library ConCert.Examples.ExchangeBuggy.ExchangeBuggyTests

Library ConCert.Examples.ExchangeBuggy.ExchangeBuggyGens

Library ConCert.Execution.Test.LocalBlockchain

Library ConCert.Execution.Test.QCTest

Library ConCert.Execution.Test.TestNotation

• Test parameters

Library ConCert.Execution.Test.TraceGens

Library ConCert.Execution.Test.TestUtils

Library ConCert.Execution.Test.ChainPrinters

Library ConCert.Execution.Circulation

Library ConCert.Execution.Serializable

Library ConCert.Execution.Monad

Library ConCert.Execution.ContractMonads

Library ConCert.Execution.ChainedList

Library ConCert.Execution.ResultMonad

Library ConCert.Execution.OptionMonad

Library ConCert.Execution.Finite

Library ConCert.Execution.ContractCommon

• Definitions shared among the examples

Library ConCert.Execution.BuildUtils

Library ConCert.Execution.BoundedN

Library ConCert.Execution.Blockchain

Library ConCert.Execution.Containers

Library ConCert.Execution.InterContractCommunication

Library ConCert.Extraction.CameLIGOExtract

Library ConCert.Extraction.ConcordiumExtract

Library ConCert.Extraction.CameLIGOPretty

• Pretty-printing CameLIGO code
  • Features/limitations
  • The pretty-printer

Library ConCert.Extraction.LiquidityPretty

• Pretty-printing Liquidity code
  • Features/limitations
  • The pretty-printer

Library ConCert.Extraction.SpecializeChainBase

Library ConCert.Extraction.Common

Library ConCert.Extraction.LiquidityExtract

Library ConCert.Extraction.PrettyPrinterMonad

Library ConCert.Extraction.Tests.RecordExtractionLiquidityTests

Library ConCert.Extraction.Tests.NumLiteralTests

Library ConCert.Extraction.Tests.CameLIGOExtractionTests

• Extraction of various contracts to CameLIGO