-
Notifications
You must be signed in to change notification settings - Fork 14
/
Copy pathstats-master.md
38 lines (38 loc) · 5.83 KB
/
stats-master.md
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
| | Files | Folder | #LoC | Theorems | Implementations | Documentation | #Doc/#LoC (%) | Proved |
|----|-----------------------------|------------------------------|--------|------------|-------------------|-----------------|-----------------|----------|
| 0 | ActiveValidatorBounds.p.dfy | beacon | 52 | 3 | 0 | 29 | 56 | 3 |
| 1 | BeaconChainTypes.dfy | beacon | 54 | 0 | 0 | 171 | 317 | 0 |
| 2 | Helpers.dfy | beacon | 1003 | 9 | 89 | 670 | 67 | 98 |
| 3 | Helpers.p.dfy | beacon | 136 | 13 | 0 | 114 | 84 | 13 |
| 4 | Helpers.s.dfy | beacon | 136 | 9 | 6 | 67 | 49 | 15 |
| 5 | AttestationsTypes.dfy | beacon/attestations | 30 | 0 | 0 | 68 | 227 | 0 |
| 6 | ForkChoice.dfy | beacon/forkchoice | 229 | 3 | 15 | 172 | 75 | 18 |
| 7 | ForkChoiceTypes.dfy | beacon/forkchoice | 9 | 0 | 0 | 17 | 189 | 0 |
| 8 | Crypto.dfy | beacon/helpers | 7 | 0 | 1 | 3 | 43 | 1 |
| 9 | Math.dfy | beacon/helpers | 3 | 0 | 0 | 114 | 3800 | 0 |
| 10 | MathHelper.dfy | beacon/helpers/helper_lemmas | 3 | 0 | 0 | 413 | 13767 | 0 |
| 11 | EpochProcessing.dfy | beacon/statetransition | 384 | 0 | 14 | 127 | 33 | 14 |
| 12 | EpochProcessing.s.dfy | beacon/statetransition | 398 | 24 | 0 | 336 | 84 | 24 |
| 13 | ProcessOperations.dfy | beacon/statetransition | 361 | 0 | 11 | 119 | 33 | 11 |
| 14 | ProcessOperations.p.dfy | beacon/statetransition | 160 | 10 | 0 | 74 | 46 | 10 |
| 15 | ProcessOperations.s.dfy | beacon/statetransition | 410 | 12 | 6 | 137 | 33 | 18 |
| 16 | StateTransition.dfy | beacon/statetransition | 215 | 0 | 8 | 126 | 59 | 8 |
| 17 | StateTransition.s.dfy | beacon/statetransition | 213 | 11 | 1 | 100 | 47 | 12 |
| 18 | Validators.dfy | beacon/validators | 11 | 0 | 0 | 53 | 482 | 0 |
| 19 | Merkleise.dfy | merkle | 504 | 9 | 18 | 135 | 27 | 27 |
| 20 | BitListSeDes.dfy | ssz | 262 | 7 | 3 | 64 | 24 | 10 |
| 21 | BitVectorSeDes.dfy | ssz | 155 | 4 | 3 | 53 | 34 | 7 |
| 22 | BoolSeDes.dfy | ssz | 22 | 0 | 2 | 3 | 14 | 2 |
| 23 | BytesAndBits.dfy | ssz | 90 | 7 | 6 | 44 | 49 | 13 |
| 24 | Constants.dfy | ssz | 104 | 0 | 0 | 36 | 35 | 0 |
| 25 | IntSeDes.dfy | ssz | 130 | 2 | 2 | 20 | 15 | 4 |
| 26 | Serialise.dfy | ssz | 514 | 3 | 5 | 36 | 7 | 8 |
| 27 | DafTests.dfy | utils | 62 | 0 | 4 | 25 | 40 | 4 |
| 28 | Eth2Types.dfy | utils | 227 | 1 | 3 | 77 | 34 | 4 |
| 29 | Helpers.dfy | utils | 220 | 11 | 3 | 103 | 47 | 14 |
| 30 | MathHelpers.dfy | utils | 293 | 18 | 6 | 105 | 36 | 24 |
| 31 | NativeTypes.dfy | utils | 28 | 0 | 0 | 13 | 46 | 0 |
| 32 | NonNativeTypes.dfy | utils | 8 | 0 | 0 | 6 | 75 | 0 |
| 33 | SeqHelpers.dfy | utils | 69 | 8 | 2 | 58 | 84 | 10 |
| 34 | SetHelpers.dfy | utils | 74 | 6 | 0 | 50 | 68 | 6 |
| 35 | | TOTAL | 6576 | 170 | 208 | 3738 | 57 | 378 |