| 8afa834 | Danil Annenkov | 25 February 2022, 11:56:07 UTC | Switch to LIGO 0.34.0; uncomment extraction of CounterSubsetTypes | 25 February 2022, 11:56:07 UTC |
| ca28da9 | Danil Annenkov | 24 February 2022, 19:58:46 UTC | Increase http.postBuffer | 24 February 2022, 19:58:46 UTC |
| 0438dfe | Danil Annenkov | 24 February 2022, 17:00:11 UTC | Fixed commit version in concert-std; uncomment boardroom voting extraction; update counter with subset types to LIGO (was not added to the previous commit) | 24 February 2022, 17:00:11 UTC |
| 74ba4fe | Danil Annenkov | 24 February 2022, 14:27:25 UTC | Pin concordium repo to a particilar commit; uncomment boardroom voting extraction | 24 February 2022, 14:27:25 UTC |
| 5d48f89 | Danil Annenkov | 23 February 2022, 10:37:15 UTC | Add inner and mutual fixpoint examples to Rust extraction | 23 February 2022, 10:37:15 UTC |
| 5b491e4 | Danil | 02 September 2021, 20:48:47 UTC | Merge remote-tracking branch 'upstream/master' into journal-2021 | 02 September 2021, 20:48:47 UTC |
| 67e9f2c | Danil | 02 September 2021, 20:48:16 UTC | Uncomment extraction of the counter with subset types | 02 September 2021, 20:48:16 UTC |
| 1fce313 | Danil | 02 September 2021, 20:47:19 UTC | Update README: extend the project structure description | 02 September 2021, 20:47:19 UTC |
| 06ffb81 | Danil | 02 September 2021, 08:04:59 UTC | Link to the journal-2021 branch in README | 02 September 2021, 08:04:59 UTC |
| 3472ccf | Danil | 02 September 2021, 08:01:12 UTC | Merge remote-tracking branch 'upstream/master' into journal-2021 | 02 September 2021, 08:01:12 UTC |
| 112c56d | Danil | 01 September 2021, 13:46:14 UTC | Update README; process extraction resutls by default | 01 September 2021, 13:46:14 UTC |
| 66f528d | Danil | 01 September 2021, 09:34:02 UTC | CI: push only the extraction resutls from the main repo and the journal-2021 branch | 01 September 2021, 09:34:02 UTC |
| 20b1878 | Danil | 01 September 2021, 09:28:04 UTC | CI: push only the extraction resutls from the master branch of the mainrepo | 01 September 2021, 09:28:04 UTC |
| ac28d68 | Danil | 01 September 2021, 09:00:30 UTC | CI: push the extraction results for the journal-2021 branch | 01 September 2021, 09:00:30 UTC |
| e3275e5 | Danil | 01 September 2021, 08:55:34 UTC | Merge branch 'master' into journal-2021 | 01 September 2021, 08:55:34 UTC |
| 8b3608f | Danil | 31 August 2021, 13:00:28 UTC | CI: don't push the extraction results on pull requests. | 31 August 2021, 13:00:28 UTC |
| 1da9986 | Danil | 31 August 2021, 11:56:28 UTC | CI: uncomment pushing the extraction results | 31 August 2021, 11:56:28 UTC |
| 41c4970 | Danil | 31 August 2021, 10:32:21 UTC | Merge remote-tracking branch 'upstream/master' | 31 August 2021, 10:32:21 UTC |
| 3b276fd | Danil Annenkov | 31 August 2021, 10:14:31 UTC | CI config for building extraction (#114) Use a Docker image with compilers; compile extraction output on build | 31 August 2021, 10:14:31 UTC |
| b87b18d | Danil | 31 August 2021, 09:03:43 UTC | Comment out push to the extraction repo for now | 31 August 2021, 09:03:43 UTC |
| 2846033 | Danil | 31 August 2021, 07:25:07 UTC | CI: add git username | 31 August 2021, 07:25:07 UTC |
| 351ca9e | Danil | 30 August 2021, 11:11:48 UTC | Remove feature(unsigned_abs) from Rust extraction prelude; uncomment the rest of the contract extraction examples | 30 August 2021, 11:11:48 UTC |
| 97624a1 | Danil | 30 August 2021, 10:04:53 UTC | Test rust extraction; fix gitignore | 30 August 2021, 10:04:53 UTC |
| 22b32d4 | Danil | 25 August 2021, 12:25:53 UTC | Add cargo to PATH in build.yml | 25 August 2021, 12:26:16 UTC |
| 63bfd88 | Danil | 25 August 2021, 10:56:38 UTC | CI: debug | 25 August 2021, 10:56:38 UTC |
| fcc4ed3 | Danil | 24 August 2021, 13:57:34 UTC | CI: debug | 24 August 2021, 13:57:34 UTC |
| 196faea | Danil | 24 August 2021, 13:55:13 UTC | CI: remove sudo; debug | 24 August 2021, 13:55:13 UTC |
| fe05553 | Danil | 24 August 2021, 12:57:37 UTC | CI: Try with sudo again | 24 August 2021, 12:57:37 UTC |
| 02d6508 | Danil | 24 August 2021, 11:53:41 UTC | CI: redirect liquidity stderr to a file; Docker: configure git to fetch through https | 24 August 2021, 11:53:41 UTC |
| e60f39d | Danil | 23 August 2021, 20:34:40 UTC | Forgot to include build config :) | 23 August 2021, 20:34:40 UTC |
| cb11643 | Danil | 23 August 2021, 19:57:00 UTC | CI: move testing back to the build step;comment out ERC20 extraction to Liquidity | 23 August 2021, 19:57:00 UTC |
| 6dc3d6d | Danil | 23 August 2021, 16:26:10 UTC | Debug CI | 23 August 2021, 16:26:10 UTC |
| a5263c5 | Danil | 23 August 2021, 14:57:21 UTC | More opam-related fixes | 23 August 2021, 14:57:21 UTC |
| ed669c9 | Danil | 23 August 2021, 14:17:49 UTC | Add setting opam env variables in the testing step of CI | 23 August 2021, 14:17:49 UTC |
| 2c911d8 | Danil | 23 August 2021, 13:27:15 UTC | Add some sudos to the build.yaml | 23 August 2021, 13:27:15 UTC |
| 1625478 | Danil | 23 August 2021, 11:30:12 UTC | Try fixing the build | 23 August 2021, 11:30:12 UTC |
| d8cfcef | Danil | 21 August 2021, 13:47:36 UTC | Test extraction as a separate step after build | 21 August 2021, 13:47:36 UTC |
| 6e393ea | Danil | 20 August 2021, 13:52:02 UTC | Add views for the Elm web app | 20 August 2021, 13:52:02 UTC |
| eb4c278 | Danil | 20 August 2021, 13:09:38 UTC | Add tests dir placeholder for elm extraction | 20 August 2021, 13:09:38 UTC |
| 1580353 | Danil | 20 August 2021, 12:29:20 UTC | Add src folder placeholder for elm | 20 August 2021, 12:29:20 UTC |
| 1d6d429 | Danil | 20 August 2021, 11:43:10 UTC | Fix a typo in build.yaml | 20 August 2021, 11:43:10 UTC |
| 5a85e5f | Danil | 20 August 2021, 11:16:35 UTC | add src for elm; fix build.yaml | 20 August 2021, 11:16:35 UTC |
| f7fe8d1 | Danil | 20 August 2021, 10:17:22 UTC | Add more clean-up targets to Makefile; change build.yaml | 20 August 2021, 10:17:22 UTC |
| b917451 | Danil | 20 August 2021, 06:47:55 UTC | Fix build.yaml | 20 August 2021, 06:47:55 UTC |
| 8e809b4 | Danil | 20 August 2021, 06:39:40 UTC | Forgot build.yaml | 20 August 2021, 06:39:40 UTC |
| 68fcd94 | Danil | 20 August 2021, 06:30:46 UTC | Experimenting with github actions: pushing the extraction resutls to another repo; commented out escrow extraction for now | 20 August 2021, 06:30:46 UTC |
| 2cb1ad4 | Danil | 19 August 2021, 19:27:41 UTC | Add elm to Dockerfile; test extraction as a separate step | 19 August 2021, 19:27:41 UTC |
| 7ece1d1 | Danil | 19 August 2021, 11:36:10 UTC | Use a Docker image with compilers; compile extraction output on build | 19 August 2021, 11:36:10 UTC |
| bfb974a | Danil | 14 August 2021, 20:13:08 UTC | Merge branch 'master' into journal-2021 | 14 August 2021, 20:13:08 UTC |
| 988b37a | Danil | 14 August 2021, 20:11:49 UTC | Uncomment redirecting the extracted Escrow code | 14 August 2021, 20:11:49 UTC |
| 5e4241a | Danil | 13 August 2021, 20:58:00 UTC | Merge branch 'master' into journal-2021 | 13 August 2021, 20:58:00 UTC |
| dfaed8b | Danil Annenkov | 13 August 2021, 20:54:40 UTC | CameLIGO extraction cleanup; fixed various small issues with wrappers; call context as a record; fic bugs in literal printing; improve extraction testing in makefile (#113) | 13 August 2021, 20:54:40 UTC |
| 5c960c1 | 4ever2 | 09 August 2021, 08:44:12 UTC | Contract induction add outgoing acts to CallFacts (#111) * Add outgoing acts to CallFacts * Adapt existing proofs to new CallFacts signature | 09 August 2021, 08:44:12 UTC |
| 59264a2 | Danil | 05 August 2021, 19:51:58 UTC | Merge remote-tracking branch 'upstream/master' into journal-2021 | 05 August 2021, 19:51:58 UTC |
| 83765ec | Danil | 05 August 2021, 19:50:30 UTC | Add docker config with full concert | 05 August 2021, 19:50:30 UTC |
| 0b5ee96 | Danil Annenkov | 05 August 2021, 19:48:46 UTC | Fix comments (#112) | 05 August 2021, 19:48:46 UTC |
| 56ddcc5 | Danil | 05 August 2021, 19:47:18 UTC | Fix comments | 05 August 2021, 19:47:18 UTC |
| 5eb12f3 | Danil | 31 July 2021, 13:34:38 UTC | Fix cameligo extraction tests | 31 July 2021, 13:34:38 UTC |
| b07f07f | Danil | 30 July 2021, 14:55:39 UTC | Fix path in a plugin example | 30 July 2021, 14:55:39 UTC |
| b140f31 | Danil Annenkov | 30 July 2021, 14:14:52 UTC | Moved target dirs for extraction in one place; renamed CounterRefinementTypes to CounterSubsetTypes;update scripts to build LIGO (#110) | 30 July 2021, 14:14:52 UTC |
| 97cf725 | Mikkel Milo | 30 July 2021, 13:17:27 UTC | generalize type in pre-post-assertion | 30 July 2021, 13:17:27 UTC |
| 959540c | Danil Annenkov | 30 July 2021, 13:15:54 UTC | Add (a prototype of) the numeric literal printing; escrow extracts as it is; fixes to Liquidity extraction (closes #90) (#109) | 30 July 2021, 13:15:54 UTC |
| 8e0e6e2 | Milo | 29 July 2021, 09:33:54 UTC | Liquidity record printing fix + BoardroomVoting Extraction (#108) * liq extraction with chainbase add liq extraction with chainbase specialization fix issue with records * add chainbase specialisation to liq extract * fix after rebase * liq extraction with chainbase add liq extraction with chainbase specialization fix issue with records * add chainbase specialisation to liq extract * fix after rebase * liq extraction with chainbase add liq extraction with chainbase specialization fix issue with records * BV extraction WIP + add reserved names to pretty-printers * boardroom extraction WIP * Boardroom WIP 2 * Boardroom WIP 3 * WIP * WIP2 * BV extract WIP * make specialized boardrm for extraction, fix in liq extraction * Add boardroom extract, fix some bugs in pretty printers * fix record printing in liquidity + unit tests | 29 July 2021, 09:33:54 UTC |
| d3a9566 | Danil | 27 July 2021, 13:34:53 UTC | Add more safe_pred to Elm examples; update gitignore | 27 July 2021, 13:34:53 UTC |
| 78e0111 | Milo | 27 July 2021, 13:11:18 UTC | Escrow extraction, extraction improvements, and fixes. (#106) add escrow extract to cameligo, fix pp bugs, fix constructor capitalization bug | 27 July 2021, 13:11:18 UTC |
| a8b4fd0 | Bas Spitters | 26 July 2021, 08:54:17 UTC | Update README.md | 26 July 2021, 08:54:17 UTC |
| 28f56a7 | Danil Annenkov | 16 July 2021, 11:29:09 UTC | Fixes in concordium extraction (#104) Fixes in Concordium extraction: derive Reject; more remapping; fix receive wrapper to match the balance update semantics; post-processing of Rust extraction; tests for extracted Escrow | 16 July 2021, 11:29:09 UTC |
| daae096 | Milo | 07 July 2021, 11:30:14 UTC | add youtube link to readme | 07 July 2021, 11:30:14 UTC |
| 3b824a1 | Milo | 05 July 2021, 11:22:33 UTC | Extraction improvements, cameligo extraction of counter with refinement types (#103) * add chainbase specialisation to liq extract * fix record printing, and some capitalization bugs * extract counterrefinement to cameligo * truncated sub int for cameligo | 05 July 2021, 11:22:33 UTC |
| e466915 | Bas Spitters | 04 July 2021, 05:38:00 UTC | ml family paper | 04 July 2021, 05:38:00 UTC |
| 3f6f704 | Bas Spitters | 04 July 2021, 05:34:34 UTC | ml family paper | 04 July 2021, 05:34:34 UTC |
| 1441332 | Danil Annenkov | 29 June 2021, 18:53:08 UTC | Misc fixes in extraction (#100) * Add more beta-reductions to inlining; inline definitions in inductive types; cleaned up ERC20 extraction to CameLIGO; misc fixes in Liquidity pretty-printing; fixed deboxing of type aliases * Update extraction/theories/LPretty.v Co-authored-by: Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com> * Fix comments in Elm tests Co-authored-by: Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com> | 29 June 2021, 18:53:08 UTC |
| 4c2dae8 | Danil Annenkov | 21 June 2021, 18:44:43 UTC | Update README: rearrange papers, add new Coq WC paper. | 21 June 2021, 18:44:43 UTC |
| f30536c | 4ever2 | 19 June 2021, 17:24:39 UTC | Invalid actions (#101) * Update coq-stdpp * Update ChainStep to allow dropping invalid user actions * Adapt proofs to new ChainStep * More proofs updated * Adapt ltacs in Blockchain.v to new ChainStep * Update proofs in Circulation.v * Update ltac in Blockchain.v * no message * Use intuition in proof * Shorter proof without intuition * Remove inhabited from step_action_invalid constructor | 19 June 2021, 17:24:39 UTC |
| 5fd6a9e | 4ever2 | 18 June 2021, 13:21:45 UTC | Discard invalid actions (#99) * Update ChainStep to allow dropping invalid user actions * Adapt proofs to new ChainStep | 18 June 2021, 13:21:45 UTC |
| c867494 | 4ever2 | 18 June 2021, 08:38:01 UTC | QuickChick testing improvements (#98) * Update coq-stdpp * QC changes * Update old tests to work with new TraceGens.v changes * Add file with all tests * Reverse broken test fixes * Fix incompatible notation in EIP20TokenTests.v * Add modules to AllTests.v file to avoid imports conflicting. Also adds tests that no longer works * Fix pre_post_assertion not checking if the action was for the correct contract | 18 June 2021, 08:38:01 UTC |
| c4fa5d2 | Danil Annenkov | 27 May 2021, 12:11:59 UTC | Handling the elimination from empty types (#96) * Handling the elimination from empty types; * add inlining to the CameLIGO pipeline; * improve performance of CameLIGO extraction; fix printing of pattern-matching on lists and printing of iterated lambdas for CameLIGO; * Printing the false elim code in Rust and Liquidity; fix capitalisation of variables for CameLIGO and Liquidity. | 27 May 2021, 12:11:59 UTC |
| f291ce9 | Danil Annenkov | 17 May 2021, 20:50:37 UTC | Opam config, pin to a new MetaCoq commit (#95) opam config; pin to new MetaCoq commit | 17 May 2021, 20:50:37 UTC |
| a78a6ab | Danil | 17 May 2021, 13:43:00 UTC | Fix opam config | 17 May 2021, 13:43:00 UTC |
| f9655c0 | Danil | 17 May 2021, 13:31:04 UTC | Add opam config | 17 May 2021, 13:31:04 UTC |
| b6992ef | Danil Annenkov | 06 May 2021, 19:51:57 UTC | Remove partial_alter (closes #91); fix inlining (#94) | 06 May 2021, 19:51:57 UTC |
| c44e068 | Danil | 03 May 2021, 15:16:05 UTC | Update ElmForms | 04 May 2021, 07:53:11 UTC |
| 3b8e1a8 | Bas Spitters | 28 April 2021, 05:48:52 UTC | Update README.md | 28 April 2021, 05:48:52 UTC |
| fb5ab02 | 4ever2 | 15 April 2021, 07:52:54 UTC | BAT Token implementation fix (#89) Fix BAT try_create_tokens overwriting current balance | 15 April 2021, 07:52:54 UTC |
| 280da2a | Jakob Botsch Nielsen | 07 April 2021, 10:24:51 UTC | Implement 'push-button' extraction (#88) * Implement 'push-button' extraction Implement some more automated extraction that can take contracts written for the ConCert framework and extract them to Concordium almost fully automatically. To accomplish this we generate wrappers that convert between the Concordium types and the ConCert types, including for the transfer type. Calls are not yet supported. In addition: - Add a stack interpreter example to ConCert.Execution.Examples that can run in the execution layer, and extract this from RustInterp.v instead of the old more ad-hoc extraction. - Implement Serializable instances for ascii/string, which were needed in the stack interpreter. - Remove ForPaper.v, which is not terribly important to have in master anymore, since it exists in the relevant tags. - Add a way to specify overridden masks to the dearg transform so that init and receive remain untouched by dearging. - Switch the Rust counter extraction over to the version that's in ConCert examples since the old more ad-hoc extraction no longer works. In the future we may want to have the other versions of the counter in the ConCert framework as well so we can extract those. - Add extraction of the Escrow contract to Concordium. - Change the default attributes in Rust extraction as types should no longer require Copy. - Add concert-std and concert-std-derive Rust packages that provide supporter types for our extracted contracts and also automatic derivation for serialization/deserialization that works with references and recursive types. - Add notation <! foo %>, that from a glob-ref produces an approriate Coq type. For example, <! plus !> produces a kername for plus, <! nat !> produces an inductive and <! O !> produces an inductive * nat. - Add and fix various more remappings when extracting Concordium. - The ind_attrs are now properly applied to inductives instead of kernames. - ##name## was allowed in remapped constants, but not in remapped type aliases. Fix this. - Remove the extraction of cached cells for closures, since this was not fully implemented yet. We might want to implement this at some point to avoid excessive allocations of curried closures. | 07 April 2021, 10:24:51 UTC |
| 56e26d4 | Danil Annenkov | 29 March 2021, 15:19:17 UTC | Certifying passes (#86) * Certifying (proof-generation) expansion of match branches * Certifying inlining * Introduce the certifying pipeline: apply transforms at the template coq level and generate proofs after all template passes; * Integrated the pipeline into Liquidity and Elm extraction. Co-authored-by: Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com> | 29 March 2021, 15:19:17 UTC |
| e076443 | Milo | 29 March 2021, 09:04:24 UTC | ERC20 extraction to liquidity (#85) * add erc20 extract to liq, fix some bugs in liq pp * update coqproj * cleanup * remove unused import | 29 March 2021, 09:04:24 UTC |
| bd9f671 | Jakob Botsch Nielsen | 17 March 2021, 14:03:28 UTC | Update docker file for newest MetaCoq | 17 March 2021, 14:03:28 UTC |
| a5a4529 | Danil Annenkov | 17 March 2021, 13:52:55 UTC | Adapting ConCert to the newest MetaCoq (coq-8.11 branch) (#83) * Adapting ConCert to the newest MetaCoq https://github.com/MetaCoq/metacoq/commit/8d576c70957c0dce2053f2a7272b231f41c3d43f Changes: - some lemmas and definitions in PCUIC meta-theory, nothing seriously affecting our proofs. - primitive datatypes (int63, float) are supported by MetaCoq now. We don't handle them in our pretty-printers for now. * Update MetaCoq commit hash * Remove redundant line Co-authored-by: Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com> Co-authored-by: Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com> | 17 March 2021, 13:52:55 UTC |
| 3cb415a | Jakob Botsch Nielsen | 16 March 2021, 14:19:13 UTC | Only allow contracts access to their own balance (#82) Remove the account_balance function from Chain and add instead ctx_contract_balance to the ContractCallContext. This is is the only thing our contracts use and it means that we match the models of our target languages better. It also means we do not need Proper instances anymore for contracts. | 16 March 2021, 14:19:13 UTC |
| de54d9e | Jakob Botsch Nielsen | 15 March 2021, 13:01:54 UTC | Save field names of inductive ctors when extracting (#81) | 15 March 2021, 13:01:54 UTC |
| 1da1d02 | Danil Annenkov | 13 March 2021, 11:43:19 UTC | Elm web application (#80) * a web application consisting of a form for entering a user name and a password. Uses dependent types to encode the validity of the data stored in the application model. * Fix identifier names to avoid shadowing clashes in Elm * Fix deboxing of type aliases. * Rename Midlang extraction to Elm extraction Co-authored-by: Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com> | 13 March 2021, 11:43:19 UTC |
| eb260f8 | Bas Spitters | 11 March 2021, 15:49:02 UTC | Update README.md (#79) | 11 March 2021, 15:49:02 UTC |
| c44ce13 | Eske | 04 March 2021, 12:19:42 UTC | Update coq-stdpp | 08 March 2021, 11:19:02 UTC |
| bf2daa6 | Danil Annenkov | 01 March 2021, 14:20:31 UTC | Extraction: integration with the Concordium infrastructure WIP (#77) * Infrastructure for Concordium integration. * Add a mapping for customising the printing of enum attributes in Rust * Concordium extract module config * Add simple wrappers for Concordium Rust extraction. Extract simply-typed/refinement-typed counter contracts * Interpreter extraction WIP (+ extracted Rust code with manual instances/fixes). | 01 March 2021, 14:20:31 UTC |
| 75b0305 | Danil Annenkov | 20 February 2021, 09:59:09 UTC | Fix anchor | 20 February 2021, 09:59:09 UTC |
| c8639c1 | Danil Annenkov | 26 January 2021, 13:54:01 UTC | Update citations | 26 January 2021, 13:54:01 UTC |
| ea3611a | Bas Spitters | 26 January 2021, 13:38:24 UTC | Update README.md Adding CPP21 | 26 January 2021, 13:38:24 UTC |
| 97e88db | Danil | 11 December 2020, 15:01:15 UTC | Fixing the build process to generate extracted output | 11 December 2020, 15:01:15 UTC |
| 76611ce | Danil Annenkov | 11 December 2020, 13:11:56 UTC | Add extraction artifacts to the build | 11 December 2020, 13:11:56 UTC |
