Correct functional attributes, default account creation

runtimeverification / polkadot-verification

Verification of Polkadot WASM code

Other

9 stars 6 forks source link

Closed ehildenb closed 4 years ago

ehildenb commented 4 years ago

Fixes: #60

Adds account_exists and create_account primitives which other parts of the spec can use.

Also corrects some functional attribute rules to make sure they are total functions.