consistent naming specs

runtimeverification · Mar 20, 2020 · 8436bce · 8436bce
1 parent fc22f6b
commit 8436bce
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 10 deletions.
diff --git a/deposit/bytecode-verification/Makefile b/deposit/bytecode-verification/Makefile
@@ -17,10 +17,10 @@ SPEC_NAMES:=
 SPEC_NAMES += init-success
 SPEC_NAMES += init-revert
 
-SPEC_NAMES += get_deposit_root-success-loop1-then
-SPEC_NAMES += get_deposit_root-success-loop1-else
-SPEC_NAMES += get_deposit_root-success-loop-body-then
-SPEC_NAMES += get_deposit_root-success-loop-body-else
+SPEC_NAMES += get_deposit_root-success-init-then
+SPEC_NAMES += get_deposit_root-success-init-else
+SPEC_NAMES += get_deposit_root-success-loop-enter-then
+SPEC_NAMES += get_deposit_root-success-loop-enter-else
 SPEC_NAMES += get_deposit_root-success-loop-exit
 SPEC_NAMES += get_deposit_root-revert
 

diff --git a/deposit/bytecode-verification/deposit-spec.ini b/deposit/bytecode-verification/deposit-spec.ini
@@ -255,7 +255,7 @@ WORD_STACK_LOOP: {LOOP_BOUND} : {LOOP_INDEX_ADDR} : .WordStack
 LOOP_BOUND: 32
 LOOP_INDEX_ADDR: 416
 
-[get_deposit_root-success-loop1]
+[get_deposit_root-success-init]
 pc: 0 => {PC_LOOPHEAD}
 word_stack: .WordStack => 1 : {WORD_STACK_LOOP}
 local_mem: .Map => NEW_MEM
@@ -266,7 +266,7 @@ local_mem: .Map => NEW_MEM
     andBool #range(NEW_MEM, 384, 32) ==K #buf(32, DEPOSIT_COUNT /Int 2)
     andBool #range(NEW_MEM, 416, 32) ==K #buf(32, 1)
 
-[get_deposit_root-success-loop1-then]
+[get_deposit_root-success-init-then]
 NODE_1: #sha256(#buf(32, {BRANCH_0}) ++ #buf(32, 0))
 BRANCH_0: select(M, #hashedLocation({COMPILER}, {BRANCH}, 0))
 +requires:
@@ -275,7 +275,7 @@ BRANCH_0: select(M, #hashedLocation({COMPILER}, {BRANCH}, 0))
 GAS_COST: 1728
 MEM_COST: 672
 
-[get_deposit_root-success-loop1-else]
+[get_deposit_root-success-init-else]
 NODE_1: #sha256(#buf(32, 0) ++ #buf(32, {ZERO_HASHES_0}))
 ZERO_HASHES_0: select(M, #hashedLocation({COMPILER}, {ZERO_HASHES}, 0))
 +requires:
@@ -301,7 +301,7 @@ LOCAL_MEM_LOOPHEAD: MEM
     andBool #rangeUInt(256, HEIGHT)
 PRE_MEM_COST: 672
 
-[get_deposit_root-success-loop-body]
+[get_deposit_root-success-loop-enter]
 pc: {PC_LOOPHEAD}
 word_stack: (HEIGHT => HEIGHT +Int 1) : {WORD_STACK_LOOP}
 local_mem: {LOCAL_MEM_LOOPHEAD} => NEW_MEM
@@ -315,7 +315,7 @@ local_mem: {LOCAL_MEM_LOOPHEAD} => NEW_MEM
     // conditions
     andBool HEIGHT =/=Int 32
 
-[get_deposit_root-success-loop-body-then]
+[get_deposit_root-success-loop-enter-then]
 NODE_NEW: #sha256(#buf(32, {BRANCH_HEIGHT}) ++ #buf(32, NODE))
 BRANCH_HEIGHT: select(M, #hashedLocation({COMPILER}, {BRANCH}, HEIGHT))
 +requires:
@@ -324,7 +324,7 @@ BRANCH_HEIGHT: select(M, #hashedLocation({COMPILER}, {BRANCH}, HEIGHT))
 GAS_COST: 1350
 MEM_COST: 672
 
-[get_deposit_root-success-loop-body-else]
+[get_deposit_root-success-loop-enter-else]
 NODE_NEW: #sha256(#buf(32, NODE) ++ #buf(32, {ZERO_HASHES_HEIGHT}))
 ZERO_HASHES_HEIGHT: select(M, #hashedLocation({COMPILER}, {ZERO_HASHES}, HEIGHT))
 +requires: