issues
search
runtimeverification
/
polkadot-verification
Verification of Polkadot WASM code
Other
9
stars
6
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Source updates
#81
ehildenb
closed
4 years ago
1
Update dependency: deps/wasm-semantics
#80
rv-jenkins
closed
4 years ago
0
Use upstreamed coverage handling functionality
#79
ehildenb
closed
4 years ago
0
Update dependency: deps/wasm-semantics
#78
rv-jenkins
closed
4 years ago
0
Simple proofs about semantics
#77
ehildenb
closed
4 years ago
1
Update dependencies
#76
rv-jenkins
closed
4 years ago
0
Update dependencies
#75
rv-jenkins
closed
4 years ago
0
Update dependencies
#74
rv-jenkins
closed
4 years ago
0
Update dependencies
#73
rv-jenkins
closed
4 years ago
0
LICENSE: add license file
#72
ehildenb
closed
4 years ago
0
Update link of Polkadot Spec PDF
#71
lamafab
closed
4 years ago
0
Update dependencies
#70
rv-jenkins
closed
4 years ago
0
Correct functional attributes, default account creation
#69
ehildenb
closed
4 years ago
0
Harness for writing proofs about `set-balance`
#68
ehildenb
closed
4 years ago
0
Update dependencies
#67
rv-jenkins
closed
4 years ago
0
Updates and fixes to Rule Merging
#66
ehildenb
closed
4 years ago
1
Update dependencies
#65
rv-jenkins
closed
4 years ago
0
Implement EntryActions and public getters
#64
Demi-Marie
closed
4 years ago
0
Update dependencies
#63
rv-jenkins
closed
4 years ago
0
Write specs for public getters
#62
Demi-Marie
closed
4 years ago
0
Update dependencies
#61
rv-jenkins
closed
4 years ago
0
Implicitly initialize accounts when they are assigned non-zero balance but don't exist
#60
ehildenb
closed
4 years ago
1
Add log `<events>` to existing semantics
#59
ehildenb
opened
4 years ago
0
Add `<accountSet>` cell, and update appropriately when accounts are added/deleted.
#58
ehildenb
opened
4 years ago
0
Proof (Invariant): No zero-balance accounts
#57
ehildenb
opened
4 years ago
0
Proof (Invariant): EntryAction does not allow balances between `0` and `<existentialDeposit>`
#56
ehildenb
opened
4 years ago
0
Proof (Invariant): `<totalIssuance>` being the sum of balances in the state
#55
ehildenb
opened
4 years ago
1
Define which entrypoints are interesting for high-level properties/invariants
#54
ehildenb
closed
4 years ago
2
Update dependencies
#53
rv-jenkins
closed
4 years ago
0
Update dependencies
#52
rv-jenkins
closed
4 years ago
0
Bump Substrate dependency
#51
Demi-Marie
closed
4 years ago
0
Update dependencies
#50
rv-jenkins
closed
4 years ago
0
Update dependencies
#49
rv-jenkins
closed
4 years ago
0
Updates since previous master
#48
Demi-Marie
closed
4 years ago
1
Remove k term module
#47
ehildenb
closed
4 years ago
0
Set balance rules preparation
#46
cheme
closed
4 years ago
0
Rule merge silently failing
#45
ehildenb
closed
4 years ago
1
Generate coverage lists directly with Makefile
#44
ehildenb
closed
4 years ago
0
BUG: `domains.k` overlapping symbols
#43
ehildenb
closed
4 years ago
1
Project Roadmap
#42
ehildenb
opened
5 years ago
1
Update to use new auto-unparsers from pyk
#41
ehildenb
closed
5 years ago
0
Auto unparsing based on definition, limit coverage to semantic rules
#40
ehildenb
closed
5 years ago
3
Crashing on missing smtlib expression when merging rules
#39
ehildenb
closed
5 years ago
0
Rule merging is producing the incorrect result
#38
ehildenb
closed
5 years ago
1
Prove that the generated merged rules are all-path true
#37
ehildenb
closed
4 years ago
0
Always generate `allRules.txt` even without `--coverage`
#36
ehildenb
closed
5 years ago
3
Discussion about how rule merging should look
#35
ehildenb
closed
4 years ago
2
Make Haskell backend rule merger use rule IDs instead of labels
#34
ehildenb
closed
5 years ago
0
Draft new proposal with finer milestones from #20
#33
ehildenb
closed
5 years ago
1
Extract rule traces from simple test-suite
#32
ehildenb
closed
5 years ago
0
Previous
Next