Library ConCert.Extraction.PrettyPrinterMonad

Library ConCert.Extraction.CameLIGOPretty

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

Library ConCert.Extraction.LiquidityExtract

Library ConCert.Extraction.Common

Library ConCert.Extraction.SpecializeChainBase

Library ConCert.Extraction.ConcordiumExtract

Library ConCert.Extraction.CameLIGOExtract

Library ConCert.Extraction.LiquidityPretty

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

Library ConCert.Extraction.Tests.CameLIGOExtractionTests

• Extraction of various contracts to CameLIGO

Library ConCert.Extraction.Tests.NumLiteralTests

Library ConCert.Extraction.Tests.RecordExtractionLiquidityTests

Library ConCert.Embedding.Extraction.SimpleBlockchainExt

• A simply-typed version of the blockchain execution environment

Library ConCert.Embedding.Extraction.Liquidity

Library ConCert.Embedding.Extraction.PreludeExt

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

Library ConCert.Embedding.Prelude

• Prelude -- definitions of basic of data types

Library ConCert.Embedding.CertifyingTranslate

• Certifying translation
  • Negation on booleans

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.pcuic.PCUICCorrectness

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

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.PCUICTranslate

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

Library ConCert.Embedding.pcuic.PCUICtoTemplate

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

Library ConCert.Embedding.pcuic.PCUICFacts

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

Library ConCert.Embedding.Tests

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

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.SimpleBlockchain

• A simply-typed version of the blockchain execution environment

Library ConCert.Embedding.Utils

Library ConCert.Embedding.Misc

• Some facts not found in the standard library

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.TranslationUtils

Library ConCert.Embedding.EvalE

• Interpreter for the λsmart language

Library ConCert.Embedding.Notations

• Notations for the deep embedding

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.Execution.Finite

Library ConCert.Execution.BlockchainBFS

Library ConCert.Execution.ContractProperties

Library ConCert.Execution.BlockchainDFS

Library ConCert.Execution.Monad

Library ConCert.Execution.SerializableSound

Library ConCert.Execution.Blockchain

Library ConCert.Execution.InterContractCommunication

Library ConCert.Execution.BoundedN

Library ConCert.Execution.Serializable

Library ConCert.Execution.BlockchainTheories

Library ConCert.Execution.ChainedList

Library ConCert.Execution.Circulation

Library ConCert.Execution.SerializableBase

Library ConCert.Execution.ContractMonads

Library ConCert.Execution.SerializableDerive

Library ConCert.Execution.BlockchainBase

Library ConCert.Execution.OptionMonad

Library ConCert.Execution.BlockchainBuilder

Library ConCert.Execution.Containers

Library ConCert.Execution.ContractCommon

• Definitions shared among the examples

Library ConCert.Execution.ResultMonad

Library ConCert.Execution.BlockchainInduction

Library ConCert.Execution.SerializableInstances

Library ConCert.Execution.Test.TraceGens

Library ConCert.Execution.Test.LocalBlockchain

Library ConCert.Execution.Test.TestNotation

• Test parameters

Library ConCert.Execution.Test.TestUtils

Library ConCert.Execution.Test.QCTest

Library ConCert.Execution.Test.ChainPrinters

Library ConCert.Utils.Automation

• This file implements various helper tactics

Library ConCert.Utils.BytestringExtra

Library ConCert.Utils.RecordSet

Library ConCert.Utils.StringExtra

Library ConCert.Utils.BSEnv

• Evaluation environments

Library ConCert.Utils.Extras

Library ConCert.Utils.Env

• Evaluation environments

Library ConCert.Utils.RecordUpdate

Library ConCert.Examples.PiggyBank.PiggyBankCorrect

• Piggybank contract
  • Functional properties
  • Safety properties

Library ConCert.Examples.PiggyBank.PiggyBankExtractLIGO

Library ConCert.Examples.PiggyBank.PiggyBankExtractLiquidity

Library ConCert.Examples.PiggyBank.PiggyBankExtractRust

Library ConCert.Examples.PiggyBank.PiggyBank

• Piggy Bank Contract
• Types
• Error codes
• Implementation

Library ConCert.Examples.Congress.Congress

Library ConCert.Examples.Congress.LocalBlockchainTests

Library ConCert.Examples.Congress.tests.Congress_BuggyTests

Library ConCert.Examples.Congress.tests.CongressGens

Library ConCert.Examples.Congress.tests.CongressTests

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_Buggy

Library ConCert.Examples.Congress.CongressCorrect

Library ConCert.Examples.Counter.extraction.CounterRefTypesMidlang

• Extraction of a counter contract with refinement types to Midlang

Library ConCert.Examples.Counter.extraction.CounterDepCertifiedLiquidity

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

Library ConCert.Examples.Counter.extraction.CounterRust

Library ConCert.Examples.Counter.extraction.CounterSubsetTypesLIGO

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

Library ConCert.Examples.Counter.extraction.CounterSubsetTypesLiquidity

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

Library ConCert.Examples.Counter.extraction.CounterCertifiedLiquidity

• Extraction of a simple counter contract

Library ConCert.Examples.Counter.extraction.CounterLIGO

• Extraction of various contracts to CameLIGO

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.Dexter.Dexter

Library ConCert.Examples.Dexter.DexterGens

Library ConCert.Examples.Dexter.DexterPrinters

Library ConCert.Examples.Dexter.DexterTests

Library ConCert.Examples.Escrow.extraction.EscrowMidlang

Library ConCert.Examples.Escrow.extraction.EscrowLiquidity

• Extraction of Escrow to CameLIGO and liquidity

Library ConCert.Examples.Escrow.extraction.EscrowLIGO

• Extraction of Escrow to CameLIGO and liquidity

Library ConCert.Examples.Escrow.extraction.EscrowRust

Library ConCert.Examples.Escrow.tests.EscrowTests

Library ConCert.Examples.Escrow.tests.EscrowPrinters

Library ConCert.Examples.Escrow.tests.EscrowGens

Library ConCert.Examples.Escrow.EscrowCorrect

Library ConCert.Examples.Escrow.Escrow

Library ConCert.Examples.BoardroomVoting.BoardroomVotingExtractionCameLIGO

• Extraction of the Boardroom voting contract CameLIGO

Library ConCert.Examples.BoardroomVoting.Egcd

Library ConCert.Examples.BoardroomVoting.Euler

Library ConCert.Examples.BoardroomVoting.BoardroomVoting

Library ConCert.Examples.BoardroomVoting.extract.ExtractBoardroomVotingLIGO

• Extraction of the Boardroom voting contract CameLIGO

Library ConCert.Examples.BoardroomVoting.BoardroomVotingTest

Library ConCert.Examples.BoardroomVoting.BoardroomVotingExtractionLiquidity

• Extraction of the Boardroom voting contract Liquidity

Library ConCert.Examples.BoardroomVoting.BoardroomMath

Library ConCert.Examples.BoardroomVoting.BoardroomVotingZ

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.CrowdfundingData

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

Library ConCert.Examples.Crowdfunding.CrowdfundingCorrect

• Properties of the crowdfunding contract

Library ConCert.Examples.Crowdfunding.extract.ExtractCrowdfundingCameLIGO

• Extraction of various contracts to CameLIGO

Library ConCert.Examples.Crowdfunding.extract.ExtractCrowdfundingLiquidity

• Extraction of a crowdfunding 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.CrowdfundingCameLIGO

• Extraction of various contracts to CameLIGO

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.Crowdfunding

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

Library ConCert.Examples.Crowdfunding.CrowdfundingLiquidity

• Extraction of a crowdfunding contract

Library ConCert.Examples.iTokenBuggy.iTokenBuggyPrinters

Library ConCert.Examples.iTokenBuggy.iTokenBuggyGens

Library ConCert.Examples.iTokenBuggy.iTokenBuggy

Library ConCert.Examples.iTokenBuggy.iTokenBuggyTests

Library ConCert.Examples.StackInterpreter.StackInterpreterRustExtract

Library ConCert.Examples.StackInterpreter.StackInterpreter

Library ConCert.Examples.StackInterpreter.extract.ExtractStackInterpLiquidity

• Extraction of an interpreter for a stack based DSL

Library ConCert.Examples.StackInterpreter.extract.ExtractStackInterpLIGO

• Extraction of an interpreter for a stack based DSL

Library ConCert.Examples.StackInterpreter.extract.ExtractStackInterpRust

Library ConCert.Examples.StackInterpreter.StackInterpreterLiquidityExtract

• 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.StackInterpreterExtract

• Extraction of an interpreter for a stack based DSL

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.CIS1.CIS1wccd

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

Library ConCert.Examples.CIS1.CIS1Utils

Library ConCert.Examples.FA2.FA2Printers

Library ConCert.Examples.FA2.FA2Token

Library ConCert.Examples.FA2.FA2TokenTests

Library ConCert.Examples.FA2.TestContracts

Library ConCert.Examples.FA2.FA2Interface

Library ConCert.Examples.FA2.FA2LegacyInterface

Library ConCert.Examples.FA2.FA2Gens

Library ConCert.Examples.ExchangeBuggy.ExchangeBuggyGens

Library ConCert.Examples.ExchangeBuggy.ExchangeBuggy

Library ConCert.Examples.ExchangeBuggy.ExchangeBuggyPrinters

Library ConCert.Examples.ExchangeBuggy.ExchangeBuggyTests

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.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.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.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.extract.ExtractCPMMLIGO

Library ConCert.Examples.Dexter2.extract.ExtractFA12LIGO

Library ConCert.Examples.Dexter2.Dexter2Tests

• Test setup
  • Setup parameters
  • Setup actions
• Tests

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.Dexter2CPMMExtractLIGO

• Extracting the Main Contract

Library ConCert.Examples.Dexter2.Dexter2Gens

• Dexter2 CPMM generators
• FA2 generators
• Combined generators

Library ConCert.Examples.Dexter2.Dexter2FA12ExtractLIGO

• Extracting Liquidity Token

Library ConCert.Examples.Dexter2.Dexter2Printers

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

Library ConCert.Examples.Dexter2.Dexter2CommonExtract

• Common extraction setup

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.BAT.BATPrinters

Library ConCert.Examples.BAT.BATFixed

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

Library ConCert.Examples.BAT.BATAltFixTests

Library ConCert.Examples.BAT.BAT

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

Library ConCert.Examples.BAT.BATFixedTests

Library ConCert.Examples.BAT.BATAltFix

• Basic Attention Token contract
• Contract functions
  • Init
  • Create Tokens
  • Refund
  • Finalize
  • 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.BATTestCommon

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.BATGens

Library ConCert.Examples.BAT.BATCommon

• Basic Attention Token

Library ConCert.Examples.BAT.BATTests

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.EIP20.EIP20Token

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

Library ConCert.Examples.EIP20.EIP20LiquidityExtraction

• Extraction of a simple counter contract

Library ConCert.Examples.EIP20.EIP20TokenGens

Library ConCert.Examples.EIP20.EIP20TokenPrinters

Library ConCert.Examples.EIP20.EIP20TokenTests

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.EIP20CameLIGOExtraction

• Extraction of various contracts to CameLIGO