update

src/SUMMARY.md

@@ -11,22 +11,23 @@
 
 # Circuits
 
-- [AIR](./air/air.md)
+- [The AIR Arithmetization](./air/air.md)
 
-# Protocol
+# STARK
 
 - [STARK](./stark/overview.md)
-
-# PCS
-
 - [FRI](./fri/fri.md)
 
-# Cairo
+# Cairo: a zkVM
 
 - [Cairo](./cairo/cairo.md)
 - [Cairo public memory](./cairo/memory.md)
+- [Bootloader](./cairo/bootloader.md)
 
-# Verifying Cairo programs on Ethereum
+# Starkex: Verifying Cairo programs on Ethereum
 
-- [Bootloader](./cairo/bootloader.md)
-- []()
+- []()
+
+# Starknet
+
+- [Starknet](./starknet/starknet.md)

src/cairo/cairo.md

@@ -1,5 +1,7 @@
 # Cairo
 
+Check cairo book: https://book.cairo-lang.org/
+
 There's different ways to write for the Cairo VM:
 
 * using Cairo instructions directly, documented in the Cairo paper (good luck) 

src/fri/deep.md

@@ -0,0 +1,12 @@
+# Domain Extension for Eliminating Pretenders (DEEP)
+
+* sounds like an upgrade to FRI in order to reduce the number of queries while keeping the same soundness
+* but risc0 says it's not:
+
+> Shortly after the FRI protocol was released, an alternative protocol called DEEP-FRI was released. Although DEEP-FRI was initially thought to have improved soundness relative to FRI, the Proximity Gaps for Reed-Solomon Codes paper shows that the original FRI protocol offers the same soundness results as DEEP-FRI at less computational complexity. The RISC Zero ZKP system uses the original FRI protocol.
+
+from: https://dev.risczero.com/reference-docs/about-fri
+
+* yet starkware seems to use it with their DEEP as well as OODS (out-of-domain sampling) stuff
+* DEEP-FRI is described in section 5.2 of the DEEP-FRI paper
+* DEEP-ALI is described later in that same paper. It's a STIK (which you can isntantiate as a STARK like ethSTARK) that makes use of DEEP-FRI

src/math/code_theory.md

@@ -1 +1,62 @@
 # Code Theory
+
+* I think "succinct proofs and linear algebra" provides a good intro and notation
+
+## Hamming weight
+
+hamming weight of a string is the number of non-zero entries.
+
+> The Hamming weight of a string is the number of symbols that are different from the zero-symbol of the alphabet used
+
+For $s = (1, 0, 0, 1, 1)$ we have:
+
+$$
+\text{hamming_weight}(s) = 3
+$$
+
+in other words for $\vec{x} \in F^n$ we have:
+
+$$
+\text{hamming_weight}(\vec{x}) = |\{ i | x[i] \neq 0 \}|
+$$
+
+## Hamming Distance
+
+> In information theory, the Hamming distance between two strings of equal length is the number of positions at which the corresponding symbols are different.
+
+$$
+\text{hamming_distance}(\vec{x}, \vec{y}) = |\{ i | x[i] \neq y[i] \}|
+$$
+
+## Repeated code
+
+$$
+G = [I_n, \cdots, I_n]^t
+$$
+
+($I_n$ is the identity, repeated $k$ times in the matrix)
+
+$$
+G \vec{x} = [x[0], \cdots, x[n-1], x[0], \cdots, x[n-1], \cdots]
+$$
+
+($\vec{x}$ repeated $k$ times)
+
+## Reed–Solomon error correcting code
+
+$$
+RS[F, D, \rho] := \{ f : D \rightarrow F : deg(f) < \rho \cdot |D| \}
+$$
+
+"the RS code of rate $\rho$ evaluated over $D$".
+
+## Johnson bound
+
+What is Johnson bound?
+
+> TODO: We should explain it here, and also make sure we have defined everything we need to understand it.
+
+Let $V \in F^D$ be a code with minimum relative distance $1 - \rho$, for $\rho \in (0, 1)$.
+Then $V$ is $(1 - \sqrt{\rho} - \epsilon, 1/(2 \epsilon \sqrt{\rho}))$-list-decodable for every $\epsilon \in (0, 1 - \sqrt{\rho})$.
+
+> TODO: is this the conjecture, or is conjecture 2.3 from the DEEP paper the conjecture based on the Jonhson bound?

src/stark/stark.md

@@ -0,0 +1,19 @@
+# STARKs
+
+https://eprint.iacr.org/2018/046.pdf section 3
+
+## IOP: Interactive Oracle Proof
+
+* 
+
+## STIK: Scalable Transparent IOP of Knowledge
+
+* 
+* "A STARK, defined later, is a realization of a scalable and transparent IOP of knowledge (STIK)"
+* 
+
+## STARK: 
+
+## ethSTARK
+
+is this the main STARK that everyone seems to use? (at least starkware's GPS and risc0)

src/starkex/bootloader.md

@@ -0,0 +1,2 @@
+# Bootloader
+

src/starkex/cairo.md

@@ -0,0 +1,12 @@
+# Verifying Cairo proofs
+
+Verifying a SHARP Cairo proof on the Starkex contracts is done in a number of transactions:
+
+* 3 Verify Merkle transactions ([example](https://etherscan.io/tx/0x5ad19d4524e0d2f2281dd71b8b1030fca7131ce74b821b936f73df2cba9d65e5))
+* 8 Verify FRI transactions ([example](https://etherscan.io/tx/0xccc7446d9e5e14892496ee3956f0e9579c2f56b8e70441623aa283c302130201))
+* A bunch of Register Continuous Memory Page ([example](https://etherscan.io/tx/0x6862ef5e0ce7599124e7c81625130990a102f483dde292d76b8d869b7d280ea7))
+* A single Verify Proof and Register ([example](https://etherscan.io/tx/0x720571bcac39e6b973537d7dd2ba253072e6f82c634ce361de73769d026ce4a1))
+
+The reason the verification of a proof is split in multiple transactions is because proofs are too large, and the verification cost too much gas, to fit in a single transaction. 
+
+> Note: Proofs can be split using [stark-evm-adapter](https://github.com/zksecurity/stark-evm-adapter/)

src/starkex/facts.md

@@ -0,0 +1,106 @@
+# Fact Registry
+
+The [Starkex contracts](https://github.com/starkware-libs/starkex-contracts/) implement the verifier side of the [SHARP service](https://starkware.co/resource/joining-forces-sharp/). 
+In other words, when people create proofs using the [SHARP service](https://starkware.co/resource/joining-forces-sharp/), they can get them verified on Ethereum using the [Starkex contracts](https://github.com/starkware-libs/starkex-contracts/).
+
+First, let's introduce what a fact is: a fact can be any computation that was computed by some logic in the smart contract. For example, a fact can be: "_we successfully verified a proof for this Cairo program and these public inputs_".
+This example is actually the main fact that Starkex will register for the different applications making use of it.
+But internally, other facts are used whenever a computation (like verifying a proof) is split in different transactions that need to produce a snapshot of what has been done so far and resume from other snapshots. This is explained in more details in the [Verifying Cairo proofs](./cairo.md) section.
+
+A fact is represented (or authenticated) by a hash of it. As such, it is important that different applications or different contexts use "different" hash functions not to have collisions. This can be done by adding some domain separation string to the hash function.
+
+## The Fact Registry
+
+Let's introduce the smart contract in charge of these facts, [FactRegistry.sol](https://github.com/starkware-libs/starkex-contracts/blob/aecf37f2278b2df233edd13b686d0aa9462ada02/scalable-dex/contracts/src/components/FactRegistry.sol):
+
+```solidity
+contract FactRegistry is IQueryableFactRegistry {
+    // Mapping: fact hash -> true.
+    mapping(bytes32 => bool) private verifiedFact
+```
+
+As you can see, facts are just tracked via a hashmap. Registering a fact is such straightfoward:
+
+```solidity
+    function registerFact(bytes32 factHash) internal {
+        // This function stores the fact hash in the mapping.
+        verifiedFact[factHash] = true;
+```
+
+As well as checking if a fact has been registered:
+
+```solidity
+    function isValid(bytes32 fact) external view override returns (bool) {
+        return _factCheck(fact);
+    }
+```
+
+## Example of registering a fact
+
+An example of registering a fact can be seen, for example at the end of a proof verification. In [GpsStatementVerifier.sol:verifyProofAndRegister()](https://github.com/starkware-libs/starkex-contracts/blob/aecf37f2278b2df233edd13b686d0aa9462ada02/evm-verifier/solidity/contracts/gps/GpsStatementVerifier.sol#L71):
+
+```solidity
+    function verifyProofAndRegister(
+        uint256[] calldata proofParams,
+        uint256[] calldata proof,
+        uint256[] calldata taskMetadata,
+        uint256[] calldata cairoAuxInput,
+        uint256 cairoVerifierId
+    ) external {
+        // TRUNCATED...
+
+        registerGpsFacts(taskMetadata, publicMemoryPages, cairoAuxInput[OFFSET_OUTPUT_BEGIN_ADDR]);
+    }
+```
+
+where `registerGpsFacts` is defined as:
+
+```solidity
+    function registerGpsFacts(
+        uint256[] calldata taskMetadata,
+        uint256[] memory publicMemoryPages,
+        uint256 outputStartAddress
+    ) internal {
+        // TRUNCATED...
+
+        // Register the fact for each task.
+        for (task = 0; task < nTasks; task++) {
+            // TRUNCATED...
+
+            bytes32 fact = keccak256(abi.encode(programHash, programOutputFact));
+
+            // TRUNCATED...
+            registerFact(fact);
+
+            // TRUNCATED...
+        }
+
+        // TRUNCATED...
+    }
+```
+
+## Example of checking if a fact is registered
+
+[Starknet]() is one user of SHARP, and as such their smart contract uses the fact registry.
+
+The main function of Starknet is [`updateState()`](https://github.com/mimoo/starknet-contracts/blob/main/contracts/Starknet.sol#L176) which updates the state based on proofs that have been verified:
+
+```solidity
+    function updateState(
+        int256 sequenceNumber,
+        uint256[] calldata programOutput,
+        uint256 onchainDataHash,
+        uint256 onchainDataSize
+    ) external onlyOperator {
+        // TRUNCATED...
+        
+        bytes32 sharpFact = keccak256(
+            abi.encode(programHash(), stateTransitionFact)
+        );
+        require(
+            IFactRegistry(verifier()).isValid(sharpFact),
+            "NO_STATE_TRANSITION_PROOF"
+        );
+
+        // TRUNCATED...
+```

src/starkex/starkex.md

@@ -0,0 +1,14 @@
+# Starkex
+
+The starkex contract live in https://github.com/starkware-libs/starkex-contracts
+They implement the [SHARP (SHARed Prover)](https://starkware.co/resource/joining-forces-sharp/) verifier, which allows us to verify SHARP proofs on Ethereum.
+
+> Note: A number of contracts refer to "GPS" which is the old name for SHARP (general-proving service).
+
+Any application on Ethereum that wants to use Cairo can make use of this service to verify proofs.
+The flow is split in two parts:
+
+1. The proof is sent to the SHARP service, which verifies it and returns a fact.
+2. The application can check that the fact has been verified.
+
+We explain what "facts" are in [facts section](/facts.md).

src/starknet/starknet.md

@@ -0,0 +1,3 @@
+# Starknet
+
+See more: https://book.starknet.io/