https://github.com/AU-COBRA/ConCert

sort by:
Revision Author Date Message Commit Date
3382e48 Dexter1 tests (#171) 24 May 2022, 20:50:09 UTC
9b13381 Refactor tests (#170) 23 May 2022, 22:18:43 UTC
a6da977 Rename Dexter contract (#169) 22 May 2022, 22:33:15 UTC
a136989 Fix Dexter tests (#168) 21 May 2022, 13:00:05 UTC
c298332 Add missing opam fields (#167) 17 May 2022, 18:41:51 UTC
2ddc4a3 Upgrade fa2 interface (#164) 17 May 2022, 09:45:18 UTC
0586e06 Make max action generation attempts configurable (#165) 11 May 2022, 12:39:26 UTC
3e2099f [CameLIGO] Remove init wrapper (#161) 06 May 2022, 12:47:43 UTC
151774c Time tests (#162) 06 May 2022, 12:45:05 UTC
8550e28 Add a variable shadowing test for CameLIGO (#159) 05 May 2022, 19:03:38 UTC
83cdd00 Pin concordium-std to version 2.0.0 (#160) 05 May 2022, 13:45:22 UTC
98a3d53 Fix cameligo contract wrapper (#158) 28 April 2022, 19:06:46 UTC
d069920 Update links (#155) 27 April 2022, 12:51:30 UTC
dfe6c4b Split example files (#154) 27 April 2022, 11:36:07 UTC
51b1ce7 Test framework improvements (#153) 27 April 2022, 09:19:25 UTC
ec565e0 Update README.md 16 April 2022, 17:10:30 UTC
d6a01aa Dexter2 set_delegate remap (#152) * Remove implicit serializable argument from FA2, FA1.2 and Dexter2 message definitions * Fix FA2 callback show instance * Rename init and receive in Dexter2 lqt and CPMM contracts as a workaround to coq extraction bug * Move null_address and set_delegate_call parameters to into module type * Remap set_delegate_call to Tezos operation in Dexter2 CPMM extraction * Remap key_hash type 07 April 2022, 18:53:34 UTC
4815305 CameLIGO extraction update (#151) fix printing recursive functions; fix params of polymorphic functions; fix tez subtraction; update ligo compiler; fix type annotations. 28 March 2022, 09:15:22 UTC
0399316 Add more general FA1.2 token implementation. (#148) 18 March 2022, 15:21:17 UTC
02d8473 Move examples (#147) 18 March 2022, 12:48:42 UTC
14579e0 Add inner and mutual fixpoint examples to Rust extraction (#145) 15 March 2022, 09:47:08 UTC
12fdfdf Clean up imports (#144) 08 March 2022, 13:52:38 UTC
77bdbed FA2 callback changes (#143) 28 February 2022, 11:27:27 UTC
a31b0f4 Split printing of serialized values (#142) 28 February 2022, 10:53:53 UTC
db1125b BAT contract (#141) 25 February 2022, 11:35:12 UTC
aebe2ac Build workflow improvements (#140) 25 February 2022, 10:33:42 UTC
356b40f Fix build process (#138) 15 February 2022, 09:30:21 UTC
20bf24a Update CameLIGOPretty.v (#137) (cherry picked from commit 8228ffd979588781fc86f7a393749f7d0e51ef4c) 09 February 2022, 06:25:03 UTC
84cbd69 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 Pin coq-stdpp to version 1.5.0 (#135) 02 February 2022, 14:11:36 UTC
c4afa74 Update ligo compiler to v0.34.0 (includes a bug fix) (#134) 02 February 2022, 13:03:43 UTC
5925263 Dexter 2: move files, readme, clean up printing (#133) 02 February 2022, 12:21:08 UTC
c87eeb3 Dexter2 safety proofs (#132) 01 February 2022, 08:27:10 UTC
a7983df Extract Dexter 2 Liquidity token (#130) 31 January 2022, 12:18:39 UTC
718bc53 Extraction of Dexter 2 CPMM (#129) 24 January 2022, 14:09:31 UTC
1f3ec76 Add permission control to CIS1; implement permission check in wccd (#128) 06 January 2022, 15:21:03 UTC
27bc4c7 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 Dexter2 implementation changes (#125) 21 December 2021, 15:19:43 UTC
9c7469d Fix typos in CIS1Spec (#126) 20 December 2021, 20:31:57 UTC
f76a8f8 Eip20 proofs (#124) * EIP20 changes * Make comments compatible with coqdoc in EIP20Token.v 20 December 2021, 20:31:22 UTC
cd3c65b Destruct chain step fix (#123) * Add origin to destuct_chain_step ltac 16 December 2021, 08:03:11 UTC
81eda74 Move coqdocjs and toc to separate dirs; add toc license; update readme 07 December 2021, 12:21:05 UTC
fa51dd0 CIS-1: Concordium Token Standard (#121) 07 December 2021, 10:12:19 UTC
4a5916f Fix typo in comment (#122) Fix a tiny typo in comments 04 December 2021, 11:37:25 UTC
523e743 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 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 Nitpicks on proof automation in Dexter2 23 September 2021, 09:23:44 UTC
a67bdf2 Dexter2 (#116) Add Dexter2 implementation 22 September 2021, 06:22:06 UTC
67e9f2c Uncomment extraction of the counter with subset types 02 September 2021, 20:48:16 UTC
1fce313 Update README: extend the project structure description 02 September 2021, 20:47:19 UTC
112c56d Update README; process extraction resutls by default 01 September 2021, 13:46:14 UTC
20b1878 CI: push only the extraction resutls from the master branch of the mainrepo 01 September 2021, 09:28:04 UTC
8b3608f CI: don't push the extraction results on pull requests. 31 August 2021, 13:00:28 UTC
1da9986 CI: uncomment pushing the extraction results 31 August 2021, 11:56:28 UTC
41c4970 Merge remote-tracking branch 'upstream/master' 31 August 2021, 10:32:21 UTC
3b276fd 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 Comment out push to the extraction repo for now 31 August 2021, 09:03:43 UTC
2846033 CI: add git username 31 August 2021, 07:25:07 UTC
351ca9e Remove feature(unsigned_abs) from Rust extraction prelude; uncomment the rest of the contract extraction examples 30 August 2021, 11:11:48 UTC
97624a1 Test rust extraction; fix gitignore 30 August 2021, 10:04:53 UTC
22b32d4 Add cargo to PATH in build.yml 25 August 2021, 12:26:16 UTC
63bfd88 CI: debug 25 August 2021, 10:56:38 UTC
fcc4ed3 CI: debug 24 August 2021, 13:57:34 UTC
196faea CI: remove sudo; debug 24 August 2021, 13:55:13 UTC
fe05553 CI: Try with sudo again 24 August 2021, 12:57:37 UTC
02d6508 CI: redirect liquidity stderr to a file; Docker: configure git to fetch through https 24 August 2021, 11:53:41 UTC
e60f39d Forgot to include build config :) 23 August 2021, 20:34:40 UTC
cb11643 CI: move testing back to the build step;comment out ERC20 extraction to Liquidity 23 August 2021, 19:57:00 UTC
6dc3d6d Debug CI 23 August 2021, 16:26:10 UTC
a5263c5 More opam-related fixes 23 August 2021, 14:57:21 UTC
ed669c9 Add setting opam env variables in the testing step of CI 23 August 2021, 14:17:49 UTC
2c911d8 Add some sudos to the build.yaml 23 August 2021, 13:27:15 UTC
1625478 Try fixing the build 23 August 2021, 11:30:12 UTC
d8cfcef Test extraction as a separate step after build 21 August 2021, 13:47:36 UTC
6e393ea Add views for the Elm web app 20 August 2021, 13:52:02 UTC
eb4c278 Add tests dir placeholder for elm extraction 20 August 2021, 13:09:38 UTC
1580353 Add src folder placeholder for elm 20 August 2021, 12:29:20 UTC
1d6d429 Fix a typo in build.yaml 20 August 2021, 11:43:10 UTC
5a85e5f add src for elm; fix build.yaml 20 August 2021, 11:16:35 UTC
f7fe8d1 Add more clean-up targets to Makefile; change build.yaml 20 August 2021, 10:17:22 UTC
b917451 Fix build.yaml 20 August 2021, 06:47:55 UTC
8e809b4 Forgot build.yaml 20 August 2021, 06:39:40 UTC
68fcd94 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 Add elm to Dockerfile; test extraction as a separate step 19 August 2021, 19:27:41 UTC
7ece1d1 Use a Docker image with compilers; compile extraction output on build 19 August 2021, 11:36:10 UTC
988b37a Uncomment redirecting the extracted Escrow code 14 August 2021, 20:11:49 UTC
dfaed8b 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 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 Add docker config with full concert 05 August 2021, 19:50:30 UTC
0b5ee96 Fix comments (#112) 05 August 2021, 19:48:46 UTC
5eb12f3 Fix cameligo extraction tests 31 July 2021, 13:34:38 UTC
b07f07f Fix path in a plugin example 30 July 2021, 14:55:39 UTC
b140f31 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 generalize type in pre-post-assertion 30 July 2021, 13:17:27 UTC
959540c 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 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 Add more safe_pred to Elm examples; update gitignore 27 July 2021, 13:34:53 UTC
78e0111 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 Update README.md 26 July 2021, 08:54:17 UTC
28f56a7 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
back to top