evm-types, Makefile: tangle filter for #Ceil(padToWidth) & related ru…

…les.
runtimeverification · Apr 18, 2020 · 005e91a · 005e91a
1 parent 9d41a6d
commit 005e91a
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/Makefile b/Makefile
@@ -183,10 +183,10 @@ web3_kore := $(web3_dir)/$(MAIN_DEFN_FILE)-kompiled/definition.kore
 
 # Tangle definition from *.md files
 
-concrete_tangle := .k:not(.node):not(.symbolic):not(.nobytes):not(.memmap),.standalone,.concrete,.bytes,.membytes
-java_tangle     := .k:not(.node):not(.concrete):not(.bytes):not(.memmap):not(.membytes),.standalone,.symbolic,.nobytes
-haskell_tangle  := .k:not(.node):not(.concrete):not(.nobytes):not(.memmap),.standalone,.symbolic,.bytes,.membytes
-node_tangle     := .k:not(.standalone):not(.symbolic):not(.nobytes):not(.memmap),.node,.concrete,.bytes,.membytes
+concrete_tangle := .k:not(.node):not(.symbolic):not(.nobytes):not(.memmap):not(.symbolic-bytes),.standalone,.concrete,.bytes,.membytes
+java_tangle     := .k:not(.node):not(.concrete):not(.bytes):not(.memmap):not(.membytes):not(.symbolic-bytes),.standalone,.symbolic,.nobytes
+haskell_tangle  := .k:not(.node):not(.concrete):not(.nobytes):not(.memmap),.standalone,.symbolic,.bytes,.membytes,.symbolic-bytes
+node_tangle     := .k:not(.standalone):not(.symbolic):not(.nobytes):not(.memmap):not(.symbolic-bytes),.node,.concrete,.bytes,.membytes
 
 defn: $(defn_files)
 llvm-defn:    $(llvm_files)

diff --git a/evm-types.md b/evm-types.md
@@ -425,7 +425,7 @@ A cons-list is used for the EVM wordstack.
 
 -   Definedness conditions for `WS [ N ]`, `WS [ N := W ]`, `BA [ N .. W ]`.
 
-```{.k .symbolic}
+```{.k .symbolic-bytes}
     rule #Ceil(WS[N])        => {((0 <=Int N) andBool (N <Int #sizeWordStack(WS)))            #Equals true}  [anywhere]
     rule #Ceil(WS[ N := W ]) => {((0 <=Int N) andBool (N <Int #sizeWordStack(WS)))            #Equals true}  [anywhere]
     rule #Ceil(BA[ N .. W ]) => {((0 <=Int N) andBool (0 <=Int W))                            #Equals true}  [anywhere]