From fd1ba19b27f2ffd0e94423319007acda972e522a Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Tue, 23 Apr 2024 10:04:09 +1200 Subject: [PATCH 01/32] Initial skeleton --- CIP-XXX/CIP-XXX.md | 73 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 73 insertions(+) create mode 100644 CIP-XXX/CIP-XXX.md diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md new file mode 100644 index 0000000000..5000de114a --- /dev/null +++ b/CIP-XXX/CIP-XXX.md @@ -0,0 +1,73 @@ +--- +CIP: ??? +Title: Logical operations +Category: Plutus +Status: Proposed +Authors: + - Koz Ross + - Sparsa Roychowdhury +Implementors: [] +Discussions: + - https://github.com/cardano-foundation/CIPs/pull/? +Created: YYYY-MM-DD +License: Apache-2.0 +--- + +## Abstract + +We describe the semantics of a set of logical operations for Plutus +`BuiltinByteString`s. Specifically, we provide descriptions for: + +- Bitwise logical AND, OR, XOR and complement; +- Reading a bit value at a given index; +- Setting a bit value at a given index. + +As part of this, we also describe the bit ordering within a `BuiltinByteString`, +and provide some laws these operations should obey. + +## Motivation: why is this CIP necessary? + +TODO: Add case for integer set + +TODO: Another 1-2 example uses + +## Specification + +We describe the proposed operations in several stages. First, we specify a +scheme for indexing individual bits (rather than whole bytes) in a +`BuiltinByteString`. We then specify the semantics of each operation, as well as +giving costing expectations. Lastly, we provide some laws that these operations +are supposed to obey, as well as giving some specific examples of results from +the use of these operations. + +### Bit indexing scheme + +TODO: Specify this + +### Operation semantics + +TODO: Specify + +### Laws and examples + +TODO: Make some + +## Rationale: how does this CIP achieve its goals? + +TODO: Explain goals relative examples, give descriptions of non-existent +alternatives + +## Path to Active + +### Acceptance Criteria + +TODO: Fill these in (lower priority) + +### Implementation Plan + +These operations will be implemented by MLabs, to be merged into Plutus Core +after review. + +## Copyright + +This CIP is licensed under [Apache-2.0](http://www.apache.org/licenses/LICENSE-2.0). From 27612a997132b2fd7536a9c5a0ff604230303a27 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Tue, 23 Apr 2024 11:16:36 +1200 Subject: [PATCH 02/32] Note replicate operation --- CIP-XXX/CIP-XXX.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 5000de114a..758b71fc98 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -20,7 +20,8 @@ We describe the semantics of a set of logical operations for Plutus - Bitwise logical AND, OR, XOR and complement; - Reading a bit value at a given index; -- Setting a bit value at a given index. +- Setting a bit value at a given index; and +- Replicating a byte a given number of times. As part of this, we also describe the bit ordering within a `BuiltinByteString`, and provide some laws these operations should obey. From e3db45289c43b7c46d5abdaa7846bbc4c85f9ed2 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Tue, 30 Apr 2024 10:15:16 +1200 Subject: [PATCH 03/32] Start on semantics --- CIP-XXX/CIP-XXX.md | 157 +++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 150 insertions(+), 7 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 758b71fc98..7becee8716 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -3,13 +3,13 @@ CIP: ??? Title: Logical operations Category: Plutus Status: Proposed -Authors: +Authors: + - Koz Ross +Implementors: - Koz Ross - - Sparsa Roychowdhury -Implementors: [] Discussions: - https://github.com/cardano-foundation/CIPs/pull/? -Created: YYYY-MM-DD +Created: 2024-04-30 License: Apache-2.0 --- @@ -20,7 +20,7 @@ We describe the semantics of a set of logical operations for Plutus - Bitwise logical AND, OR, XOR and complement; - Reading a bit value at a given index; -- Setting a bit value at a given index; and +- Setting bits value at given indices; and - Replicating a byte a given number of times. As part of this, we also describe the bit ordering within a `BuiltinByteString`, @@ -43,11 +43,154 @@ the use of these operations. ### Bit indexing scheme -TODO: Specify this +TODO: Specify ### Operation semantics -TODO: Specify +We describe precisely the operations we intend to implement, and their +semantics. These operations will have the following signatures: + +* `builtinLogicalAnd :: BuiltinBool -> BuiltinByteString -> BuiltinByteString -> + BuiltinByteString` +* `builtinLogicalOr :: BuiltinBool -> BuiltinByteString -> BuiltinByteString -> + BuiltinByteString` +* `builtinLogicalXor :: BuiltinBool -> BuiltinByteString -> BuiltinByteString -> + BuiltinByteString` +* `builtinLogicalComplement :: BuiltinByteString -> BuiltinByteString` +* `builtinReadBit :: BuiltinByteString -> BuiltinInteger -> BuiltinBool` +* `builtinSetBits :: BuiltinByteString -> [(BuiltinInteger, BuiltinBool)] -> + BuiltinByteString` +* `builtinReplicate :: BuiltinInteger -> BuiltinInteger -> BuiltinByteString` + +#### Padding versus truncation semantics + +For the binary logical operations (that is, `builtinLogicalAnd`, +`builtinLogicalOr` and `builtinLogicalXor`), the we have two choices of +semantics when handling `BuiltinByteString` arguments of different lengths. We +can either produce a result whose length is the _minimum_ of the two arguments +(which we call _truncation semantics_), or produce a result whose length is the +_maximum_ of the two arguments (which we call _padding semantics_). As these can +both be useful depending on context, we allow both, controlled by a +`BuiltinBool` flag, on all the operations listed above. + +TODO: Example + +#### `builtinLogicalAnd` + +`builtinLogicalAnd` takes three arguments; we name and describe them below. + +1. Whether padding semantics should be used. If this argument is `False`, + truncation semantics are used instead. This is the _padding semantics + argument_, and has type `BuiltinBool`. +2. The first input `BuiltinByteString`. This is the _first data argument_. +3. The second input `BuiltinByteString`. This is the _second data argument_. + +Let $b_1, b_2$ refer to the first data argument and the second data +argument respectively, and let $n_1, n_2$ be their respective lengths in bytes. +Let the result of `builtinLogicalAnd`, given $b_1, b_2$ and some padding +semantics argument, be $b_r$, of length $n_r$ in bytes. We use $b_1[i]$ to refer +to the $i$th bit of $b_1$ (and analogously for +$b_2, b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) +for the exact specification of this. + +If the padding semantics argument is `True`, then we have $n_r = \max \{ n_1, +n_2 \}$; otherwise, $n_r = \min \{ n_1, n_2 \}$. For all $i \in 0, 1, \ldots 8 +\cdot n_r - 1$, we have + +$$ +b_r[i] = \begin{cases} + b_0[i] & n_1 < n_0 \text{ and } n_r > \min { n_1, n_2 } \\ + b_1[i] & n_0 < n_1 \text { and } n_r > \min { n_1, n_2 } \\ + 1 & b_0[i] = b_1[i] = 1 \\ + 0 & \text{otherwise} \\ + \end{cases} +$$ + +#### `builtinLogicalOr` + +`builtinLogicalOr` takes three arguments; we name and describe them below. + +1. Whether padding semantics should be used. If this argument is `False`, + truncation semantics are used instead. This is the _padding semantics + argument_, and has type `BuiltinBool`. +2. The first input `BuiltinByteString`. This is the _first data argument_. +3. The second input `BuiltinByteString`. This is the _second data argument_. + +Let $b_1, b_2$ refer to the first data argument and the second data +argument respectively, and let $n_1, n_2$ be their respective lengths in bytes. +Let the result of `builtinLogicalOr`, given $b_1, b_2$ and some padding +semantics argument, be $b_r$, of length $n_r$ in bytes. We use $b_1[i]$ to refer +to the $i$th bit of $b_1$ (and analogously for +$b_2, b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) +for the exact specification of this. + +If the padding semantics argument is `True`, then we have $n_r = \max \{ n_1, +n_2 \}$; otherwise, $n_r = \min \{ n_1, n_2 \}$. For all $i \in 0, 1, \ldots 8 +\cdot n_r - 1$, we have + +$$ +b_r[i] = \begin{cases} + b_0[i] & n_1 < n_0 \text{ and } n_r > \min { n_1, n_2 } \\ + b_1[i] & n_0 < n_1 \text { and } n_r > \min { n_1, n_2 } \\ + 0 & b_0[i] = b_1[i] = 0 \\ + 1 & \text{otherwise} \\ + \end{cases} +$$ + +#### `builtinLogicalXor` + +`builtinLogicalXor` takes three arguments; we name and describe them below. + +1. Whether padding semantics should be used. If this argument is `False`, + truncation semantics are used instead. This is the _padding semantics + argument_, and has type `BuiltinBool`. +2. The first input `BuiltinByteString`. This is the _first data argument_. +3. The second input `BuiltinByteString`. This is the _second data argument_. + +Let $b_1, b_2$ refer to the first data argument and the second data +argument respectively, and let $n_1, n_2$ be their respective lengths in bytes. +Let the result of `builtinLogicalXor`, given $b_1, b_2$ and some padding +semantics argument, be $b_r$, of length $n_r$ in bytes. We use $b_1[i]$ to +refer to the $i$th bit of $b_1$ (and analogously for +$b_2, b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) +for the exact specification of this. + +If the padding semantics argument is `True`, then we have $n_r = \max \{ n_1, +n_2 \}$; otherwise, $n_r = \min \{ n_1, n_2 \}$. For all $i \in 0, 1, \ldots 8 +\cdot n_r - 1$, we have + +$$ +b_r[i] = \begin{cases} + b_0[i] & n_1 < n_0 \text{ and } n_r > \min { n_1, n_2 } \\ + b_1[i] & n_0 < n_1 \text { and } n_r > \min { n_1, n_2 } \\ + 0 & b_0[i] = b_1[i] \\ + 1 & \text{otherwise} \\ + \end{cases} +$$ + +#### `builtinLogicalComplement` + +`builtinLogicalComplement` takes a single argument, of type `BuiltinByteString`; +let $b$ refer to that argument, and $n$ its length in bytes. Let $b_r$ be +the result of `builtinLogicalComplement`; its length in bytes is also $n$. We +use $b[i]$ to refer to the $i$th bit of $b$ (and analogously for $b_r$); see the +[section on the bit indexing scheme](#bit-indexing-scheme) for the exact +specification of this. + +For all $i \in 0, 1, \ldots , 8 \cdot n - 1$, we have + +$$ +b_r[i] = \begin{cases} + 0 & b[i] = 1\\ + 1 & \text{otherwise}\\ + \end{cases} +$$ + +#### `builtinReadBit` + +#### `builtinSetBits` + +#### `builtinReplicate` ### Laws and examples From a03b963753f13c8bb4bd9b2d03329be232588f59 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Tue, 30 Apr 2024 12:08:53 +1200 Subject: [PATCH 04/32] Finish semantics --- CIP-XXX/CIP-XXX.md | 115 ++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 108 insertions(+), 7 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 7becee8716..0424aba7a4 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -99,9 +99,9 @@ n_2 \}$; otherwise, $n_r = \min \{ n_1, n_2 \}$. For all $i \in 0, 1, \ldots 8 $$ b_r[i] = \begin{cases} - b_0[i] & n_1 < n_0 \text{ and } n_r > \min { n_1, n_2 } \\ - b_1[i] & n_0 < n_1 \text { and } n_r > \min { n_1, n_2 } \\ - 1 & b_0[i] = b_1[i] = 1 \\ + b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ + b_1[i] & \text{if } n_0 < n_1 \text { and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ + 1 & \text{if } b_0[i] = b_1[i] = 1 \\ 0 & \text{otherwise} \\ \end{cases} $$ @@ -130,8 +130,8 @@ n_2 \}$; otherwise, $n_r = \min \{ n_1, n_2 \}$. For all $i \in 0, 1, \ldots 8 $$ b_r[i] = \begin{cases} - b_0[i] & n_1 < n_0 \text{ and } n_r > \min { n_1, n_2 } \\ - b_1[i] & n_0 < n_1 \text { and } n_r > \min { n_1, n_2 } \\ + b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ + b_1[i] & n_0 < n_1 \text { and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ 0 & b_0[i] = b_1[i] = 0 \\ 1 & \text{otherwise} \\ \end{cases} @@ -161,8 +161,8 @@ n_2 \}$; otherwise, $n_r = \min \{ n_1, n_2 \}$. For all $i \in 0, 1, \ldots 8 $$ b_r[i] = \begin{cases} - b_0[i] & n_1 < n_0 \text{ and } n_r > \min { n_1, n_2 } \\ - b_1[i] & n_0 < n_1 \text { and } n_r > \min { n_1, n_2 } \\ + b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ + b_1[i] & \text{if } n_0 < n_1 \text { and } i \geq 8 \cdot \min { n_1, n_2 } \\ 0 & b_0[i] = b_1[i] \\ 1 & \text{otherwise} \\ \end{cases} @@ -188,10 +188,111 @@ $$ #### `builtinReadBit` +`builtinReadBit` takes two arguments; we name and describe them below. + +1. The `BuiltinByteString` in which the bit we want to read can be found. This + is the _data argument_. +2. A bit index into the data argument, of type `BuiltinInteger`. This is the + _index argument_. + +Let $b$ refer to the data argument, of length $n$ in bytes, and let $i$ refer to +the index argument. We use $b[i]$ to refer to the $i$th bit of $b$; see the +[section on the bit indexing scheme](#bit-indexing-scheme) for the exact +specification of this. + +If $i < 0$ or $i \geq 8 \cdot n$, then `builtinReadBit` +fails. In this case, the resulting error message must specify _at least_ the +following information: + +* That `builtinReadBit` failed due to an out-of-bounds index argument; and +* What `BuiltinInteger` was passed as an index argument. + +Otherwise, if $b[i] = 0$, `builtinReadBit` returns `False`, and if $b[i] = 1$, +`builtinReadBit` returns `True`. + #### `builtinSetBits` +`builtinSetBits` takes two arguments: we name and describe them below. + +1. The `BuiltinByteString` in which we want to change some bits. This is the + _data argument_. +2. A list of index-value pairs, indicating which positions in the data argument + should be changed to which value. This is the _change list argument_. Each + index has type `BuiltinInteger`, while each value has type `BuiltinBool`. + +Let $C = (i_1, v_1), (i_2, v_2), \ldots , (i_k, v_k)$ refer to the change list +argument, and $b$ the data argument of length $n$ in bytes. Let $b_r$ be the +result of `builtinSetBits`, whose length is also $n$. We use $b[i]$ to refer to +the $i$th bit of $b$ (and analogously, $b_r$); see the [section on the bit +indexing scheme](#bit-indexing-scheme) for the exact specification of this. + +If the change list argument is empty, the result is $b$. If the change list +argument is a singleton, let $(i, v)$ refer to its only index-value pair. If $i +< 0$ or i \geq 8 \cdot n$, then `builtinSetBits` fails. In this case, the +resulting error message must specify _at least_ the following information: + +* That `builtinSetBits` failed due to an out-of-bounds index argument; and +* What `BuiltinInteger` was passed as the index part of the index-value pair. + +Otherwise, for all $j \in 0, 1, \ldots 8 \cdot n - 1$, we have + +$$ +b_r[j] = \begin{cases} + 0 & \text{if } j = i \text{ and } b = \texttt{False}// + 1 & \text{if } j = i \text{ and } b = \texttt{True}// + b[j] & \text{otherwise}// + \end{cases} +$$ + +if the change list argument is longer than a singleton, suppose that we can +process a change list argument of length $1 \leq m$, and let $b_m$ be the result +of such processing. There are two possible outcomes for $b_m$: + +1. An error. In this case, we define the result of `builtinSetBits` on such a + change list as that error. +2. A `BuiltinByteString`. + +From here, when we refer to $b_m$, we refer to the `BuiltinByteString` option. + +We observe that any change list $C^{\prime}$ of length $m + +1$ will have the form of some other change list $C_m$, with an additional +element $(i_{m + 1}, v_{m + 1})$ at the end. We define the result of +`builtinSetBits` with data argument $b$ and change list argument $C^{\prime}$ +as the result of `builtinSetBits` with data argument $b_m$ and the change list +argument $(i_{m + 1}, v_{m + 1})$; as this change list is a singleton, we can +process it according to the description above. + #### `builtinReplicate` +`builtinReplicate` takes two arguments; we name and describe them below. + +1. The desired result length, of type `BuiltinInteger`. This is the _length + argument_. +2. The byte to place at each position in the result, represented as a + `BuiltinInteger` (corresponding to the unsigned integer this byte encodes). + This is the _byte argument_. + +Let $n$ be the length argument, and $w$ the byte argument. If $n < 0$, then +`builtinReplicate` fails. In this case, the resulting error message must specify +_at least_ the following information: + +* That `builtinReplicate` failed due to a negative length argument; and +* What `BuiltinInteger` was passed as the length argument. + +If $n \geq 0$, and $w < 0$ or $w > 255$, then `builtinReplicate` fails. In this +case, the resulting error message must specify _at least_ the following +information: + +* That `builtinReplicate` failed due to the byte argument not being a valid + byte; and +* What `BuiltinInteger` was passed as the byte argument. + +Otherwise, let $b$ be the result of `builtinReplicate`, and let $b[i]$ be the +byte at position $i$ of $b$, as per `builtinIndexByteString`. We have: + +* The length (in bytes) of $b$ is $n$; and +* For all $i \in 0, 1, \ldots, n - 1$, $b[i] = w$. + ### Laws and examples TODO: Make some From 4ece4151ae20dbc90b401d8d1facef4f2c84a1a4 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Tue, 30 Apr 2024 14:20:45 +1200 Subject: [PATCH 05/32] Finish laws --- CIP-XXX/CIP-XXX.md | 211 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 209 insertions(+), 2 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 0424aba7a4..4b83c92de4 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -73,7 +73,11 @@ _maximum_ of the two arguments (which we call _padding semantics_). As these can both be useful depending on context, we allow both, controlled by a `BuiltinBool` flag, on all the operations listed above. -TODO: Example +For example, consider the `BuiltinByteString`s `x = [0x00, 0xF0, 0xFF]` and `y = +[0xFF, 0xF0]`. Under padding semantics, the result of `builtinLogicalAnd`, +`builtinLogicalOr` or `builtinLogicalXor` using these two as arguments would +have a length of 3; under truncation semantics, the result would have a length +of 2 instead. #### `builtinLogicalAnd` @@ -295,7 +299,200 @@ byte at position $i$ of $b$, as per `builtinIndexByteString`. We have: ### Laws and examples -TODO: Make some +#### Binary operations + +We describe laws for all three operations that work over two +`BuiltinByteStrings`, that is, `builtinLogicalAnd`, `builtinLogicalOr` and +`builtinLogicalXor`, together, as many of them are similar (and related). We +describe padding semantics and truncation semantics laws, as they are slightly +different. + +All three operations above, under both padding and truncation semantics, are +[commutative semigroups][special-semigroups]. Thus, we have: + +```haskell +builtinLogicalAnd s x y = builtinLogicalAnd s y x + +builtinLogicalAnd s x (builtinLogicalAnd s y z) = builtinLogicalAnd s +(builtinLogicalAnd s x y) z + +-- and the same for builtinLogicalOr and builtinLogicalXor +``` + +Note that the semantics (designated as `s` above) must be consistent in order +for these laws to hold. Furthermore, under padding semantics, all the above +operations are [commutative monoids][commutative-monoid]: + +```haskell +builtinLogicalAnd True x "" = builtinLogicalAnd True "" x = x + +-- and the same for builtinLogicalOr and builtinLogicalXor +``` + +Under truncation semantics, `""` (that is, the empty `BuiltinByteString`) acts +instead as an [absorbing element][absorbing-element]: + +```haskell +builtinLogicalAnd False x "" = builtinLogicalAnd False "" x = "" + +-- and the same for builtinLogicalOr and builtinLogicalXor +``` + +`builtinLogicalAnd` and `builtinLogicalOr` are also [semilattices][semilattice], +due to their idempotence: + +```haskell +builtinLogicalAnd s x x = x + +-- and the same for builtinLogicalOr +``` + +`builtinLogicalXor` is instead involute: + +```haskell +builtinLogicalXor s x (builtinLogicalXor s x x) = builtinLogicalXor s +(builtinLogicalXor s x x) x = x +``` + +Additionally, under padding semantics, `builtinLogicalAnd` and +`builtinLogicalOr` are [self-distributive][distributive]: + +```haskell +builtinLogicalAnd True x (builtinLogicalAnd True y z) = builtinLogicalAnd True +(builtinLogicalAnd True x y) (builtinLogicalAnd True x z) + +builtinLogicalAnd True (builtinLogicalAnd True x y) z = builtinLogicalAnd True +(builtinLogicalAnd True x z) (builtinLogicalAnd True y z) + +-- and the same for builtinLogicalOr +``` + +Under truncation semantics, `builtinLogicalAnd` is only left-distributive over +itself, `builtinLogicalOr` and `builtinLogicalXor`: + +```haskell +builtinLogicalAnd False x (builtinLogicalAnd False y z) = builtinLogicalAnd +False (builtinLogicalAnd False x y) (builtinLogicalAnd False x z) + +builtinLogicalAnd False x (builtinLogicalOr False y z) = builtinLogicalOr False +(builtinLogicalAnd False x y) (builtinLogicalAnd False x z) + +builtinLogicalAnd False x (builtinLogicalXor False y z) = builtinLogicalXor +False (builtinLogicalAnd False x y) (builtinLogicalAnd False x z) +``` + +`builtinLogicalOr` under truncation semantics is left-distributive over itself +and `bitwiseLogicalAnd`: + +```haskell +builtinLogicalOr False x (builtinLogicalOr False y z) = builtinLogicalOr False +(builtinLogicalOr False x y) (builtinLogicalOr False x z) + +builtinLogicalOr False x (builtinLogicalAnd False y z) = builtinLogicalAnd False +(builtinLogicalOr False x y) (builtinLogicalOr False x z) +``` + +If the first and second data arguments to these operations have the same length, +these operations satisfy several additional laws. We describe these briefly +below, with the added note that, in this case, padding and truncation semantics +coincide: + +* `builtinLogicalAnd` and `builtinLogicalOr` form a [bounded lattice][lattice] +* `builtinLogicalAnd` is [distributive][distributive] over itself, `builtinLogicalOr` and + `builtinLogicalXor` +* `builtinLogicalOr` is [distributive][distributive] over itself and `builtinLogicalAnd` + +We do not specify these laws here, as they do not hold in general. At the same +time, we expect that any implementation of these operations will be subject to +these laws. + +#### `builtinLogicalComplement` + +The main law of `builtinLogicalComplement` is involution: + +```haskell +builtinLogicalComplement (builtinLogicalComplement x) = x +``` + +In combination with `builtinLogicalAnd` and `builtinLogicalOr`, +`builtinLogicalComplement` gives rise to the famous [De Morgan laws][de-morgan], irrespective of semantics: + +```haskell +builtinLogicalComplement (builtinLogicalAnd s x y) = builtinLogicalOr s +(builtinLogicalComplement x) (builtinLogicalComplement y) + +builtinLogicalComplement (builtinLogicalOr s x y) = builtinLogicalAnd s +(builtinLogicalComplement x) (builtinLogicalComplement y) +``` + +For `builtinLogicalXor`, we instead have (again, irrespective of semantics): + +```haskell +builtinLogicalXor s x (builtinLogicalComplement x) = x +``` + +#### Bit reading and modification + +Throughout, we assume any index arguments to be 'in-bounds'; that is, all the +index arguments used in the statements of any law are such that the operation +they are applied to wouldn't produce an error. + +The first law of `builtinSetBits` is similar to the [set-twice law of +lenses][lens-laws]: + +```haskell +builtinSetBits bs [(i, b1), (i, b2)] = builtinSetBits bs [(i, b2)] +``` + +Together with `builtinReadBit`, we obtain the remaining two analogues to the lens +laws: + +```haskell +-- writing to an index, then reading from that index, gets you what you wrote +builtinReadBit (builtinSetBits bs [(i, b)]) i = b + +-- if you read from an index, then write that value to that same index, nothing +-- happens +builtinSetBits bs [(i, builtinReadBit bs i)] = bs +``` + +Furthermore, given a fixed data argument, `builtinSetBits` acts as a [monoid +homomorphism][monoid-homomorphism] from functions to lists under concatenation: + +```haskell +-- identity function corresponds to empty list +builtinSetBits bs [] = bs + +-- composition is concatenation of change list arguments +builtinSetBits (builtinSetBits bs is) js = builtinSetBits bs (is <> js) +``` + +#### `builtinReplicate` + +Given a fixed byte argument, `builtinReplicate` acts as a [monoid +homomorphism][monoid-homomorphism] from natural numbers under addition to +`BuiltinByteString`s under concatenation: + +```haskell +builtinReplicate 0 w = "" + +builtinReplicate (n + m) w = builtinReplicate n w <> builtinReplicate m w +``` + +Additionally, for any 'in-bounds' index (that is, any index for which +`builtinIndexByteString` won't error) `i`, we have + +```haskell +builtinIndexByteString (builtinReplicate n w) i = w +``` + +Lastly, we have + +```haskell +builtinSizeOfByteString (builtinReplicate n w) = n +``` + +TODO: Examples ## Rationale: how does this CIP achieve its goals? @@ -316,3 +513,13 @@ after review. ## Copyright This CIP is licensed under [Apache-2.0](http://www.apache.org/licenses/LICENSE-2.0). + +[special-semigroups]: https://en.wikipedia.org/wiki/Special_classes_of_semigroups +[commutative-monoid]: https://en.wikipedia.org/wiki/Monoid#Commutative_monoid +[absorbing-element]: https://en.wikipedia.org/wiki/Zero_element#Absorbing_elements +[semilattice]: https://en.wikipedia.org/wiki/Semilattice +[distributive]: https://en.wikipedia.org/wiki/Distributive_property +[lattice]: https://en.wikipedia.org/wiki/Lattice_(order) +[de-morgan]: https://en.wikipedia.org/wiki/De_Morgan%27s_laws +[lens-laws]: https://oleg.fi/gists/posts/2017-04-18-glassery.html#laws:lens +[monoid-homomorphism]: https://en.wikipedia.org/wiki/Monoid#Monoid_homomorphisms From 93f648a1636fad75b41a8bfb297d6d4f8a8ae9c2 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Tue, 30 Apr 2024 14:23:03 +1200 Subject: [PATCH 06/32] Typoes --- CIP-XXX/CIP-XXX.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 4b83c92de4..15d06db437 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -135,8 +135,8 @@ n_2 \}$; otherwise, $n_r = \min \{ n_1, n_2 \}$. For all $i \in 0, 1, \ldots 8 $$ b_r[i] = \begin{cases} b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ - b_1[i] & n_0 < n_1 \text { and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ - 0 & b_0[i] = b_1[i] = 0 \\ + b_1[i] & \text{if } n_0 < n_1 \text { and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ + 0 & \text{if } b_0[i] = b_1[i] = 0 \\ 1 & \text{otherwise} \\ \end{cases} $$ @@ -167,7 +167,7 @@ $$ b_r[i] = \begin{cases} b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ b_1[i] & \text{if } n_0 < n_1 \text { and } i \geq 8 \cdot \min { n_1, n_2 } \\ - 0 & b_0[i] = b_1[i] \\ + 0 & \text{if } b_0[i] = b_1[i] \\ 1 & \text{otherwise} \\ \end{cases} $$ @@ -185,7 +185,7 @@ For all $i \in 0, 1, \ldots , 8 \cdot n - 1$, we have $$ b_r[i] = \begin{cases} - 0 & b[i] = 1\\ + 0 & \text{if } b[i] = 1\\ 1 & \text{otherwise}\\ \end{cases} $$ From 37d217d08de9d27c4afbb22aaf30fa130be445b0 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Wed, 1 May 2024 10:32:32 +1200 Subject: [PATCH 07/32] Integer set example --- CIP-XXX/CIP-XXX.md | 106 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 105 insertions(+), 1 deletion(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 15d06db437..45a71b3bd6 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -28,7 +28,104 @@ and provide some laws these operations should obey. ## Motivation: why is this CIP necessary? -TODO: Add case for integer set +Bitwise operations, both over fixed-width and variable-width blocks of bits, +have a range of uses, including data structures (especially +[succinct][succinct-data-structures] ones) and cryptography. Currently, +operations on individual bits in Plutus Core are difficult, or outright +impossible, while also keeping within the tight constraints required onchain. +While it is possible to some degree to work with individual _bytes_ over +`BuiltinByteString`s, this isn't sufficient, or efficient, when bit +maniputations are required. + +To demonstrate where bitwise operations would allow onchain possibilities that +are currently either impractical or impossible, we give the following use cases. + +### Case 1: integer set + +An _integer set_ (also known as a bit set, bitmap, or bitvector) is a +[succinct][succinct-data-structures] data structure for representing a set of +numbers in a pre-defined range $[0, n)$ for some $n \in \mathbb{N}$. The +structure supports the following operations: + +* Construction given a fixed number of elements, as well as the bound $n$. +* Construction of the empty set (contains no elements) and the universe + (contains all elements). +* Set union, intersection, complement and difference (symmetric and asymmetric). +* Membership testing for a specific element. +* Inserting or removing elements. + +These structures have a range of uses. In addition to being used as sets of +bounded natural numbers, an integer set could also represent an array of Boolean +values. These have [a range of applications][bitvector-apps], mostly as +'backends' for other, more complex structures. Furthermore, by using some index +arithmetic, integer sets can also be used to represent +[binary matrices][binary-matrix] (in any number of +dimensions), which have an even wider range of uses: + +* Representations of graphs in [adjacency-matrix][adjacency-matrix] form +* [Checking the rules for a game of Go][go-binary-matrix] +* [FSM representation][finite-state-machine-4vl] +* Representation of an arbitrary binary relation between finite sets + +The succinctness of the integer set (and the other succinct data structures it +enables) is particularly valuable on-chain, due to the limited transaction size +and memory available. + +Typically, such a structure would be represented as a packed array of bytes +(similar to the Haskell `ByteString`). Essentially, given a bound $n$, the +packed array has a length in bytes large enough to contain at least $n$ bits, +with a bit at position $i$ corresponding to the value $i \in \mathbb{N}$. This +representation ensures the succinctness of the structure (at most 7 bits of +overhead are required if $n = 8k + 1$ for some $k \in \mathbb{N}$), and +also allows all the above operations to be implemented efficiently: + +* Construction given a fixed number of elements and the bound $n$ involves + allocating the packed array, then modifying some bits to be set. +* Construction of the empty set is a packed array where every byte is `0x00`, + while the universe is a packed array where every byte is `0xFF`. +* Set union is bitwise OR over both arguments. +* Set intersection is bitwise AND over both arguments. +* Set complement is bitwise complement over the entire packed array. +* Symmetric set difference is bitwise XOR over both arguments; asymmetric set + difference can be defined using a combination of bitwise complement and + bitwise OR. +* Membership testing is checking whether a bit is set. +* Inserting an element is setting the corresponding bit. +* Removing an element is clearing the corresponding bit. + +Given that this is a packed representation, these operations can be implemented +very efficiently by relying on the cache-friendly properties of packed array +traversals, as well as making use of optimized routines available in many +languages. Thus, this structure can be used to efficiently represent sets of +numbers in any bounded range (as ranges not starting from $0$ can be represented +by storing an offset), while also being minimal in space usage. + +Currently, such a structure cannot be easily implemented in Plutus Core while +preserving the properties described above. The two options using existing +primitives are either to use `[BuiltinInteger]`, or to mimic the above +operations over `BuiltinByteString`. The first of these is not space _or_ +time-efficient: each `BuiltinInteger` takes up multiple machine words of space, +and the list overheads introduced are linear in the number of items stored, +destroying succinctness; membership testing, insertion and removal require +either maintaining an ordered list or forcing linear scans for at least some +operations, which are inefficient over lists; and 'bulk' operations like union, +intersection and complement become very difficult and time-consuming. The second +is not much better: while we preserve succinctness, there is no easy way to +access individual bits, only bytes, which would require a division-remainder +loop for each such operation, with all the overheads this imposes; intersection, +union and symmetric difference would have to be simulated byte-by-byte, +requiring large lookup tables or complex conditional logic; and construction +would require immense amounts of copying and tricky byte construction logic. +While it is not outright impossible to make such a structure using current +primitives, it would be so impractical that it could never see real use. + +Furthermore, for sparse (or dense) integer sets (that is, where either most +elements in the range are absent or present respectively), a range of +[compression techniques][bitmap-index-compression] have been developed. All of +these rely on bitwise operations to achieve their goals, and can potentially +yield significant space savings in many cases. Given the limitations onchain +that we have to work within, having such techniques available to implementers +would be a huge potential advantage. TODO: Another 1-2 example uses @@ -523,3 +620,10 @@ This CIP is licensed under [Apache-2.0](http://www.apache.org/licenses/LICENSE-2 [de-morgan]: https://en.wikipedia.org/wiki/De_Morgan%27s_laws [lens-laws]: https://oleg.fi/gists/posts/2017-04-18-glassery.html#laws:lens [monoid-homomorphism]: https://en.wikipedia.org/wiki/Monoid#Monoid_homomorphisms +[succinct-data-structures]: https://en.wikipedia.org/wiki/Succinct_data_structure +[adjacency-matrix]: https://en.wikipedia.org/wiki/Adjacency_matrix +[binary-matrix]: https://en.wikipedia.org/wiki/Logical_matrix +[go-binary-matrix]: https://senseis.xmp.net/?BinMatrix +[finite-state-machine-4vl]: https://en.wikipedia.org/wiki/Four-valued_logic#Matrix_machine +[bitvector-apps]: https://en.wikipedia.org/wiki/Bit_array#Applications +[bitmap-index-compression]: https://en.wikipedia.org/wiki/Bitmap_index#Compression From b331b699adbec7ef6e602b3b4a5a94a448054cf9 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Wed, 1 May 2024 11:05:19 +1200 Subject: [PATCH 08/32] Integer set example, other bits --- CIP-XXX/CIP-XXX.md | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 45a71b3bd6..a82d4247b3 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -600,17 +600,34 @@ alternatives ### Acceptance Criteria -TODO: Fill these in (lower priority) +We consider the following criteria to be essential for acceptance: + +* A proof-of-concept implementation of the operations specified in this + document, outside of the Plutus source tree. The implementation must be in + GHC Haskell, without relying on the FFI. +* The proof-of-concept implementation must have tests, demonstrating that it + behaves as the specification requires. +* The proof-of-concept implementation must demonstrate that it will + successfully build, and pass its tests, using all GHC versions currently + usable to build Plutus (8.10, 9.2 and 9.6 at the time of writing), across all + [Tier 1][tier-1-ghc] platforms. + +Ideally, the implementation should also demonstrate its performance +characteristics by well-designed benchmarks. ### Implementation Plan -These operations will be implemented by MLabs, to be merged into Plutus Core -after review. +MLabs has begun the [implementation of the proof-of-concept][mlabs-impl] as +required in the acceptance criteria. Upon completion, we will send a pull +request to Plutus with the implementation of the primitives for Plutus +Core, mirroring the proof-of-concept. ## Copyright This CIP is licensed under [Apache-2.0](http://www.apache.org/licenses/LICENSE-2.0). +[mlabs-impl]: https://github.com/mlabs-haskell/plutus-integer-bytestring +[tier-1-ghc]: https://gitlab.haskell.org/ghc/ghc/-/wikis/platforms#tier-1-platforms [special-semigroups]: https://en.wikipedia.org/wiki/Special_classes_of_semigroups [commutative-monoid]: https://en.wikipedia.org/wiki/Monoid#Commutative_monoid [absorbing-element]: https://en.wikipedia.org/wiki/Zero_element#Absorbing_elements From b1a83a24cefe1838181ddec82349b9087125350d Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Wed, 1 May 2024 12:13:51 +1200 Subject: [PATCH 09/32] Start on bit indexing scheme --- CIP-XXX/CIP-XXX.md | 92 +++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 91 insertions(+), 1 deletion(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index a82d4247b3..7fdcdeb8fa 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -140,7 +140,97 @@ the use of these operations. ### Bit indexing scheme -TODO: Specify +We begin by observing that a `BuiltinByteString` is a packed array of bytes +(that is, `BuiltinInteger`s in the range $[0, 255]$) according to the API +provided by existing Plutus Core primitives. In particular, we have the ability +to access individual bytes by index as a primitive operation. Thus, we can view +a `BuiltinByteString` as an indexed collection of bytes; for any +`BuiltinByteString` $b$ of length $n$, and any $i \in 0, 1, \ldots, n - 1$, we +define $b\\{i\\}$ as the byte at index $i$ in $b$, as defined by the +`builtinIndexByteString` primitive. In essence, for any `BuiltinByteString` of +length `n`, we have _byte_ indexes as follows: + +```mermaid +block-beta +columns 1 + block:BBS + A["0"] + B["1"] + C["..."] + D["n - 1"] + end +``` + +To view a `BuiltinByteString` as an indexed collection of _bits_, we must first +consider the bit ordering within a byte. Suppose $i \in 0, 1, \ldots, 7$ is an +index into a byte $w$. We say that the bit at $i$ in $w$ is _set_ when + +$$ +\left \lfloor \frac{w}{2^{i}} \right \rfloor \mod 2 \equiv 1 +$$ + +Otherwise, the bit at $i$ in $w$ is _clear_. We define $w[i]$ to be $1$ when +the bit at $i$ in $w$ is set, and $0$ otherwise; this is the _value_ at index +$i$ in $w$. + +For example, consider the byte represented by the `BuiltinInteger` 42. By the +above scheme, we have the following: + +| Bit index | Set or clear? | +|-----------|---------------| +| $0$ | Clear | +| $1$ | Set | +| $2$ | Clear | +| $3$ | Set | +| $4$ | Clear | +| $5$ | Set | +| $6$ | Clear | +| $7$ | Clear | + +Put another way, we can view $w[i] = 1$ to mean that the $(i + 1)$ th least significant +digit in $w$'s binary representation is $1$, and likewise, $w[i] = 0$ would mean +that the $i$th least significant digit in $w$'s binary representation is $0$. +Continuing with the above example, $42$ is represented in binary as `00101010`; +we can see that the second-least-significant, fourth-least-significant, and +sixth-least-significant digits are `1`, and all the others are zero. This +description mirrors the way bytes are represented on machine architectures. + +We now extend the above scheme to `BuiltinByteString`s. Let $b$ be a +`BuiltinByteString` whose length is $n$, and let $i \in 0, 1, \ldots, 8 \cdot n - 1$. +For any $j \in 0, 1, \ldots, n - 1$, let $j^{\prime} = n - j - 1$. We say that the bit +at $i$ in $b$ is set if + +$$ +b\left\\{\left(\left\lfloor \frac{i}{8} \right\rfloor\right)^{\prime}\right\\}[i\mod 8] = 1 +$$ + +We define the bit at $i$ in $b$ being clear analogously. Similarly to bits in a +byte, we define $b[i]$ to be $1$ when the bit at $i$ in $b$ is set, and $0$ +otherwise; similarly to bytes, we term this the _value_ at index $i$ in $b$. + +As an example, consider the `BuiltinByteString` `[42, 57, 133]`: that is, the +`BuiltinByteString` $b$ such that $b\\{0\\} = 42$, $b\\{1\\} = 57$ and $b\\{2\\} += 133$. We observe that the range of 'valid' bit indexes $i$ into $b$ is in +$[0, 3 \cdot 8 - 1 = 23]$. Consider $i = 4$; by the definition above, this +corresponds to the _byte_ index 2, as $\left\lfloor\frac{4}{8}\right\rfloor = +0$, and $3 - 0 - 1 = 2$ (as $b$ has length $3$). Within the byte $133$, this +means we have $\left\lfloor\frac{133}{2^4}\right\rfloor \mod 2 \equiv 0$. Thus, +$b[4] = 0$. Consider instead the index $i = 19$; by the definition above, this +corresponds to the _byte_ index 0, as $\left\lfloor\frac{19}{8}\right\rfloor = +2$, and $3 - 2 - 1 = 0$. Within the byte $42$, this means we have +$\left\lfloor\frac{42}{2^3}\right\rfloor `mod 2 \equiv 1$. Thus, $b[19] = 1$. + +Put another way, our _byte_ indexes run 'the opposite way' to our _bit_ indexes. +Thus, for any `BuiltinByteString` of length $n$, we have _bit_ indexes relative +_byte_ indexes as follows: + +```mermaid +block-beta +columns 4 +A["0"] B["1"] C["..."] D["n - 1"] +``` + +TODO: Diagram ### Operation semantics From f783f6aa68894d404ec2c749386e48c86f5b378c Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Wed, 1 May 2024 14:11:58 +1200 Subject: [PATCH 10/32] Finish bit index specification, consistency edit --- CIP-XXX/CIP-XXX.md | 41 ++++++++++++++++++----------------------- 1 file changed, 18 insertions(+), 23 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 7fdcdeb8fa..5a0004856a 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -150,15 +150,10 @@ define $b\\{i\\}$ as the byte at index $i$ in $b$, as defined by the `builtinIndexByteString` primitive. In essence, for any `BuiltinByteString` of length `n`, we have _byte_ indexes as follows: -```mermaid -block-beta -columns 1 - block:BBS - A["0"] - B["1"] - C["..."] - D["n - 1"] - end +``` +| Index | 0 | 1 | ... | n - 1 | +|-------|----|----| ... |----------| +| Byte | w0 | w1 | ... | w(n - 1) | ``` To view a `BuiltinByteString` as an indexed collection of _bits_, we must first @@ -224,13 +219,13 @@ Put another way, our _byte_ indexes run 'the opposite way' to our _bit_ indexes. Thus, for any `BuiltinByteString` of length $n$, we have _bit_ indexes relative _byte_ indexes as follows: -```mermaid -block-beta -columns 4 -A["0"] B["1"] C["..."] D["n - 1"] ``` - -TODO: Diagram +| Byte index | 0 | 1 | ... | n - 1 | +|------------|--------------------------------|----| ... |-------------------------------| +| Byte | w0 | w1 | ... | w(n - 1) | +|------------|--------------------------------|----| ... |-------------------------------| +| Bit index | 8n - 1 | 8n - 2 | ... | 8n - 8 | ... | 7 | 6 | 5 | 4 | 3 | 2 | 1 | 0 | +``` ### Operation semantics @@ -280,7 +275,7 @@ Let $b_1, b_2$ refer to the first data argument and the second data argument respectively, and let $n_1, n_2$ be their respective lengths in bytes. Let the result of `builtinLogicalAnd`, given $b_1, b_2$ and some padding semantics argument, be $b_r$, of length $n_r$ in bytes. We use $b_1[i]$ to refer -to the $i$th bit of $b_1$ (and analogously for +to the value at index $i$ of $b_1$ (and analogously for $b_2, b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) for the exact specification of this. @@ -311,7 +306,7 @@ Let $b_1, b_2$ refer to the first data argument and the second data argument respectively, and let $n_1, n_2$ be their respective lengths in bytes. Let the result of `builtinLogicalOr`, given $b_1, b_2$ and some padding semantics argument, be $b_r$, of length $n_r$ in bytes. We use $b_1[i]$ to refer -to the $i$th bit of $b_1$ (and analogously for +to the value at index $i$ of $b_1$ (and analogously for $b_2, b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) for the exact specification of this. @@ -342,7 +337,7 @@ Let $b_1, b_2$ refer to the first data argument and the second data argument respectively, and let $n_1, n_2$ be their respective lengths in bytes. Let the result of `builtinLogicalXor`, given $b_1, b_2$ and some padding semantics argument, be $b_r$, of length $n_r$ in bytes. We use $b_1[i]$ to -refer to the $i$th bit of $b_1$ (and analogously for +refer to the value at index $i$ of $b_1$ (and analogously for $b_2, b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) for the exact specification of this. @@ -364,8 +359,8 @@ $$ `builtinLogicalComplement` takes a single argument, of type `BuiltinByteString`; let $b$ refer to that argument, and $n$ its length in bytes. Let $b_r$ be the result of `builtinLogicalComplement`; its length in bytes is also $n$. We -use $b[i]$ to refer to the $i$th bit of $b$ (and analogously for $b_r$); see the -[section on the bit indexing scheme](#bit-indexing-scheme) for the exact +use $b[i]$ to refer to the value at index $i$ of $b$ (and analogously for $b_r$); +see the [section on the bit indexing scheme](#bit-indexing-scheme) for the exact specification of this. For all $i \in 0, 1, \ldots , 8 \cdot n - 1$, we have @@ -387,8 +382,8 @@ $$ _index argument_. Let $b$ refer to the data argument, of length $n$ in bytes, and let $i$ refer to -the index argument. We use $b[i]$ to refer to the $i$th bit of $b$; see the -[section on the bit indexing scheme](#bit-indexing-scheme) for the exact +the index argument. We use $b[i]$ to refer to the value at index $i$t of $b$; see +the [section on the bit indexing scheme](#bit-indexing-scheme) for the exact specification of this. If $i < 0$ or $i \geq 8 \cdot n$, then `builtinReadBit` @@ -414,7 +409,7 @@ Otherwise, if $b[i] = 0$, `builtinReadBit` returns `False`, and if $b[i] = 1$, Let $C = (i_1, v_1), (i_2, v_2), \ldots , (i_k, v_k)$ refer to the change list argument, and $b$ the data argument of length $n$ in bytes. Let $b_r$ be the result of `builtinSetBits`, whose length is also $n$. We use $b[i]$ to refer to -the $i$th bit of $b$ (and analogously, $b_r$); see the [section on the bit +the value at index $i$ of $b$ (and analogously, $b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) for the exact specification of this. If the change list argument is empty, the result is $b$. If the change list From cbd3141640c6baaaa408d0139f0d5de3b0e28c43 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Wed, 1 May 2024 14:29:21 +1200 Subject: [PATCH 11/32] Typoes --- CIP-XXX/CIP-XXX.md | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 5a0004856a..8e5414ff0c 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -279,14 +279,14 @@ to the value at index $i$ of $b_1$ (and analogously for $b_2, b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) for the exact specification of this. -If the padding semantics argument is `True`, then we have $n_r = \max \{ n_1, -n_2 \}$; otherwise, $n_r = \min \{ n_1, n_2 \}$. For all $i \in 0, 1, \ldots 8 +If the padding semantics argument is `True`, then we have $n_r = \max \\{ n_1, +n_2 \\}$; otherwise, $n_r = \min \\{ n_1, n_2 \\}$. For all $i \in 0, 1, \ldots 8 \cdot n_r - 1$, we have $$ b_r[i] = \begin{cases} - b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ - b_1[i] & \text{if } n_0 < n_1 \text { and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ + b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \\{ n_1, n_2 \\} \\ + b_1[i] & \text{if } n_0 < n_1 \text { and } i \geq 8 \cdot \min \\{ n_1, n_2 \\} \\ 1 & \text{if } b_0[i] = b_1[i] = 1 \\ 0 & \text{otherwise} \\ \end{cases} @@ -316,8 +316,8 @@ n_2 \}$; otherwise, $n_r = \min \{ n_1, n_2 \}$. For all $i \in 0, 1, \ldots 8 $$ b_r[i] = \begin{cases} - b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ - b_1[i] & \text{if } n_0 < n_1 \text { and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ + b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \\{ n_1, n_2 \\} \\ + b_1[i] & \text{if } n_0 < n_1 \text { and } i \geq 8 \cdot \min \\{ n_1, n_2 \\} \\ 0 & \text{if } b_0[i] = b_1[i] = 0 \\ 1 & \text{otherwise} \\ \end{cases} @@ -347,8 +347,8 @@ n_2 \}$; otherwise, $n_r = \min \{ n_1, n_2 \}$. For all $i \in 0, 1, \ldots 8 $$ b_r[i] = \begin{cases} - b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \{ n_1, n_2 \} \\ - b_1[i] & \text{if } n_0 < n_1 \text { and } i \geq 8 \cdot \min { n_1, n_2 } \\ + b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \\{ n_1, n_2 \\} \\ + b_1[i] & \text{if } n_0 < n_1 \text { and } i \geq 8 \cdot \min \\{ n_1, n_2 \\} \\ 0 & \text{if } b_0[i] = b_1[i] \\ 1 & \text{otherwise} \\ \end{cases} @@ -424,9 +424,9 @@ Otherwise, for all $j \in 0, 1, \ldots 8 \cdot n - 1$, we have $$ b_r[j] = \begin{cases} - 0 & \text{if } j = i \text{ and } b = \texttt{False}// - 1 & \text{if } j = i \text{ and } b = \texttt{True}// - b[j] & \text{otherwise}// + 0 & \text{if } j = i \text{ and } b = \texttt{False}\\ + 1 & \text{if } j = i \text{ and } b = \texttt{True}\\ + b[j] & \text{otherwise}\\ \end{cases} $$ @@ -473,11 +473,12 @@ information: byte; and * What `BuiltinInteger` was passed as the byte argument. -Otherwise, let $b$ be the result of `builtinReplicate`, and let $b[i]$ be the -byte at position $i$ of $b$, as per `builtinIndexByteString`. We have: +Otherwise, let $b$ be the result of `builtinReplicate`, and let $b\\{i\\}$ be the +byte at position $i$ of $b$, as per [the section describing the bit indexing +scheme](#bit-indexing-scheme). We have: * The length (in bytes) of $b$ is $n$; and -* For all $i \in 0, 1, \ldots, n - 1$, $b[i] = w$. +* For all $i \in 0, 1, \ldots, n - 1$, $b\\{i\\} = w$. ### Laws and examples From aae98f3508fbac883f31e3ecd17d33be157efede Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Thu, 2 May 2024 10:01:40 +1200 Subject: [PATCH 12/32] Justification --- CIP-XXX/CIP-XXX.md | 383 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 381 insertions(+), 2 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 8e5414ff0c..e11d1f4b18 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -679,8 +679,380 @@ TODO: Examples ## Rationale: how does this CIP achieve its goals? -TODO: Explain goals relative examples, give descriptions of non-existent -alternatives +The operations, and semantics, described in this CIP provide a set of +well-defined bitwise logical operations, as well as bitwise access and +modification, to allow cases similar to Case 1 to be performed efficiently and +conveniently. Furthermore, the semantics we describe would be reasonably +familiar to users of other programming languages (including Haskell) which have +provisions for bitwise logical operations of this kind, as well as some way of +extending these operations to operate on packed byte vectors. At the same time, +there are several choices we have made that are somewhat unusual, or could +potentially have been implemented differently based on existing work: most +notably, our choice of bit indexing scheme, the padding-versus-truncation +semantics, and the multiplicitous definition of bit modification. Among existing +work, a particularly important example is [CIP-58][cip-58], which makes +provisions for operations similar to the ones described here, and from which we +differ in several important ways. We clarify the reasoning behind our choices, +and how they differ from existing work, below. + +Aside from the issues we list below, we don't consider other operations +controversial. Indeed, `bitwiseLogicalComplement` has a direct parallel to the +implementation in [CIP-58][cip-58], and `builtinReplicate` is a direct wrapper +around the `replicate` function in `ByteString`. Thus, we do not discuss them +further here. + +### Bit indexing scheme + +The bit indexing scheme we describe here is designed around two +considerations. Firstly, we want operations on these bits, as well as those +results, to be as consistent and as predictable as possible: any individual +familiar with such operations on variable-length bitvectors from another +language shouldn't be surprised by the semantics. Secondly, we want to +anticipate future bitwise operation extensions, such as shifts and rotations, +and have the indexing scheme support efficient implementations (and predictable +semantics) for these. + +While prior art for bit access (and modification) exists +in almost any programming language, these are typically over types of fixed +width (usually bytes, machine words, or something similar); for variable-width +types, these typically are either not implemented at all, or if they are +implemented, this is done in an external library, with varying support for +certain operations. An example of the first is Haskell's `ByteString`, which has +no way to even access, much less modify, individual bits; an example of the +second is the [CRoaring][croaring] library for C, which supports all the +operations we describe in this CIP, along with multiple others. In the second +case, the _exact_ arrangement of bits inside the representation is not something +users are exposed to directly: instead, the bitvector type is opaque, and the +library only guarantees consistency of API. In our case, this is not a viable +choice, as we require bit access _and_ byte access to both work on +`BuiltinByteString`, and thus, some consistency of representation is required. + +The scheme for indexing bits within a byte that we describe in [the relevant +section](#bit-indexing-scheme) is the same as the one used by the `Data.Bits` +API in Haskell for `Word8` bit indexing, and mirrors the decisions of most +languages that provide such an API at all, as well as the conventional +definition of such operations as `(w >> i) & 1` for access, `w | (1 << i)` for +setting, and `w & ~(1 << i)` for clearing. We could choose to 'flip' this +indexing, by using a similar operation for 'index flipping' as we currently use +for bytes: essentially, instead of + +$$ +\left \lfloor \frac{w}{2^{i}} \right \rfloor \mod 2 \equiv 1 +$$ + +we would instead use + +$$ +\left \lfloor \frac{w}{2^{8 - i - 1}} \right \rfloor \mod 2 \equiv 1 +$$ + +to designate bit $i$ as set (and analogously for clear). Together with the +ability to choose _not_ to flip the _byte_ index, we get four possibilities, +which have [been described previously][too-many-ways-1]. For clarity, we name, +and describe, them below. Throughout, we use `n` as the length of a given +`BuiltinByteString` in bytes. + +The first possibility is that we 'flip' neither bit, nor byte, indexes. We call +this the _no-flip variant_: + +``` +| Byte index | 0 | 1 | ... | n - 1 | +|------------|-------------------------------|-------------------| ... |--------------------------------| +| Byte | w0 | w1 | ... | w(n - 1) | +|------------|-------------------------------|-------------------| ... |--------------------------------| +| Bit index | 7 | 6 | 5 | 4 | 3 | 2 | 1 | 0 | 15 | 14 | ... | 8 | ... | 8n - 1 | 8n - 2 | ... | 8n - 8 | +``` + +The second possibility is that we 'flip' _both_ bit and byte indexes. We call +this the _both-flip variant_: + +``` +| Byte index | 0 | ... | n - 2 | n - 1 | +|------------|--------------------------------| ... |------------------|-------------------------------| +| Byte | w0 | ... | w (n - 2) | w(n - 1) | +|------------|--------------------------------| ... |------------------|-------------------------------| +| Bit index | 8n - 8 | 8n - 7 | ... | 8n - 1 | ... | 8 | 9 | ... | 15 | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | +``` + +The third possibility is that we 'flip' _bit_ indexes, but not _byte_ indexes. +We call this the _bit-flip variant_: + +``` +| Byte index | 0 | 1 | ... | n - 1 | +|------------|-------------------------------|--------------| ... |--------------------------------| +| Byte | w0 | w1 | ... | w(n - 1) | +|------------|-------------------------------|--------------| ... |--------------------------------| +| Bit index | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | ... | 15 | ... | 8n - 8 | 8n - 7 | ... | 8n - 1 | +``` + +The fourth possibility is the one we describe in the [bit indexing scheme +section](#bit-indexing-scheme), which is also the scheme chosen by CIP-58. We +repeat it below for clarity: + +``` +| Byte index | 0 | 1 | ... | n - 1 | +|------------|--------------------------------|----| ... |-------------------------------| +| Byte | w0 | w1 | ... | w(n - 1) | +|------------|--------------------------------|----| ... |-------------------------------| +| Bit index | 8n - 1 | 8n - 2 | ... | 8n - 8 | ... | 7 | 6 | 5 | 4 | 3 | 2 | 1 | 0 | +``` + +On the face of it, these schemes appear equivalent: they are all consistent, and +all have formal descriptions, and quite similar ones at that. However, we +believe that only the one we chose is the correct one. To explain this, we +introduce two notions that we consider to be both intuitive and important, +then specify why our choice of indexing scheme fits those notions better than +any other. + +The first notion is _index locality_. Intuitively, this states that if +two indexes are 'close' (in that their absolute difference is small), the values +at those indexes should be 'close' (in that their positioning in memory should +be separated less). We believe this notion to be reasonable, as this is an +expectation from array indexing (and indeed, `BuiltinByteString` indexing), as +well as the reason why packed array data is efficient on modern memory +hierarchies. Extending this notion to bits, we can observe that the both-flip +and no-flip variants of the bit indexing scheme do not preserve index locality: +the separation between a bit at index $0$ and index $1$ is _significantly_ +different to the separation between a bit at index $7$ and index $8$ in both +representations, despite their absolute difference being identical. Thus, we +believe that these two variants are not viable, as they are not only confusing +from the point of view of behaviour, they would also make implementation of +future operations (such as shifts or rotations) significantly harder to both do, +and also reason about. Thus, only the bit-flip variant, as well as our choice, +remain contenders. + +The second notion is _conversion agreement_. To describe this notion, we first +observe that, according to the definition of the bit indexing scheme given [in +the corresponding section](#bit-indexing-scheme), as well as the corresponding +definition for the bit-flip variant, we view a `BuiltinByteString` of length $n$ +as a binary natural number with exactly $8n$ digits, and the value at index $i$ +corresponds to the digits whose place value is either $2^i$ (for the bit-flip +variant), or $2^{8n - i - 1}$ (for our chosen method). Put another way, under +the specification for the bit-flip variant, the least significant binary digit +is first, whereas in our chosen specification, the least significant binary +digit is last. + +When viewed this way, we can immediately see a potential problem, as by indexing +a `BuiltinByteString`, we get back a `BuiltinInteger`, which has a numerical +value as a natural number in the range $[0, 255]$. It would thus be sensible +that, given a `BuiltinByteString` that is non-empty, if we were to get the +values at bit indexes $0$ through $7$, and treat them as their corresponding +place value in a summation, we should obtain the same answer as indexing +whichever byte those bits come from. We call this notion _conversion agreement_, +due to its relation to [an existing CIP][conversion-cip], which allows us to +(essentially) view a `BuiltinByteString` as a natural number in base-256. +Indeed, the case is analogous, with the only difference being that we are +concerned with the positioning of base-256 digits, not binary ones. + +Consider the `BuiltinByteString` whose only byte is $42$, whose representation +is as follows: + +``` +| Byte index | 0 | +|------------|----------| +| Byte | 00101010 | +``` + +Under the bit-flip variant, our bit indexes would be as follows: + +``` +| Byte index | 0 | +|------------|-------------------------------| +| Byte | 0 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | +|------------|-------------------------------| +| Bit index | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | +``` + +However, this immediately causes a problem: under this indexing scheme, we imply +that the $2^2 = 4$ place value is $1$ in $42$'s binary representation, but +this is not the case. This fails conversion agreement. However, our choice +produces the correct answer: + +``` +| Byte index | 0 | +|------------|-------------------------------| +| Byte | 0 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | +|------------|-------------------------------| +| Bit index | 7 | 6 | 5 | 4 | 3 | 2 | 1 | 0 | +``` + +Here, the $4$ place value is correctly $0$. Indeed, our choice simply 'extends' +the bit ordering (in the place value sense) employed by all machine +architectures for bytes in their sense as natural numbers within a fixed range. +This was also the choice made by [CIP-58][cip-58], for similar reasons. + +While the bit-flip variant has the advantage of 'agreement' between byte and bit +indexes, we believe that conversion agreement is the more important property to +have, not only for consistency with our described semantics, but also to some +extent for consistency with the conversion primitives [described in another +existing CIP][conversion-cip]. Given that the aforementioned CIP has already +been implemented into Plutus Core, we think that our choice is the only viable +one if consistency is desirable. + +### Padding versus truncation + +For the operations defined in this CIP taking two `BuiltinByteString` arguments +(that is, `builtinLogicalAnd`, `builtinLogicalOr`, and `builtinLogicalXor`), +when the two arguments have identical lengths, the semantics are natural, +mirroring the corresponding operations on the +[Boolean algebra $\mathbb{2}^{8n}$][boolean-algebra-2], where $n$ is the length +of either argument in bytes. When the arguments do _not_ have matching lengths, +however, the situation becomes more complex, as there are several ways in which +we could define these operations. The most natural possibilities are as follows; +we repeat some of the definitions used [in the corresponding +section](#padding-versus-truncation-semantics). + +* Extend the shorter argument with the identity element (1 for + `builtinLogicalAnd`, 0 otherwise) to match the length of the longer argument, + then perform the operation as if on matching-length arguments. We call this + _padding semantics_. +* Ignore the bytes of the longer argument whose indexes would not be valid for + the shorter argument, then perform the operation as if on matching-length + arguments. We call this _truncation semantics_. +* Fail with an error whenever argument lengths don't match. We call this + _match semantics_. + +It is not a priori clear which of these we should choose: they are subject to +different laws (as evidenced by the [corresponding +section](#laws-and-examples)), none of which are strict supersets of each other +(at least not for _all_ inputs possible). While [CIP-58][cip-58] chose match +semantics, we believe this was not the correct decision: we use Case 1 to +justify the benefit of having other semantics described above available. + +Consider the following operation: given a bound $k$ and an integer set, remove +all elements smaller than $k$ from the set. This can be done using +`bitwiseLogicalAnd` and a mask where the first $k - 1$ bits are clear. However, +under match semantics, the mask would have to have a length equal to the integer +set representation; under padding semantics, the mask would only need to have a +length proportional to $k$. This is noteworthy, as padding the mask would +require an additional copy operation, only to produce a value that would be +discarded immediately. + +Consider instead the following operation: given two integer sets with different +(upper) bounds, take their intersection, producing an integer set whose size is +the minimum of the two. This can once again be done using `bitwiseLogicalAnd`, +but under match semantics (or padding semantics for that matter), we would first +have to slice the longer argument, while under truncation semantics, we wouldn't +need to. + +Match semantics can be useful for Case 1 as well. Consider the case that a +representation of an integer set is supplied as an +input datum (in its `Data` encoding). In order to deserialize it, we need to +verify at least whether it has the right length in bytes to represent an integer +set with a given bound. Under padding or truncation semantics, we would have to +check this at deserialization time; under exact match semantics, provided we +were sure that at least one argument is of a known size, we could simply perform +the necessary operations and let the match semantics error if given something +inappropriate. + +It is also worth noting that truncation semantics are well-established in the +Haskell ecosystem. Viewed another way, all of the operations under discussion in +this sections are specialized versions of the `zipWith` operation; Haskell +libraries provide this type of operation for a range of linear collections, +including lists, `Vector`s, and mostly notably, `ByteString`s. In all of these +cases, truncation semantics are what is implemented; it would be surprising to +developers coming from Haskell to find that they have to do additional work to +replicate them in Plutus. While we don't anticipate direct use of Plutus Core +primitives by developers (although this is not an unheard-of case), we should +enable library authors to build familiar APIs _on top of_ Plutus Core +primitives, which suggests truncation semantics should be available, at least as +an option. + +All the above suggests that no _single_ choice of semantics will satisfy all +reasonable needs, if only from the point of view of efficiency. This suggests, +much as for [conversion primitives][conversion-cip] and endianness issues, that +the primitive should allow a choice in what semantics get used for any given +call. Ideally, we would allow a choice of any of the three options described +above; however, this is awkward to do in Plutus Core. While the choice between +_two_ options is straightforward (pass a `BuiltinBool`), the choice between +_three_ options would either require multiple `BuiltinBool` arguments, or a +`BuiltinInteger` argument with 'designated values' (such as 'negative means +truncation, zero means match, positive means padding'). Neither of these are +ideal choices, as they involve either argument redundancy or additional checks +(and erroring when they don't match). In light of this, we elected to choose +only two of the three semantics and have this choice for any given call be +controlled by a `BuiltinBool` flag. + +This naturally leads to the question of which of the three semantics above we +can afford not to have. We believe that match semantics are the right ones to +exclude. Firstly, technically we can still have match semantics by using either +padding or truncation semantics plus a length check beforehand: this is a cheap +operation, unlike simulating padding semantics for example, which would have +non-trivial cost. Secondly, due to the preponderance of truncation semantics in +Haskell, we feel excluding it as an option is wrong. Lastly, we believe that +outside of error checking, exact match semantics give few benefits over padding +or truncation semantics, for performance and otherwise. This combination of +reasoning leads us to naturally consider padding and truncation as the two to +keep, and this guided our implementation choices. + +### Bit setting + +`builtinSetBits` in our description takes a change list argument, allowing +changing multiple bits at once. This is an added complexity, and an argument can +be made that something similar to the following operation would be sufficient: + +```haskell +builtinSetBit :: BuiltinByteString -> BuiltinInteger -> BuiltinBool -> +BuiltinByteString +``` + +Essentially, `builtinSetBit bs i v` would be equivalent to `builtinSetBits bs +[(i, v)]` as currently defined. This was the choice made by [CIP-58][cip-58], +with the consideration of simplicity in mind. + +At the same time, due to the immutability semantics of Plutus Core, each time +`builtinSetBit` is called, a copy of its `BuiltinByteString` argument would have +to be made. Thus, a sequence of $k$ `builtinSetBit` calls in a fold over a +`BuiltinByteString` of length $n$ would require $\Theta(nk)$ time and +$\Theta(nk)$ space. Meanwhile, if we instead used `builtinSetBits`, the time +drops to $\Theta(n + k)$ and the space to $\Theta(n)$, which is a non-trivial +improvement. While we cannot avoid the worst-case copying behaviour of +`builtinSetBit` (if we have a critical path of read-write dependencies of length +$k$, for example), and 'list packing' carries some cost, we have +[benchmarks][benchmarks-bits] that show not only that this 'packing cost' is +essentially zero, but that for `BuiltinByteString`s of 30 bytes or fewer, +copying completely overwhelms the work required to set the bits in the first +place. This alone is a strong argument for having `builtinSetBits` instead; +indeed, there is prior art for doing this [in the `vector` library][vector], for +the exact reasons we give here. + +The argument could also be made whether this design should be extended to other +primitive operations in this CIP which both take `BuiltinByteString` arguments +and also produce `BuiltinByteString` results. We believe that this is not as +justified as in the `builtinSetBits` case, for several reasons. Firstly, for +`builtinLogicalComplement`, it's not even clear what benefit this would have at +all: the only possible signature such an operation would have is +`[BuiltinByteString] -> [BuiltinByteString]`, which in effect would be a +specialized form of mapping. Even the _general_ form of mapping is not +considered suitable as a primitive operation in Plutus Core! + +Secondly, the +benefits to performance wouldn't be nearly as significant in theory, and likely +in practice. Consider this hypothetical operation (with fold semantics): + +```haskell +builtinLogicalXors :: BuiltinBool -> [BuiltinByteString] -> BuiltinByteString +``` + +Simulating this operation as a fold using `builtinLogicalXor`, in the worst +case, irrespective of padding or truncation semantics, requires $\Theta(nk)$ +time and space, where $n$ is the size of each `BuiltinByteString` in the +argument list, and $k$ is the length of the argument list itself. Using +`builtinLogicalXors` would reduce the space required to $\Theta(n)$, but not +affect the time complexity at all. + +Lastly, it is questionable whether 'bulk' operations like `builtinLogicalXors` +above would see as much use as `builtinSetBits`. In the context of Case 1, +`builtinLogicalXors` corresponds to taking the symmetric difference of multiple +integer sets; it seems unlikely that the number of sets we'd want to do this +with would be higher than 2 often. However, in the same context, +`builtinSetBits` corresponds to constructing an integer set given a list of +members (or, for that matter, _non_-members): this is an operation that is both +required by the case description, and also unarguably useful often. + +On the basis of the above, we believe that choosing to implement +`builtinSetBits` as a 'bulk' operation, but to leave others as 'singular' is the +right choice. ## Path to Active @@ -730,3 +1102,10 @@ This CIP is licensed under [Apache-2.0](http://www.apache.org/licenses/LICENSE-2 [finite-state-machine-4vl]: https://en.wikipedia.org/wiki/Four-valued_logic#Matrix_machine [bitvector-apps]: https://en.wikipedia.org/wiki/Bit_array#Applications [bitmap-index-compression]: https://en.wikipedia.org/wiki/Bitmap_index#Compression +[cip-58]: https://github.com/cardano-foundation/CIPs/tree/master/CIP-0058 +[croaring]: https://github.com/RoaringBitmap/CRoaring +[too-many-ways-1]: https://fgiesen.wordpress.com/2018/02/19/reading-bits-in-far-too-many-ways-part-1 +[conversion-cip]: https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-XXXX +[benchmarks-bits]: https://github.com/mlabs-haskell/plutus-integer-bytestring/blob/koz/logical/bench/naive/Main.hs#L74-L83 +[vector]: https://hackage.haskell.org/package/vector-0.13.1.0/docs/Data-Vector.html#v:-47--47- +[boolean-algebra-2]: https://en.wikipedia.org/wiki/Two-element_Boolean_algebra From 43d300ab9a16f3d5c2e69ae02f168a10b128c861 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Fri, 3 May 2024 10:46:27 +1200 Subject: [PATCH 13/32] Examples --- CIP-XXX/CIP-XXX.md | 242 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 239 insertions(+), 3 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index e11d1f4b18..4c8bef9c42 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -292,6 +292,33 @@ b_r[i] = \begin{cases} \end{cases} $$ +Some examples of the intended behaviour of `builtinLogicalAnd` follow. For +brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. + +``` +-- truncation semantics +builtinLogicalAnd False [] [0xFF] => [] + +builtinLogicalAnd False [0xFF] [] => [] + +builtinLogicalAnd False [0xFF] [0x00] => [0x00] + +builtinLogicalAnd False [0x00] [0xFF] => [0x00] + +builtinLogicalAnd False [0x4F, 0x00] [0xF4] => [0x44] + +-- padding semantics +builtinLogicalAnd True [] [0xFF] => [0xFF] + +builtinLogicalAnd True [0xFF] [] => [0xFF] + +builtinLogicalAnd False [0xFF] [0x00] => [0x00] + +builtinLogicalAnd False [0x00] [0xFF] => [0x00] + +builtinLogicalAnd False [0x4F, 0x00] [0xF4] => [0x44, 0x00] +``` + #### `builtinLogicalOr` `builtinLogicalOr` takes three arguments; we name and describe them below. @@ -323,6 +350,33 @@ b_r[i] = \begin{cases} \end{cases} $$ +Some examples of the intended behaviour of `builtinLogicalOr` follow. For +brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. + +``` +-- truncation semantics +builtinLogicalOr False [] [0xFF] => [] + +builtinLogicalOr False [0xFF] [] => [] + +builtinLogicalOr False [0xFF] [0x00] => [0xFF] + +builtinLogicalOr False [0x00] [0xFF] => [0xFF] + +builtinLogicalOr False [0x4F, 0x00] [0xF4] => [0xFF] + +-- padding semantics +builtinLogicalOr True [] [0xFF] => [0xFF] + +builtinLogicalOr True [0xFF] [] => [0xFF] + +builtinLogicalOr False [0xFF] [0x00] => [0xFF] + +builtinLogicalOr False [0x00] [0xFF] => [0xFF] + +builtinLogicalOr False [0x4F, 0x00] [0xF4] => [0xFF, 0x00] +``` + #### `builtinLogicalXor` `builtinLogicalXor` takes three arguments; we name and describe them below. @@ -354,6 +408,33 @@ b_r[i] = \begin{cases} \end{cases} $$ +Some examples of the intended behaviour of `builtinLogicalXor` follow. For +brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. + +``` +-- truncation semantics +builtinLogicalXor False [] [0xFF] => [] + +builtinLogicalXor False [0xFF] [] => [] + +builtinLogicalXor False [0xFF] [0x00] => [0xFF] + +builtinLogicalXor False [0x00] [0xFF] => [0xFF] + +builtinLogicalXor False [0x4F, 0x00] [0xF4] => [0xBB] + +-- padding semantics +builtinLogicalOr True [] [0xFF] => [0xFF] + +builtinLogicalOr True [0xFF] [] => [0xFF] + +builtinLogicalOr False [0xFF] [0x00] => [0xFF] + +builtinLogicalOr False [0x00] [0xFF] => [0xFF] + +builtinLogicalOr False [0x4F, 0x00] [0xF4] => [0xBB, 0x00] +``` + #### `builtinLogicalComplement` `builtinLogicalComplement` takes a single argument, of type `BuiltinByteString`; @@ -372,6 +453,17 @@ b_r[i] = \begin{cases} \end{cases} $$ +Some examples of the intended behaviour of `builtinLogicalComplement` follow. For +brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. + +``` +builtinLogicalComplement [] => [] + +builtinLogicalComplement [0x0F] => [0xF0] + +builtinLogicalComplement [0x4F, 0xF4] => [0xB0, 0x0B] +``` + #### `builtinReadBit` `builtinReadBit` takes two arguments; we name and describe them below. @@ -396,6 +488,46 @@ following information: Otherwise, if $b[i] = 0$, `builtinReadBit` returns `False`, and if $b[i] = 1$, `builtinReadBit` returns `True`. +Some examples of the intended behaviour of `builtinReadBit` follow. For +brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. + +``` +-- Indexing an empty BuiltinByteString fails +builtinReadBit [] 0 => error + +builtinReadBit [] 345 => error + +-- Negative indexes fail +builtinReadBit [] (-1) => error + +builtinReadBit [0xFF] (-1) => error + +-- Indexing reads 'from the end' +builtinReadBit [0xF4] 0 => False + +builtinReadBit [0xF4] 1 => False + +builtinReadBit [0xF4] 2 => True + +builtinReadBit [0xF4] 3 => False + +builtinReadBit [0xF4] 4 => True + +builtinReadBit [0xF4] 5 => True + +builtinReadBit [0xF4] 6 => True + +builtinReadBit [0xF4] 7 => True + +-- Out-of-bounds indexes fail +builtinReadBit [0xF4] 8 => error + +builtinReadBit [0xFF, 0xF4] 16 => error + +-- Larger indexes read backwards into the bytes from the end +builtinReadBit [0xF4, 0xFF] 10 => False +``` + #### `builtinSetBits` `builtinSetBits` takes two arguments: we name and describe them below. @@ -448,6 +580,86 @@ as the result of `builtinSetBits` with data argument $b_m$ and the change list argument $(i_{m + 1}, v_{m + 1})$; as this change list is a singleton, we can process it according to the description above. +Some examples of the intended behaviour of `builtinSetBits` follow. For +brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. + +``` +-- Writing an empty BuiltinByteString fails +builtinSetBits [] [(0, False)] => error + +-- Irrespective of index +builtinSetBits [] [(15, False)] => error + +-- And value +builtinSetBits [] [(0, True)] => error + +-- And multiplicity +builtinSetBits [] [(0, False), (1, False)] => error + +-- Negative indexes fail +builtinSetBits [0xFF] [((-1), False)] => error + +-- Even when mixed with valid ones +builtinSetBits [0xFF] [(0, False), ((-1), True)] => error + +-- In any position +builtinSetBits [0xFF] [((-1), True), (0, False)] => error + +-- Out-of-bounds indexes fail +builtinSetBits [0xFF] [(8, False)] => error + +-- Even when mixed with valid ones +builtinSetBits [0xFF] [(1, False), (8, False)] => error + +-- In any position +builtinSetBits [0xFF] [(8, False), (1, False)] => error + +-- Bits are written 'from the end' +builtinSetBits [0xFF] [(0, False)] => [0xFE] + +builtinSetBits [0xFF] [(1, False)] => [0xFD] + +builtinSetBits [0xFF] [(2, False)] => [0xFB] + +builtinSetBits [0xFF] [(3, False)] => [0xF7] + +builtinSetBits [0xFF] [(4, False)] => [0xEF] + +builtinSetBits [0xFF] [(5, False)] => [0xDF] + +builtinSetBits [0xFF] [(6, False)] => [0xBF] + +builtinSetBits [0xFF] [(7, False)] => [0x7F] + +-- True value sets the bit +builtinSetBits [0x00] [(5, True)] => [0x20] + +-- False value clears the bit +builtinSetBits [0xFF] [(5, False)] => [0xDF] + +-- Larger indexes write backwards into the bytes from the end +builtinSetBits [0xF4, 0xFF] [(10, True)] => [0xF0, 0xFF] + +-- Multiple items in a change list apply cumulatively +builtinSetBits [0xF4, 0xFF] [(10, True), (1, False)] => [0xF0, 0xFD] + +builtinSetBits (builtinSetBits [0xF4, 0xFF] [(10, True)]) [(1, False)] => [0xF0, 0xFD] + +-- Order within a changelist is unimportant among unique indexes +builtinSetBits [0xF4, 0xFF] [(1, False), (10, True)] => [0xF0, 0xFD] + +-- But _is_ important for identical indexes +builtinSetBits [0x00, 0xFF] [(10, True), (10, False)] => [0x00, 0xFF] + +builtinSetBits [0x00, 0xFF] [(10, False), (10, True)] => [0x04, 0xFF] + +-- Setting an already set bit does nothing +builtinSetBits [0xFF] [(0, True)] => [0xFF] + +-- Clearing an already clear bit does nothing +builtinSetBits [0x00] [(0, False)] => [0x00] +``` + #### `builtinReplicate` `builtinReplicate` takes two arguments; we name and describe them below. @@ -480,7 +692,33 @@ scheme](#bit-indexing-scheme). We have: * The length (in bytes) of $b$ is $n$; and * For all $i \in 0, 1, \ldots, n - 1$, $b\\{i\\} = w$. -### Laws and examples +Some examples of the intended behaviour of `builtinReplicate` follow. For +brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. + +``` +-- Replicating a negative number of times fails +builtinReplicate (-1) 0 => error + +-- Irrespective of byte argument +builtinReplicate (-1) 3 => error + +-- Out-of-bounds byte arguments fail +builtinReplicate 1 (-1) => error + +builtinReplicate 1 256 => error + +-- Irrespective of length argument +builtinReplicate 4 (-1) => error + +builtinReplicate 4 256 => error + +-- Length of result matches length argument, and all bytes are the same +builtinReplicate 0 0xFF => [] + +builtinReplicate 4 0xFF => [0xFF, 0xFF, 0xFF, 0xFF] +``` + +### Laws #### Binary operations @@ -675,8 +913,6 @@ Lastly, we have builtinSizeOfByteString (builtinReplicate n w) = n ``` -TODO: Examples - ## Rationale: how does this CIP achieve its goals? The operations, and semantics, described in this CIP provide a set of From a94c64ec66768935cb3e5635b2d2e4412c93d7ee Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Fri, 3 May 2024 12:28:58 +1200 Subject: [PATCH 14/32] Add hashing case --- CIP-XXX/CIP-XXX.md | 59 ++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 54 insertions(+), 5 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 4c8bef9c42..72fa0e9280 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -127,7 +127,45 @@ yield significant space savings in many cases. Given the limitations onchain that we have to work within, having such techniques available to implementers would be a huge potential advantage. -TODO: Another 1-2 example uses +### Case 2: hashing + +[Hashing][hashing], that is, computing a fixed-length 'fingerprint' or 'digest' +of a variable-length input (typically viewed as binary) is a common task +required in a range of applications. Most notably, hashing is a key tool in +cryptographic protocols and applications, either in its own right, or as part of +a larger task. The value of such functionality is such that Plutus Core already +contains primitives for certain hash functions, specifically two variants of +[SHA256][sha-256] and [BLAKE2b][blake2b]. At the same time, hash functions +choices are often determined by protocol or use case, and providing individual +primitives for every possible hash function is not a scalable choice. It is much +preferrable to give necessary tools to implement such functionality to users of +Plutus (Core), allowing them to use whichever hash function(s) their +applications require. + +As an example, we consider the [Argon2][argon2] family of hash functions. In +order to implement any of this family requires the following operations: + +1. Conversion of numbers to bytes +2. Bytestring concatenation +3. BLAKE2b hashing +4. Floor division +5. Indexing bytes in a bytestring +6. Logical XOR + +Operations 1 to 5 are already provided by Plutus Core (with 1 being included [in +a recent CIP][conversion-cip]); however, without logical XOR, no function in the +Argon2 family could be implemented. While in theory, it could be simulated with +what operations already exist, much as with Case 1, this would be impractical at +best, and outright impossible at worst, due to the severe limits imposed +on-chain. This is particularly the case here, as all Argon2 variants call +logical XOR in a loop, whose step count is defined by _multiple_ user-specified +(or protocol-specified) parameters. + +We observe that this requirement for logical XOR is not unique to the Argon2 +family of hash functions. Indeed, logical XOR is widely used for [a variety of +cryptographic applications][xor-crypto], as it is both a low-cost mixing +function that happens to be self-inverting, as well as preserving randomness +(that is, a random bit XORed with a non-random bit will give a random bit). ## Specification @@ -1117,13 +1155,19 @@ the bit ordering (in the place value sense) employed by all machine architectures for bytes in their sense as natural numbers within a fixed range. This was also the choice made by [CIP-58][cip-58], for similar reasons. +We also note that conversion agreement matters for Case 2, in the wider context +of the interaction between [conversion primitives][conversion-cip] and logical +XOR. The Argon2 family of hashes use certain inputs (which happen to be numbers) +both as numbers and also as blocks of binary, which means that any inconsistency +would cause strange (and possibly quite surprising) results when implementing +any of those functions. This once again suggests that our choice is the right +one, as it is the only one that would ensure conversion agreement. + While the bit-flip variant has the advantage of 'agreement' between byte and bit indexes, we believe that conversion agreement is the more important property to -have, not only for consistency with our described semantics, but also to some -extent for consistency with the conversion primitives [described in another -existing CIP][conversion-cip]. Given that the aforementioned CIP has already +have. Given that the [conversion primitives CIP][conversion-cip] has already been implemented into Plutus Core, we think that our choice is the only viable -one if consistency is desirable. +one in light of both this fact, and the Cases we have stated here. ### Padding versus truncation @@ -1345,3 +1389,8 @@ This CIP is licensed under [Apache-2.0](http://www.apache.org/licenses/LICENSE-2 [benchmarks-bits]: https://github.com/mlabs-haskell/plutus-integer-bytestring/blob/koz/logical/bench/naive/Main.hs#L74-L83 [vector]: https://hackage.haskell.org/package/vector-0.13.1.0/docs/Data-Vector.html#v:-47--47- [boolean-algebra-2]: https://en.wikipedia.org/wiki/Two-element_Boolean_algebra +[hashing]: https://en.wikipedia.org/wiki/Hash_function +[sha256]: https://en.wikipedia.org/wiki/Secure_Hash_Algorithms +[blake2b]: https://en.wikipedia.org/wiki/BLAKE_(hash_function) +[argon2]: https://en.wikipedia.org/wiki/Argon2 +[xor-crypto]: https://en.wikipedia.org/wiki/Exclusive_or#Bitwise_operation From 2b64b03d6f3ee1a0782ff9930a58ea32198b5d3e Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Fri, 3 May 2024 13:48:28 +1200 Subject: [PATCH 15/32] Typoes --- CIP-XXX/CIP-XXX.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 72fa0e9280..892bb031a3 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -9,7 +9,7 @@ Implementors: - Koz Ross Discussions: - https://github.com/cardano-foundation/CIPs/pull/? -Created: 2024-04-30 +Created: 2024-05-03 License: Apache-2.0 --- @@ -135,7 +135,7 @@ required in a range of applications. Most notably, hashing is a key tool in cryptographic protocols and applications, either in its own right, or as part of a larger task. The value of such functionality is such that Plutus Core already contains primitives for certain hash functions, specifically two variants of -[SHA256][sha-256] and [BLAKE2b][blake2b]. At the same time, hash functions +[SHA256][sha256] and [BLAKE2b][blake2b]. At the same time, hash functions choices are often determined by protocol or use case, and providing individual primitives for every possible hash function is not a scalable choice. It is much preferrable to give necessary tools to implement such functionality to users of @@ -143,7 +143,7 @@ Plutus (Core), allowing them to use whichever hash function(s) their applications require. As an example, we consider the [Argon2][argon2] family of hash functions. In -order to implement any of this family requires the following operations: +order to implement any variant of this family requires the following operations: 1. Conversion of numbers to bytes 2. Bytestring concatenation From 174996acce2150b3839b8dc06f859a3b73dfa607 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Fri, 3 May 2024 13:53:29 +1200 Subject: [PATCH 16/32] Add costings --- CIP-XXX/CIP-XXX.md | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 892bb031a3..84ffef94fc 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -172,9 +172,8 @@ function that happens to be self-inverting, as well as preserving randomness We describe the proposed operations in several stages. First, we specify a scheme for indexing individual bits (rather than whole bytes) in a `BuiltinByteString`. We then specify the semantics of each operation, as well as -giving costing expectations. Lastly, we provide some laws that these operations -are supposed to obey, as well as giving some specific examples of results from -the use of these operations. +giving costing expectations and some examples. Lastly, we provide some laws that +these operations are supposed to obey. ### Bit indexing scheme @@ -282,6 +281,18 @@ semantics. These operations will have the following signatures: BuiltinByteString` * `builtinReplicate :: BuiltinInteger -> BuiltinInteger -> BuiltinByteString` +For costing, we assume the following costing: + +| Operation | Cost | +|-----------|------| +| `builtinLogicalAnd` | Linear in longest `BuiltinByteString` argument | +| `builtinLogicalOr` | Linear in longest `BuiltinByteString` argument | +| `builtinLogicalXor` | Linear in longest `BuiltinByteString` argument | +| `builtinLogicalComplement` | Linear in `BuiltinByteString` argument | +| `builtinReadBit` | Constant | +| `builtinSetBits` | Additively linear in both arguments | +| `builtinReplicate` | Linear in the _value_ of the first argument | + #### Padding versus truncation semantics For the binary logical operations (that is, `builtinLogicalAnd`, From b8da94f614be94450e922ba0307fac11c434f2e4 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Fri, 3 May 2024 13:54:17 +1200 Subject: [PATCH 17/32] Wording --- CIP-XXX/CIP-XXX.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 84ffef94fc..b7cdbf8b32 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -173,7 +173,7 @@ We describe the proposed operations in several stages. First, we specify a scheme for indexing individual bits (rather than whole bytes) in a `BuiltinByteString`. We then specify the semantics of each operation, as well as giving costing expectations and some examples. Lastly, we provide some laws that -these operations are supposed to obey. +any implementation of these operations is expected to obey. ### Bit indexing scheme From f682790ee2bddda900d29dcfb89fe44267fb4f3a Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Fri, 3 May 2024 13:56:21 +1200 Subject: [PATCH 18/32] Typoes, wording --- CIP-XXX/CIP-XXX.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index b7cdbf8b32..08b86d899b 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -250,7 +250,7 @@ means we have $\left\lfloor\frac{133}{2^4}\right\rfloor \mod 2 \equiv 0$. Thus, $b[4] = 0$. Consider instead the index $i = 19$; by the definition above, this corresponds to the _byte_ index 0, as $\left\lfloor\frac{19}{8}\right\rfloor = 2$, and $3 - 2 - 1 = 0$. Within the byte $42$, this means we have -$\left\lfloor\frac{42}{2^3}\right\rfloor `mod 2 \equiv 1$. Thus, $b[19] = 1$. +$\left\lfloor\frac{42}{2^3}\right\rfloor\mod 2 \equiv 1$. Thus, $b[19] = 1$. Put another way, our _byte_ indexes run 'the opposite way' to our _bit_ indexes. Thus, for any `BuiltinByteString` of length $n$, we have _bit_ indexes relative @@ -281,7 +281,7 @@ semantics. These operations will have the following signatures: BuiltinByteString` * `builtinReplicate :: BuiltinInteger -> BuiltinInteger -> BuiltinByteString` -For costing, we assume the following costing: +We assume the following costing: | Operation | Cost | |-----------|------| @@ -595,7 +595,7 @@ indexing scheme](#bit-indexing-scheme) for the exact specification of this. If the change list argument is empty, the result is $b$. If the change list argument is a singleton, let $(i, v)$ refer to its only index-value pair. If $i -< 0$ or i \geq 8 \cdot n$, then `builtinSetBits` fails. In this case, the +< 0$ or $i \geq 8 \cdot n$, then `builtinSetBits` fails. In this case, the resulting error message must specify _at least_ the following information: * That `builtinSetBits` failed due to an out-of-bounds index argument; and @@ -619,7 +619,8 @@ of such processing. There are two possible outcomes for $b_m$: change list as that error. 2. A `BuiltinByteString`. -From here, when we refer to $b_m$, we refer to the `BuiltinByteString` option. +From here, when we refer to $b_m$, we refer to the `BuiltinByteString` outcome; +in the case of the first outcome, we simply 'forward' the result. We observe that any change list $C^{\prime}$ of length $m + 1$ will have the form of some other change list $C_m$, with an additional @@ -1186,7 +1187,7 @@ For the operations defined in this CIP taking two `BuiltinByteString` arguments (that is, `builtinLogicalAnd`, `builtinLogicalOr`, and `builtinLogicalXor`), when the two arguments have identical lengths, the semantics are natural, mirroring the corresponding operations on the -[Boolean algebra $\mathbb{2}^{8n}$][boolean-algebra-2], where $n$ is the length +[Boolean algebra][boolean-algebra-2] $\textbf{2}^{8n}$, where $n$ is the length of either argument in bytes. When the arguments do _not_ have matching lengths, however, the situation becomes more complex, as there are several ways in which we could define these operations. The most natural possibilities are as follows; From 8c7528e72ce960e13d9458dc750c15f70f2300c7 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Mon, 6 May 2024 06:50:12 +1200 Subject: [PATCH 19/32] Fix links to CIP-121, our implementation --- CIP-XXX/CIP-XXX.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 08b86d899b..3a75e12207 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -153,7 +153,7 @@ order to implement any variant of this family requires the following operations: 6. Logical XOR Operations 1 to 5 are already provided by Plutus Core (with 1 being included [in -a recent CIP][conversion-cip]); however, without logical XOR, no function in the +a CIP-121][conversion-cip]); however, without logical XOR, no function in the Argon2 family could be implemented. While in theory, it could be simulated with what operations already exist, much as with Case 1, this would be impractical at best, and outright impossible at worst, due to the severe limits imposed @@ -1125,7 +1125,7 @@ that, given a `BuiltinByteString` that is non-empty, if we were to get the values at bit indexes $0$ through $7$, and treat them as their corresponding place value in a summation, we should obtain the same answer as indexing whichever byte those bits come from. We call this notion _conversion agreement_, -due to its relation to [an existing CIP][conversion-cip], which allows us to +due to its relation to [CIP-121][conversion-cip], which allows us to (essentially) view a `BuiltinByteString` as a natural number in base-256. Indeed, the case is analogous, with the only difference being that we are concerned with the positioning of base-256 digits, not binary ones. @@ -1168,7 +1168,7 @@ architectures for bytes in their sense as natural numbers within a fixed range. This was also the choice made by [CIP-58][cip-58], for similar reasons. We also note that conversion agreement matters for Case 2, in the wider context -of the interaction between [conversion primitives][conversion-cip] and logical +of the interaction between [CIP-121 primitives][conversion-cip] and logical XOR. The Argon2 family of hashes use certain inputs (which happen to be numbers) both as numbers and also as blocks of binary, which means that any inconsistency would cause strange (and possibly quite surprising) results when implementing @@ -1177,7 +1177,7 @@ one, as it is the only one that would ensure conversion agreement. While the bit-flip variant has the advantage of 'agreement' between byte and bit indexes, we believe that conversion agreement is the more important property to -have. Given that the [conversion primitives CIP][conversion-cip] has already +have. Given that the [CIP-121][conversion-cip] has already been implemented into Plutus Core, we think that our choice is the only viable one in light of both this fact, and the Cases we have stated here. @@ -1252,7 +1252,7 @@ an option. All the above suggests that no _single_ choice of semantics will satisfy all reasonable needs, if only from the point of view of efficiency. This suggests, -much as for [conversion primitives][conversion-cip] and endianness issues, that +much as for [CIP-121 primitives][conversion-cip] and endianness issues, that the primitive should allow a choice in what semantics get used for any given call. Ideally, we would allow a choice of any of the three options described above; however, this is awkward to do in Plutus Core. While the choice between @@ -1397,8 +1397,8 @@ This CIP is licensed under [Apache-2.0](http://www.apache.org/licenses/LICENSE-2 [cip-58]: https://github.com/cardano-foundation/CIPs/tree/master/CIP-0058 [croaring]: https://github.com/RoaringBitmap/CRoaring [too-many-ways-1]: https://fgiesen.wordpress.com/2018/02/19/reading-bits-in-far-too-many-ways-part-1 -[conversion-cip]: https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-XXXX -[benchmarks-bits]: https://github.com/mlabs-haskell/plutus-integer-bytestring/blob/koz/logical/bench/naive/Main.hs#L74-L83 +[conversion-cip]: https://github.com/mlabs-haskell/CIPs/blob/koz/to-from-bytestring/CIP-0121/README.md +[benchmarks-bits]: https://github.com/mlabs-haskell/plutus-integer-bytestring/blob/main/bench/naive/Main.hs#L74-L83 [vector]: https://hackage.haskell.org/package/vector-0.13.1.0/docs/Data-Vector.html#v:-47--47- [boolean-algebra-2]: https://en.wikipedia.org/wiki/Two-element_Boolean_algebra [hashing]: https://en.wikipedia.org/wiki/Hash_function From a6268ba93f8bd71443893bdeea91b369f8470973 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Thu, 16 May 2024 10:44:57 +1200 Subject: [PATCH 20/32] Note that costing is for both time and memory --- CIP-XXX/CIP-XXX.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 3a75e12207..2d129e322f 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -281,7 +281,7 @@ semantics. These operations will have the following signatures: BuiltinByteString` * `builtinReplicate :: BuiltinInteger -> BuiltinInteger -> BuiltinByteString` -We assume the following costing: +We assume the following costing, for both memory and execution time: | Operation | Cost | |-----------|------| From 72552ec3c1f146c9bdb60ebbe07a2f9fcceb8a25 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Thu, 16 May 2024 10:46:28 +1200 Subject: [PATCH 21/32] Fix typo in bit setting description --- CIP-XXX/CIP-XXX.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 2d129e322f..87cf2fad6b 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -605,8 +605,8 @@ Otherwise, for all $j \in 0, 1, \ldots 8 \cdot n - 1$, we have $$ b_r[j] = \begin{cases} - 0 & \text{if } j = i \text{ and } b = \texttt{False}\\ - 1 & \text{if } j = i \text{ and } b = \texttt{True}\\ + 0 & \text{if } j = i \text{ and } v = \texttt{False}\\ + 1 & \text{if } j = i \text{ and } v = \texttt{True}\\ b[j] & \text{otherwise}\\ \end{cases} $$ From 5992efb46973186d3c3ff2edef5585a270e51797 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Thu, 16 May 2024 11:11:27 +1200 Subject: [PATCH 22/32] Clarify relationship to CIPs 58 and 121 --- CIP-XXX/CIP-XXX.md | 47 +++++++++++++++++++++++++++++++++++++--------- 1 file changed, 38 insertions(+), 9 deletions(-) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-XXX/CIP-XXX.md index 87cf2fad6b..67d75c650b 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-XXX/CIP-XXX.md @@ -987,6 +987,20 @@ implementation in [CIP-58][cip-58], and `builtinReplicate` is a direct wrapper around the `replicate` function in `ByteString`. Thus, we do not discuss them further here. +### Relationship to CIP-58 and CIP-121 + +Our work relates to both [CIP-58][cip-58] and [CIP-121][cip-121]. Essentially, +our goal with both this CIP and CIP-121 is to both break CIP-58 into more +manageable (and reviewable) parts, and also address some of the design choices +in CIP-58 that were not as good (or as clear) as they could have been. In this +regard, this CIP is a direct continuation of CIP-121; CIP-121 dealt with +conversions between `BuiltinByteString` and `BuiltinInteger`, while this CIP +handles bit indexing more generally, as well as 'parallel' logical operations +that operate on all the bits of a `BuiltinByteString` in bulk. + +We describe how our work in this CIP relates to (and in some cases, supercedes) +CIP-58, as well as how it follows on from CIP-121, in more detail below. + ### Bit indexing scheme The bit indexing scheme we describe here is designed around two @@ -1126,9 +1140,12 @@ values at bit indexes $0$ through $7$, and treat them as their corresponding place value in a summation, we should obtain the same answer as indexing whichever byte those bits come from. We call this notion _conversion agreement_, due to its relation to [CIP-121][conversion-cip], which allows us to -(essentially) view a `BuiltinByteString` as a natural number in base-256. -Indeed, the case is analogous, with the only difference being that we are -concerned with the positioning of base-256 digits, not binary ones. +(essentially) view a `BuiltinByteString` as a natural number in base-256. While +CIP-121 allows two different views of a natural number (specifically, whether +the first _byte_ index corresponds to the highest or the lowest place value), +our case applies equally in both situations (as described below). The only difference +in our case is that we are concerned with the positioning of binary digits, not +base-256 ones. Consider the `BuiltinByteString` whose only byte is $42$, whose representation is as follows: @@ -1139,6 +1156,11 @@ is as follows: | Byte | 00101010 | ``` +Indeed, if we used the CIP-121 conversion primitive +[`builtinByteStringToInteger`](https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-0121#builtinbytestringtointeger) +to convert it to its `BuiltinInteger` equivalent, this is the answer we would +get, regardless of which digit arrangement we choose. + Under the bit-flip variant, our bit indexes would be as follows: ``` @@ -1170,10 +1192,16 @@ This was also the choice made by [CIP-58][cip-58], for similar reasons. We also note that conversion agreement matters for Case 2, in the wider context of the interaction between [CIP-121 primitives][conversion-cip] and logical XOR. The Argon2 family of hashes use certain inputs (which happen to be numbers) -both as numbers and also as blocks of binary, which means that any inconsistency -would cause strange (and possibly quite surprising) results when implementing -any of those functions. This once again suggests that our choice is the right -one, as it is the only one that would ensure conversion agreement. +both as numbers (meaning, arithmetic operations), and also as blocks of binary +(meaning, XOR operations specifically). This is common in a range of +applications that rely on bitwise operations, both in cryptography and +elsewhere, whether for performance, functionality, or both. In such situations, +users of the primitives, and in our specific case, conversions, must be +confident that their changes 'translate' in the way they expect between these +two 'views' of the data. This once again suggests that our choice is the right +one, as it is the only one that would ensure conversion agreement. While some +care would be needed in multi-byte cases, as only most-significant-first +conversions maintain this behaviour, this is not difficult to remember. While the bit-flip variant has the advantage of 'agreement' between byte and bit indexes, we believe that conversion agreement is the more important property to @@ -1315,8 +1343,9 @@ justified as in the `builtinSetBits` case, for several reasons. Firstly, for `builtinLogicalComplement`, it's not even clear what benefit this would have at all: the only possible signature such an operation would have is `[BuiltinByteString] -> [BuiltinByteString]`, which in effect would be a -specialized form of mapping. Even the _general_ form of mapping is not -considered suitable as a primitive operation in Plutus Core! +specialized form of mapping. While an argument could be made for a _general_ +form of mapping as a Plutus Core primitive, it wouldn't be reasonable for an +operation like this to be considered for such. Secondly, the benefits to performance wouldn't be nearly as significant in theory, and likely From ed91288fe138b826456ed6f0271b857af735ba5f Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Mon, 20 May 2024 08:23:13 +1200 Subject: [PATCH 23/32] Now CIP 122 --- CIP-XXX/CIP-XXX.md => CIP-0122/CIP-0122.md | 4 ++-- README.md | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) rename CIP-XXX/CIP-XXX.md => CIP-0122/CIP-0122.md (99%) diff --git a/CIP-XXX/CIP-XXX.md b/CIP-0122/CIP-0122.md similarity index 99% rename from CIP-XXX/CIP-XXX.md rename to CIP-0122/CIP-0122.md index 67d75c650b..67ce67ef1c 100644 --- a/CIP-XXX/CIP-XXX.md +++ b/CIP-0122/CIP-0122.md @@ -1,5 +1,5 @@ --- -CIP: ??? +CIP: 122 Title: Logical operations Category: Plutus Status: Proposed @@ -8,7 +8,7 @@ Authors: Implementors: - Koz Ross Discussions: - - https://github.com/cardano-foundation/CIPs/pull/? + - https://github.com/cardano-foundation/CIPs/pull/806 Created: 2024-05-03 License: Apache-2.0 --- diff --git a/README.md b/README.md index 1812ff6c16..0b709ae9b7 100644 --- a/README.md +++ b/README.md @@ -101,6 +101,7 @@ CIP Editors meetings are public, recorded, and [published on Youtube](https://ww | 0110 | [Plutus v1 compatible script references](./CIP-0110) | Proposed | | 0114 | [CBOR Tags Registry](./CIP-0114) | Proposed | | 0115 | [CBOR tag definition - ED25519-BIP32 Keys](./CIP-0115) | Proposed | +| 0122 | [Logical operations](./CIP-0122) | Proposed | | 0381 | [Plutus Support for Pairings Over BLS12-381](./CIP-0381) | Proposed | | 1694 | [A proposal for entering the Voltaire phase](./CIP-1694) | Proposed | | 1852 | [HD (Hierarchy for Deterministic) Wallets for Cardano](./CIP-1852/) | Active | From 413f5aab5ecc356ea03d8c02647f0c4d92698e9b Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Mon, 20 May 2024 10:03:36 +1200 Subject: [PATCH 24/32] Rename operations to match the Plutus Core PR --- CIP-0122/CIP-0122.md | 489 +++++++++++++++++++++---------------------- 1 file changed, 244 insertions(+), 245 deletions(-) diff --git a/CIP-0122/CIP-0122.md b/CIP-0122/CIP-0122.md index 67ce67ef1c..5259867fed 100644 --- a/CIP-0122/CIP-0122.md +++ b/CIP-0122/CIP-0122.md @@ -153,7 +153,7 @@ order to implement any variant of this family requires the following operations: 6. Logical XOR Operations 1 to 5 are already provided by Plutus Core (with 1 being included [in -a CIP-121][conversion-cip]); however, without logical XOR, no function in the +CIP-121][conversion-cip]); however, without logical XOR, no function in the Argon2 family could be implemented. While in theory, it could be simulated with what operations already exist, much as with Case 1, this would be impractical at best, and outright impossible at worst, due to the severe limits imposed @@ -163,7 +163,7 @@ logical XOR in a loop, whose step count is defined by _multiple_ user-specified We observe that this requirement for logical XOR is not unique to the Argon2 family of hash functions. Indeed, logical XOR is widely used for [a variety of -cryptographic applications][xor-crypto], as it is both a low-cost mixing +cryptographic applications][xor-crypto], as it is a low-cost mixing function that happens to be self-inverting, as well as preserving randomness (that is, a random bit XORed with a non-random bit will give a random bit). @@ -269,34 +269,34 @@ _byte_ indexes as follows: We describe precisely the operations we intend to implement, and their semantics. These operations will have the following signatures: -* `builtinLogicalAnd :: BuiltinBool -> BuiltinByteString -> BuiltinByteString -> +* `bitwiseLogicalAnd :: BuiltinBool -> BuiltinByteString -> BuiltinByteString -> BuiltinByteString` -* `builtinLogicalOr :: BuiltinBool -> BuiltinByteString -> BuiltinByteString -> +* `bitwiseLogicalOr :: BuiltinBool -> BuiltinByteString -> BuiltinByteString -> BuiltinByteString` -* `builtinLogicalXor :: BuiltinBool -> BuiltinByteString -> BuiltinByteString -> +* `bitwiseLogicalXor :: BuiltinBool -> BuiltinByteString -> BuiltinByteString -> BuiltinByteString` -* `builtinLogicalComplement :: BuiltinByteString -> BuiltinByteString` -* `builtinReadBit :: BuiltinByteString -> BuiltinInteger -> BuiltinBool` -* `builtinSetBits :: BuiltinByteString -> [(BuiltinInteger, BuiltinBool)] -> +* `bitwiseLogicalComplement :: BuiltinByteString -> BuiltinByteString` +* `readBit :: BuiltinByteString -> BuiltinInteger -> BuiltinBool` +* `writeBits :: BuiltinByteString -> [(BuiltinInteger, BuiltinBool)] -> BuiltinByteString` -* `builtinReplicate :: BuiltinInteger -> BuiltinInteger -> BuiltinByteString` +* `replicateByteString :: BuiltinInteger -> BuiltinInteger -> BuiltinByteString` We assume the following costing, for both memory and execution time: | Operation | Cost | |-----------|------| -| `builtinLogicalAnd` | Linear in longest `BuiltinByteString` argument | -| `builtinLogicalOr` | Linear in longest `BuiltinByteString` argument | -| `builtinLogicalXor` | Linear in longest `BuiltinByteString` argument | -| `builtinLogicalComplement` | Linear in `BuiltinByteString` argument | -| `builtinReadBit` | Constant | -| `builtinSetBits` | Additively linear in both arguments | -| `builtinReplicate` | Linear in the _value_ of the first argument | +| `bitwiseLogicalAnd` | Linear in longest `BuiltinByteString` argument | +| `bitwiseLogicalOr` | Linear in longest `BuiltinByteString` argument | +| `bitwiseLogicalXor` | Linear in longest `BuiltinByteString` argument | +| `bitwiseLogicalComplement` | Linear in `BuiltinByteString` argument | +| `readBit` | Constant | +| `writeBits` | Additively linear in both arguments | +| `replicateByteString` | Linear in the _value_ of the first argument | #### Padding versus truncation semantics -For the binary logical operations (that is, `builtinLogicalAnd`, -`builtinLogicalOr` and `builtinLogicalXor`), the we have two choices of +For the binary logical operations (that is, `bitwiseLogicalAnd`, +`bitwiseLogicalOr` and `bitwiseLogicalXor`), the we have two choices of semantics when handling `BuiltinByteString` arguments of different lengths. We can either produce a result whose length is the _minimum_ of the two arguments (which we call _truncation semantics_), or produce a result whose length is the @@ -305,14 +305,14 @@ both be useful depending on context, we allow both, controlled by a `BuiltinBool` flag, on all the operations listed above. For example, consider the `BuiltinByteString`s `x = [0x00, 0xF0, 0xFF]` and `y = -[0xFF, 0xF0]`. Under padding semantics, the result of `builtinLogicalAnd`, -`builtinLogicalOr` or `builtinLogicalXor` using these two as arguments would +[0xFF, 0xF0]`. Under padding semantics, the result of `bitwiseLogicalAnd`, +`bitwiseLogicalOr` or `bitwiseLogicalXor` using these two as arguments would have a length of 3; under truncation semantics, the result would have a length of 2 instead. -#### `builtinLogicalAnd` +#### `bitwiseLogicalAnd` -`builtinLogicalAnd` takes three arguments; we name and describe them below. +`bitwiseLogicalAnd` takes three arguments; we name and describe them below. 1. Whether padding semantics should be used. If this argument is `False`, truncation semantics are used instead. This is the _padding semantics @@ -322,7 +322,7 @@ of 2 instead. Let $b_1, b_2$ refer to the first data argument and the second data argument respectively, and let $n_1, n_2$ be their respective lengths in bytes. -Let the result of `builtinLogicalAnd`, given $b_1, b_2$ and some padding +Let the result of `bitwiseLogicalAnd`, given $b_1, b_2$ and some padding semantics argument, be $b_r$, of length $n_r$ in bytes. We use $b_1[i]$ to refer to the value at index $i$ of $b_1$ (and analogously for $b_2, b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) @@ -341,36 +341,36 @@ b_r[i] = \begin{cases} \end{cases} $$ -Some examples of the intended behaviour of `builtinLogicalAnd` follow. For +Some examples of the intended behaviour of `bitwiseLogicalAnd` follow. For brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. ``` -- truncation semantics -builtinLogicalAnd False [] [0xFF] => [] +bitwiseLogicalAnd False [] [0xFF] => [] -builtinLogicalAnd False [0xFF] [] => [] +bitwiseLogicalAnd False [0xFF] [] => [] -builtinLogicalAnd False [0xFF] [0x00] => [0x00] +bitwiseLogicalAnd False [0xFF] [0x00] => [0x00] -builtinLogicalAnd False [0x00] [0xFF] => [0x00] +bitwiseLogicalAnd False [0x00] [0xFF] => [0x00] -builtinLogicalAnd False [0x4F, 0x00] [0xF4] => [0x44] +bitwiseLogicalAnd False [0x4F, 0x00] [0xF4] => [0x44] -- padding semantics -builtinLogicalAnd True [] [0xFF] => [0xFF] +bitwiseLogicalAnd True [] [0xFF] => [0xFF] -builtinLogicalAnd True [0xFF] [] => [0xFF] +bitwiseLogicalAnd True [0xFF] [] => [0xFF] -builtinLogicalAnd False [0xFF] [0x00] => [0x00] +bitwiseLogicalAnd False [0xFF] [0x00] => [0x00] -builtinLogicalAnd False [0x00] [0xFF] => [0x00] +bitwiseLogicalAnd False [0x00] [0xFF] => [0x00] -builtinLogicalAnd False [0x4F, 0x00] [0xF4] => [0x44, 0x00] +bitwiseLogicalAnd False [0x4F, 0x00] [0xF4] => [0x44, 0x00] ``` -#### `builtinLogicalOr` +#### `bitwiseLogicalOr` -`builtinLogicalOr` takes three arguments; we name and describe them below. +`bitwiseLogicalOr` takes three arguments; we name and describe them below. 1. Whether padding semantics should be used. If this argument is `False`, truncation semantics are used instead. This is the _padding semantics @@ -380,7 +380,7 @@ builtinLogicalAnd False [0x4F, 0x00] [0xF4] => [0x44, 0x00] Let $b_1, b_2$ refer to the first data argument and the second data argument respectively, and let $n_1, n_2$ be their respective lengths in bytes. -Let the result of `builtinLogicalOr`, given $b_1, b_2$ and some padding +Let the result of `bitwiseLogicalOr`, given $b_1, b_2$ and some padding semantics argument, be $b_r$, of length $n_r$ in bytes. We use $b_1[i]$ to refer to the value at index $i$ of $b_1$ (and analogously for $b_2, b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) @@ -399,36 +399,36 @@ b_r[i] = \begin{cases} \end{cases} $$ -Some examples of the intended behaviour of `builtinLogicalOr` follow. For +Some examples of the intended behaviour of `bitwiseLogicalOr` follow. For brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. ``` -- truncation semantics -builtinLogicalOr False [] [0xFF] => [] +bitwiseLogicalOr False [] [0xFF] => [] -builtinLogicalOr False [0xFF] [] => [] +bitwiseLogicalOr False [0xFF] [] => [] -builtinLogicalOr False [0xFF] [0x00] => [0xFF] +bitwiseLogicalOr False [0xFF] [0x00] => [0xFF] -builtinLogicalOr False [0x00] [0xFF] => [0xFF] +bitwiseLogicalOr False [0x00] [0xFF] => [0xFF] -builtinLogicalOr False [0x4F, 0x00] [0xF4] => [0xFF] +bitwiseLogicalOr False [0x4F, 0x00] [0xF4] => [0xFF] -- padding semantics -builtinLogicalOr True [] [0xFF] => [0xFF] +bitwiseLogicalOr True [] [0xFF] => [0xFF] -builtinLogicalOr True [0xFF] [] => [0xFF] +bitwiseLogicalOr True [0xFF] [] => [0xFF] -builtinLogicalOr False [0xFF] [0x00] => [0xFF] +bitwiseLogicalOr False [0xFF] [0x00] => [0xFF] -builtinLogicalOr False [0x00] [0xFF] => [0xFF] +bitwiseLogicalOr False [0x00] [0xFF] => [0xFF] -builtinLogicalOr False [0x4F, 0x00] [0xF4] => [0xFF, 0x00] +bitwiseLogicalOr False [0x4F, 0x00] [0xF4] => [0xFF, 0x00] ``` -#### `builtinLogicalXor` +#### `bitwiseLogicalXor` -`builtinLogicalXor` takes three arguments; we name and describe them below. +`bitwiseLogicalXor` takes three arguments; we name and describe them below. 1. Whether padding semantics should be used. If this argument is `False`, truncation semantics are used instead. This is the _padding semantics @@ -438,7 +438,7 @@ builtinLogicalOr False [0x4F, 0x00] [0xF4] => [0xFF, 0x00] Let $b_1, b_2$ refer to the first data argument and the second data argument respectively, and let $n_1, n_2$ be their respective lengths in bytes. -Let the result of `builtinLogicalXor`, given $b_1, b_2$ and some padding +Let the result of `bitwiseLogicalXor`, given $b_1, b_2$ and some padding semantics argument, be $b_r$, of length $n_r$ in bytes. We use $b_1[i]$ to refer to the value at index $i$ of $b_1$ (and analogously for $b_2, b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) @@ -457,38 +457,38 @@ b_r[i] = \begin{cases} \end{cases} $$ -Some examples of the intended behaviour of `builtinLogicalXor` follow. For +Some examples of the intended behaviour of `bitwiseLogicalXor` follow. For brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. ``` -- truncation semantics -builtinLogicalXor False [] [0xFF] => [] +bitwiseLogicalXor False [] [0xFF] => [] -builtinLogicalXor False [0xFF] [] => [] +bitwiseLogicalXor False [0xFF] [] => [] -builtinLogicalXor False [0xFF] [0x00] => [0xFF] +bitwiseLogicalXor False [0xFF] [0x00] => [0xFF] -builtinLogicalXor False [0x00] [0xFF] => [0xFF] +bitwiseLogicalXor False [0x00] [0xFF] => [0xFF] -builtinLogicalXor False [0x4F, 0x00] [0xF4] => [0xBB] +bitwiseLogicalXor False [0x4F, 0x00] [0xF4] => [0xBB] -- padding semantics -builtinLogicalOr True [] [0xFF] => [0xFF] +bitwiseLogicalOr True [] [0xFF] => [0xFF] -builtinLogicalOr True [0xFF] [] => [0xFF] +bitwiseLogicalOr True [0xFF] [] => [0xFF] -builtinLogicalOr False [0xFF] [0x00] => [0xFF] +bitwiseLogicalOr False [0xFF] [0x00] => [0xFF] -builtinLogicalOr False [0x00] [0xFF] => [0xFF] +bitwiseLogicalOr False [0x00] [0xFF] => [0xFF] -builtinLogicalOr False [0x4F, 0x00] [0xF4] => [0xBB, 0x00] +bitwiseLogicalOr False [0x4F, 0x00] [0xF4] => [0xBB, 0x00] ``` -#### `builtinLogicalComplement` +#### `bitwiseLogicalComplement` -`builtinLogicalComplement` takes a single argument, of type `BuiltinByteString`; +`bitwiseLogicalComplement` takes a single argument, of type `BuiltinByteString`; let $b$ refer to that argument, and $n$ its length in bytes. Let $b_r$ be -the result of `builtinLogicalComplement`; its length in bytes is also $n$. We +the result of `bitwiseLogicalComplement`; its length in bytes is also $n$. We use $b[i]$ to refer to the value at index $i$ of $b$ (and analogously for $b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) for the exact specification of this. @@ -502,20 +502,20 @@ b_r[i] = \begin{cases} \end{cases} $$ -Some examples of the intended behaviour of `builtinLogicalComplement` follow. For +Some examples of the intended behaviour of `bitwiseLogicalComplement` follow. For brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. ``` -builtinLogicalComplement [] => [] +bitwiseLogicalComplement [] => [] -builtinLogicalComplement [0x0F] => [0xF0] +bitwiseLogicalComplement [0x0F] => [0xF0] -builtinLogicalComplement [0x4F, 0xF4] => [0xB0, 0x0B] +bitwiseLogicalComplement [0x4F, 0xF4] => [0xB0, 0x0B] ``` -#### `builtinReadBit` +#### `readBit` -`builtinReadBit` takes two arguments; we name and describe them below. +`readBit` takes two arguments; we name and describe them below. 1. The `BuiltinByteString` in which the bit we want to read can be found. This is the _data argument_. @@ -527,59 +527,59 @@ the index argument. We use $b[i]$ to refer to the value at index $i$t of $b$; se the [section on the bit indexing scheme](#bit-indexing-scheme) for the exact specification of this. -If $i < 0$ or $i \geq 8 \cdot n$, then `builtinReadBit` +If $i < 0$ or $i \geq 8 \cdot n$, then `readBit` fails. In this case, the resulting error message must specify _at least_ the following information: -* That `builtinReadBit` failed due to an out-of-bounds index argument; and +* That `readBit` failed due to an out-of-bounds index argument; and * What `BuiltinInteger` was passed as an index argument. -Otherwise, if $b[i] = 0$, `builtinReadBit` returns `False`, and if $b[i] = 1$, -`builtinReadBit` returns `True`. +Otherwise, if $b[i] = 0$, `readBit` returns `False`, and if $b[i] = 1$, +`readBit` returns `True`. -Some examples of the intended behaviour of `builtinReadBit` follow. For +Some examples of the intended behaviour of `readBit` follow. For brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. ``` -- Indexing an empty BuiltinByteString fails -builtinReadBit [] 0 => error +readBit [] 0 => error -builtinReadBit [] 345 => error +readBit [] 345 => error -- Negative indexes fail -builtinReadBit [] (-1) => error +readBit [] (-1) => error -builtinReadBit [0xFF] (-1) => error +readBit [0xFF] (-1) => error -- Indexing reads 'from the end' -builtinReadBit [0xF4] 0 => False +readBit [0xF4] 0 => False -builtinReadBit [0xF4] 1 => False +readBit [0xF4] 1 => False -builtinReadBit [0xF4] 2 => True +readBit [0xF4] 2 => True -builtinReadBit [0xF4] 3 => False +readBit [0xF4] 3 => False -builtinReadBit [0xF4] 4 => True +readBit [0xF4] 4 => True -builtinReadBit [0xF4] 5 => True +readBit [0xF4] 5 => True -builtinReadBit [0xF4] 6 => True +readBit [0xF4] 6 => True -builtinReadBit [0xF4] 7 => True +readBit [0xF4] 7 => True -- Out-of-bounds indexes fail -builtinReadBit [0xF4] 8 => error +readBit [0xF4] 8 => error -builtinReadBit [0xFF, 0xF4] 16 => error +readBit [0xFF, 0xF4] 16 => error -- Larger indexes read backwards into the bytes from the end -builtinReadBit [0xF4, 0xFF] 10 => False +readBit [0xF4, 0xFF] 10 => False ``` -#### `builtinSetBits` +#### `writeBits` -`builtinSetBits` takes two arguments: we name and describe them below. +`writeBits` takes two arguments: we name and describe them below. 1. The `BuiltinByteString` in which we want to change some bits. This is the _data argument_. @@ -589,16 +589,16 @@ builtinReadBit [0xF4, 0xFF] 10 => False Let $C = (i_1, v_1), (i_2, v_2), \ldots , (i_k, v_k)$ refer to the change list argument, and $b$ the data argument of length $n$ in bytes. Let $b_r$ be the -result of `builtinSetBits`, whose length is also $n$. We use $b[i]$ to refer to +result of `writeBits`, whose length is also $n$. We use $b[i]$ to refer to the value at index $i$ of $b$ (and analogously, $b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) for the exact specification of this. If the change list argument is empty, the result is $b$. If the change list argument is a singleton, let $(i, v)$ refer to its only index-value pair. If $i -< 0$ or $i \geq 8 \cdot n$, then `builtinSetBits` fails. In this case, the +< 0$ or $i \geq 8 \cdot n$, then `writeBits` fails. In this case, the resulting error message must specify _at least_ the following information: -* That `builtinSetBits` failed due to an out-of-bounds index argument; and +* That `writeBits` failed due to an out-of-bounds index argument; and * What `BuiltinInteger` was passed as the index part of the index-value pair. Otherwise, for all $j \in 0, 1, \ldots 8 \cdot n - 1$, we have @@ -615,7 +615,7 @@ if the change list argument is longer than a singleton, suppose that we can process a change list argument of length $1 \leq m$, and let $b_m$ be the result of such processing. There are two possible outcomes for $b_m$: -1. An error. In this case, we define the result of `builtinSetBits` on such a +1. An error. In this case, we define the result of `writeBits` on such a change list as that error. 2. A `BuiltinByteString`. @@ -625,94 +625,94 @@ in the case of the first outcome, we simply 'forward' the result. We observe that any change list $C^{\prime}$ of length $m + 1$ will have the form of some other change list $C_m$, with an additional element $(i_{m + 1}, v_{m + 1})$ at the end. We define the result of -`builtinSetBits` with data argument $b$ and change list argument $C^{\prime}$ -as the result of `builtinSetBits` with data argument $b_m$ and the change list +`writeBits` with data argument $b$ and change list argument $C^{\prime}$ +as the result of `writeBits` with data argument $b_m$ and the change list argument $(i_{m + 1}, v_{m + 1})$; as this change list is a singleton, we can process it according to the description above. -Some examples of the intended behaviour of `builtinSetBits` follow. For +Some examples of the intended behaviour of `writeBits` follow. For brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. ``` -- Writing an empty BuiltinByteString fails -builtinSetBits [] [(0, False)] => error +writeBits [] [(0, False)] => error -- Irrespective of index -builtinSetBits [] [(15, False)] => error +writeBits [] [(15, False)] => error -- And value -builtinSetBits [] [(0, True)] => error +writeBits [] [(0, True)] => error -- And multiplicity -builtinSetBits [] [(0, False), (1, False)] => error +writeBits [] [(0, False), (1, False)] => error -- Negative indexes fail -builtinSetBits [0xFF] [((-1), False)] => error +writeBits [0xFF] [((-1), False)] => error -- Even when mixed with valid ones -builtinSetBits [0xFF] [(0, False), ((-1), True)] => error +writeBits [0xFF] [(0, False), ((-1), True)] => error -- In any position -builtinSetBits [0xFF] [((-1), True), (0, False)] => error +writeBits [0xFF] [((-1), True), (0, False)] => error -- Out-of-bounds indexes fail -builtinSetBits [0xFF] [(8, False)] => error +writeBits [0xFF] [(8, False)] => error -- Even when mixed with valid ones -builtinSetBits [0xFF] [(1, False), (8, False)] => error +writeBits [0xFF] [(1, False), (8, False)] => error -- In any position -builtinSetBits [0xFF] [(8, False), (1, False)] => error +writeBits [0xFF] [(8, False), (1, False)] => error -- Bits are written 'from the end' -builtinSetBits [0xFF] [(0, False)] => [0xFE] +writeBits [0xFF] [(0, False)] => [0xFE] -builtinSetBits [0xFF] [(1, False)] => [0xFD] +writeBits [0xFF] [(1, False)] => [0xFD] -builtinSetBits [0xFF] [(2, False)] => [0xFB] +writeBits [0xFF] [(2, False)] => [0xFB] -builtinSetBits [0xFF] [(3, False)] => [0xF7] +writeBits [0xFF] [(3, False)] => [0xF7] -builtinSetBits [0xFF] [(4, False)] => [0xEF] +writeBits [0xFF] [(4, False)] => [0xEF] -builtinSetBits [0xFF] [(5, False)] => [0xDF] +writeBits [0xFF] [(5, False)] => [0xDF] -builtinSetBits [0xFF] [(6, False)] => [0xBF] +writeBits [0xFF] [(6, False)] => [0xBF] -builtinSetBits [0xFF] [(7, False)] => [0x7F] +writeBits [0xFF] [(7, False)] => [0x7F] -- True value sets the bit -builtinSetBits [0x00] [(5, True)] => [0x20] +writeBits [0x00] [(5, True)] => [0x20] -- False value clears the bit -builtinSetBits [0xFF] [(5, False)] => [0xDF] +writeBits [0xFF] [(5, False)] => [0xDF] -- Larger indexes write backwards into the bytes from the end -builtinSetBits [0xF4, 0xFF] [(10, True)] => [0xF0, 0xFF] +writeBits [0xF4, 0xFF] [(10, True)] => [0xF0, 0xFF] -- Multiple items in a change list apply cumulatively -builtinSetBits [0xF4, 0xFF] [(10, True), (1, False)] => [0xF0, 0xFD] +writeBits [0xF4, 0xFF] [(10, True), (1, False)] => [0xF0, 0xFD] -builtinSetBits (builtinSetBits [0xF4, 0xFF] [(10, True)]) [(1, False)] => [0xF0, 0xFD] +writeBits (writeBits [0xF4, 0xFF] [(10, True)]) [(1, False)] => [0xF0, 0xFD] -- Order within a changelist is unimportant among unique indexes -builtinSetBits [0xF4, 0xFF] [(1, False), (10, True)] => [0xF0, 0xFD] +writeBits [0xF4, 0xFF] [(1, False), (10, True)] => [0xF0, 0xFD] -- But _is_ important for identical indexes -builtinSetBits [0x00, 0xFF] [(10, True), (10, False)] => [0x00, 0xFF] +writeBits [0x00, 0xFF] [(10, True), (10, False)] => [0x00, 0xFF] -builtinSetBits [0x00, 0xFF] [(10, False), (10, True)] => [0x04, 0xFF] +writeBits [0x00, 0xFF] [(10, False), (10, True)] => [0x04, 0xFF] -- Setting an already set bit does nothing -builtinSetBits [0xFF] [(0, True)] => [0xFF] +writeBits [0xFF] [(0, True)] => [0xFF] -- Clearing an already clear bit does nothing -builtinSetBits [0x00] [(0, False)] => [0x00] +writeBits [0x00] [(0, False)] => [0x00] ``` -#### `builtinReplicate` +#### `replicateByteString` -`builtinReplicate` takes two arguments; we name and describe them below. +`replicateByteString` takes two arguments; we name and describe them below. 1. The desired result length, of type `BuiltinInteger`. This is the _length argument_. @@ -721,51 +721,51 @@ builtinSetBits [0x00] [(0, False)] => [0x00] This is the _byte argument_. Let $n$ be the length argument, and $w$ the byte argument. If $n < 0$, then -`builtinReplicate` fails. In this case, the resulting error message must specify +`replicateByteString` fails. In this case, the resulting error message must specify _at least_ the following information: -* That `builtinReplicate` failed due to a negative length argument; and +* That `replicateByteString` failed due to a negative length argument; and * What `BuiltinInteger` was passed as the length argument. -If $n \geq 0$, and $w < 0$ or $w > 255$, then `builtinReplicate` fails. In this +If $n \geq 0$, and $w < 0$ or $w > 255$, then `replicateByteString` fails. In this case, the resulting error message must specify _at least_ the following information: -* That `builtinReplicate` failed due to the byte argument not being a valid +* That `replicateByteString` failed due to the byte argument not being a valid byte; and * What `BuiltinInteger` was passed as the byte argument. -Otherwise, let $b$ be the result of `builtinReplicate`, and let $b\\{i\\}$ be the +Otherwise, let $b$ be the result of `replicateByteString`, and let $b\\{i\\}$ be the byte at position $i$ of $b$, as per [the section describing the bit indexing scheme](#bit-indexing-scheme). We have: * The length (in bytes) of $b$ is $n$; and * For all $i \in 0, 1, \ldots, n - 1$, $b\\{i\\} = w$. -Some examples of the intended behaviour of `builtinReplicate` follow. For +Some examples of the intended behaviour of `replicateByteString` follow. For brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. ``` -- Replicating a negative number of times fails -builtinReplicate (-1) 0 => error +replicateByteString (-1) 0 => error -- Irrespective of byte argument -builtinReplicate (-1) 3 => error +replicateByteString (-1) 3 => error -- Out-of-bounds byte arguments fail -builtinReplicate 1 (-1) => error +replicateByteString 1 (-1) => error -builtinReplicate 1 256 => error +replicateByteString 1 256 => error -- Irrespective of length argument -builtinReplicate 4 (-1) => error +replicateByteString 4 (-1) => error -builtinReplicate 4 256 => error +replicateByteString 4 256 => error -- Length of result matches length argument, and all bytes are the same -builtinReplicate 0 0xFF => [] +replicateByteString 0 0xFF => [] -builtinReplicate 4 0xFF => [0xFF, 0xFF, 0xFF, 0xFF] +replicateByteString 4 0xFF => [0xFF, 0xFF, 0xFF, 0xFF] ``` ### Laws @@ -773,8 +773,8 @@ builtinReplicate 4 0xFF => [0xFF, 0xFF, 0xFF, 0xFF] #### Binary operations We describe laws for all three operations that work over two -`BuiltinByteStrings`, that is, `builtinLogicalAnd`, `builtinLogicalOr` and -`builtinLogicalXor`, together, as many of them are similar (and related). We +`BuiltinByteStrings`, that is, `bitwiseLogicalAnd`, `bitwiseLogicalOr` and +`bitwiseLogicalXor`, together, as many of them are similar (and related). We describe padding semantics and truncation semantics laws, as they are slightly different. @@ -782,12 +782,12 @@ All three operations above, under both padding and truncation semantics, are [commutative semigroups][special-semigroups]. Thus, we have: ```haskell -builtinLogicalAnd s x y = builtinLogicalAnd s y x +bitwiseLogicalAnd s x y = bitwiseLogicalAnd s y x -builtinLogicalAnd s x (builtinLogicalAnd s y z) = builtinLogicalAnd s -(builtinLogicalAnd s x y) z +bitwiseLogicalAnd s x (bitwiseLogicalAnd s y z) = bitwiseLogicalAnd s +(bitwiseLogicalAnd s x y) z --- and the same for builtinLogicalOr and builtinLogicalXor +-- and the same for bitwiseLogicalOr and bitwiseLogicalXor ``` Note that the semantics (designated as `s` above) must be consistent in order @@ -795,72 +795,72 @@ for these laws to hold. Furthermore, under padding semantics, all the above operations are [commutative monoids][commutative-monoid]: ```haskell -builtinLogicalAnd True x "" = builtinLogicalAnd True "" x = x +bitwiseLogicalAnd True x "" = bitwiseLogicalAnd True "" x = x --- and the same for builtinLogicalOr and builtinLogicalXor +-- and the same for bitwiseLogicalOr and bitwiseLogicalXor ``` Under truncation semantics, `""` (that is, the empty `BuiltinByteString`) acts instead as an [absorbing element][absorbing-element]: ```haskell -builtinLogicalAnd False x "" = builtinLogicalAnd False "" x = "" +bitwiseLogicalAnd False x "" = bitwiseLogicalAnd False "" x = "" --- and the same for builtinLogicalOr and builtinLogicalXor +-- and the same for bitwiseLogicalOr and bitwiseLogicalXor ``` -`builtinLogicalAnd` and `builtinLogicalOr` are also [semilattices][semilattice], +`bitwiseLogicalAnd` and `bitwiseLogicalOr` are also [semilattices][semilattice], due to their idempotence: ```haskell -builtinLogicalAnd s x x = x +bitwiseLogicalAnd s x x = x --- and the same for builtinLogicalOr +-- and the same for bitwiseLogicalOr ``` -`builtinLogicalXor` is instead involute: +`bitwiseLogicalXor` is instead involute: ```haskell -builtinLogicalXor s x (builtinLogicalXor s x x) = builtinLogicalXor s -(builtinLogicalXor s x x) x = x +bitwiseLogicalXor s x (bitwiseLogicalXor s x x) = bitwiseLogicalXor s +(bitwiseLogicalXor s x x) x = x ``` -Additionally, under padding semantics, `builtinLogicalAnd` and -`builtinLogicalOr` are [self-distributive][distributive]: +Additionally, under padding semantics, `bitwiseLogicalAnd` and +`bitwiseLogicalOr` are [self-distributive][distributive]: ```haskell -builtinLogicalAnd True x (builtinLogicalAnd True y z) = builtinLogicalAnd True -(builtinLogicalAnd True x y) (builtinLogicalAnd True x z) +bitwiseLogicalAnd True x (bitwiseLogicalAnd True y z) = bitwiseLogicalAnd True +(bitwiseLogicalAnd True x y) (bitwiseLogicalAnd True x z) -builtinLogicalAnd True (builtinLogicalAnd True x y) z = builtinLogicalAnd True -(builtinLogicalAnd True x z) (builtinLogicalAnd True y z) +bitwiseLogicalAnd True (bitwiseLogicalAnd True x y) z = bitwiseLogicalAnd True +(bitwiseLogicalAnd True x z) (bitwiseLogicalAnd True y z) --- and the same for builtinLogicalOr +-- and the same for bitwiseLogicalOr ``` -Under truncation semantics, `builtinLogicalAnd` is only left-distributive over -itself, `builtinLogicalOr` and `builtinLogicalXor`: +Under truncation semantics, `bitwiseLogicalAnd` is only left-distributive over +itself, `bitwiseLogicalOr` and `bitwiseLogicalXor`: ```haskell -builtinLogicalAnd False x (builtinLogicalAnd False y z) = builtinLogicalAnd -False (builtinLogicalAnd False x y) (builtinLogicalAnd False x z) +bitwiseLogicalAnd False x (bitwiseLogicalAnd False y z) = bitwiseLogicalAnd +False (bitwiseLogicalAnd False x y) (bitwiseLogicalAnd False x z) -builtinLogicalAnd False x (builtinLogicalOr False y z) = builtinLogicalOr False -(builtinLogicalAnd False x y) (builtinLogicalAnd False x z) +bitwiseLogicalAnd False x (bitwiseLogicalOr False y z) = bitwiseLogicalOr False +(bitwiseLogicalAnd False x y) (bitwiseLogicalAnd False x z) -builtinLogicalAnd False x (builtinLogicalXor False y z) = builtinLogicalXor -False (builtinLogicalAnd False x y) (builtinLogicalAnd False x z) +bitwiseLogicalAnd False x (bitwiseLogicalXor False y z) = bitwiseLogicalXor +False (bitwiseLogicalAnd False x y) (bitwiseLogicalAnd False x z) ``` -`builtinLogicalOr` under truncation semantics is left-distributive over itself +`bitwiseLogicalOr` under truncation semantics is left-distributive over itself and `bitwiseLogicalAnd`: ```haskell -builtinLogicalOr False x (builtinLogicalOr False y z) = builtinLogicalOr False -(builtinLogicalOr False x y) (builtinLogicalOr False x z) +bitwiseLogicalOr False x (bitwiseLogicalOr False y z) = bitwiseLogicalOr False +(bitwiseLogicalOr False x y) (bitwiseLogicalOr False x z) -builtinLogicalOr False x (builtinLogicalAnd False y z) = builtinLogicalAnd False -(builtinLogicalOr False x y) (builtinLogicalOr False x z) +bitwiseLogicalOr False x (bitwiseLogicalAnd False y z) = bitwiseLogicalAnd False +(bitwiseLogicalOr False x y) (bitwiseLogicalOr False x z) ``` If the first and second data arguments to these operations have the same length, @@ -868,38 +868,38 @@ these operations satisfy several additional laws. We describe these briefly below, with the added note that, in this case, padding and truncation semantics coincide: -* `builtinLogicalAnd` and `builtinLogicalOr` form a [bounded lattice][lattice] -* `builtinLogicalAnd` is [distributive][distributive] over itself, `builtinLogicalOr` and - `builtinLogicalXor` -* `builtinLogicalOr` is [distributive][distributive] over itself and `builtinLogicalAnd` +* `bitwiseLogicalAnd` and `bitwiseLogicalOr` form a [bounded lattice][lattice] +* `bitwiseLogicalAnd` is [distributive][distributive] over itself, `bitwiseLogicalOr` and + `bitwiseLogicalXor` +* `bitwiseLogicalOr` is [distributive][distributive] over itself and `bitwiseLogicalAnd` We do not specify these laws here, as they do not hold in general. At the same time, we expect that any implementation of these operations will be subject to these laws. -#### `builtinLogicalComplement` +#### `bitwiseLogicalComplement` -The main law of `builtinLogicalComplement` is involution: +The main law of `bitwiseLogicalComplement` is involution: ```haskell -builtinLogicalComplement (builtinLogicalComplement x) = x +bitwiseLogicalComplement (bitwiseLogicalComplement x) = x ``` -In combination with `builtinLogicalAnd` and `builtinLogicalOr`, -`builtinLogicalComplement` gives rise to the famous [De Morgan laws][de-morgan], irrespective of semantics: +In combination with `bitwiseLogicalAnd` and `bitwiseLogicalOr`, +`bitwiseLogicalComplement` gives rise to the famous [De Morgan laws][de-morgan], irrespective of semantics: ```haskell -builtinLogicalComplement (builtinLogicalAnd s x y) = builtinLogicalOr s -(builtinLogicalComplement x) (builtinLogicalComplement y) +bitwiseLogicalComplement (bitwiseLogicalAnd s x y) = bitwiseLogicalOr s +(bitwiseLogicalComplement x) (bitwiseLogicalComplement y) -builtinLogicalComplement (builtinLogicalOr s x y) = builtinLogicalAnd s -(builtinLogicalComplement x) (builtinLogicalComplement y) +bitwiseLogicalComplement (bitwiseLogicalOr s x y) = bitwiseLogicalAnd s +(bitwiseLogicalComplement x) (bitwiseLogicalComplement y) ``` -For `builtinLogicalXor`, we instead have (again, irrespective of semantics): +For `bitwiseLogicalXor`, we instead have (again, irrespective of semantics): ```haskell -builtinLogicalXor s x (builtinLogicalComplement x) = x +bitwiseLogicalXor s x (bitwiseLogicalComplement x) = x ``` #### Bit reading and modification @@ -908,59 +908,57 @@ Throughout, we assume any index arguments to be 'in-bounds'; that is, all the index arguments used in the statements of any law are such that the operation they are applied to wouldn't produce an error. -The first law of `builtinSetBits` is similar to the [set-twice law of +The first law of `writeBits` is similar to the [set-twice law of lenses][lens-laws]: ```haskell -builtinSetBits bs [(i, b1), (i, b2)] = builtinSetBits bs [(i, b2)] +writeBits bs [(i, b1), (i, b2)] = writeBits bs [(i, b2)] ``` -Together with `builtinReadBit`, we obtain the remaining two analogues to the lens +Together with `readBit`, we obtain the remaining two analogues to the lens laws: ```haskell -- writing to an index, then reading from that index, gets you what you wrote -builtinReadBit (builtinSetBits bs [(i, b)]) i = b +readBit (writeBits bs [(i, b)]) i = b -- if you read from an index, then write that value to that same index, nothing -- happens -builtinSetBits bs [(i, builtinReadBit bs i)] = bs +writeBits bs [(i, readBit bs i)] = bs ``` -Furthermore, given a fixed data argument, `builtinSetBits` acts as a [monoid -homomorphism][monoid-homomorphism] from functions to lists under concatenation: +Furthermore, given a fixed data argument, `writeBits` acts as a [monoid +homomorphism][monoid-homomorphism] lists under concatenation to functions: ```haskell --- identity function corresponds to empty list -builtinSetBits bs [] = bs +writeBits bs [] = bs --- composition is concatenation of change list arguments -builtinSetBits (builtinSetBits bs is) js = builtinSetBits bs (is <> js) +writeBits bs (is <> js) = writeBits (writeBits bs is) js ``` -#### `builtinReplicate` +#### `replicateByteString` -Given a fixed byte argument, `builtinReplicate` acts as a [monoid +Given a fixed byte argument, `replicateByteString` acts as a [monoid homomorphism][monoid-homomorphism] from natural numbers under addition to `BuiltinByteString`s under concatenation: ```haskell -builtinReplicate 0 w = "" +replicateByteString 0 w = "" -builtinReplicate (n + m) w = builtinReplicate n w <> builtinReplicate m w +replicateByteString (n + m) w = replicateByteString n w <> replicateByteString m w ``` Additionally, for any 'in-bounds' index (that is, any index for which `builtinIndexByteString` won't error) `i`, we have ```haskell -builtinIndexByteString (builtinReplicate n w) i = w +builtinIndexByteString (replicateByteString n w) i = w ``` Lastly, we have ```haskell -builtinSizeOfByteString (builtinReplicate n w) = n +builtinSizeOfByteString (replicateByteString n w) = n ``` ## Rationale: how does this CIP achieve its goals? @@ -983,7 +981,7 @@ and how they differ from existing work, below. Aside from the issues we list below, we don't consider other operations controversial. Indeed, `bitwiseLogicalComplement` has a direct parallel to the -implementation in [CIP-58][cip-58], and `builtinReplicate` is a direct wrapper +implementation in [CIP-58][cip-58], and `replicateByteString` is a direct wrapper around the `replicate` function in `ByteString`. Thus, we do not discuss them further here. @@ -1212,7 +1210,7 @@ one in light of both this fact, and the Cases we have stated here. ### Padding versus truncation For the operations defined in this CIP taking two `BuiltinByteString` arguments -(that is, `builtinLogicalAnd`, `builtinLogicalOr`, and `builtinLogicalXor`), +(that is, `bitwiseLogicalAnd`, `bitwiseLogicalOr`, and `bitwiseLogicalXor`), when the two arguments have identical lengths, the semantics are natural, mirroring the corresponding operations on the [Boolean algebra][boolean-algebra-2] $\textbf{2}^{8n}$, where $n$ is the length @@ -1223,7 +1221,7 @@ we repeat some of the definitions used [in the corresponding section](#padding-versus-truncation-semantics). * Extend the shorter argument with the identity element (1 for - `builtinLogicalAnd`, 0 otherwise) to match the length of the longer argument, + `bitwiseLogicalAnd`, 0 otherwise) to match the length of the longer argument, then perform the operation as if on matching-length arguments. We call this _padding semantics_. * Ignore the bytes of the longer argument whose indexes would not be valid for @@ -1243,8 +1241,8 @@ Consider the following operation: given a bound $k$ and an integer set, remove all elements smaller than $k$ from the set. This can be done using `bitwiseLogicalAnd` and a mask where the first $k - 1$ bits are clear. However, under match semantics, the mask would have to have a length equal to the integer -set representation; under padding semantics, the mask would only need to have a -length proportional to $k$. This is noteworthy, as padding the mask would +set representation; under padding semantics, the mask would only need to have $\Theta(k)$ +length. This is noteworthy, as padding the mask would require an additional copy operation, only to produce a value that would be discarded immediately. @@ -1294,12 +1292,13 @@ only two of the three semantics and have this choice for any given call be controlled by a `BuiltinBool` flag. This naturally leads to the question of which of the three semantics above we -can afford not to have. We believe that match semantics are the right ones to -exclude. Firstly, technically we can still have match semantics by using either +can afford to exclude: we believe that match semantics are the choice, for +several reasons. Firstly, technically we can still have match semantics by using either padding or truncation semantics plus a length check beforehand: this is a cheap operation, unlike simulating padding semantics for example, which would have non-trivial cost. Secondly, due to the preponderance of truncation semantics in -Haskell, we feel excluding it as an option is wrong. Lastly, we believe that +Haskell, we feel that excluding them as an option is both surprising and wrong. +Lastly, we believe that outside of error checking, exact match semantics give few benefits over padding or truncation semantics, for performance and otherwise. This combination of reasoning leads us to naturally consider padding and truncation as the two to @@ -1307,72 +1306,72 @@ keep, and this guided our implementation choices. ### Bit setting -`builtinSetBits` in our description takes a change list argument, allowing +`writeBits` in our description takes a change list argument, allowing changing multiple bits at once. This is an added complexity, and an argument can be made that something similar to the following operation would be sufficient: ```haskell -builtinSetBit :: BuiltinByteString -> BuiltinInteger -> BuiltinBool -> +writeBit :: BuiltinByteString -> BuiltinInteger -> BuiltinBool -> BuiltinByteString ``` -Essentially, `builtinSetBit bs i v` would be equivalent to `builtinSetBits bs +Essentially, `writeBit bs i v` would be equivalent to `writeBits bs [(i, v)]` as currently defined. This was the choice made by [CIP-58][cip-58], with the consideration of simplicity in mind. At the same time, due to the immutability semantics of Plutus Core, each time -`builtinSetBit` is called, a copy of its `BuiltinByteString` argument would have -to be made. Thus, a sequence of $k$ `builtinSetBit` calls in a fold over a +`writeBit` would be called, we would have to copy its `BuiltinByteString` +argument. Thus, a sequence of $k$ `setBit` calls in a fold over a `BuiltinByteString` of length $n$ would require $\Theta(nk)$ time and -$\Theta(nk)$ space. Meanwhile, if we instead used `builtinSetBits`, the time +$\Theta(nk)$ space. Meanwhile, if we instead used `writeBits`, the time drops to $\Theta(n + k)$ and the space to $\Theta(n)$, which is a non-trivial improvement. While we cannot avoid the worst-case copying behaviour of -`builtinSetBit` (if we have a critical path of read-write dependencies of length +`setBit` (if we have a critical path of read-write dependencies of length $k$, for example), and 'list packing' carries some cost, we have [benchmarks][benchmarks-bits] that show not only that this 'packing cost' is essentially zero, but that for `BuiltinByteString`s of 30 bytes or fewer, -copying completely overwhelms the work required to set the bits in the first -place. This alone is a strong argument for having `builtinSetBits` instead; +copying completely overwhelms the work required to modify the bits specified in +the changelist argument. This alone is good evidence for having `writeBits` instead; indeed, there is prior art for doing this [in the `vector` library][vector], for the exact reasons we give here. The argument could also be made whether this design should be extended to other primitive operations in this CIP which both take `BuiltinByteString` arguments and also produce `BuiltinByteString` results. We believe that this is not as -justified as in the `builtinSetBits` case, for several reasons. Firstly, for -`builtinLogicalComplement`, it's not even clear what benefit this would have at +justified as in the `writeBits` case, for several reasons. Firstly, for +`bitwiseLogicalComplement`, it's not clear what benefit this would have at all: the only possible signature such an operation would have is `[BuiltinByteString] -> [BuiltinByteString]`, which in effect would be a specialized form of mapping. While an argument could be made for a _general_ form of mapping as a Plutus Core primitive, it wouldn't be reasonable for an operation like this to be considered for such. -Secondly, the -benefits to performance wouldn't be nearly as significant in theory, and likely -in practice. Consider this hypothetical operation (with fold semantics): +Secondly, the performance benefits of such an operation aren't nearly as +significant in theory, and likely wouldn't be in practice either. Consider +this hypothetical operation (with fold semantics): ```haskell -builtinLogicalXors :: BuiltinBool -> [BuiltinByteString] -> BuiltinByteString +bitwiseLogicalXors :: BuiltinBool -> [BuiltinByteString] -> BuiltinByteString ``` -Simulating this operation as a fold using `builtinLogicalXor`, in the worst +Simulating this operation as a fold using `bitwiseLogicalXor`, in the worst case, irrespective of padding or truncation semantics, requires $\Theta(nk)$ time and space, where $n$ is the size of each `BuiltinByteString` in the argument list, and $k$ is the length of the argument list itself. Using -`builtinLogicalXors` would reduce the space required to $\Theta(n)$, but not -affect the time complexity at all. +`bitwiseLogicalXors` instead would reduce the space required to $\Theta(n)$, +but would not affect the time complexity at all. -Lastly, it is questionable whether 'bulk' operations like `builtinLogicalXors` -above would see as much use as `builtinSetBits`. In the context of Case 1, -`builtinLogicalXors` corresponds to taking the symmetric difference of multiple +Lastly, it is questionable whether 'bulk' operations like `bitwiseLogicalXors` +above would see as much use as `writeBits`. In the context of Case 1, +`bitwiseLogicalXors` corresponds to taking the symmetric difference of multiple integer sets; it seems unlikely that the number of sets we'd want to do this -with would be higher than 2 often. However, in the same context, -`builtinSetBits` corresponds to constructing an integer set given a list of +with would frequently be higher than 2. However, in the same context, +`writeBits` corresponds to constructing an integer set given a list of members (or, for that matter, _non_-members): this is an operation that is both -required by the case description, and also unarguably useful often. +required by the case description, and also much more likely to be used often. On the basis of the above, we believe that choosing to implement -`builtinSetBits` as a 'bulk' operation, but to leave others as 'singular' is the +`writeBits` as a 'bulk' operation, but to leave others as 'singular' is the right choice. ## Path to Active From 61f6576ae6bc95498f0e6e6cbce8e326adb96012 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Mon, 20 May 2024 11:03:37 +1200 Subject: [PATCH 25/32] Rephrase writeBits as a recursive definition --- CIP-0122/CIP-0122.md | 46 +++++++++++++++----------------------------- 1 file changed, 16 insertions(+), 30 deletions(-) diff --git a/CIP-0122/CIP-0122.md b/CIP-0122/CIP-0122.md index 5259867fed..d4a0158b43 100644 --- a/CIP-0122/CIP-0122.md +++ b/CIP-0122/CIP-0122.md @@ -587,19 +587,20 @@ readBit [0xF4, 0xFF] 10 => False should be changed to which value. This is the _change list argument_. Each index has type `BuiltinInteger`, while each value has type `BuiltinBool`. -Let $C = (i_1, v_1), (i_2, v_2), \ldots , (i_k, v_k)$ refer to the change list -argument, and $b$ the data argument of length $n$ in bytes. Let $b_r$ be the -result of `writeBits`, whose length is also $n$. We use $b[i]$ to refer to -the value at index $i$ of $b$ (and analogously, $b_r$); see the [section on the bit -indexing scheme](#bit-indexing-scheme) for the exact specification of this. +Let $b$ refer to the data argument of length $n$ in bytes. We define `writeBits` +recursively over the structure of the change list argument. Throughout, we use +$b_r$ to refer to the result of `writeBits`, whose length is also $n$. We use +$b[i]$ to refer to the value at index $i$ of $b$ (and analogously, $b_r$); see +the [section on the bit indexing scheme](#bit-indexing-scheme) for the exact +specification of this. -If the change list argument is empty, the result is $b$. If the change list -argument is a singleton, let $(i, v)$ refer to its only index-value pair. If $i -< 0$ or $i \geq 8 \cdot n$, then `writeBits` fails. In this case, the -resulting error message must specify _at least_ the following information: +If the change list argument is empty, we return the data argument unchanged. +Otherwise, let $(i, v)$ be the head of the change list argument, and $\ell$ its +tail. If $i < 0$ or $i \geq 8 \cdot n$, then `writeBits` fails. In this case, +the resulting error message must specify at _least_ the following information: * That `writeBits` failed due to an out-of-bounds index argument; and -* What `BuiltinInteger` was passed as the index part of the index-value pair. +* What `BuiltinInteger` was passed as $i$. Otherwise, for all $j \in 0, 1, \ldots 8 \cdot n - 1$, we have @@ -611,24 +612,9 @@ b_r[j] = \begin{cases} \end{cases} $$ -if the change list argument is longer than a singleton, suppose that we can -process a change list argument of length $1 \leq m$, and let $b_m$ be the result -of such processing. There are two possible outcomes for $b_m$: - -1. An error. In this case, we define the result of `writeBits` on such a - change list as that error. -2. A `BuiltinByteString`. - -From here, when we refer to $b_m$, we refer to the `BuiltinByteString` outcome; -in the case of the first outcome, we simply 'forward' the result. - -We observe that any change list $C^{\prime}$ of length $m + -1$ will have the form of some other change list $C_m$, with an additional -element $(i_{m + 1}, v_{m + 1})$ at the end. We define the result of -`writeBits` with data argument $b$ and change list argument $C^{\prime}$ -as the result of `writeBits` with data argument $b_m$ and the change list -argument $(i_{m + 1}, v_{m + 1})$; as this change list is a singleton, we can -process it according to the description above. +Then, if we did not fail as described above, we repeat the `writeBits` +operation, but with $b_r$ as the data argument and $\ell$ as the change list +argument. Some examples of the intended behaviour of `writeBits` follow. For brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. @@ -695,7 +681,7 @@ writeBits [0xF4, 0xFF] [(10, True), (1, False)] => [0xF0, 0xFD] writeBits (writeBits [0xF4, 0xFF] [(10, True)]) [(1, False)] => [0xF0, 0xFD] --- Order within a changelist is unimportant among unique indexes +-- Order within a change list is unimportant among unique indexes writeBits [0xF4, 0xFF] [(1, False), (10, True)] => [0xF0, 0xFD] -- But _is_ important for identical indexes @@ -1331,7 +1317,7 @@ $k$, for example), and 'list packing' carries some cost, we have [benchmarks][benchmarks-bits] that show not only that this 'packing cost' is essentially zero, but that for `BuiltinByteString`s of 30 bytes or fewer, copying completely overwhelms the work required to modify the bits specified in -the changelist argument. This alone is good evidence for having `writeBits` instead; +the change list argument. This alone is good evidence for having `writeBits` instead; indeed, there is prior art for doing this [in the `vector` library][vector], for the exact reasons we give here. From 79038ac7aa4b3ba24ca20676840b911fdc75caa4 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Mon, 20 May 2024 13:55:00 +1200 Subject: [PATCH 26/32] Clarify bit indexing scheme reasoning --- CIP-0122/CIP-0122.md | 168 ++++++++++++++++++++++++++++++------------- 1 file changed, 117 insertions(+), 51 deletions(-) diff --git a/CIP-0122/CIP-0122.md b/CIP-0122/CIP-0122.md index d4a0158b43..0a3ba163a5 100644 --- a/CIP-0122/CIP-0122.md +++ b/CIP-0122/CIP-0122.md @@ -1105,8 +1105,36 @@ future operations (such as shifts or rotations) significantly harder to both do, and also reason about. Thus, only the bit-flip variant, as well as our choice, remain contenders. -The second notion is _conversion agreement_. To describe this notion, we first -observe that, according to the definition of the bit indexing scheme given [in +The second notion is _most-significant-first conversion agreement_. This notion +refers to the [CIP-121 concept of the same name][cip-121-big-endian], and +ensures that (at least for the most-significant-first arrangement), the +following workflow doesn't produce unexpected results: + +1. Convert a `BuiltinInteger` to `BuiltinByteString` using + `builtinIntegerToByteString` with the most-significant-first endianness + argument. +2. Manipulate the bits of the result of step 1 using the operations specified + here. +3. Convert the result of step 2 back to a `BuiltinInteger` using + `builtinByteStringToInteger` with the most-significant-first endianness + argument. + +This workflow is directly relevant to Case 2. The Argon2 family of hashes use +certain inputs (which happen to be numbers) both as numbers (meaning, for +arithmetic operatons) and also as blocks of binary (specifically for XOR). This +is not unique to Argon2, or even hashing, as a range of operations (especially +in cryptographic applications) use similar approaches, whether for performance, +semantics or both. In such cases, users of our primitives (both logical and +conversion) must be confident that their changes 'translate' in the way they +expect between these two 'views' of the data. + +The choice of most-significant-first as the arrangement that we must agree with +seems somewhat arbitrary at a glance, for two reasons: firstly, it's not clear +why we must pick a single arrangement to be consistent with; secondly, the +reasoning for the choice of most-significant-first over most-significant-last +as the arrangement to agree with isn't immediately apparent. To see why this is +the only choice that we consider reasonable, we first observe that, according +to the definition of the bit indexing scheme given [in the corresponding section](#bit-indexing-scheme), as well as the corresponding definition for the bit-flip variant, we view a `BuiltinByteString` of length $n$ as a binary natural number with exactly $8n$ digits, and the value at index $i$ @@ -1114,22 +1142,19 @@ corresponds to the digits whose place value is either $2^i$ (for the bit-flip variant), or $2^{8n - i - 1}$ (for our chosen method). Put another way, under the specification for the bit-flip variant, the least significant binary digit is first, whereas in our chosen specification, the least significant binary -digit is last. - -When viewed this way, we can immediately see a potential problem, as by indexing -a `BuiltinByteString`, we get back a `BuiltinInteger`, which has a numerical -value as a natural number in the range $[0, 255]$. It would thus be sensible -that, given a `BuiltinByteString` that is non-empty, if we were to get the -values at bit indexes $0$ through $7$, and treat them as their corresponding -place value in a summation, we should obtain the same answer as indexing -whichever byte those bits come from. We call this notion _conversion agreement_, -due to its relation to [CIP-121][conversion-cip], which allows us to -(essentially) view a `BuiltinByteString` as a natural number in base-256. While -CIP-121 allows two different views of a natural number (specifically, whether -the first _byte_ index corresponds to the highest or the lowest place value), -our case applies equally in both situations (as described below). The only difference -in our case is that we are concerned with the positioning of binary digits, not -base-256 ones. +digit is last. CIP-121's conversion primitives mirror this reasoning: the +most-significant-first arrangement corresponds to our chosen method, while the +most-significant-last arrangement corresponds to the bit-flip variant instead. +The difference is the digit value: for us, the digit value is (effectively) 2, +while for CIP-121's conversion primitives, it is 256 instead. + +We also observe that, when we index a `BuiltinByteString`'s _bytes_, we get back +a `BuiltinInteger`, whic has a numerical value as a natural number in the range +$[0, 255]$. Putting these two observations together, we consider it sensible +that, given a non-empty `BuiltinByteString`, if we were to get the values at bit +indexes $0$ through $7$, then sum their corresponding place values (treating +clear bits as $0$ and set bits as the appropriate place value), we should get +the same result as indexing whichever byte those bits came from. Consider the `BuiltinByteString` whose only byte is $42$, whose representation is as follows: @@ -1140,12 +1165,13 @@ is as follows: | Byte | 00101010 | ``` -Indeed, if we used the CIP-121 conversion primitive -[`builtinByteStringToInteger`](https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-0121#builtinbytestringtointeger) -to convert it to its `BuiltinInteger` equivalent, this is the answer we would -get, regardless of which digit arrangement we choose. +We note that, if we index this `BuiltinByteString` at byte position $0$, we get +back the answer $42$. Furthermore, if we use `builtinByteStringToInteger` from +CIP-121 with such a `BuiltinByteString`, we get the result $42$ as well, +regardless of the endianness argument we choose. -Under the bit-flip variant, our bit indexes would be as follows: +Under the bit-flip variant, the bit indexes of this `BuiltinByteString` would be +as follows: ``` | Byte index | 0 | @@ -1155,10 +1181,10 @@ Under the bit-flip variant, our bit indexes would be as follows: | Bit index | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | ``` -However, this immediately causes a problem: under this indexing scheme, we imply -that the $2^2 = 4$ place value is $1$ in $42$'s binary representation, but -this is not the case. This fails conversion agreement. However, our choice -produces the correct answer: +However, we immediately see a problem: under this indexing scheme, the $2^2 = 4$ +place value is $1$, which would suggest that in the binary representation of +$42$, the corresponding digit is also $1$. However, this is not the case. Under +our scheme of choice however, we get the correct answer: ``` | Byte index | 0 | @@ -1168,30 +1194,69 @@ produces the correct answer: | Bit index | 7 | 6 | 5 | 4 | 3 | 2 | 1 | 0 | ``` -Here, the $4$ place value is correctly $0$. Indeed, our choice simply 'extends' -the bit ordering (in the place value sense) employed by all machine -architectures for bytes in their sense as natural numbers within a fixed range. -This was also the choice made by [CIP-58][cip-58], for similar reasons. - -We also note that conversion agreement matters for Case 2, in the wider context -of the interaction between [CIP-121 primitives][conversion-cip] and logical -XOR. The Argon2 family of hashes use certain inputs (which happen to be numbers) -both as numbers (meaning, arithmetic operations), and also as blocks of binary -(meaning, XOR operations specifically). This is common in a range of -applications that rely on bitwise operations, both in cryptography and -elsewhere, whether for performance, functionality, or both. In such situations, -users of the primitives, and in our specific case, conversions, must be -confident that their changes 'translate' in the way they expect between these -two 'views' of the data. This once again suggests that our choice is the right -one, as it is the only one that would ensure conversion agreement. While some -care would be needed in multi-byte cases, as only most-significant-first -conversions maintain this behaviour, this is not difficult to remember. - -While the bit-flip variant has the advantage of 'agreement' between byte and bit -indexes, we believe that conversion agreement is the more important property to -have. Given that the [CIP-121][conversion-cip] has already -been implemented into Plutus Core, we think that our choice is the only viable -one in light of both this fact, and the Cases we have stated here. +Here, the $4$ place value is correctly $0$. This demonstrates that of the two +indexing scheme possibilities that preserve index locality, only one can be +consistent with _any_ choice of byte arrangement, whether most-significant-first +or most-significant-last: the one we chose. This implies that we cannot be +consistent with both arrangements while also preserving index locality. + +Let us now consider a larger example `BuiltinByteString`: + +``` +| Byte index | 0 | 1 | +|------------|----------|----------| +| Byte | 00101010 | 11011011 | +``` + +This would produce two different results when converted with +`builtinByteStringToInteger`, depending on the choice of endianness argument: + +* For the most-significant-first arrangement, the result is $42 * 256 + 223 = + 10975$. +* For the most-significant-last arrangement, the result is $223 * 256 + 42 = + 57130$. + +These have the following 'breakdowns' in base-2: + +* $10975 = 8096 + 2048 + 512 + 256 + 32 + 16 + 8 + 4 + 2 + 1 = 2^13 + 2^11 + 2^9 + 2^8 + 2^5 + 2^4 + 2^3 + 2^2 + 2^1 + 2^0$ +* $57130 = 32768 + 16386 + 4096 + 2048 + 1024 + 512 + 256 + 32 + 8 + 2 = 2^15 + 2^14 + 2^12 + 2^11 + 2^10 + 2^9 + 2^8 + 2^5 + 2^3 + 2^1$ + +Under the bit-flip variant, the bit indexes of this `BuiltinByteString` would be +as follows: + +``` +| Byte index | 0 | 1 | +|------------|-------------------------------|-------------------------------------| +| Byte | 0 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 1 | 0 | 1 | 1 | 0 | 1 | 1 | +|------------|-------------------------------|-------------------------------------| +| Bit index | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | +``` + +We immediately see a problem, as in this representation, it suggests that the +$2^1 = 2$ place value has zero digit value. This is true of _neither_ $10975$ +nor $57130$'s base-2 forms, which have the $2$ place value with a $1$ digit +value. This suggests that the bit-flip variant cannot agree with _either_ choice +of arrangement in general. + +However, if we view the bit indexes using our chosen scheme: + +``` +| Byte index | 0 | 1 | +|------------|-------------------------------------|-------------------------------| +| Byte | 0 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 1 | 0 | 1 | 1 | 0 | 1 | 1 | +|------------|-------------------------------------|-------------------------------| +| Bit index | 15 | 14 | 13 | 12 | 11 | 10 | 9 | 8 | 7 | 6 | 5 | 4 | 3 | 2 | 1 | 0 | +``` + +the $2$ place value is correctly shown as having a digit value of 1. + +Combining these observations, we note that, assuming we value index locality, +choosing our scheme gives us consistency with the most-significant-first +arrangement, as well as consistency with byte indexing digit values, but +choosing the bit-flip variant gives us _neither_. As we need both index locality +_and_ consistency with at least one arrangement, our choice is the correct one. +The fact that we also get byte indexing digit values being consistent is another +reason for our choice. ### Padding versus truncation @@ -1420,3 +1485,4 @@ This CIP is licensed under [Apache-2.0](http://www.apache.org/licenses/LICENSE-2 [blake2b]: https://en.wikipedia.org/wiki/BLAKE_(hash_function) [argon2]: https://en.wikipedia.org/wiki/Argon2 [xor-crypto]: https://en.wikipedia.org/wiki/Exclusive_or#Bitwise_operation +[cip-121-big-endian]: https://github.com/mlabs-haskell/CIPs/blob/koz/to-from-bytestring/CIP-0121/README.md#representation From ef3ecb9cf3f6500428abb16f55f1614d32491570 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Tue, 21 May 2024 09:04:24 +1200 Subject: [PATCH 27/32] Remove README entry for CIP-122 Co-authored-by: Robert Phair --- README.md | 1 - 1 file changed, 1 deletion(-) diff --git a/README.md b/README.md index 0b709ae9b7..1812ff6c16 100644 --- a/README.md +++ b/README.md @@ -101,7 +101,6 @@ CIP Editors meetings are public, recorded, and [published on Youtube](https://ww | 0110 | [Plutus v1 compatible script references](./CIP-0110) | Proposed | | 0114 | [CBOR Tags Registry](./CIP-0114) | Proposed | | 0115 | [CBOR tag definition - ED25519-BIP32 Keys](./CIP-0115) | Proposed | -| 0122 | [Logical operations](./CIP-0122) | Proposed | | 0381 | [Plutus Support for Pairings Over BLS12-381](./CIP-0381) | Proposed | | 1694 | [A proposal for entering the Voltaire phase](./CIP-1694) | Proposed | | 1852 | [HD (Hierarchy for Deterministic) Wallets for Cardano](./CIP-1852/) | Active | From 60f3a1dc6e93054c76b6befa63b6b4aee08c6561 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Thu, 6 Jun 2024 07:13:07 +1200 Subject: [PATCH 28/32] Match CIP title Co-authored-by: Ryan <44342099+Ryun1@users.noreply.github.com> --- CIP-0122/CIP-0122.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CIP-0122/CIP-0122.md b/CIP-0122/CIP-0122.md index 0a3ba163a5..d5a6a6071f 100644 --- a/CIP-0122/CIP-0122.md +++ b/CIP-0122/CIP-0122.md @@ -1,6 +1,6 @@ --- CIP: 122 -Title: Logical operations +Title: Logical operations over BuiltinByteString Category: Plutus Status: Proposed Authors: From 1afbef149d29f8a404b4dff7e87f372d3c77f3da Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Thu, 6 Jun 2024 07:42:49 +1200 Subject: [PATCH 29/32] Fix bad examples for writeBits --- CIP-0122/CIP-0122.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/CIP-0122/CIP-0122.md b/CIP-0122/CIP-0122.md index d5a6a6071f..dea0b435e6 100644 --- a/CIP-0122/CIP-0122.md +++ b/CIP-0122/CIP-0122.md @@ -674,15 +674,15 @@ writeBits [0x00] [(5, True)] => [0x20] writeBits [0xFF] [(5, False)] => [0xDF] -- Larger indexes write backwards into the bytes from the end -writeBits [0xF4, 0xFF] [(10, True)] => [0xF0, 0xFF] +writeBits [0xF4, 0xFF] [(10, False)] => [0xF0, 0xFF] -- Multiple items in a change list apply cumulatively -writeBits [0xF4, 0xFF] [(10, True), (1, False)] => [0xF0, 0xFD] +writeBits [0xF4, 0xFF] [(10, False), (1, False)] => [0xF0, 0xFD] -writeBits (writeBits [0xF4, 0xFF] [(10, True)]) [(1, False)] => [0xF0, 0xFD] +writeBits (writeBits [0xF4, 0xFF] [(10, False)]) [(1, False)] => [0xF0, 0xFD] -- Order within a change list is unimportant among unique indexes -writeBits [0xF4, 0xFF] [(1, False), (10, True)] => [0xF0, 0xFD] +writeBits [0xF4, 0xFF] [(1, False), (10, False)] => [0xF0, 0xFD] -- But _is_ important for identical indexes writeBits [0x00, 0xFF] [(10, True), (10, False)] => [0x00, 0xFF] From 1482add39abf264ea93c5c0bb5fa5fa2929fcc68 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Thu, 6 Jun 2024 11:02:57 +1200 Subject: [PATCH 30/32] Fix bitwise binary op descriptions, specify padding more explicitly --- CIP-0122/CIP-0122.md | 136 ++++++++++++++++++++++--------------------- 1 file changed, 71 insertions(+), 65 deletions(-) diff --git a/CIP-0122/CIP-0122.md b/CIP-0122/CIP-0122.md index dea0b435e6..dc7849d1b7 100644 --- a/CIP-0122/CIP-0122.md +++ b/CIP-0122/CIP-0122.md @@ -304,11 +304,38 @@ _maximum_ of the two arguments (which we call _padding semantics_). As these can both be useful depending on context, we allow both, controlled by a `BuiltinBool` flag, on all the operations listed above. +In cases where we have arguments of different lengths, in order to produce a +result of the appropriate lengths, one of the arguments needs to be either +padded or truncated. Let `short` and `long` refer to the `BuiltinByteString` +argument of shorter length, and of longer length, respectively. The following +table describes what happens to the arguments before the operation: + +| Semantics | `short` | `long` | +|-----------|---------|--------| +| Padding | Pad at high _byte_ indexes | Unchanged | +| Truncation | Unchanged | Truncate high _byte_ indexes | + +We pad with different bytes depending on operation: for `bitwiseLogicalAnd`, we +pad with `0xFF`, while for `bitwiseLogicalOr` and `bitwiseLogicalXor` we pad +with `0x00` instead. We refer to arguments so changed as +_semantics-modified_ arguments. + For example, consider the `BuiltinByteString`s `x = [0x00, 0xF0, 0xFF]` and `y = -[0xFF, 0xF0]`. Under padding semantics, the result of `bitwiseLogicalAnd`, -`bitwiseLogicalOr` or `bitwiseLogicalXor` using these two as arguments would -have a length of 3; under truncation semantics, the result would have a length -of 2 instead. +[0xFF, 0xF0]`. The following table describes what the semantics-modified +versions of these arguments would become for each operation and each semantics: + +| Operation | Semantics | `x` | `y` | +|-----------|-----------|-----|-----| +| `bitwiseLogicalAnd` | Padding | `[0x00, 0xF0, 0xFF]` | `[0xFF, 0xF0, 0xFF]` | +| `bitwiseLogicalAnd` | Truncation | `[0x00, 0xF0]` | `[0xFF, 0xF0]` | +| `bitwiseLogicalOr` | Padding | `[0x00, 0xF0, 0xFF]` | `[0xFF, 0xF0, 0x00]` | +| `bitwiseLogicalor` | Truncation | `[0x00, 0xF0]` | `[0xFF, 0xF0]` | +| `bitwiseLogicalXor` | Padding | `[0x00, 0xF0, 0xFF]` | `[0xFF, 0xF0, 0x00]` | +| `bitwiseLogicalXor` | Truncation | `[0x00, 0xF0]` | `[0xFF, 0xF0]` | + +Based on the above, we observe that under padding semantics, the result of any +of the listed operations would have a byte length of 3, while under truncation +semantics, the result would have a byte length of 2 instead. #### `bitwiseLogicalAnd` @@ -320,26 +347,19 @@ of 2 instead. 2. The first input `BuiltinByteString`. This is the _first data argument_. 3. The second input `BuiltinByteString`. This is the _second data argument_. -Let $b_1, b_2$ refer to the first data argument and the second data -argument respectively, and let $n_1, n_2$ be their respective lengths in bytes. -Let the result of `bitwiseLogicalAnd`, given $b_1, b_2$ and some padding -semantics argument, be $b_r$, of length $n_r$ in bytes. We use $b_1[i]$ to refer -to the value at index $i$ of $b_1$ (and analogously for -$b_2, b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) -for the exact specification of this. +Let $b_1, b_2$ refer to the semantics-modified first data argument and +semantics-modified second data argument respectively, and let $n$ be either of +their lengths in bytes; see the +[section on padding versus truncation semantics](#padding-versus-truncation-semantics) +for the exact specification of this. Let the result of `bitwiseLogicalAnd`, given +$b_1, b_2$ and some padding semantics argument, be $b_r$, also of length $n$ +in bytes. We use $b_1\\{i\\}$ to refer to the byte at index $i$ in $b_1$ (and +analogously for $b_2$, $b_r#); see the [section on the bit indexing +scheme](#bit-indexing-scheme) for the exact specification of this. -If the padding semantics argument is `True`, then we have $n_r = \max \\{ n_1, -n_2 \\}$; otherwise, $n_r = \min \\{ n_1, n_2 \\}$. For all $i \in 0, 1, \ldots 8 -\cdot n_r - 1$, we have - -$$ -b_r[i] = \begin{cases} - b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \\{ n_1, n_2 \\} \\ - b_1[i] & \text{if } n_0 < n_1 \text { and } i \geq 8 \cdot \min \\{ n_1, n_2 \\} \\ - 1 & \text{if } b_0[i] = b_1[i] = 1 \\ - 0 & \text{otherwise} \\ - \end{cases} -$$ +For all $i \in 0, 1, \ldots, n - 1$, we have +$b_r\\{i\\} = b_0\\{i\\} \text{ }\\& \text{ } b_1\\{i\\}$, where $\\&$ refers to a +[bitwise AND][bitwise-and]. Some examples of the intended behaviour of `bitwiseLogicalAnd` follow. For brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. @@ -378,29 +398,19 @@ bitwiseLogicalAnd False [0x4F, 0x00] [0xF4] => [0x44, 0x00] 2. The first input `BuiltinByteString`. This is the _first data argument_. 3. The second input `BuiltinByteString`. This is the _second data argument_. -Let $b_1, b_2$ refer to the first data argument and the second data -argument respectively, and let $n_1, n_2$ be their respective lengths in bytes. -Let the result of `bitwiseLogicalOr`, given $b_1, b_2$ and some padding -semantics argument, be $b_r$, of length $n_r$ in bytes. We use $b_1[i]$ to refer -to the value at index $i$ of $b_1$ (and analogously for -$b_2, b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) -for the exact specification of this. - -If the padding semantics argument is `True`, then we have $n_r = \max \{ n_1, -n_2 \}$; otherwise, $n_r = \min \{ n_1, n_2 \}$. For all $i \in 0, 1, \ldots 8 -\cdot n_r - 1$, we have - -$$ -b_r[i] = \begin{cases} - b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \\{ n_1, n_2 \\} \\ - b_1[i] & \text{if } n_0 < n_1 \text { and } i \geq 8 \cdot \min \\{ n_1, n_2 \\} \\ - 0 & \text{if } b_0[i] = b_1[i] = 0 \\ - 1 & \text{otherwise} \\ - \end{cases} -$$ +Let $b_1, b_2$ refer to the semantics-modified first data argument and +semantics-modified second data argument respectively, and let $n$ be either of +their lengths in bytes; see the +[section on padding versus truncation semantics](#padding-versus-truncation-semantics) +for the exact specification of this. Let the result of `bitwiseLogicalOr`, given +$b_1, b_2$ and some padding semantics argument, be $b_r$, also of length $n$ +in bytes. We use $b_1\\{i\\}$ to refer to the byte at index $i$ in $b_1$ (and +analogously for $b_2$, $b_r#); see the [section on the bit indexing +scheme](#bit-indexing-scheme) for the exact specification of this. -Some examples of the intended behaviour of `bitwiseLogicalOr` follow. For -brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. +For all $i \in 0, 1, \ldots, n - 1$, we have +$b_r\\{i\\} = b_0\\{i\\} \text{ } \| \text{ } b_1\\{i\\}$, where $\|$ refers to +a [bitwise OR][bitwise-or]. ``` -- truncation semantics @@ -436,26 +446,19 @@ bitwiseLogicalOr False [0x4F, 0x00] [0xF4] => [0xFF, 0x00] 2. The first input `BuiltinByteString`. This is the _first data argument_. 3. The second input `BuiltinByteString`. This is the _second data argument_. -Let $b_1, b_2$ refer to the first data argument and the second data -argument respectively, and let $n_1, n_2$ be their respective lengths in bytes. -Let the result of `bitwiseLogicalXor`, given $b_1, b_2$ and some padding -semantics argument, be $b_r$, of length $n_r$ in bytes. We use $b_1[i]$ to -refer to the value at index $i$ of $b_1$ (and analogously for -$b_2, b_r$); see the [section on the bit indexing scheme](#bit-indexing-scheme) -for the exact specification of this. - -If the padding semantics argument is `True`, then we have $n_r = \max \{ n_1, -n_2 \}$; otherwise, $n_r = \min \{ n_1, n_2 \}$. For all $i \in 0, 1, \ldots 8 -\cdot n_r - 1$, we have +Let $b_1, b_2$ refer to the semantics-modified first data argument and +semantics-modified second data argument respectively, and let $n$ be either of +their lengths in bytes; see the +[section on padding versus truncation semantics](#padding-versus-truncation-semantics) +for the exact specification of this. Let the result of `bitwiseLogicalXor`, given +$b_1, b_2$ and some padding semantics argument, be $b_r$, also of length $n$ +in bytes. We use $b_1\\{i\\}$ to refer to the byte at index $i$ in $b_1$ (and +analogously for $b_2$, $b_r#); see the [section on the bit indexing +scheme](#bit-indexing-scheme) for the exact specification of this. -$$ -b_r[i] = \begin{cases} - b_0[i] & \text{if } n_1 < n_0 \text{ and } i \geq 8 \cdot \min \\{ n_1, n_2 \\} \\ - b_1[i] & \text{if } n_0 < n_1 \text { and } i \geq 8 \cdot \min \\{ n_1, n_2 \\} \\ - 0 & \text{if } b_0[i] = b_1[i] \\ - 1 & \text{otherwise} \\ - \end{cases} -$$ +For all $i \in 0, 1, \ldots, n - 1$, we have +$b_r\\{i\\} = b_0\\{i\\} \text{ } \wedge \text{ } b_1\\{i\\}$, where $\wedge$ refers to +a [bitwise XOR][bitwise-xor]. Some examples of the intended behaviour of `bitwiseLogicalXor` follow. For brevity, we write `BuiltinByteString` literals as lists of hexadecimal values. @@ -1485,4 +1488,7 @@ This CIP is licensed under [Apache-2.0](http://www.apache.org/licenses/LICENSE-2 [blake2b]: https://en.wikipedia.org/wiki/BLAKE_(hash_function) [argon2]: https://en.wikipedia.org/wiki/Argon2 [xor-crypto]: https://en.wikipedia.org/wiki/Exclusive_or#Bitwise_operation -[cip-121-big-endian]: https://github.com/mlabs-haskell/CIPs/blob/koz/to-from-bytestring/CIP-0121/README.md#representation +[cip-121-big-endian]: https://github.com/mlabs-haskell/CIPs/blob/koz/to-from-bytestring/CIP-0121/README.md#representation +[bitwise-and]: https://en.wikipedia.org/wiki/Bitwise_operation#AND +[bitwise-or]: https://en.wikipedia.org/wiki/Bitwise_operation#OR +[bitwise-xor]: https://en.wikipedia.org/wiki/Bitwise_operation#XOR From 87e52fc055d2e9d54fcdde22fcf7d99dab387e67 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Thu, 6 Jun 2024 11:52:14 +1200 Subject: [PATCH 31/32] Justification --- CIP-0122/CIP-0122.md | 105 ++++++++++++++++++++++++++++++------------- 1 file changed, 74 insertions(+), 31 deletions(-) diff --git a/CIP-0122/CIP-0122.md b/CIP-0122/CIP-0122.md index dc7849d1b7..64a886ec7b 100644 --- a/CIP-0122/CIP-0122.md +++ b/CIP-0122/CIP-0122.md @@ -1274,8 +1274,8 @@ we could define these operations. The most natural possibilities are as follows; we repeat some of the definitions used [in the corresponding section](#padding-versus-truncation-semantics). -* Extend the shorter argument with the identity element (1 for - `bitwiseLogicalAnd`, 0 otherwise) to match the length of the longer argument, +* Extend the shorter argument with the identity element (all-1s for + `bitwiseLogicalAnd`, all-0s otherwise) to match the length of the longer argument, then perform the operation as if on matching-length arguments. We call this _padding semantics_. * Ignore the bytes of the longer argument whose indexes would not be valid for @@ -1284,6 +1284,16 @@ section](#padding-versus-truncation-semantics). * Fail with an error whenever argument lengths don't match. We call this _match semantics_. +Furthermore, for both padding and truncation semantics, we can choose to pad (or +truncate) _low_ index bytes or _high_ index bytes. To illustrate the difference, +consider the two `BuiltinByteString`s (written as arrays of bytes for +simplicity) `[0xFF, 0x0F, 0x00]` and `[0x8F, 0x99]`. Under padding semantics, +padding low index bytes would give us `[0x00, 0x8F, 0x99]` (or `[0xFF, 0x8F, +0x99]` depending on operation), while padding high index bytes would give us +`[0x8F, 0x99, 0x00]` (or `[0x8F, 0x99, 0xFF]` depending on operation). Under +truncation semantics, truncating low index bytes would give us `[0x0F, 0x00]`, +while truncating high index bytes would give us `[0xFF, 0x0F]`. + It is not a priori clear which of these we should choose: they are subject to different laws (as evidenced by the [corresponding section](#laws-and-examples)), none of which are strict supersets of each other @@ -1291,14 +1301,15 @@ section](#laws-and-examples)), none of which are strict supersets of each other semantics, we believe this was not the correct decision: we use Case 1 to justify the benefit of having other semantics described above available. -Consider the following operation: given a bound $k$ and an integer set, remove -all elements smaller than $k$ from the set. This can be done using -`bitwiseLogicalAnd` and a mask where the first $k - 1$ bits are clear. However, -under match semantics, the mask would have to have a length equal to the integer -set representation; under padding semantics, the mask would only need to have $\Theta(k)$ -length. This is noteworthy, as padding the mask would -require an additional copy operation, only to produce a value that would be -discarded immediately. +Consider the following operation: given a bound $k$, a 'direction' (larger or +smaller), and an integer set, remove all elements indicates by the direction and +$k$ (that is, either smaller than $k$ or larger than $k$, as indicated by the +direction). This could be done using a `bitwiseLogicalAnd` and a mask. However, +under match semantics, this mask would have to have a length equal to the +integer set representation; under padding semantics, the mask would potentially +only need $\Theta(k)$ length, depending on direction. This is noteworthy, as +padding the mask would require an additional copy operation, only to produce a +value that would be discarded immediately. Consider instead the following operation: given two integer sets with different (upper) bounds, take their intersection, producing an integer set whose size is @@ -1335,28 +1346,60 @@ reasonable needs, if only from the point of view of efficiency. This suggests, much as for [CIP-121 primitives][conversion-cip] and endianness issues, that the primitive should allow a choice in what semantics get used for any given call. Ideally, we would allow a choice of any of the three options described -above; however, this is awkward to do in Plutus Core. While the choice between +above (along with a choice of low or high index padding or truncation); +however, this is awkward to do in Plutus Core. While the choice between _two_ options is straightforward (pass a `BuiltinBool`), the choice between -_three_ options would either require multiple `BuiltinBool` arguments, or a -`BuiltinInteger` argument with 'designated values' (such as 'negative means -truncation, zero means match, positive means padding'). Neither of these are -ideal choices, as they involve either argument redundancy or additional checks -(and erroring when they don't match). In light of this, we elected to choose -only two of the three semantics and have this choice for any given call be -controlled by a `BuiltinBool` flag. - -This naturally leads to the question of which of the three semantics above we -can afford to exclude: we believe that match semantics are the choice, for -several reasons. Firstly, technically we can still have match semantics by using either -padding or truncation semantics plus a length check beforehand: this is a cheap -operation, unlike simulating padding semantics for example, which would have -non-trivial cost. Secondly, due to the preponderance of truncation semantics in -Haskell, we feel that excluding them as an option is both surprising and wrong. -Lastly, we believe that -outside of error checking, exact match semantics give few benefits over padding -or truncation semantics, for performance and otherwise. This combination of -reasoning leads us to naturally consider padding and truncation as the two to -keep, and this guided our implementation choices. +more than this number would require something like a `BuiltinInteger` argument +with 'designated values' ('0 means match', '1 means low-index padding', etc). +This is not ideal, as they involve additional checks, argument redundancy, or +both. In light of this, we made the following decisions: + +1. We would choose only two of the three semantics, and have this choice + controlled for any given call be controlled by a `BuiltinBool` flag; and +2. For padding or truncation semantics, we would _always_ use either low or high + index padding (or truncation). + +This leads naturally to two questions: which of the three semantics above we can +afford to exclude, and whether low or high index padding should be chosen. We +believe that the correct choices are to exclude match semantics, and to use +high index padding and truncation, for several reasons. + +Firstly, we can simulate +match semantics with either padding or truncation semantics, together with a +length check. While we could also simulate padding semantics via match semantics +similarly, the amount of effort (both developer and computational) required is +significantly more in that case: a length check is a constant-time operation, +while manually padding is linear at best (and even then, it requires operations +only this CIP provides, as it would be quadratic otherwise), and on top of that, +manual padding is much fiddlier and easier to get wrong. + +Secondly, truncation semantics are common enough in Haskell that we believe +excluding them as an option is both surprising and wrong. Any developer familiar +with Haskell has interacted with various `zipWith` operations, and having our +primitives behave differently to this at minimum creates friction for +implementers of higher-level abstractions atop the primitives in this CIP. While +Haskellers are not exclusive users of Plutus primitives (directly or not), there +are definitely enough of them that _not_ having truncation semantics available +would create a lot of unnecessary friction. + +Thirdly, outside of error checking, match semantics give few benefits, +performance or otherwise. The examples above demonstrate cases where padding and +truncation semantics lead to better performance, less fiddly implementations, or +both: finding such a case for match semantics outside of error checking is +difficult at best. + +This combination of reasoning leads us to consider padding and truncation as the +two semantics we should retain, and this guided our implementation choices +accordingly. With regard to padding (or truncating) low or high indexes, given +that we pad (or truncate) whole bytes by necessity, it makes the corresponding +operations (effectively) operate over bytes, or rather, they view +`BuiltinByteString`s as linear collections of bytes, rather than bits. When +viewed this way, the `zipWith` analogy with Haskell suggests that truncating +high is the correct choice: truncating low would be quite surprising to a +Haskeller familiar with how `zipWith`-style operations behave. Furthermore, as +having padding low and truncating high would be confusing (and arguably quite +strange), padding high seems like the correct choice. Thus, we decided to both +pad and truncate high in light of this. ### Bit setting From 1e4ec599130e384275ca6279fa3dca1d2f974f92 Mon Sep 17 00:00:00 2001 From: Koz Ross Date: Wed, 12 Jun 2024 07:35:59 +1200 Subject: [PATCH 32/32] Rename CIP document --- CIP-0122/{CIP-0122.md => README.md} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename CIP-0122/{CIP-0122.md => README.md} (100%) diff --git a/CIP-0122/CIP-0122.md b/CIP-0122/README.md similarity index 100% rename from CIP-0122/CIP-0122.md rename to CIP-0122/README.md