1. Name the objects
Ask what kind of thing each symbol is: integer, set element, function, witness, randomness, polynomial, or group element.
How To Read This
Use each slide as a proof-reading drill, not just a summary
2. Separate assumptions from goals
Most confusion comes from using the conclusion too early or forgetting what was actually assumed.
3. Ask what proof move fits
Direct proof, contradiction, contrapositive, or induction are different control flows. Choose one on purpose.
SP1 lens: SP1 is a zkVM that proves correct execution of programs compiled for RISC-V, and lets developers write provable programs in ordinary Rust rather than custom circuits. Read every math idea here as a way to better understand what your SP1 program is claiming when it proves a light client computation.
Slide Deck
Seven ideas you need before zk starts feeling natural
01
Math is a language of exact claims
The first job is not “solve the theorem.” It is to rewrite the statement into assumptions, variables, and a precise goal.
- Every definition is an API contract.
- Every theorem has inputs, output, and hidden dependencies.
- ZK papers compress many assumptions into a single line.
Plain English: Math statements are not prose. They are executable specifications.
ZK analogy: “Given public input x and witness w, prove C(x, w) = 1” already contains the domain, condition, and target.
SP1 association: In SP1, your statement is often “this Rust program, compiled to RISC-V, executed correctly on these inputs and exposed these public values.”
What to do: Before reading any proof, rewrite the statement as “inputs -> condition -> goal”.
Teacher Notes
Concrete example: “If a header’s parent hash matches the trusted tip and its signatures are valid, accept the next checkpoint.” Here the objects are header, trusted tip, signatures; the assumptions are hash linkage and signature validity; the goal is acceptance.
Common mistake: Saying “prove the header is valid” without listing what “valid” means. In math and in protocols, undefined words are where bugs hide.
SP1 translation: Your prover does not prove “Ethereum is valid.” It proves that your specific Rust verifier program produced a specific result on a specific input.
Claim
For every witness w, if constraints are satisfied, then the
verifier accepts.
Domain
witness space
Condition
constraints hold
Goal
acceptance follows
02
Sets train you to reason about domains
A surprising amount of later confusion is really “I forgot what object lives in what set.”
- Subset proofs become “take an arbitrary element and show it belongs.”
- Intersections model multiple simultaneous conditions.
- Cartesian products model tuples like public input, witness, randomness.
Plain English: Sets answer “where is this object allowed to live?”
ZK analogy: A valid witness often lies in an intersection like “field elements” and “satisfies all constraints”.
SP1 association: For a light client, think in domains like “well-formed headers”, “trusted checkpoints”, “execution inputs”, and “publicly committed outputs”.
Mastery check: Can you explain why proving A ⊆ B means starting with an arbitrary x in A?
Teacher Notes
Concrete example: Let A be the set of headers whose signatures verify. Let B be the set of headers accepted by your prefilter. If you want to prove A ⊆ B, pick an arbitrary header in A and show it passes the prefilter rules.
Common mistake: People often prove set equality by checking a few examples. That proves nothing. You need two containments: A ⊆ B and B ⊆ A.
SP1 translation: Keep separate sets for private inputs, public values, trusted states, and accepted outputs. Mixing them mentally makes protocol reasoning much harder.
Intersection isolates objects that satisfy both requirements.
03
Quantifiers decide the meaning of your protocol claim
ZK statements are quantifier-heavy: “for all adversaries,” “there exists a simulator,” “for every witness,” “there exists randomness.”
- Changing quantifier order changes the theorem.
- Negation flips
forallandexists. - This is the mental core of soundness and zero-knowledge definitions.
Plain English: “For every x there exists y” lets y depend on x. “There exists y for every x” requires one y to work everywhere.
ZK analogy: In simulation-based security, the order of “for every verifier” and “there exists a simulator” is the definition.
SP1 association: Soundness-style thinking for SP1 is still quantifier thinking: for every claimed program/input/output tuple, if no valid execution exists, no adversary should produce an accepting proof except with negligible probability.
Mastery check: Can you negate “for every witness there exists randomness making the transcript valid”?
Teacher Notes
Concrete example: “For every block number n, there exists a Merkle branch proving account balance at n.” This allows a different branch for each n. If you swap the order to “there exists one branch for every n,” the claim becomes absurd.
Common mistake: Reading quantifiers too fast and treating them as decoration. They are the whole meaning of the theorem.
SP1 translation: When you reason about malicious provers, invalid headers, or verifier acceptance, say the quantifiers out loud. It is the fastest way to catch a wrong security statement.
x in statements
y as response
For each input x, you may choose a different y. This is much weaker than finding one universal y.
04
Proof tactics are control flow
Direct proof, contrapositive, contradiction, and induction are not decorations. They are execution strategies.
- Direct proof: start with assumptions and derive target.
- Contrapositive: prove “not target implies not assumption.”
- Contradiction: assume failure and force impossibility.
- Induction: establish base case, then preserve invariant.
Plain English: These are not stylistic choices. They are different ways to route information from assumptions to conclusion.
ZK analogy: Soundness proofs often use contradiction or contrapositive; recursive protocol arguments often use induction.
SP1 association: If your light client processes a sequence of headers, your engineering intuition already uses induction: assume the previous checkpoint is trusted, then prove the next transition preserves validity.
What to do: When stuck, do not push symbols blindly. Switch proof mode.
Teacher Notes
Concrete example: To prove “if a header is finalized then it is descendant-consistent with the trusted checkpoint,” a contrapositive may be easier: if it is not descendant-consistent, then it cannot be finalized under your rules.
Common mistake: Starting a contradiction proof without identifying what contradiction would count as impossible. You need a hard conflict: violates a definition, assumption, or known theorem.
SP1 translation: If your verifier logic is iterative over header updates, induction is not just math class. It is the cleanest proof skeleton for chain-extension arguments.
Direct proofs are best when the target can be built from definitions and known lemmas.
05
Modular arithmetic is your first real zk-native chapter
Once you work modulo p, arithmetic becomes field arithmetic,
and that is the substrate for most modern proving systems.
- Equivalent classes explain why many integers represent one residue.
- Inverses matter because division becomes multiplication by inverse.
- Field intuition later powers FFTs, interpolation, and polynomial identities.
Plain English: Mod arithmetic means numbers wrap around. Different integers can represent the same value after wrapping.
ZK analogy: In most proving systems, witness values and constraint arithmetic happen inside a finite field F_p, not over ordinary integers.
SP1 association: SP1 lets you write normal Rust, but the proving system underneath is still algebraic. Field arithmetic, polynomial commitments, and recursion are below the surface even if your application code looks ordinary.
Mastery check: In mod 7, why do 3, 10, and 17 behave like the same element?
Teacher Notes
Concrete example: In mod 7, 10 ≡ 3 because 10 - 3 = 7, and 17 ≡ 3 because 17 - 3 = 14. They differ by multiples of 7, so they are the same residue class.
Common mistake: Thinking mod arithmetic is “ordinary arithmetic but smaller.” Division is different, inverses depend on the modulus, and equal-looking integer intuitions can fail.
SP1 translation: Even if your light-client code is written against bytes, hashes, and Rust structs, the proof system below ultimately encodes computation algebraically. That is why modular/field reasoning matters.
Mod 7 wraps integers into 7 residue classes. Every step lands on one of these positions.
06
Functions are the cleanest model for protocol maps
Provers, verifiers, encoders, commitments, and hash functions are all maps between structured sets.
- Injective: different inputs do not collide.
- Surjective: every target output is reachable.
- Bijective: perfect reversible correspondence.
Plain English: A function is a rule that assigns exactly one output to each input.
ZK analogy: Think of commitment schemes, encodings, and prover/verifier algorithms as maps between domains.
SP1 association: A useful mental model is (ELF, stdin) -> execution trace -> public values -> proof. Precompiles are specialized sub-machines that implement some maps more efficiently than generic execution.
Mastery check: Why does bijective imply invertible, but surjective alone does not?
Teacher Notes
Concrete example: A hash function takes one input and returns one output, so it is a function. It is not injective over large domains, because collisions must exist. A permutation over a fixed finite set can be bijective.
Common mistake: Confusing “hard to invert” with “not a function.” A one-way function is still a perfectly valid function; it is just computationally hard to reverse.
SP1 translation: Model your system as a sequence of maps. If you cannot say what goes in and what comes out of each stage, the prover pipeline stays mysterious.
Injective maps preserve distinctness, which is the intuition behind many “binding” style properties.
07
Bridge the book into actual zk study
This book builds mathematical maturity. It does not fully cover the main zk-specialized layers, so your second phase must add them deliberately.
- After modular arithmetic: finite fields and polynomial reasoning.
- After functions: linear algebra and maps over vectors/matrices.
- After proof fluency: cryptographic definitions and simulators.
Plain English: This book is the ramp, not the whole mountain.
ZK analogy: The book teaches you how to read and write precise claims. The next layer teaches the algebra used by PLONK, STARKs, sumcheck, and commitments.
SP1 association: The official docs say SP1 proves correct execution for RISC-V programs and uses a multilinear proof system plus optimized recursion in current versions. That means your day job can stay in Rust, but understanding fields, commitments, and recursive composition still pays off.
What to do: Finish chapters 1-7 well enough that definitions and proof skeletons no longer feel slow.
Teacher Notes
Concrete example: If you understand definitions, quantifiers, induction, modular arithmetic, and functions, then later topics like “the prover commits to multilinear evaluations and recursion compresses proofs” become learnable rather than opaque.
Common mistake: Jumping straight to PCS, recursion, or STARK internals without being fluent in proof language. That usually feels like memorization, not understanding.
SP1 translation: This foundation is what lets you move from “SP1 works” to “I can reason about what SP1 is claiming, where the costs come from, and what security statement my application relies on.”
Proof language
Induction
Mod arithmetic
Functions
Finite fields
Polynomials
Linear algebra
ZK systems