- 11 Mar, 2019 2 commits
-
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
- 10 Mar, 2019 3 commits
-
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
* Pull the functionality we need into a Containers.v file that takes care of including the proper implementations of fmaps and fsets. Additionally, this file defines notation/new names. * Stop using map/set notation for operations. This conflicts with lists/record-set and is generally a head-ache. * Switch to lists instead of AVL trees for the sets and maps. This allows us to prove (assuming proof irrelevance) what we need: FSet.of_list (FSet.elements x) = x. Prove this and the equivalent for fin maps. * Do not use program instances in Oak.v. We can do with instances which generate a lot less bloat.
-
- 08 Mar, 2019 4 commits
-
-
Jakob Botsch Nielsen authored
These functions allow interacting with contracts in a strongly-typed manner without having to serialize/deserialize manually. Also adjust test to use these.
-
Jakob Botsch Nielsen authored
This adds a small example that uses a local blockchain to deploy a congress and do a transfer with it. Also fixes bugs to make this work.
-
Jakob Botsch Nielsen authored
Coq 8.7 does not support notation patterns.
-
Jakob Botsch Nielsen authored
This implements a depth first execution of chain actions with support for deploying contracts from contracts and calling into other contracts recursively. To support these things, contracts need to exhibit a bijection of their types from and to OakValue. This machinery is modeled with type classes. Then, use this to avoid having to store strongly typed contracts anywhere; instead, a contract can be converted to a WeakContract instance (using a coercion). The WeakContract verifies that messages and states serialize/deserialize correctly and then passes everything along to the strongly typed contract under the hood.
-
- 06 Mar, 2019 2 commits
-
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
- 05 Mar, 2019 1 commit
-
-
Jakob Botsch Nielsen authored
-
- 04 Mar, 2019 4 commits
-
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
Previously a contract could not store ChainAction's in its state because of universe inconsistencies.
-
Jakob Botsch Nielsen authored
-
- 02 Mar, 2019 1 commit
-
-
Jakob Botsch Nielsen authored
-
- 01 Mar, 2019 3 commits
-
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
- 28 Feb, 2019 3 commits
-
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
This reverts commit eda9cff7. Let's just give up on Coq 8.6.
-
- 27 Feb, 2019 7 commits
-
-
Jakob Botsch Nielsen authored
Containers needs to be updated for the dev build as Coq does not use Camlp5 anymore.
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
This allows heterogenous treament of Oak types and values.
-
- 25 Feb, 2019 1 commit
-
-
Jakob Botsch Nielsen authored
-
- 22 Feb, 2019 2 commits
-
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
* Add =? operator for addresses * Add rudimentary block chain info (block number, needed by Congress.v)
-
- 21 Feb, 2019 5 commits
-
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-
- 20 Feb, 2019 2 commits
-
-
Jakob Botsch Nielsen authored
-
Jakob Botsch Nielsen authored
-