book: Document SHA-256 chip instructions and gadget interface

book/src/design/gadgets.md

@@ -0,0 +1,3 @@
+# Gadgets
+
+In this section we document the gadgets and chip designs provided by halo2.

book/src/design/gadgets/sha256.md

@@ -1,3 +1,56 @@
 # SHA-256
 
-halo2 provides a SHA-256 gadget `halo2::gadget::sha256::Sha256` which...
+## Specification
+
+SHA-256 is specified in [NIST FIPS PUB 180-4](https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf).
+
+Unlike the specification, we use $\boxplus$ for addition modulo $2^{32}$, and $+$ for
+field addition. $\oplus$ is used for XOR.
+
+## Gadget interface
+
+SHA-256 maintains state in eight 32-bit variables. It processes input as 512-bit blocks,
+but internally splits these blocks into 32-bit chunks. We therefore designed the SHA-256
+gadget to consume input in 32-bit chunks.
+
+## Chip instructions
+
+The SHA-256 gadget requires a chip with the following instructions:
+
+```rust
+pub trait Sha256Instructions: Chip {
+    /// Variable representing the SHA-256 internal state.
+    type State: Clone + fmt::Debug;
+    /// Variable representing a 32-bit word of the input block to the SHA-256 compression
+    /// function.
+    type BlockWord: Copy + fmt::Debug;
+
+    /// Places the SHA-256 IV in the circuit, returning the initial state variable.
+    fn initialization_vector(layouter: &mut impl Layouter<Self>) -> Result<Self::State, Error>;
+
+    /// Starting from the given initial state, processes a block of input and returns the
+    /// final state.
+    fn compress(
+        layouter: &mut impl Layouter<Self>,
+        initial_state: &Self::State,
+        input: [Self::BlockWord; BLOCK_SIZE],
+    ) -> Result<Self::State, Error>;
+
+    /// Converts the given state into a message digest.
+    fn digest(
+        layouter: &mut impl Layouter<Self>,
+        state: &Self::State,
+    ) -> Result<[Self::BlockWord; DIGEST_SIZE], Error>;
+}
+```
+
+TODO: Add instruction for computing padding.
+
+This set of instructions was chosen to strike a balance between the reusability of the
+instructions, and the scope for chips to internally optimise them. In particular, we
+considered splitting the compression function into its constituent parts (Ch, Maj etc),
+and providing a compression function gadget that implemented the round logic. However,
+this would prevent chips from using relative references between the various parts of a
+compression round. Having an instruction that implements all compression rounds is also
+similar to the Intel SHA extensions, which provide an instruction that performs multiple
+compression rounds.

book/src/design/gadgets/sha256/table16.md

@@ -1,19 +1,9 @@
 # 16-bit table chip for SHA-256
 
-The main chip implementation for SHA-256 in halo2 is based around a 16-bit lookup table.
+This chip implementation is based around a single 16-bit lookup table. It requires a
-This requires a minimum of $2^{16}$ circuit rows, and is therefore suitable for use in
+minimum of $2^{16}$ circuit rows, and is therefore suitable for use in larger circuits.
-larger circuits.
 
-## Specification
+We target a maximum constraint degree of $9$. That will allow us to handle constraining
-
-SHA-256 is specified in [NIST FIPS PUB 180-4](https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf).
-
-Unlike the specification, we use $\boxplus$ for addition modulo $2^{32}$, and $+$ for
-field addition.
-
-$\oplus$ is used for XOR.
-
-Let's target a max constraint degree of $9$. That will allow us to handle constraining
 carries and "small pieces" to a range of up to $\{0..7\}$ in one row.
 
 ## Compression round