Cleanup and fixes. Addressing remaining TODOs (#45)

* fixed setHistoricalRootAccumulator * cleaned up comments * deteled 2 addressed todo-s * beacon-chain: fixed the implementation of setHistoricalRootAccumulator()
runtimeverification · Aug 17, 2019 · 019a9cd · 019a9cd
1 parent 48cf014
commit 019a9cd
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 35 deletions.
diff --git a/beacon-chain.k b/beacon-chain.k
@@ -954,7 +954,7 @@ def initialize_beacon_state_from_eth1(eth1_block_hash: Hash,
        ... </k>
        <genesis-time> _ => E1TS -Int E1TS %Int SECONDS_PER_DAY +Int 2 *Int SECONDS_PER_DAY </genesis-time>
        <eth1-data> _ => #Eth1Data("", len(Deposits), E1BH) </eth1-data>  // deposit root unspecified, hence the ""
-       <latest-block-header> // unspecified roots and hence all the ""
+       <latest-block-header>
               //BeaconBlockHeader(body_root=hash_tree_root(BeaconBlockBody()))
          _ => #BeaconBlockHeader(0, zerohashes(0), zerohashes(0), hash_tree_root_blockBodyEmpty(), defaultBytes96())
        </latest-block-header>
@@ -964,7 +964,7 @@ def initialize_beacon_state_from_eth1(eth1_block_hash: Hash,
   rule <k> (. => process_deposit(Dep))
            ~> processEth1Deposits(Dep Deposits => Deposits, Leaf Leaves => Leaves, INDEX => INDEX +Int 1)
        ... </k>
-       <eth1-data> // todo: does this precisely capture Python's '*leaves[:index + 1]'?
+       <eth1-data>
          E1Data => setDepositRoot(E1Data,
             //List[DepositData, 2**DEPOSIT_CONTRACT_TREE_DEPTH]
             hash_tree_root_list(slice(Leaves, 0, INDEX +Int 1), 2 ^Int DEPOSIT_CONTRACT_TREE_DEPTH, %container, false))
@@ -2064,7 +2064,7 @@ def process_final_updates(state: BeaconState) -> None:
            ~> setCommitteesRoot((get_current_epoch() +Int 1) %Int EPOCHS_PER_HISTORICAL_VECTOR) // param: committee_root_position
            ~> resetSlashings((get_current_epoch() +Int 1) %Int EPOCHS_PER_SLASHINGS_VECTOR)     // param: (slashings index)
            ~> setRandaoMix((get_current_epoch() +Int 1) %Int EPOCHS_PER_SLASHINGS_VECTOR)       // param: (rnd mixes index)
-           ~> setHistoricalRootAccumulator((get_current_epoch() +Int 1) %Int (SLOTS_PER_HISTORICAL_ROOT /Int SLOTS_PER_EPOCH) ==K 0)  // param: (condition)
+           ~> setHistoricalRootAccumulator()
            ~> rotateEpochAttestations() ... </k>
        <slot> SLOT </slot>
        <eth1-data-votes> E1DL => #if (SLOT +Int 1) %Int SLOTS_PER_ETH1_VOTING_PERIOD ==K 0
@@ -2131,17 +2131,22 @@ def process_final_updates(state: BeaconState) -> None:
                                    )
     </randao-mixes>
 
-  syntax KItem ::= "setHistoricalRootAccumulator" "(" Bool ")"
-  rule <k> setHistoricalRootAccumulator(Condition) => .K ... </k>
+/*    if next_epoch % (SLOTS_PER_HISTORICAL_ROOT // SLOTS_PER_EPOCH) == 0:
+        historical_batch = HistoricalBatch(block_roots=state.block_roots, state_roots=state.state_roots)
+        state.historical_roots.append(hash_tree_root(historical_batch))
+*/
+  syntax KItem ::= setHistoricalRootAccumulator()
+  rule <k> setHistoricalRootAccumulator() => .K ... </k>
     <historical-roots>
-      HL => #if Condition
-            #then HL // hash_tree_root(#HistoricalBatch({values(BRS)}:>BytesList, {values(SRS)}:>BytesList))
-            // todo: throws an exception: "Could not compute least upper bound for rewrite sort. Possible candidates: []"
-            #else HL
+      HL:BytesList
+         => #if (get_current_epoch() +Int 1) %Int (SLOTS_PER_HISTORICAL_ROOT /Int SLOTS_PER_EPOCH) ==Int 0
+              #then HL +BytesList hash_tree_root(#HistoricalBatch({mapToList(BlockRoots, 0, .BytesList)}:>BytesList,
+                                                                  {mapToList(StateRoots, 0, .BytesList)}:>BytesList ))
+              #else HL
             #fi
     </historical-roots>
-    <block-roots> BRS </block-roots>
-    <state-roots> SRS </state-roots>
+    <block-roots> BlockRoots </block-roots>
+    <state-roots> StateRoots </state-roots>
 
   syntax KItem ::= "rotateEpochAttestations" "(" ")"
   rule <k> rotateEpochAttestations() => .K ... </k>

diff --git a/config.k b/config.k
@@ -58,7 +58,6 @@ class BeaconBlockBody(Container):
     voluntary_exits: List[VoluntaryExit, MAX_VOLUNTARY_EXITS]
     transfers: List[Transfer, MAX_TRANSFERS]
 */
-    // TODO: Add appropriate constraints on lists below
   configuration
     <beacon-chain>
       <k> $PGM:Pgm </k>

diff --git a/hash-tree.k b/hash-tree.k
@@ -68,7 +68,6 @@ def pack(values: Series):
     elif isinstance(values, Bitvector):
         as_integer = sum([values[i] << i for i in range(len(values))])
         return as_integer.to_bytes((values.length + 7) // 8, "little")
-    //todo question asked about apaprently variable-len packing here
     elif isinstance(values, Bitlist):
         as_integer = sum([values[i] << i for i in range(len(values))])
         return as_integer.to_bytes((values.length + 7) // 8, "little")
@@ -80,7 +79,7 @@ def pack(values: Series):
   //Version for lists
   syntax Bytes ::= pack ( list: ValueList, staticLen: Int, elemType: ElementType )
 
-  //todo using StaticLEN here, python uses dynamic len. Static seems correct. Waiting answer on slack.
+  //Using StaticLEN here. Python code above also uses static length in "values.length".
   rule pack(BL:BitList, StaticLEN, %bool) => to_bytes( toInt(BL, (StaticLEN +Int 7) /Int 8 *Int 8),
                                                        (StaticLEN +Int 7) /Int 8 )
 
@@ -613,19 +612,6 @@ for layer in range(1, 100):
   // Utility functions
   //====================================================
 
-  syntax ValueList ::= mapToList ( map: Map, index: Int, emptyList: ValueList ) [function]
-
-  rule mapToList((INDEX |-> ELEM:ProposerSlashing) MAP, INDEX, EMPTY)
-       => ELEM {mapToList(MAP, INDEX +Int 1, EMPTY)}:>ProposerSlashingList
-  rule mapToList((INDEX |-> ELEM:Validator) MAP, INDEX, EMPTY)
-       => ELEM {mapToList(MAP, INDEX +Int 1, EMPTY)}:>ValidatorList
-  rule mapToList((INDEX |-> ELEM:Bytes) MAP, INDEX, EMPTY)
-       => ELEM {mapToList(MAP, INDEX +Int 1, EMPTY)}:>BytesList
-  rule mapToList((INDEX |-> ELEM:Int) MAP, INDEX, EMPTY)
-       => ELEM {mapToList(MAP, INDEX +Int 1, EMPTY)}:>IntList
-
-  rule mapToList(.Map, _, EMPTY) => EMPTY
-
   // If 2nd arg is false, return the list unchanged. Else remove last element.
   syntax BytesList ::= removeLast ( input: BytesList, removeLast: Bool ) [function]
   rule removeLast(LIST, false) => LIST

diff --git a/types.k b/types.k
@@ -311,7 +311,6 @@ class IndexedAttestation(Container):
     data: AttestationData
     signature: BLSSignature
   */
-  // TODO: Add constraint on length of ValidatorIndexList (MAX_VALIDATORS_PER_COMMITTEE)
   syntax IndexedAttestation ::= #IndexedAttestation( IntList, IntList, AttestationData, BLSSignature )
 
   syntax IntList ::= IndexedAttestation "." "custodyBit0Indices"      [function]
@@ -328,7 +327,6 @@ class PendingAttestation(Container):
     inclusion_delay: Slot
     proposer_index: ValidatorIndex
   */
-  // TODO: Add constraint on length of BitList (MAX_VALIDATORS_PER_COMMITTEE)
   syntax PendingAttestation ::= #PendingAttestation( BitList, AttestationData, Int, ValidatorIndex ) [klabel(#PendingAttestation), symbol]
 
   syntax BitList ::= PendingAttestation "." "aggregationBits"         [function]
@@ -360,7 +358,6 @@ class HistoricalBatch(Container):
     block_roots: Vector[Hash, SLOTS_PER_HISTORICAL_ROOT]
     state_roots: Vector[Hash, SLOTS_PER_HISTORICAL_ROOT]
   */
-  // TODO: Add constraint on length of BytesList (SLOTS_PER_HISTORICAL_ROOT)
   syntax HistoricalBatch ::= #HistoricalBatch( BytesList, BytesList )
 
   /*
@@ -384,8 +381,6 @@ class CompactCommittee(Container):
     pubkeys: List[Bytes48, MAX_VALIDATORS_PER_COMMITTEE]
     compact_validators: List[uint64, MAX_VALIDATORS_PER_COMMITTEE]
   */
-  // TODO: Add constraint on length of BytesList (MAX_VALIDATORS_PER_COMMITTEE)
-  // TODO: Add constraint on length of uint64List (MAX_VALIDATORS_PER_COMMITTEE)
   syntax CompactCommittee ::= #CompactCommittee( BytesList, IntList )
 
   syntax BytesList ::= CompactCommittee "." "pubkeys"                 [function]
@@ -435,7 +430,6 @@ class Attestation(Container):
     custody_bits: Bitlist[MAX_VALIDATORS_PER_COMMITTEE]
     signature: BLSSignature
   */
-  // TODO: Add constraint on lengths of both BitList lists (MAX_VALIDATORS_PER_COMMITTEE)
   syntax Attestation ::= #Attestation( BitList, AttestationData, BitList, BLSSignature )
 
   syntax BitList ::= Attestation "." "aggregation_bits"               [function]
@@ -449,7 +443,6 @@ class Deposit(Container):
     proof: Vector[Hash, DEPOSIT_CONTRACT_TREE_DEPTH + 1]  # Merkle path to deposit data list root
     data: DepositData
   */
-  // TODO: Add constraint on length of BytesList (DEPOSIT_CONTRACT_TREE_DEPTH + 1)
   syntax Deposit ::= #Deposit( BytesList, DepositData )
 
   syntax BytesList ::= Deposit "." "proof"                           [function]
@@ -576,7 +569,6 @@ def bytes_to_int(data: bytes) -> uint64:
   rule maxAux(I IL => IL, MAX => #if I <Int MAX #then MAX #else I #fi )
   rule maxAux(.IntList, MAX) => MAX
 
-  // TODO: optimize into a tail recursive version (?)
   syntax IntList ::= sortIntList(IntList) [function]
   rule sortIntList(.IntList) => .IntList
   rule sortIntList(I IL) => minIndex(IL,I) sortIntList(listExcept(I IL, minIndex(IL, I)))
@@ -625,6 +617,10 @@ def bytes_to_int(data: bytes) -> uint64:
   rule IL1 +IntList I IL2 => (IL1 I) +IntList IL2
   rule IL  +IntList .IntList => IL
 
+  //BytesList and Bytes concatenation. For some reason (parsing?) rule RHS cannot be used directly in other rules.
+  syntax BytesList ::= BytesList "+BytesList" Bytes                   [function]
+  rule BL1 +BytesList B => BL1 B
+
   //IntList merging (no duplicates)
   //Note: if the input lists duplicate-free, the resulting list will also be duplicate-free
   syntax IntList ::= IntList "++IntList" IntList     [function]
@@ -639,6 +635,7 @@ def bytes_to_int(data: bytes) -> uint64:
     requires I >Int 0
   rule B *Bytes 0 => ""
 
+  //Dynamic length of a ValueList.
   syntax Int ::= len( ValueList )                                     [function]
 
   rule len(_ LIST:IntList) => 1 +Int len(LIST)
@@ -671,6 +668,20 @@ def bytes_to_int(data: bytes) -> uint64:
   rule len(_ LIST:CompactCommitteeList) => 1 +Int len(LIST)
   rule len(.CompactCommitteeList) => 0
 
+  //Converts K-Map representation of a python List/Vector to a K-ValueList. Only implemented for used types.
+  syntax ValueList ::= mapToList ( map: Map, index: Int, emptyList: ValueList ) [function]
+
+  rule mapToList((INDEX |-> ELEM:ProposerSlashing) MAP, INDEX, EMPTY)
+       => ELEM {mapToList(MAP, INDEX +Int 1, EMPTY)}:>ProposerSlashingList
+  rule mapToList((INDEX |-> ELEM:Validator) MAP, INDEX, EMPTY)
+       => ELEM {mapToList(MAP, INDEX +Int 1, EMPTY)}:>ValidatorList
+  rule mapToList((INDEX |-> ELEM:Bytes) MAP, INDEX, EMPTY)
+       => ELEM {mapToList(MAP, INDEX +Int 1, EMPTY)}:>BytesList
+  rule mapToList((INDEX |-> ELEM:Int) MAP, INDEX, EMPTY)
+       => ELEM {mapToList(MAP, INDEX +Int 1, EMPTY)}:>IntList
+
+  rule mapToList(.Map, _, EMPTY) => EMPTY
+
   syntax BitList ::= shiftRight(BitList)                              [function]
   rule shiftRight(BL I) => false BL
   rule shiftRight(.BitList) => .BitList