Add another builtinByteStringToInteger property, fix incorrect proper…

…ty specification
cardano-foundation · Dec 8, 2023 · 04b001e · 04b001e
1 parent 7b0c9cf
commit 04b001e
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/CIP-XXXX/README.md b/CIP-XXXX/README.md
@@ -413,10 +413,13 @@ builtinByteStringToInteger True (consByteString 0x01 (consByteString 0x01
 ```
 
 We also describe properties that any `builtinByteStringToInteger` implementation 
-must have. Throughout, `i` is not negative, and `0 <= w8 <= 255`.
+must have. Throughout, `i` is not negative, `0 <= w8 <= 255`, and `bs` is not
+empty.
 
-1. `builtinByteStringToInteger b (builtinIntegerToByteString b k i) = i`
+1. `builtinByteStringToInteger b (builtinIntegerToByteString b 0 i) = i`
 2. `builtinByteStringToInteger b (consByteString w8 emptyByteString) = w8`
+3. `builtinIntegerToByteString b (lengthOfByteString bs) (builtinByteStringToInteger b bs) =
+   bs`
 
 ## Rationale: how does this CIP achieve its goals?