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

sort by:
Revision Author Date Message Commit Date
4b3148a Update README: paper citation formatting 23 August 2022, 18:34:33 UTC
6105ff2 Update papers: add JFP citation 23 August 2022, 18:33:20 UTC
059b29b Fix coqdoc 22 August 2022, 08:32:26 UTC
19a28ac Port ConCert to Coq 8.15 (#190) 22 August 2022, 07:20:03 UTC
e1b9eee Disable dependency graph in CI (#188) 19 August 2022, 10:38:42 UTC
901d670 Porting ConCert to Metacoq v1.0+8.14 (#187) 18 August 2022, 19:10:33 UTC
4723157 Ignore files not used in build process (#186) 01 July 2022, 10:46:10 UTC
5e889ff Add doc to opam file (#185) 30 June 2022, 10:02:29 UTC
cf11841 Build dependency graphs in CI (#184) 27 June 2022, 19:44:01 UTC
4b15196 Documentation improvements (#183) 26 June 2022, 20:27:39 UTC
eddf120 Fix documentation header (#182) 24 June 2022, 13:23:39 UTC
b7d9c17 Fix documentation TOC width (#181) 24 June 2022, 12:42:49 UTC
4de53ec Fix documentation toc (#180) 24 June 2022, 12:13:22 UTC
fdf99c3 Link external documentation (#179) 23 June 2022, 14:04:08 UTC
1ff2282 Dependency graphs (#178) 23 June 2022, 13:19:14 UTC
2f83546 Fix coqdocjs css (#177) 22 June 2022, 19:41:01 UTC
eade943 Exclude AllTests.v from documentation (#176) 22 June 2022, 17:42:38 UTC
2bd5c5f Fix broken links in documentation (#175) 22 June 2022, 17:34:03 UTC
217b35c Rust arith remapping (#173) 16 June 2022, 11:33:07 UTC
c7554a2 Extend CallFacts (#174) 15 June 2022, 11:27:45 UTC
25d6d8b Update README.md 01 June 2022, 07:52:07 UTC
99c1381 Dexter2 tests (#172) 25 May 2022, 13:28:15 UTC
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
back to top