AU-COBRA/ConCert

[Liquidity] Extraction to Liquidity is broken for some examples

annenkov opened this issue · 0 comments

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.