| 93a7088 | Danil Annenkov | 03 May 2022, 08:57:42 UTC | Tweak doc style | 03 May 2022, 08:57:42 UTC |
| 3a614ed | Danil Annenkov | 02 May 2022, 13:24:24 UTC | Removed license | 02 May 2022, 13:24:24 UTC |
| ab1cc82 | Danil Annenkov | 02 May 2022, 12:39:00 UTC | Fix readme | 02 May 2022, 12:39:00 UTC |
| 00e4118 | Danil Annenkov | 02 May 2022, 12:25:54 UTC | Update README | 02 May 2022, 12:25:54 UTC |
| 9ff3f84 | Danil Annenkov | 02 May 2022, 12:12:36 UTC | Add extracted Dexter2 | 02 May 2022, 12:12:36 UTC |
| 3d66edb | Danil Annenkov | 02 May 2022, 12:01:04 UTC | Delete CI; update readme | 02 May 2022, 12:01:04 UTC |
| 1589175 | Danil Annenkov | 01 May 2022, 20:40:30 UTC | Remove docker files; remove project link | 01 May 2022, 20:40:30 UTC |
| b40ee52 | Danil Annenkov | 30 April 2022, 07:23:14 UTC | Simplify init printing | 30 April 2022, 07:23:14 UTC |
| 50fc1db | Danil Annenkov | 29 April 2022, 05:32:32 UTC | Merge branch 'ccs2022' of github.com:AU-COBRA/ConCert into ccs2022 | 29 April 2022, 05:32:32 UTC |
| 4abe10b | Danil Annenkov | 29 April 2022, 05:17:17 UTC | Remove initialisation wrapper in CameLIGO extraction | 29 April 2022, 05:17:17 UTC |
| e88ffe8 | 4ever2 | 28 April 2022, 21:26:05 UTC | Anonymise readme | 28 April 2022, 21:26:05 UTC |
| a4e63b4 | 4ever2 | 28 April 2022, 21:21:18 UTC | Anonymise readme | 28 April 2022, 21:21:18 UTC |
| 7a283dd | 4ever2 | 28 April 2022, 21:18:35 UTC | Anonymise opam file | 28 April 2022, 21:18:35 UTC |
| 79b1837 | 4ever2 | 28 April 2022, 18:26:44 UTC | Fix cameligo contract wrapper (#157) | 28 April 2022, 18:26:44 UTC |
| ad7ddff | Danil Annenkov | 28 April 2022, 11:40:50 UTC | Anonymise the READMEs | 28 April 2022, 11:40:50 UTC |
| 6da38e7 | Danil Annenkov | 28 April 2022, 09:35:37 UTC | remove papers | 28 April 2022, 09:35:37 UTC |
| f476ec4 | 4ever2 | 28 April 2022, 06:55:06 UTC | Backport Dexter2 (#156) * Backport Common.v * Backport Dexter2FA12.v * Backport FA2 changes * Backport Automation.v changes * Remove unused code * Backport Dexter2CPMM.v changes * Backport Dexter2Extract.v changes * Update CI workflow * Fix Dexter2 extraction output path | 28 April 2022, 06:55:06 UTC |
| 8228ffd | 4ever2 | 09 February 2022, 06:19:01 UTC | Update CameLIGOPretty.v (#137) | 09 February 2022, 06:19:01 UTC |
| 47472a6 | Danil Annenkov | 08 February 2022, 14:57:55 UTC | Update Dexter readme | 08 February 2022, 14:57:55 UTC |
| c0919a2 | Danil Annenkov | 08 February 2022, 13:31:50 UTC | Add Dexter 2 to the readme; Docker instructions | 08 February 2022, 13:31:50 UTC |
| 84cbd69 | Danil Annenkov | 08 February 2022, 12:17:32 UTC | Define liquidity token inteface; generalise the invariant proof to work for any contract satisfying the interface (#136) | 08 February 2022, 12:17:32 UTC |
| 0d9cae6 | 4ever2 | 02 February 2022, 14:11:36 UTC | Pin coq-stdpp to version 1.5.0 (#135) | 02 February 2022, 14:11:36 UTC |
| c4afa74 | Danil Annenkov | 02 February 2022, 13:03:43 UTC | Update ligo compiler to v0.34.0 (includes a bug fix) (#134) | 02 February 2022, 13:03:43 UTC |
| 5925263 | Danil Annenkov | 02 February 2022, 12:21:08 UTC | Dexter 2: move files, readme, clean up printing (#133) | 02 February 2022, 12:21:08 UTC |
| c87eeb3 | 4ever2 | 01 February 2022, 08:27:10 UTC | Dexter2 safety proofs (#132) | 01 February 2022, 08:27:10 UTC |
| a7983df | Danil Annenkov | 31 January 2022, 12:18:39 UTC | Extract Dexter 2 Liquidity token (#130) | 31 January 2022, 12:18:39 UTC |
| 718bc53 | Danil Annenkov | 24 January 2022, 14:09:31 UTC | Extraction of Dexter 2 CPMM (#129) | 24 January 2022, 14:09:31 UTC |
| 1f3ec76 | Danil Annenkov | 06 January 2022, 15:21:03 UTC | Add permission control to CIS1; implement permission check in wccd (#128) | 06 January 2022, 15:21:03 UTC |
| 27bc4c7 | Danil Annenkov | 06 January 2022, 11:07:55 UTC | Implementation of the Concordium's ccd wrapper token (cis1-wccd) and proofs of compliance with CIS1 (#127) | 06 January 2022, 11:07:55 UTC |
| d140acf | 4ever2 | 21 December 2021, 15:19:43 UTC | Dexter2 implementation changes (#125) | 21 December 2021, 15:19:43 UTC |
| 9c7469d | 4ever2 | 20 December 2021, 20:31:57 UTC | Fix typos in CIS1Spec (#126) | 20 December 2021, 20:31:57 UTC |
| f76a8f8 | 4ever2 | 20 December 2021, 20:31:22 UTC | Eip20 proofs (#124) * EIP20 changes * Make comments compatible with coqdoc in EIP20Token.v | 20 December 2021, 20:31:22 UTC |
| cd3c65b | 4ever2 | 16 December 2021, 08:03:11 UTC | Destruct chain step fix (#123) * Add origin to destuct_chain_step ltac | 16 December 2021, 08:03:11 UTC |
| 81eda74 | Danil Annenkov | 07 December 2021, 12:21:05 UTC | Move coqdocjs and toc to separate dirs; add toc license; update readme | 07 December 2021, 12:21:05 UTC |
| fa51dd0 | Danil Annenkov | 07 December 2021, 10:12:19 UTC | CIS-1: Concordium Token Standard (#121) | 07 December 2021, 10:12:19 UTC |
| 4a5916f | Julin S | 04 December 2021, 11:37:25 UTC | Fix typo in comment (#122) Fix a tiny typo in comments | 04 December 2021, 11:37:25 UTC |
| 523e743 | Danil Annenkov | 18 October 2021, 12:02:41 UTC | Cleaned up imports using coq-tools and some manual fixes (closes #102) (#120) Cleaned up imports using coq-tools and some manual fixes; fully qualified paths for imports (closes #102) | 18 October 2021, 12:02:41 UTC |
| d1544cc | Danil Annenkov | 12 October 2021, 09:49:00 UTC | Add call origin (#119) Add origin for calls: the call origin is available in `ContractCallContext` and also in `DeploymentInfo` and `ContractCallInfo` (closes #118) | 12 October 2021, 09:49:00 UTC |
| f579970 | Danil Annenkov | 23 September 2021, 09:23:44 UTC | Nitpicks on proof automation in Dexter2 | 23 September 2021, 09:23:44 UTC |
| a67bdf2 | 4ever2 | 22 September 2021, 06:22:06 UTC | Dexter2 (#116) Add Dexter2 implementation | 22 September 2021, 06:22:06 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 |
| 112c56d | Danil | 01 September 2021, 13:46:14 UTC | Update README; process extraction resutls by default | 01 September 2021, 13:46:14 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 |
| 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 |
| 988b37a | Danil | 14 August 2021, 20:11:49 UTC | Uncomment redirecting the extracted Escrow code | 14 August 2021, 20:11:49 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 |
| 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 |
| 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 |
