au-cobra / concert Goto Github PK

The support of recursive functions of multiple arguments has been added to LIGO: https://gitlab.com/ligolang/ligo/-/issues/1248

The pretty-printer could be simplified because wrapping multiple arguments in a tuple is no longer required.

Since we have a growing number of contracts implemented directly in Coq, maybe we should create a subfolder examples or something like this at the same level as theories? Then the structure will be aligned to how I did it for embedding and extraction

Since the implementation of the FA2Interface, a new standard has been adopted: https://gitlab.com/tezos/tzip/-/blob/master/proposals/tzip-12/fa2_interface.mligo
We propose creating a new standard FA2 interface using this exact formula, and moving the deprecated parts into a legacy version so that the old files still work.

Running make fails on systems with case insensitive file system due to uncapitalization step done in extraction/process_extraction.sh

After inlining has been added, the translation (f "") -> f is no longer necessary, so it should be removed.

Some quoted terms use the same names of nested lambda abstracted variables, E.g quoting bool_rect gives (a fragment)

tLambda {| Ast.BasicTC.binder_name := nNamed "f";   Ast.BasicTC.binder_relevance := Relevant |}
                (tApp (tRel 0) [tConstruct  {|  Ast.BasicTC.inductive_mind := ( MPfile ["Datatypes"; "Init"; "Coq"], "bool");
                                                                 Ast.BasicTC.inductive_ind := 0 |} 0 []])
                (tLambda {| Ast.BasicTC.binder_name := nNamed "f"; Ast.BasicTC.binder_relevance := Relevant |}
                                (tApp (tRel 1) [tConstruct {| Ast.BasicTC.inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "bool");
                                                                            Ast.BasicTC.inductive_ind := 0 |} 1 []]) ...

There are two vars that are named "f". Liquidity extraction produces

let coq_bool_rect (f : 'a0) (f : 'a0) (b : bool) = if b then f else f

which is clearly wrong. So we need to take care of shadowing like this.

Probably, the same problem exists in CameLIGO extraction.

Dexter1, Dexter2, and FA2 all use a deprecated FA2 interface, these should be ported to the new interface added in #164.

At least the examples CounterRefinementTypes.v, RustEIP20.v and CrowdfundingCertifiedExtraction.v produce Liquidity code that does not compile.

Here is the summary:

• CounterRefinementTypes.v - sig is identified as a record, since it has one constructor. The problematic part is here: https://github.com/AU-COBRA/ConCert/blob/master/extraction/theories/LPretty.v#L284. is_record_constr should also check whether projections are defined (projections will be produced either from "real" projections in the case of primitive projections or from names of the arguments)
• ERC20LiquidityExtraction.v - move type alias for storage from init and move it to the top level; plus, fixing #91 is required. Names to and val are reserved and cannot be used as variable names. The type of the ctx parameter of the inner local definition in the init is wrong. Here is a compilable version after some manual tweaking: https://gist.github.com/annenkov/0c65c701ee958adac16cc8d0a91a2a38
• CrowdfundingCertifiedExtraction.v - something is wrong with the remapping of amount.

In all the examples above, cosntructors of bool are printed as True and False while they should be true and false.

We only keep track of the address that initiated the current transaction in the chain of calls. All our targets (Concordium, Tezos, Dune) support both the immediate sender address and the address of the user account that originally initiated the chain of calls.

Proposal: extend ContractCallContext with a new field ctx_origin to keep track of the original account that started the call chain. Note that ctx_origin is always a user account address.

Correspondence with the target platforms:

• Concordium: ctx_origin -> HasReceiveContext::invoker, ctx_from -> HasReceiveContext.sender
• Tezos: ctx_origin -> Tezos.source, ctx_from -> Tezos.sender
• Dune: ctx_origin -> Current.source, ctx_from -> Current.sender

There are many instances of unused or duplicated imports. These should be cleaned up, potentially using coq-tools. I'm assigning this to myself.

Using partial_alter is problematic for some extraction targets. E.g. in Liquidity, closures have a type that depends on the closure context. partial_alter is a higher-order function and passing a function to it not always possible due to this restriction.

Hello everyone,

As per my understanding Concert project is two main projects:

1- An verified extraction plugins from Coq to Rust Liquidity.
2- Verified block chain applications that use the extraction plugins.

I propose we split the extraction plugin from the block chain applications from the extraction plugins, and aim to stabilize the extraction plugin and get it into coq repository:

The process looks to be relatively simple[1] give that concert already uses opam for building. but the only downside is the extra overhead needed to manage releases (stable API and not breaking compatibility ..etc).

Also that may be a good first step to ship concert extraction with coq platform[2].

[1] https://opam.ocaml.org/doc/Packaging.html#Publishing
[2] https://github.com/coq/platform

In ConCert the contract_induction lemma lets us prove statements of the form

  forall bstate caddr (trace : ChainTrace empty_state bstate),
    env_contracts bstate caddr = Some (contract : WeakContract) ->
    exists dep cstate inc_calls,
      deployment_info Setup trace caddr = Some dep /\
      contract_state bstate caddr = Some cstate /\
      incoming_calls Msg trace caddr = Some inc_calls /\
      P (chain_height bstate)
        (current_slot bstate)
        (finalized_height bstate)
        caddr
        dep
        cstate
        (env_account_balances bstate caddr)
        (outgoing_acts bstate caddr)
        inc_calls
        (outgoing_txs trace caddr).

However it is not always possible to reuse proofs on this form inside another proof proven by contract_induction. Let's say that I have already proven a lemma for some property Q which was proved using contract_induction and to prove the property P above I need the information in Q, since I have already proven Q I would like to simply apply that lemma in my proof however to apply I will need to know

reachable bstate /\
env_contracts bstate caddr = Some (contract : WeakContract) /\
deployment_info Setup trace caddr = Some dep /\
contract_state bstate caddr = Some cstate /\
incoming_calls Msg trace caddr = Some inc_calls /\

This information is not available in the goals that are produced by contract_induction so you cannot apply the lemma for Q.
As far as I can tell the CallFacts, DeployFacts and AddBlockFacts used in contract_induction were intended for this purpose and it is possible to use e.g. CallFacts if Q only need cstate. However these facts cannot be used in general to introduce any lemma in this format since none of the facts gives you both cstate, dep, inc_calls and bstate at the same time.

So if contract_induction should allow reuse of proofs it either need to change how the facts work or give the needed information in the goals produced.

The view functionality allows for querying contracts in a synchronous way. This functionality makes it easier to implement contracts that require using some data from other contracts, for example, getting data from oracles. With only message passing, it could be implemented with callbacks. This is, however, awkward and error-prone.

The view mechanism guarantees that the state will not be changed, that's why it should be relatively unproblematic to add to ConCert: the execution model stays the same, we just need to add some additional data available to contracts during the receive function call.

We can extend ConCert to handle views:

• Add view function(s) to the Contract; it could be done by using a single function that dispatches on a special "view message" (however, the return type still might be different for different views).

• Pass around the extended state. Currently, the blockchain state available to the contracts (part of the contract's signature):

Record Chain :=
 build_chain {
   chain_height : nat;
   current_slot : nat;
   finalized_height : nat;
 }.

It could be extended with a field containing the whole Environment, or some restriction of it. In this case, one could access the contract's view functions (and, maybe, state?). Possibly, some of the infrastructure from the implementations of the execution layer can be used [LocalBlockchain](https://github.com/AU-COBRA/ConCert/blob/0399316dbc882e228e5e0c0daf98b51460dc760a/execution/theories/LocalBlockchain.v#L39]

• Introduce a view_call function that will fetch a view and, if it was successfully fetched, call it.

In the current modelling of blockchains in ConCert there is no way to discard or consume actions in the chain_state_queue of a ChainState if those actions are invalid.

This is problematic for proofs reasoning about the future state of a blockchain for any ChainState since it is required that the chain_state_queue is empty to add new actions and for the blockchain to grow. However it is not possible to prove that the queue can be emptied without the option to discard those actions that cannot be evaluated and thus you can only prove anything about the future of a ChainState for ChainStates that have an empty queue.

This does not represent a real blockchain very well since a real blockchain would not get stuck growing just because an invalid transaction or contract call was sent.

It seems _CoqProject confuses Proof General, it uses the one in the "execution" folder instead of the main one.

The embedding does not compile with Coq 8.11 (using the new MetaCoq package):

File "./embedding/theories/Misc.v", line 106, characters 23-36:
Error: The reference utils.rev_ind was not found in the current environment.

We should maybe discuss which versions of Coq we want to support for full ConCert, i.e.
do we want the embedding to support multiple versions of Coq or not. Pros are that it
makes working with the project easier for other people, but a con is that it takes some more
effort.

@annenkov

Both Tezos and Concordium have a concept of entypoints which we model as a Msg type, usually represented as an inductive type with several constructors corresponding to the entrypoints. However, it's difficult to send messages to an (arbitrary) contract that supports only some of the entrypoints. Therefore, we need a more abstract notion of an interface that would allow for a more flexible way of specifying the supported entrypoints.

I was looking into extracting the counter module to concordium, using our Wasm backend for CertiCoq.

CertiCoq is currently on MetaCoq 1.3, which ConCert doesn't seem to work with.

Do you already have plans to update?

Implement a printer for lambda-smart expressions to the concrete syntax of Liquidity.

Currently, there is no easy way of running the tests. We can move the tests (QuickChick calls) to separate files and compile them with something like make quickchick