diff --git a/courses/scr403/assets/en/001.webp b/courses/scr403/assets/en/001.webp
new file mode 100644
index 00000000000..766bcb283b3
Binary files /dev/null and b/courses/scr403/assets/en/001.webp differ
diff --git a/courses/scr403/assets/en/002.webp b/courses/scr403/assets/en/002.webp
new file mode 100644
index 00000000000..1dee861be3b
Binary files /dev/null and b/courses/scr403/assets/en/002.webp differ
diff --git a/courses/scr403/assets/en/003.webp b/courses/scr403/assets/en/003.webp
new file mode 100644
index 00000000000..ea0228c046f
Binary files /dev/null and b/courses/scr403/assets/en/003.webp differ
diff --git a/courses/scr403/assets/thumbnail.webp b/courses/scr403/assets/thumbnail.webp
new file mode 100644
index 00000000000..18a7badb155
Binary files /dev/null and b/courses/scr403/assets/thumbnail.webp differ
diff --git a/courses/scr403/course.yml b/courses/scr403/course.yml
new file mode 100644
index 00000000000..66f2d79655e
--- /dev/null
+++ b/courses/scr403/course.yml
@@ -0,0 +1,44 @@
+id: 1f6d0544-c6f0-42c6-a8ef-acf485807b9d
+
+topic: protocol
+
+subtopic: script
+type: theory
+
+level: expert
+
+hours: 10
+
+teaching_format: self_paced
+
+professors_id:
+ - a3b29adb-43ee-49f4-9582-b37e9cf72858
+
+contributor_names:
+ - rogzy
+
+published_at: 2026-03-02
+
+tags:
+ - simplicity
+ - liquid
+ - scripting
+ - combinators
+ - type-system
+ - jets
+ - side-effects
+ - addresses
+ - CMR
+ - witness
+
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
+
+license: CC-BY-SA-V4
diff --git a/courses/scr403/en.md b/courses/scr403/en.md
new file mode 100644
index 00000000000..2c236323cb8
--- /dev/null
+++ b/courses/scr403/en.md
@@ -0,0 +1,842 @@
+---
+name: Delving Into Simplicity
+goal: Master the design philosophy, type system, and full lifecycle of Simplicity
+objectives:
+ - Understand the three fundamental composition methods and the nine combinators that form a complete language
+ - Build boolean logic, arithmetic, and SHA-256 from Simplicity's minimal type system
+ - Grasp how the Failure and Reader side effects enable real blockchain interaction
+ - Learn how Simplicity programs become Taproot addresses and are redeemed with witness data
+---
+
+# Delving Into Simplicity
+
+A deep dive into the theory and design decisions behind the Simplicity language, based on the complete five-part ["Delving Simplicity"](https://delvingbitcoin.org/t/delving-simplicity-part-three-fundamental-ways-of-combining-computations/1902) article series by [Dr. Russell O'Connor](https://r6.ca/), the creator of Simplicity at Blockstream Research. This course explains *why* Simplicity was designed the way it was, not how to write it.
+
+The course follows Dr. O'Connor's articles through the three fundamental ways of combining computations, the minimal type system and its completeness theorem, the construction of practical data types and arithmetic from first principles, the careful introduction of side effects for blockchain interaction, and finally how programs are committed to addresses and redeemed on-chain.
+
++++
+
+# Introduction
+
+c362889b-c630-435f-911b-724c4eca505b
+
+## Course overview
+
+cdcc40b6-c985-45b4-9bee-6f931e984476
+
+Welcome to SCR403 — Delving Into Simplicity!
+
+This course is based on the **"Delving Simplicity"** article series written by [Dr. Russell O'Connor](https://r6.ca/), an Infrastructure Tech Developer at [Blockstream](https://blockstream.com/) and the creator of Simplicity. The original articles were published on the [Delving Bitcoin](https://delvingbitcoin.org/u/roconnor-blockstream/summary) forum and form the primary source material for this course. We are grateful for his pioneering work, which made this educational content possible.
+
+### What you will learn
+
+This course explores the design philosophy and mathematical foundations behind Simplicity, the next-generation scripting language activated on the [Liquid Network](https://blockstream.com/press-releases/2025-07-31-blockstream-launches-simplicity/) in July 2025. It follows the complete five-part article series and is structured in two main content sections:
+
+1. **Foundations of Simplicity** — Why blockchain computation demands a fundamentally different language, the three ways to combine operations (sequential, parallel, conditional), and the nine core combinators that form a mathematically complete language
+2. **From Data Types to Programs** — Building boolean logic, arithmetic, and SHA-256 from first principles; understanding the Failure and Reader side effects that enable blockchain interaction; and learning how programs are committed to Taproot addresses via Commitment Merkle Roots and redeemed with witness data
+
+### Prerequisites
+
+This is an **expert-level** course (approximately 10 hours). You should be comfortable with:
+- Basic Bitcoin scripting concepts (what transaction validation does)
+- Fundamental programming concepts (types, functions, composition)
+- Some familiarity with mathematical notation is helpful but not required. We introduce everything as we go
+
+### Key resources
+
+- **Original articles**: ["Delving Simplicity"](https://delvingbitcoin.org/u/roconnor-blockstream/summary) by Dr. Russell O'Connor on Delving Bitcoin
+- **Simplicity repository**: [BlockstreamResearch/simplicity](https://github.com/BlockstreamResearch/simplicity) — source code and Rocq formal proofs
+- **Official website**: [simplicity-lang.org](https://simplicity-lang.org/) — documentation and SimplicityHL reference
+- **Blockstream blog**: [Simplicity on GitHub](https://blog.blockstream.com/en-simplicity-github/) — technical overview
+
+Ready to dive into one of the most elegant pieces of Bitcoin engineering? Let's go!
+
+## What is Simplicity?
+
+d04f3960-d7fb-44e1-b5a3-25b33d03fd38
+
+If you're coming to this course without a background in Simplicity, this chapter will orient you before we dive into the deep end.
+
+### Simplicity in a nutshell
+
+Simplicity is a **Bitcoin-native smart contract language**, live on the Liquid Network today. First envisioned by Dr. Russell O'Connor around 2012 and detailed in his 2017 paper *Simplicity: A New Language for Blockchains*, it was activated on the Liquid Network in July 2025 after years of formal verification and development.
+
+Unlike Ethereum's Solidity, which is a Turing-complete, high-level contract language, Simplicity is intentionally minimal. It has:
+- **Three type formers** (unit, sum, product)
+- **Nine combinators** (basic operations and composition rules)
+- **No loops, no recursion, no dynamic memory**
+
+From just these primitives, you can build any computation you need for transaction validation, from boolean logic to full SHA-256 hashing.
+
+### What can you do with Simplicity today?
+
+Simplicity is already powering real applications on the Liquid Network. The most notable is the [Simplicity DEX](https://docs.simplicity-lang.org/use-cases/simplicity-dex/), an oracle-free options marketplace where users trade call options on L-BTC using USDt as collateral (the underlying contract also supports puts). Other live Simplicity projects include [Swaption](https://swaption.io/) by SideSwap (options) and the open-source [Deadcat](https://github.com/Resolvr-io/deadcat) by Resolvr (prediction markets). Beyond DeFi, Simplicity enables advanced spending conditions such as vaults, covenants, and complex multisig schemes that would be impossible or unsafe in Bitcoin Script.
+
+### What this course is — and isn't
+
+This is **not** a hands-on coding tutorial. You won't write Simplicity programs here. If you're looking for that, check out:
+- [simplicity-lang.org](https://simplicity-lang.org/) — official documentation and the SimplicityHL high-level language
+- The [Simplicity GitHub repository](https://github.com/BlockstreamResearch/simplicity) — reference implementation, examples, and Rocq proofs
+- The [Blockstream blog post](https://blog.blockstream.com/en-simplicity-github/) on getting started
+
+What this course **is** about: the **philosophical and technical choices** behind Simplicity's design. Why was this language created this way? Why only nine combinators? Why no recursion? Why does it matter that the type system connects to Gentzen's sequent calculus?
+
+Think of it as understanding **why the engine was built this way** rather than learning to drive the car.
+
+### Who is this for?
+
+This course is ideal for:
+- **Protocol developers** who want to understand Simplicity's foundations before writing code
+- **Bitcoin researchers** interested in the formal verification and type-theoretic approach
+- **Computer scientists** curious about the connection between sequent calculus and blockchain computation
+- **Advanced bitcoiners** who want to go beyond surface-level understanding of Liquid's scripting capabilities
+
+If terms like "sum types", "combinators", or "sequent calculus" are entirely new to you, don't worry, we explain everything from scratch. But be prepared for a dense, mathematical journey.
+
+### From articles to course
+
+The original "Delving Simplicity" series by Dr. O'Connor is structured as five technical articles. This course reorganizes and annotates that material into a progressive learning path with quizzes to test your understanding along the way. The ideas, definitions, and proofs are his, and we've adapted the format for structured education.
+
+# Foundations of Simplicity
+
+a5976618-94ab-4b29-b9aa-040d35c68e5d
+
+## Fundamental Ways of Combining Computations
+
+6d46e77a-7e60-473b-b230-418da5ae44eb
+
+Now that Simplicity has been activated on the Liquid Network, I'd like to do an in-depth dive into the philosophy and design of the Simplicity language.
+
+Bitcoin's transaction validation is a significantly different application from regular programming language design. Block space cost is at a premium so programs need to be compact. The programs in Bitcoin transactions are only ever executed on a single input and everyone executes the program on the same input. Also, the agent authorizing the transaction already knows the outcome of the computation in advance: that the transaction is valid.
+
+Typically the authorizing agent will run much more expensive computations to derive witness data attesting to the transaction's validity, whereas programs run on the blockchain need to check the witness data for validity. Checking validity is often much cheaper than proving validity.
+
+We've designed Simplicity with these sorts of unique language design challenges in mind. For example, Simplicity requires unexecuted branches be pruned so they do not appear on the blockchain. Preprocessing steps are carefully designed to exhibit (quasi-)linear time complexity in the size of the Simplicity program. Static analysis is used instead of "gas", which cannot be computed without executing code in a prescribed manner, so that the details of the execution model do not become consensus critical. No dynamic memory allocation during execution. And so on.
+
+Before delving into the design details of Simplicity, I want to begin this series with some programming philosophy about the general ways of combining basic building blocks to create new functionality.
+
+### Composition
+
+Suppose one is designing a language for programmable transactions for a blockchain like Bitcoin. In particular, programs only have access to the transaction data and the UTXO data of the inputs, and execution only determines transaction validity (which lets the result of execution be cached). Let's say one starts with some set of basic operations that can perform various tasks such as basic computations, reading and/or processing data from the transaction, and signature verification. Each operation consumes some type of input (possibly empty) and returns some type of output. What are the ways we can combine these basic operations into more complex operations?
+
+### Sequential Composition
+
+
+
+The most fundamental composition method is sequential composition. If we have two basic operations, one whose output data type matches the input data type of the other, then we can combine these two operations into a new composite operation. This new operation runs these two basic operations in sequence, taking as input the input of the first operation, passing the output of that first operation into the input of the second operation, and ultimately returning the output of that second operation.
+
+Of course, we don't need to restrict ourselves to just combining basic operations. Now that we have some composite operations, we can combine those using functional composition as well.
+
+In mathematics, this sequential composition is often just called "composition", and one might think that this is the only way of composing things. However, we have other ways of composing operations.
+
+### Parallel Composition
+
+
+
+Suppose that we have two operations, they could be basic or complex operations, and they both take the same type of input. A second fundamental way of composing these two operations is to execute them both on the same input. This is called parallel composition, and the type of output is the "product" of the types of the outputs of the original operations and contains the pair of the two outputs.
+
+While this is called "parallel" composition, and the two operations could in principle be executed in parallel, parallel execution isn't an operational requirement. We can implement parallel composition "sequentially" by executing one operation first and then the second operation. We don't care about the details of how parallel composition is implemented as long as the output is the same.
+
+### Conditional Composition
+
+
+
+Conditional composition is the dual of parallel composition. In this case we have two operations that produce the same output, and we compose them by choosing one of them to execute. The input to this composite operation is the "sum" or "tagged union" of the types of the inputs of the original operation. In this instance the tag, "Left" or "Right", is a single bit in the input's data which determines which type of data is being carried, and hence which of the two operations can be executed.
+
+Conditional composition operates in the same way even when the input is the sum of two identical types. The sum type still contains a tag, and the value of that tag determines which of the two operations is to be executed.
+
+### Composition in Bitcoin Script
+
+There are many ways of realizing these three kinds of composition in various programming languages. In Bitcoin Script, sequential composition is realized (approximately) by the concatenation of two routines (this is why Bitcoin Script is called a concatenative programming language) since the output of one routine is left on the stack to be consumed by the subsequent routine. Parallel composition is achieved by use of duplicate and swap operations to manipulate the stack so that two routines can be run on the same input. Things are not entirely straightforward since what we are calling the "product" of types is typically realized by utilizing multiple stack items. Hopefully you can see the general idea.
+
+Conditional composition is, of course, realized by `OP_IF` which branches based on the value on the stack. In this case the top stack item plays the role of a tag, and usually the next item or items on the stack are of different "types" that depend on the value of the tag. For each case the stack item types may only be suitable for processing by one of the branches in the `OP_IF`. However after we reach `OP_ENDIF` the stack items must be of consistent "type" such that the remaining script is capable of proceeding independent of which branch was previously taken.
+
+### Composition in Simplicity
+
+We designed Simplicity with combinators that directly implement these three forms of composition. Along with a few more combinators to support other basic operations related to the product and sum types, the core Simplicity language ends up consisting of nine combinators that are adequate to express any finite computation. We will discuss this in more detail in the next chapter.
+
+### A Fourth Kind of Composition
+
+Before ending we should mention that there is at least one more kind of composition found in Computer Science, which is "recursive composition". In recursive composition one operation is iterated multiple times.
+
+Note that Bitcoin Script does not support recursive composition, and similarly, we have explicitly excluded unbounded recursion from Simplicity's design. Our thesis is that unbounded iterative computation is better implemented using recursive covenants which compute over multiple transactions. This allows users to avoid block space and standardness constraints and better predict transaction costs.
+
+That being said, there are ways of abusing Simplicity's delegation feature to provide something resembling unbounded recursive composition, which we may discuss later in this series.
+
+### Conclusion
+
+We reviewed the three major forms of composition for transforming basic operations into complex operations:
+
+- sequential composition
+- parallel composition
+- conditional composition
+
+We discussed how these forms of composition are realized in Bitcoin Script, and hinted at how they have influenced the design of the Simplicity language. We noted that the fourth kind of composition, recursive composition, is specifically excluded from both Simplicity and Bitcoin Script.
+
+In the next chapter we will describe the nine combinators that make up the core of the Simplicity language, how they serve to directly realize these three forms of composition, and how this forms a complete language for describing any finite computation.
+
+## Combinator Completeness of Simplicity
+
+2a10a6ba-fada-4556-a673-3ae8c0794bf0
+
+In this chapter we introduce the core Simplicity language and show that the language is complete, meaning that any finite computation can be expressed within it.
+
+### Simplicity Types
+
+Simplicity supports three fundamental type constructors. The product type `A × B` represents parallel composition outputs, while the sum type `A + B` (tagged union) handles conditional composition inputs. The third type is the unit type.
+
+### Unit Type
+
+The unit type, denoted `𝟙` or `ONE`, contains exactly one value: the empty tuple `⟨⟩` or `()`. This zero-bit data type carries no information.
+
+### Sum Type
+
+A sum type `A + B` combines two types with tags indicating "left" or "right." Values are written as `σᴸ(a)` or `inl(a)` for left-tagged values and `σᴿ(b)` or `inr(b)` for right-tagged values. The tags remain distinct even when combining identical types.
+
+#### Boolean Type
+
+The type `𝟙 + 𝟙`, denoted `𝟚` or `TWO`, represents a one-bit type with two values. By convention, `σᴸ⟨⟩` represents false/zero, while `σᴿ⟨⟩` represents true/one.
+
+### Product Type
+
+Product types `A × B` contain value pairs written as `⟨a, b⟩` or `(a, b)`. The type `𝟚 × 𝟚` has four values, distinct from the four values in `𝟚 + 𝟚`.
+
+### Core Simplicity Expressions
+
+Operations are denoted as `f : A ⊢ B`, meaning input type `A` and output type `B`. Simplicity is "first-order" — it lacks function types.
+
+### Two Basic Operations
+
+The core language provides two basic operations:
+
+**Identity (`iden`).** The identity operation passes its input through unchanged:
+
+```
+iden : A ⊢ A
+⟦iden⟧(a) = a
+```
+
+**Unit (`unit`).** The unit operation discards its input and returns the empty tuple:
+
+```
+unit : A ⊢ 𝟙
+⟦unit⟧(a) = ⟨⟩
+```
+
+These form families with one operation per type.
+
+### Three Composition Combinators
+
+Sequential composition uses `comp f g` (written `f ⨾ g` or `f >>> g`):
+
+```
+If f : A ⊢ B and g : B ⊢ C, then
+comp f g : A ⊢ C
+⟦f ⨾ g⟧(a) = ⟦g⟧(⟦f⟧(a))
+```
+
+Parallel composition uses `pair f g` (written `f ▵ g` or `f &&& g`):
+
+```
+If f : A ⊢ B and g : A ⊢ C, then
+pair f g : A ⊢ B × C
+⟦f ▵ g⟧(a) = ⟨⟦f⟧(a), ⟦g⟧(a)⟩
+```
+
+Conditional composition uses `case f g : (A + B) × C ⊢ D`, providing branches access to shared environment `C`:
+
+```
+If f : A × C ⊢ D and g : B × C ⊢ D, then
+case f g : (A + B) × C ⊢ D
+⟦case f g⟧⟨σᴸ(a), c⟩ = ⟦f⟧⟨a, c⟩
+⟦case f g⟧⟨σᴿ(b), c⟩ = ⟦g⟧⟨b, c⟩
+```
+
+Why does conditional composition take this shape — a sum paired with a shared environment `C` — rather than a simpler `copair f g : A + B ⊢ C` that merely picks a branch? Because a bare `copair` cannot express **distribution**: the function `dist : (A + B) × C ⊢ A × C + B × C` that pushes a shared input into whichever branch is taken. By building the environment `C` directly into `case`, Simplicity obtains conditional composition *and* distribution from a single combinator — one of the key design decisions that keeps the core language down to nine combinators.
+
+### Four More Combinators
+
+Product consumption uses `take` and `drop`:
+
+**take** extracts the left element:
+
+```
+If f : A ⊢ C, then
+take f : A × B ⊢ C
+⟦take f⟧⟨a, b⟩ = ⟦f⟧(a)
+```
+
+**drop** extracts the right element:
+
+```
+If f : B ⊢ C, then
+drop f : A × B ⊢ C
+⟦drop f⟧⟨a, b⟩ = ⟦f⟧(b)
+```
+
+Sum production uses `injl` and `injr`:
+
+**injl** wraps with a left tag:
+
+```
+If f : A ⊢ B, then
+injl f : A ⊢ B + C
+⟦injl f⟧(a) = σᴸ(⟦f⟧(a))
+```
+
+**injr** wraps with a right tag:
+
+```
+If f : A ⊢ C, then
+injr f : A ⊢ B + C
+⟦injr f⟧(a) = σᴿ(⟦f⟧(a))
+```
+
+### The Nine Core Combinators
+
+In total, Simplicity has exactly nine core combinators:
+
+| Combinator | Purpose |
+|---|---|
+| `iden` | Pass input through |
+| `unit` | Discard input |
+| `comp` | Sequential composition |
+| `pair` | Parallel composition |
+| `case` | Conditional composition |
+| `take` | Extract left from product |
+| `drop` | Extract right from product |
+| `injl` | Inject into left of sum |
+| `injr` | Inject into right of sum |
+
+### Simplicity and the Sequent Calculus
+
+Simplicity's design derives from the conjunctive-disjunctive fragment of Gentzen's sequent calculus. More precisely, it is a variant of the *functional interpretation* of the sequent calculus, which is itself analogous to the Curry-Howard correspondence between natural deduction and the lambda calculus. The combinator rules exhibit "smaller types in premises than conclusions," enabling the Bit Machine — Simplicity's abstract stack machine interpreter — to minimize data copying during execution.
+
+### Values are not Expressions
+
+Simplicity expressions denote operations, not values. The notation `scribe b : A ⊢ B` represents a unique expression always returning value `b`, serving as notational convenience rather than a combinator. This mirrors Bitcoin Script, where operations like `OP_1` push values rather than express them directly.
+
+### Simplicity's Completeness Theorem
+
+With all nine combinators in hand, how do we know we aren't missing something — that these nine really are enough? The Simplicity Completeness theorem answers this: for any function between (finite) Simplicity types, some Simplicity expression denotes it. The proof is constructive — it shows how to build the expression:
+
+1. **Decompose the input**: Using nested `case` expressions, fully decompose any input of any type into its constituent bits
+2. **Build a lookup table**: For each possible input, use `scribe` to produce the corresponding output
+3. **Assemble**: The nested cases and scribes together form a giant lookup table that implements the function
+
+This theorem is formally verified in the Rocq proof assistant (formerly Coq). The proof is part of the official Simplicity repository and has been machine-checked for correctness.
+
+While the completeness theorem guarantees that Simplicity's nine combinators can express any function between (finite) Simplicity types, resulting expressions from the lookup-table construction are impractically large. A function on 256-bit inputs would require a lookup table with 2²⁵⁶ entries. This is why the next chapters focus on building efficient expressions that exploit the structure of computations, rather than brute-forcing everything through lookup tables.
+
+### Conclusion
+
+Simplicity's core language includes a type system and combinators enabling any finite computation. While the Completeness theorem guarantees expressiveness, resulting expressions from the generic construction are impractically large. Practical Simplicity development involves exploiting computational structure for succinct expressions. The next chapters explore data structures, transaction interactions, and additional combinators.
+
+# From Data Types to Programs
+
+08528a6f-d310-4675-b8cd-4e9b93b3c009
+
+## Building Data Types
+
+9981ae62-ae50-4770-adf2-b253d1e08de3
+
+In the previous chapters, we showed how Simplicity's core set of combinators are enough to implement any finite pure computation. This chapter shows how to build practical data structures and computations from these primitives — the same way computers are built from logic gates.
+
+### Boolean Logic
+
+The Boolean type, denoted `𝟚`, equals `𝟙 + 𝟙` and has two values: `σᴸ⟨⟩` (false) and `σᴿ⟨⟩` (true). Using the core combinators, Boolean logic operators can be constructed.
+
+#### And Operation
+
+The logical `and : 𝟚 × 𝟚 ⊢ 𝟚` operation takes two bits and returns one bit. The implementation branches on the first bit: if false, return false; otherwise, return the second bit.
+
+```
+and ≔ case (injl unit) (drop iden) : 𝟚 × 𝟚 ⊢ 𝟚
+```
+
+Testing with `⟨false, false⟩`:
+
+```
+⟦and⟧⟨false, false⟩
+ = {expand the notation for false}
+⟦and⟧⟨σᴸ⟨⟩, σᴸ⟨⟩⟩
+ = {expand the definition of and}
+⟦case (injl unit) (drop iden)⟧⟨σᴸ⟨⟩, σᴸ⟨⟩⟩
+ = {evaluate case for σᴸ}
+⟦injl unit⟧⟨⟨⟩, σᴸ⟨⟩⟩
+ = {evaluate injl}
+σᴸ(⟦unit⟧⟨⟨⟩, σᴸ⟨⟩⟩)
+ = {evaluate unit}
+σᴸ⟨⟩
+ = {by the notation for false}
+false
+```
+
+Testing with `⟨true, true⟩`:
+
+```
+⟦and⟧⟨true, true⟩
+ = {expand the notation for true and the definition of and}
+⟦case (injl unit) (drop iden)⟧⟨σᴿ⟨⟩, σᴿ⟨⟩⟩
+ = {evaluate case for σᴿ}
+⟦drop iden⟧⟨⟨⟩, σᴿ⟨⟩⟩
+ = {evaluate drop}
+⟦iden⟧(σᴿ⟨⟩)
+ = {evaluate iden}
+σᴿ⟨⟩
+ = {by the notation for true}
+true
+```
+
+#### Other Logic Operations
+
+The `not` operation requires a helper combinator:
+
+```
+ f : A ⊢ C g : B ⊢ C
+--------------------------------------------------------------
+copair f g ≔ iden ▵ unit ⨾ case (take f) (take g) : A + B ⊢ C
+```
+
+The initial `iden ▵ unit : A ⊢ A × 𝟙` adds an empty "environment" to the input, enabling the `case` combinator to apply. The use of `take` in the two branches drops this empty environment to execute `f` or `g`.
+
+Other Boolean logical operations:
+
+- `or ≔ case (drop iden) (injr unit) : 𝟚 × 𝟚 ⊢ 𝟚`
+- `not ≔ copair (injr unit) (injl unit) : 𝟚 ⊢ 𝟚`
+- `xor ≔ case (drop iden) (drop not) : 𝟚 × 𝟚 ⊢ 𝟚`
+
+### Bit Adders
+
+A "half-adder" takes two bits and adds them, producing a two-bit output: a carry bit and sum bit.
+
+```
+half-adder ≔ and ▵ xor : 𝟚 × 𝟚 ⊢ 𝟚 × 𝟚
+```
+
+A "full-adder" adds three bits, producing two-bit output. The input uses nested tuple `(𝟚 × 𝟚) × 𝟚`.
+
+For nested tuples, compact notation is used:
+
+- `O f` denotes `take f`
+- `I f` denotes `drop f`
+- `H` denotes `iden`
+
+For example, `I O H` means `drop (take iden) : A × (B × C) ⊢ B`, extracting the middle value. The notation evokes binary digits: when thinking of nested tuples as binary trees, the notation represents reversed binary digits of tree positions. These expressions form De Bruijn indices for Simplicity.
+
+**Note:** The `I`, `O`, and `H` notation only applies to subexpressions consisting solely of `take`, `drop`, and `iden`.
+
+The full-adder composes two half-adders, taking logical `or` of the carry bits:
+
+```
+full-adder ≔ take half-adder ▵ I H
+ ⨾ O O H ▵ (O I H ▵ I H ⨾ half-adder)
+ ⨾ (O H ▵ I O H ⨾ or) ▵ I I H
+ : (𝟚 × 𝟚) × 𝟚 ⊢ 𝟚 × 𝟚
+```
+
+In the first line, `take half-adder ▵ I H : (𝟚 × 𝟚) × 𝟚 ⊢ (𝟚 × 𝟚) × 𝟚` runs the half-adder on the first two bits, saving the last bit.
+
+In the second line, `O O H ▵ (O I H ▵ I H ⨾ half-adder) : (𝟚 × 𝟚) × 𝟚 ⊢ 𝟚 × (𝟚 × 𝟚)` saves the first bit (the carry-out of the first half-adder) and runs the half-adder on the last two bits.
+
+In the last line, `(O H ▵ I O H ⨾ or) ▵ I I H: 𝟚 × (𝟚 × 𝟚) ⊢ 𝟚 × 𝟚` takes the logical OR of the first two bits (carry-outs of both half-adders) and returns the sum-out bit of the second half-adder.
+
+This demonstrates Simplicity programming: using `I`, `O`, and `H` notation to reference data bits, forming suitable "environments" for calling other functions via sequential composition.
+
+Users don't define low-level operations directly. Later this series discusses standard library jets implementing common functions. End users aren't expected to program directly in Simplicity, similar to Bitcoin Script. Instead, higher-level languages like SimplicityHL generate Simplicity code, managing subexpression "environments" and translating named variables into appropriate `take` and `drop` sequences.
+
+### Vectors
+
+Fixed-length vectors are defined by forming iterated products of type `A`:
+
+- `A² ≔ A × A`
+- `A⁴ ≔ A² × A²`
+- `A⁸ ≔ A⁴ × A⁴`
+- `…`
+
+These may be written as `A^2`, `A^4`, `A^8`, etc.
+
+Vectors are defined only for lengths that are powers of two. Other powers require choosing bracketing conventions.
+
+Given expression `f : A ⊢ B`, repeated pairing "maps" it over fixed-length vectors:
+
+- `f² ≔ f ▵ f : A² ⊢ B²`
+- `f⁴ ≔ f² ▵ f² : A⁴ ⊢ B⁴`
+- `f⁸ ≔ f⁴ ▵ f⁴ : A⁸ ⊢ B⁸`
+
+Given function `f : A × B ⊢ B`, iteration or "folding" over fixed-length vectors:
+
+- `fold-right-2 f ≔ O O H ▵ (O I H ▵ I H ⨾ f) ⨾ f : A² × B ⊢ B`
+- `fold-right-4 f ≔ fold-right-2 (fold-right-2 f) : A⁴ × B ⊢ B`
+- `fold-right-8 f ≔ fold-right-2 (fold-right-4 f) : A⁸ × B ⊢ B`
+
+Many variations exist. Given `f : A × B ⊢ C`, "zip" over paired vectors with `zip-n f : (Aⁿ × Bⁿ) ⊢ Cⁿ`. Given `f : (A × B) × C ⊢ C`, fold over paired vectors with `bifold-right-n f : (Aⁿ × Bⁿ) ⊢ C`. Combining `map` and `fold-right` creates accumulating combinators: `f : A × C ⊢ C × B` yields `map-accum-right-n f : Aⁿ × C ⊢ C × Bⁿ`. Many more variants are possible.
+
+#### Multi-bit Words
+
+A bit vector yields multi-bit integers. For example, `𝟚³²` is a 32-bit word type. `𝟚²⁵⁶` is a 256-bit word type, suitable for hashes and cryptographic operations.
+
+Using the full-adder, a variant of vector operations defines a "ripple carry adder" over multi-bit words:
+
+```
+full-adder-n ≔ zip-accum-right-n full-adder : (𝟚ⁿ × 𝟚ⁿ) × 𝟚 ⊢ 𝟚 × 𝟚ⁿ
+```
+
+`full-adder-n` takes two n-bit binary numbers and a one-bit carry-input, returning a one-bit carry-out flag and an n-bit sum.
+
+#### SHA-256
+
+By recursively defining arithmetic operations on multi-bit words — subtraction, multiplication, division — and bit-wise logical operations such as logical AND, OR, XOR, and repeatedly combining these, even SHA-256's block compression function can be built:
+
+```
+sha256-hash-block ≔ … : 𝟚²⁵⁶ × 𝟚⁵¹² ⊢ 𝟚²⁵⁶
+```
+
+The SHA-256 compression is formally defined using Simplicity within the Rocq proof assistant (formerly Coq), with a formal proof that the `sha256-hash-block` implementation is correct.
+
+The compression runs too slowly as raw Simplicity. Jets execute common functions like SHA-256 compression natively. Pure Simplicity implementations serve as formal specifications for jets.
+
+### Option Types
+
+Option types result from taking a sum with the unit type:
+
+```
+Option A ≔ 𝟙 + A
+```
+
+The type `Option A` may be written as `A?` or `𝕊 A` (where `𝕊` means "successor"). Functions map over option types:
+
+```
+ f : A ⊢ B
+------------------------------------------
+f? ≔ copair (injl unit) (injr f) : A? ⊢ B?
+```
+
+Monadic combinators such as bind can be defined:
+
+```
+ f : A ⊢ B?
+---------------------------------------
+bind f ≔ copair (injl unit) f : A? ⊢ B?
+```
+
+### Variable Length Buffers
+
+"Buffers" are types for partially filled vectors:
+
+- `Aᑉ² ≔ A?`
+- `Aᑉ⁴ ≔ A²? × Aᑉ²`
+- `Aᑉ⁸ ≔ A⁴? × Aᑉ⁴`
+- `…`
+
+The type `Xᑉ⁸` expands to `(1 + X⁴) × ((1 + X²) × (1 + X))`. Treating this as a polynomial and expanding yields `1 + X + X² + X³ + X⁴ + X⁵ + X⁶ + X⁷`. Interpreting as a type, it represents the sum of all possible tuples of X up to 7, including the empty tuple. This is exactly the type of lists with length strictly less than 8.
+
+Like vectors, mapping and folding operations can be defined over buffers. Stack operations include `push-9eafe498-0765-419a-a69d-a74a9cdf3713
+
+In the previous chapters, we showed how to build some data structures and computations using Simplicity's core set of combinators. As we noted, the core combinators are enough to implement any finite pure computation. This raises the question: what more can be achieved? We can add additional side effects to our expressions.
+
+There are various kinds of possible side effects for expressions: state update, writing to a log, throwing an exception, reading from an environment, calling a continuation, etc. The side effects available in Simplicity will depend on the application.
+
+For Bitcoin and Liquid applications, we currently have two side effects: the Failure effect, which is an exception effect where the exception has type `𝟙`, and the Reader effect which allows data from the transaction environment to be accessed. Our core combinators are "pure"; they have no side effects. However, jets can introduce new primitives that do have side effects.
+
+### Jets with Effects
+
+We will talk more about jets later in this course, but here we introduce a few example jets to illustrate their side effects.
+
+#### Bip0340-verify
+
+`bip0340-verify : (𝟚²⁵⁶ × 𝟚²⁵⁶) × 𝟚⁵¹² ⊢ 𝟙` is a jet for an expression that takes an x-only pubkey, a 256-bit message, and a Schnorr signature, and returns nothing! According to its type, it ought to behave the same as a `unit`. The difference lies in the jet's side effect: if the signature validation fails, then the entire computation is aborted by throwing an exception (of unit type). This is the Failure effect.
+
+#### Verify
+
+`verify : 𝟚 ⊢ 𝟙` is a barebones jet for expressing the Failure effect. If `verify`'s input is `false`, the entire computation is aborted, by throwing an exception. If the input is `true`, nothing is returned, but the computation can continue.
+
+#### Transaction Hashes
+
+`sig-all-hash : 𝟙 ⊢ 𝟚²⁵⁶` appears to be a constant function, since there is only one possible input value: the empty tuple. However, this jet reads from the transaction environment and produces a hash of transaction data that is analogous to the `SIGHASH_ALL` message digest used in Bitcoin Script's signature verification. This is an example of the Reader effect: the value returned depends on the transaction environment that the jet is executed within. There are several other hashing jets that hash various subsets of the transaction environment data to help build custom message digests for signatures.
+
+#### Introspection Jets
+
+`input-sequence : 𝟚³² ⊢ 𝟚³²?` is a function that takes an input index and returns the transaction's sequence number for that input, optionally returning nothing if the index is out of bounds. Again, the output value is not a pure function of the input index, but rather, the operation uses the Reader effect to access the transaction environment in order to determine the output value. There are several other introspection jets that return various fragments of the transaction environment data.
+
+### Classifying Effects
+
+Not all side effects are created equal. Some side effects behave nicer than others. We can classify effects by how amenable they are to program transformations.
+
+#### Commutative Effects
+
+A commutative effect is one where, if you swap the outputs of two expressions, you can safely swap the expressions themselves without changing the expression's effect. Consider `swap = I H ▵ O H : A × B ⊢ B × A`. If `f ▵ g ⨾ swap = g ▵ f` for every expression `f` and `g` with side effects, then the effects are commutative.
+
+Reading transaction data from the environment is a commutative effect because the result of reading from the environment is the same, no matter what order we execute the reading in.
+
+In general, throwing an exception is not a commutative effect. If `f` throws some exception `e₁` and `g` throws some other exception `e₂`, then which exception is thrown from the pair of `f` and `g` depends on the order they are executed in.
+
+However, in the special case of the Failure effect, in which only a unit typed exception can be thrown, the effect is commutative. No matter which of `f` or `g` throws an exception, the resulting exception will be the same, because there is only one possible exception value.
+
+#### Idempotent Effects
+
+An idempotent effect is one where, if you duplicate the output of an expression, you can safely duplicate the expression itself without changing the expression's effect. Consider `dup = iden ▵ iden : A ⊢ A × A`. If `f ⨾ dup = dup ⨾ f ▵ f` for every `f` with side effects, then the effects are idempotent.
+
+Reading transaction data from the environment is an idempotent effect. Throwing an exception is also an idempotent effect. Even though only one of the two duplicated expressions will be executed, any exception thrown by `dup ⨾ f ▵ f` will be the same as the exception thrown by `f ⨾ dup`.
+
+However, writing to a log may not be idempotent, as duplicating the effect would cause the log message to appear twice. However, if the log consists of a _set_ of messages instead of a _list_ of messages, then the effect would be idempotent (and commutative) because set insertion is itself an idempotent operation.
+
+#### Unitary Effects
+
+A unitary effect is one where, if you discard the output of an expression, you can safely discard the expression itself without changing the expression's effects. If it is always the case that `f ⨾ unit = unit` for every `f` with side effects, then your effects are unitary.
+
+Reading data from the environment is one of the few types of unitary effects. If the result of reading transaction data from the environment is discarded, the whole expression performing the read may be discarded.
+
+The failure effect isn't unitary. If `f` throws an exception then so will `f ⨾ unit`; execution will not even make it to the `unit` combinator before the computation is aborted. On the other hand, `unit` obviously would not throw any exception, so the effects of `f ⨾ unit` and `unit` would be different.
+
+To summarize, here is how the effects discussed above fare against these three properties:
+
+| Effect | Commutative | Idempotent | Unitary |
+| --- | :---: | :---: | :---: |
+| Reader (transaction environment) | ✓ | ✓ | ✓ |
+| Failure (unit-typed exception) | ✓ | ✓ | ✗ |
+| Writer (log as a set) | ✓ | ✓ | ✗ |
+| General exceptions (arbitrary type) | ✗ | ✓ | ✗ |
+
+### Effects Allowed in Simplicity
+
+The more well-behaved properties that a type of effect has, the more room a Simplicity optimizer has for transforming programs that use those effects. Ideally we would only allow effects that have all three properties: commutative, idempotent, and unitary. This would allow an optimizer to perform any sort of program transformation it would like. However, reading from an environment is the only effect that satisfies all three properties.
+
+Instead we demand that Simplicity effects are commutative and idempotent. Both the effects we use in Simplicity, the Failure effect and the Reader effect, are commutative and idempotent. This allows a large class of optimizations to be performed on Simplicity code.
+
+However, the "discard" transformation described above, attempting to replace `f ⨾ unit` with `unit`, or any similar transformation is not allowed if `f` may produce a Failure effect. Indeed, imagine if `f` contained a `bip0340-verify` assertion. It would be disastrous to attempt to optimize that check away.
+
+### Why Allow Side Effects At All?
+
+Why does Simplicity even allow side effects at all? Wouldn't it be better if every program took the entire transaction as input and returned a Boolean output that decides if a transaction is valid or not?
+
+#### Batch Verification
+
+One reason we have the Failure effect is to support [batch verification](https://github.com/bitcoin/bips/blob/c9a6ca6297eb8de850f6b64dafb8e60ee9b64d66/bip-0340.mediawiki#batch-verification) of Schnorr signatures. In batch verification, many individual Schnorr signature checks are pooled together in such a way that if any single signature check fails, then the entire batch fails.
+
+This batching procedure improves efficiency over individually verifying each signature. The downside is that if the batch verification fails, then we do not learn which specific signature check or checks failed.
+
+By using the failure side effect, `bip0340-verify` ensures that if a signature check fails, the whole transaction fails. If `bip0340-verify` were instead to return `𝟚`, a Boolean type, for success or failure, then a failing signature check could still lead to a branch where the script succeeds. In such a case we would need to know if the particular signature is valid or not, and thus we wouldn't be able to take advantage of batch verification.
+
+#### Precomputed Transaction Data
+
+A problem in early Bitcoin Script was that the hashing function used to create message digests for signatures was linear in the size of the transaction. Typically every input creates at least one message digest for signature verification, so overall the amount of hashing was quadratic in the transaction size.
+
+This problem was fixed in Segwit and later iterations of Bitcoin Script by redefining the message digests so that they could be computed in constant time per signature check. This relies on having `PrecomputedTransactionData`, which precomputes hashes of transaction data once and is then shared by each input's sighash computations. Simplicity's transaction hashing jets rely on the same kind of precomputed transaction data in order to ensure the jets run in constant time.
+
+Suppose `sig-all-hash` didn't use the Reader effect. Suppose we somehow managed to build a Simplicity type for the transaction environment. Let's call it `TxEnv`, so that `sig-all-hash : TxEnv ⊢ 𝟚²⁵⁶` was the jet's type. Such a definition would require the `sig-all-hash` jet to be able to compute the hash of any transaction, not just the transaction it is involved with. Simplicity programs could copy the given `TxEnv` and pass a modified copy of it to `sig-all-hash`. In such a case `sig-all-hash` couldn't rely on `PrecomputedTransactionData`, and we would be back to requiring linear time in whatever transaction data was passed into this version of `sig-all-hash`.
+
+Because `sig-all-hash : 𝟙 ⊢ 𝟚²⁵⁶` uses the Reader effect to access the transaction data, it _only_ gets access to a fixed transaction environment. For that reason, the jet's implementation can safely use `PrecomputedTransactionData` and operate in constant time.
+
+### Cross-Input Signature Aggregation
+
+While neither Liquid nor Bitcoin support [cross-input signature aggregation](https://hrf.org/latest/cisa-research-paper/) at this point in time, we would like to check that Simplicity can be compatible with it when the time comes.
+
+While details haven't been worked out, we imagine half-aggregation being implemented using a Writer effect. That is, a new jet with a type such as `half-agg-verify : (𝟚²⁵⁶ × 𝟚²⁵⁶) × 𝟚²⁵⁶ ⊢ 𝟙` would take a public key, message digest, and the `r`-component of a Schnorr signature (a Schnorr signature consists of an `r`-component and an `s`-component) and write it to a transaction log before continuing on with execution. Then, elsewhere in the transaction or with the transaction, an aggregate `s`-component for all half-aggregated Schnorr signatures would be provided. The transaction would only be valid when such an aggregate `s`-component is provided for all the logged keys, messages, and `r`-components.
+
+To meet Simplicity's requirements, this Writer effect needs to be idempotent and commutative. This can be ensured by treating the writer log as a set of key, message, `r`-component tuples. This works because set operations are idempotent and commutative. Treating the log as a set of values would be compatible with the half-aggregation verification algorithm.
+
+### Conclusion
+
+In this chapter we looked at adding side effects to the computations that Simplicity can do. We classified various kinds of effects according to how well-behaved they are with respect to various kinds of program transformation. We decided to restrict Simplicity's effects to those that are commutative and idempotent.
+
+The two effects we use for Bitcoin and Liquid applications are the Reader effect, for accessing the transaction environment, and the Failure effect, for aborting and failing the program. Some jets make use of primitive operations where these sorts of side effects can occur.
+
+The Failure effect determines the output of a Simplicity program: the program either fails, making the transaction invalid, or the program succeeds. The Reader effect provides one sort of input to a Simplicity program: the environment containing transaction data. But we also need to provide other inputs, such as digital signatures, to Simplicity programs.
+
+In the next chapter we will look at what Simplicity programs are, how they are turned into addresses, and how we add other inputs, such as signatures, to Simplicity programs.
+
+## Programs and Addresses
+
+961652e3-8f7d-4c2a-8b55-9a990b91a0dd
+
+In the previous chapter we described two side effects used in Simplicity: the Failure effect, which determines a program's success or failure, and the Reader effect, which provides access to the transaction environment. Now we turn to the practical question: what exactly is a Simplicity program, and how does it become an address on the blockchain?
+
+### Simplicity Programs
+
+A Simplicity program is defined as a Simplicity expression of type `𝟙 ⊢ 𝟙`. This type signature means the program takes no meaningful input (just the unit value) and produces no meaningful output (just the unit value). The Reader effect captures the transaction environment input, while the Failure effect indicates success or failure. These effects handle I/O rather than Simplicity types themselves.
+
+### Commitment Merkle Root
+
+Rather than storing complete programs on-chain, Bitcoin employs commitments — a practice extending from Pay-to-Script-Hash (P2SH). Simplicity uses a Commitment Merkle Root (CMR).
+
+Each combinator receives a SHA-256 tag derived from the pattern: `Simplicity␟Commitment␟[identifier]`, where `␟` represents ASCII code 31 (the unit separator).
+
+Each tag is the SHA-256 hash of the corresponding pre-image string listed below:
+
+| Combinator | Tag pre-image (ASCII string) |
+|---|---|
+| `iden` | `Simplicity␟Commitment␟iden` |
+| `unit` | `Simplicity␟Commitment␟unit` |
+| `comp` | `Simplicity␟Commitment␟comp` |
+| `pair` | `Simplicity␟Commitment␟pair` |
+| `case` | `Simplicity␟Commitment␟case` |
+| `take` | `Simplicity␟Commitment␟take` |
+| `drop` | `Simplicity␟Commitment␟drop` |
+| `injl` | `Simplicity␟Commitment␟injl` |
+| `injr` | `Simplicity␟Commitment␟injr` |
+
+A Simplicity expression is then recursively hashed into a 256-bit CMR by computing a tagged SHA-256 midstate for each combinator together with the CMRs of its arguments (write `#ᶜ(e)` for the CMR of expression `e`, and `∥` for byte concatenation):
+
+| Combinator | CMR rule |
+|---|---|
+| `iden` | `#ᶜ(iden) = SHA-256-midstate(tag_iden ∥ tag_iden)` |
+| `unit` | `#ᶜ(unit) = SHA-256-midstate(tag_unit ∥ tag_unit)` |
+| `comp f g` | `#ᶜ(comp f g) = SHA-256-midstate(tag_comp ∥ tag_comp ∥ #ᶜ(f) ∥ #ᶜ(g))` |
+| `pair f g` | `#ᶜ(pair f g) = SHA-256-midstate(tag_pair ∥ tag_pair ∥ #ᶜ(f) ∥ #ᶜ(g))` |
+| `case f g` | `#ᶜ(case f g) = SHA-256-midstate(tag_case ∥ tag_case ∥ #ᶜ(f) ∥ #ᶜ(g))` |
+| `take f` | `#ᶜ(take f) = SHA-256-midstate(tag_take ∥ tag_take ∥ 32·0x00 ∥ #ᶜ(f))` |
+| `drop f` | `#ᶜ(drop f) = SHA-256-midstate(tag_drop ∥ tag_drop ∥ 32·0x00 ∥ #ᶜ(f))` |
+| `injl f` | `#ᶜ(injl f) = SHA-256-midstate(tag_injl ∥ tag_injl ∥ 32·0x00 ∥ #ᶜ(f))` |
+| `injr f` | `#ᶜ(injr f) = SHA-256-midstate(tag_injr ∥ tag_injr ∥ 32·0x00 ∥ #ᶜ(f))` |
+
+Binary combinators (`comp`, `pair`, `case`) concatenate the CMRs of both children; unary combinators (`take`, `drop`, `injl`, `injr`) concatenate their single child's CMR after 32 bytes of `0x00` padding; and the nullary leaves (`iden`, `unit`) hash their tag alone. Two conventions keep this cheap to compute: SHA-256 midstates are used so that **each expression requires at most one call to the SHA-256 compression function** (assuming the midstate up to the constant tags is precomputed), and the one-argument constructors prefix their argument with 32 bytes of `0x00` padding, which allows for a little extra precomputation for implementations that want it.
+
+For the `unit` combinator — a nullary constructor with no argument sub-expressions — this rule specialises to `#ᶜ(unit) = SHA-256-midstate(tag_unit ∥ tag_unit)`, where `tag_unit = SHA-256(Simplicity␟Commitment␟unit)` (the tag is fed in twice). The resulting CMR for the trivial `unit` program is:
+
+```
+0xc40a10263f7436b4160acbef1c36fba4be4d95df181a968afeab5eac247adff7
+```
+
+Critically, the CMR does not commit to the types of Simplicity expressions, relying instead on type inference during redemption.
+
+### Addresses
+
+Addresses employ BIP-0341's Taproot mechanism with CMRs committed under TapLeaf version `0xbe`. The process involves:
+
+1. Computing a TapLeaf tagged hash combining the version byte, CMR length, and CMR itself
+2. Tweaking an internal public key (using a NUMS point when no key-spend path is desired)
+3. Converting to bech32m format
+4. Adding appropriate checksums
+
+When no key-spend path is desired, the internal public key is set to a **NUMS** ("Nothing-Up-My-Sleeve") point: a curve point deliberately chosen so that nobody knows its discrete logarithm — in other words, a point with no corresponding private key. Because no one can ever produce a signature for it, the key-spend path is provably unusable, and the output can be spent *only* through the committed Simplicity script path. In a real application, this NUMS point should be randomized as recommended by BIP-0341, so that outputs with no key-spend path are indistinguishable from ordinary Taproot outputs (a privacy benefit).
+
+#### From Simplicity to Address
+
+Let's walk through the whole derivation for the simplest program possible: `unit : 𝟙 ⊢ 𝟙`, a no-op that always succeeds.
+
+**1. Combinator tag.** First compute the `unit` tag:
+
+```
+tag_unit = SHA-256(Simplicity␟Commitment␟unit)
+ = 0xd723083cff3c75e29f296707ecf2750338f100591c86e0c71717f807ff3cf69d
+```
+
+**2. CMR.** Feed the tag in twice to obtain the program's CMR:
+
+```
+CMR = #ᶜ(unit) = SHA-256-midstate(tag_unit ∥ tag_unit)
+ = 0xc40a10263f7436b4160acbef1c36fba4be4d95df181a968afeab5eac247adff7
+```
+
+**3. TapLeaf hash.** Prefix the CMR with Simplicity's TapLeaf version `0xbe` and the CMR length `0x20` (32 bytes), then take the Elements TapLeaf tagged hash (a tagged hash is `hash_str(x) = SHA-256(SHA-256(str) ∥ SHA-256(str) ∥ x)`):
+
+```
+hash_TapLeaf/elements(0xbe ∥ 0x20 ∥ CMR)
+ = 0x44cc38311ec7e5dfb7b573baf38449496ecd334eb5509cfed1b4fd30da8dd41c
+```
+
+With only this one leaf there are no TapBranches, so this hash is already the TapTree root.
+
+**4. TapTweak.** Since we want no key-spend path, we use the BIP-0341 NUMS point as the internal key and tweak it with the TapTree root:
+
+```
+internal_pk = 0x50929b74c1a04954b78b4b6035e97a5e078a5a0f28ec96d547bfee9ace803ac0
+t = hash_TapTweak/elements(internal_pk ∥ 0x44cc38311ec7e5dfb7b573baf38449496ecd334eb5509cfed1b4fd30da8dd41c)
+ = 0xb3bef172389b0937d7e5a8b15cfa41e776777f13f2f659cb06220a6ff0658285
+```
+
+**5. Output key.** Tweak the internal key on the curve, `output_pk = lift_x(internal_pk) ⊕ t·G` (the elliptic-curve arithmetic is summarized here), giving the x-only output key `0x2cb0c20acd7340b4d4b65f6a60e2888d0d64e3267261f3b3cf7290e5af3f9e09`.
+
+**6. Bech32m address.** Encode the x-only output key, prefix a `p` (the SegWit v1 witness-version character), add the Liquid-testnet human-readable prefix `tex1`, and append the Bech32m checksum. The final address is:
+
+```
+tex1p9jcvyzkdwdqtf49kta4xpc5g35xkfcexwfsl8v70w2gwttelncyshxjk56
+```
+
+That was a lot of work — but much of it is mandated by Taproot itself, not by Simplicity.
+
+### Witness Expressions
+
+A new combinator type addresses the absence of input to Simplicity programs: the witness expression. The `witness` combinator permits signature data and other witness material to be integrated into programs.
+
+```
+ w : B
+-----------------
+witness w : A ⊢ B
+```
+
+The witness expression's semantics is straightforward: it ignores its input and simply returns the value `w` (which may be of any Simplicity type), i.e. `⟦witness w⟧(a) = w`. This adds **no new expressiveness** — by the completeness theorem, Simplicity can already build any such constant function (recall the `scribe` macro from the previous chapters). The point of the `witness` combinator lies entirely in its **CMR**: the value `w` is **excluded** from the expression's CMR, so the address can be computed before `w` is known, and `w` is supplied at redemption time.
+
+This design choice supports pruning — unexecuted conditional branches needn't be revealed on-chain, including their associated witness expressions. When a branch is pruned, the verifier only needs the CMR of the pruned subtree, not its actual content.
+
+### Witness Values
+
+It may seem like a limitation that a witness expression can hold only a *value*, and not a more general Simplicity expression. But programs for UTXO-based blockchains are executed only once. There is no need to pass a whole sub-expression into a witness node: the user can simply run that sub-expression themselves, off-chain, and transcribe its output into the witness value to obtain the very same result.
+
+(Later in this course we will meet the `disconnect` combinator, which behaves much like a witness expression that *does* take an entire Simplicity expression as its argument.)
+
+An alternative design would feed all witness data in as an argument to the top-level Simplicity program. Witness expressions are preferred for two reasons. First, **pruning**: unexecuted branches of `case` expressions are never revealed on-chain, and any witness expressions inside those branches are pruned away along with them. Second, **locality**: witness expressions let us place each witness value exactly where it is used, instead of threading it down from the program's top-level input.
+
+### Type Inference
+
+Since CMRs don't commit to types, the type system is reconstructed during redemption. Simplicity's type inference algorithm determines the minimal types for each subexpression based on the combinator structure. More precisely, inference computes the *principal* (most general) type of every subexpression; any type variables that remain free are then instantiated to the unit type `𝟙`, which yields a unique, minimal type for the program.
+
+### Conclusion
+
+In this chapter we established that Simplicity programs are expressions of type `𝟙 ⊢ 𝟙`, explained how Commitment Merkle Roots are constructed from tagged SHA-256 hashes of each combinator, and showed how CMRs are turned into on-chain addresses via BIP-0341 Taproot. We introduced witness expressions as the mechanism for providing signature data and other inputs at spending time without committing to their values at address creation time.
+
+# Final Section
+
+96952535-4aa6-4e78-91e2-d12e9df895d4
+
+## Reviews & Ratings
+
+fb0b0133-39ea-497b-bd36-198be42c4fab
+true
+
+## Final Exam
+
+2cc5e818-abcb-4a0a-9991-7a492c572e2d
+true
+
+## Conclusion
+
+8ade24bd-a84f-4d25-8f64-bdfa8b58926c
+true
diff --git a/courses/scr403/quizz/000/en.yml b/courses/scr403/quizz/000/en.yml
new file mode 100644
index 00000000000..0a9a0e0ac48
--- /dev/null
+++ b/courses/scr403/quizz/000/en.yml
@@ -0,0 +1,12 @@
+question: Why does Simplicity exclude dynamic memory allocation during execution?
+answer: To enable static analysis and rule out entire classes of bugs and attacks.
+wrong_answers:
+ - Because the Liquid Network does not support low-level memory operations.
+ - To reduce the programming learning curve for new smart-contract developers.
+ - Because Bitcoin Script itself also lacks any dynamic memory allocation.
+explanation: >-
+ Simplicity avoids dynamic memory allocation so that all resource usage
+ can be determined statically before execution. This enables predictable
+ resource bounds and eliminates vulnerabilities related to memory management,
+ which is critical in a blockchain validation context.
+reviewed: false
diff --git a/courses/scr403/quizz/000/question.yml b/courses/scr403/quizz/000/question.yml
new file mode 100644
index 00000000000..a1c8e05da4d
--- /dev/null
+++ b/courses/scr403/quizz/000/question.yml
@@ -0,0 +1,14 @@
+id: 35ccd3ce-33df-4542-91d9-a558d92548df
+chapterId: 6d46e77a-7e60-473b-b230-418da5ae44eb
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/001/en.yml b/courses/scr403/quizz/001/en.yml
new file mode 100644
index 00000000000..e5d0c7dc390
--- /dev/null
+++ b/courses/scr403/quizz/001/en.yml
@@ -0,0 +1,12 @@
+question: What does sequential composition produce when chaining operation f (A → B) with operation g (B → C)?
+answer: A single composite operation from A to C, with f's output feeding into g.
+wrong_answers:
+ - A pair value containing both intermediate outputs of type B and C.
+ - A conditional that chooses between f and g based on the input.
+ - Two separate operations that run independently, sharing no data.
+explanation: >-
+ Sequential composition chains two operations end-to-end. The output of the
+ first operation becomes the input of the second. In Simplicity, this is
+ expressed with the comp combinator: comp f g applies f first, then g to
+ the result.
+reviewed: false
diff --git a/courses/scr403/quizz/001/question.yml b/courses/scr403/quizz/001/question.yml
new file mode 100644
index 00000000000..8a02612cb9b
--- /dev/null
+++ b/courses/scr403/quizz/001/question.yml
@@ -0,0 +1,14 @@
+id: 5c6d0109-ffe1-4da5-813d-204c9f467111
+chapterId: 6d46e77a-7e60-473b-b230-418da5ae44eb
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/002/en.yml b/courses/scr403/quizz/002/en.yml
new file mode 100644
index 00000000000..fcd47a0dcb8
--- /dev/null
+++ b/courses/scr403/quizz/002/en.yml
@@ -0,0 +1,12 @@
+question: In parallel composition, what happens to the input?
+answer: Both operations receive the same input, and their outputs form a product (pair).
+wrong_answers:
+ - The input is split in half, with each operation receiving one separate part.
+ - One operation processes the input first, and the other receives the modified result.
+ - The input is tagged and routed to just one of the two operations to process.
+explanation: >-
+ Parallel composition gives the same unmodified input to both operations
+ simultaneously. The results are bundled into a product type (pair). In
+ Simplicity, this uses the pair combinator, written f ▵ g, which produces
+ ⟨f(a), g(a)⟩ for input a.
+reviewed: false
diff --git a/courses/scr403/quizz/002/question.yml b/courses/scr403/quizz/002/question.yml
new file mode 100644
index 00000000000..01c7574ffe8
--- /dev/null
+++ b/courses/scr403/quizz/002/question.yml
@@ -0,0 +1,14 @@
+id: 9428566d-1ead-4d47-ba46-6b636029c0ef
+chapterId: 6d46e77a-7e60-473b-b230-418da5ae44eb
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/003/en.yml b/courses/scr403/quizz/003/en.yml
new file mode 100644
index 00000000000..238e7f91241
--- /dev/null
+++ b/courses/scr403/quizz/003/en.yml
@@ -0,0 +1,12 @@
+question: What is a sum type (A + B) in Simplicity?
+answer: "A tagged union: a value is either a left-tagged A or a right-tagged B."
+wrong_answers:
+ - A type that contains all values from both A and B simultaneously.
+ - An arithmetic addition of the two component types' bit sizes.
+ - A function type that maps every input from A to an output in B.
+explanation: >-
+ A sum type A + B is a tagged union. Each value carries a one-bit tag
+ indicating whether it's a left variant (of type A) or a right variant
+ (of type B). Even when A and B are the same type, left-tagged and
+ right-tagged values remain distinct.
+reviewed: false
diff --git a/courses/scr403/quizz/003/question.yml b/courses/scr403/quizz/003/question.yml
new file mode 100644
index 00000000000..ca103ebb2e8
--- /dev/null
+++ b/courses/scr403/quizz/003/question.yml
@@ -0,0 +1,14 @@
+id: aa208130-3c60-4310-9867-dc6f80e8aba1
+chapterId: 2a10a6ba-fada-4556-a673-3ae8c0794bf0
+difficulty: easy
+duration: 15
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/004/en.yml b/courses/scr403/quizz/004/en.yml
new file mode 100644
index 00000000000..6dd836d334d
--- /dev/null
+++ b/courses/scr403/quizz/004/en.yml
@@ -0,0 +1,12 @@
+question: How many core combinators does Simplicity have?
+answer: Nine (iden, unit, comp, pair, case, take, drop, injl, injr).
+wrong_answers:
+ - Three (sequential composition, parallel composition, conditional).
+ - Five (comp, pair, case, take, and drop combinators only).
+ - Twelve (the nine core plus three extra extension combinators).
+explanation: >-
+ Simplicity has exactly nine core combinators. Two basic operations (iden
+ and unit), three composition methods (comp, pair, case), and four
+ accessors (take, drop for products, injl and injr for sums). These nine
+ are sufficient to express any function between Simplicity types.
+reviewed: false
diff --git a/courses/scr403/quizz/004/question.yml b/courses/scr403/quizz/004/question.yml
new file mode 100644
index 00000000000..afad9fdf060
--- /dev/null
+++ b/courses/scr403/quizz/004/question.yml
@@ -0,0 +1,14 @@
+id: 54a868ea-e48c-4afc-a68a-f57b3d06c041
+chapterId: 2a10a6ba-fada-4556-a673-3ae8c0794bf0
+difficulty: easy
+duration: 15
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/005/en.yml b/courses/scr403/quizz/005/en.yml
new file mode 100644
index 00000000000..36eee3d759d
--- /dev/null
+++ b/courses/scr403/quizz/005/en.yml
@@ -0,0 +1,11 @@
+question: What does the 'take' combinator do?
+answer: It extracts the left component of a product, discarding the right.
+wrong_answers:
+ - It removes an element from a sum type, discarding the tag bit.
+ - It sequentially composes two separate operations end to end.
+ - It wraps a value with a left tag to build up a new sum type.
+explanation: >-
+ The take combinator is an extractor for product types. Given take f
+ applied to a pair ⟨a, b⟩, it discards b and applies f to a. Combined
+ with iden, take iden extracts the first element of any pair.
+reviewed: false
diff --git a/courses/scr403/quizz/005/question.yml b/courses/scr403/quizz/005/question.yml
new file mode 100644
index 00000000000..ca6cabb8811
--- /dev/null
+++ b/courses/scr403/quizz/005/question.yml
@@ -0,0 +1,14 @@
+id: 3f77abbb-10d4-41c6-a269-ccf8e0c44ff5
+chapterId: 2a10a6ba-fada-4556-a673-3ae8c0794bf0
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/006/en.yml b/courses/scr403/quizz/006/en.yml
new file mode 100644
index 00000000000..4458f55b340
--- /dev/null
+++ b/courses/scr403/quizz/006/en.yml
@@ -0,0 +1,12 @@
+question: What does the completeness theorem guarantee about Simplicity?
+answer: That any function between two Simplicity types can be built from the nine combinators.
+wrong_answers:
+ - That Simplicity programs are guaranteed to always terminate in constant time.
+ - That Simplicity is Turing-complete and can simulate any Turing machine at all.
+ - That every valid Simplicity program has one single unique representation.
+explanation: >-
+ The completeness theorem proves that for any function between finite
+ Simplicity types, there exists a Simplicity expression that computes it.
+ The constructive proof builds a lookup table using nested case and scribe
+ expressions. This has been formally verified in the Rocq proof assistant.
+reviewed: false
diff --git a/courses/scr403/quizz/006/question.yml b/courses/scr403/quizz/006/question.yml
new file mode 100644
index 00000000000..b0a082c0085
--- /dev/null
+++ b/courses/scr403/quizz/006/question.yml
@@ -0,0 +1,14 @@
+id: 963fde32-783e-4e20-8c3f-cae31bdcc2bf
+chapterId: 2a10a6ba-fada-4556-a673-3ae8c0794bf0
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/007/en.yml b/courses/scr403/quizz/007/en.yml
new file mode 100644
index 00000000000..df6d01d6667
--- /dev/null
+++ b/courses/scr403/quizz/007/en.yml
@@ -0,0 +1,13 @@
+question: How is the boolean type (𝟚) defined in Simplicity?
+answer: As the sum type 𝟙 + 𝟙, holding exactly two values (false and true).
+wrong_answers:
+ - As a product type 𝟙 × 𝟙 that would then hold only one value.
+ - As a special primitive type built directly into the language.
+ - As a 32-bit integer type restricted to just the values 0 and 1.
+explanation: >-
+ The boolean type 𝟚 is defined as 𝟙 + 𝟙, a sum of two unit types. The
+ left-tagged value σᴸ⟨⟩ represents false (0) and the right-tagged value
+ σᴿ⟨⟩ represents true (1). This is a one-bit data type built from just
+ the unit type and the sum type former — the product former is not
+ needed.
+reviewed: false
diff --git a/courses/scr403/quizz/007/question.yml b/courses/scr403/quizz/007/question.yml
new file mode 100644
index 00000000000..947449e88ac
--- /dev/null
+++ b/courses/scr403/quizz/007/question.yml
@@ -0,0 +1,14 @@
+id: c0dc9faf-1c10-4082-82c3-e4b07e7217f9
+chapterId: 2a10a6ba-fada-4556-a673-3ae8c0794bf0
+difficulty: easy
+duration: 15
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/008/en.yml b/courses/scr403/quizz/008/en.yml
new file mode 100644
index 00000000000..a6040732401
--- /dev/null
+++ b/courses/scr403/quizz/008/en.yml
@@ -0,0 +1,13 @@
+question: How does the logical AND operation work in Simplicity?
+answer: It branches on the first bit — if false it returns false, else the second bit.
+wrong_answers:
+ - It multiplies the two boolean values together using the product type.
+ - It uses a lookup table with all four possible input combinations.
+ - It applies the XOR combinator and then the NOT combinator to the result.
+explanation: >-
+ AND is defined as case (injl unit) (drop iden). The case combinator
+ branches on the first bit. If it's false (left-tagged), injl unit
+ returns false regardless of the second bit. If it's true (right-tagged),
+ drop iden returns the second bit unchanged. This matches the AND truth
+ table.
+reviewed: false
diff --git a/courses/scr403/quizz/008/question.yml b/courses/scr403/quizz/008/question.yml
new file mode 100644
index 00000000000..e265ff4540e
--- /dev/null
+++ b/courses/scr403/quizz/008/question.yml
@@ -0,0 +1,14 @@
+id: e5e0c93e-c244-4d00-ac35-7bc6e4533813
+chapterId: 9981ae62-ae50-4770-adf2-b253d1e08de3
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/009/en.yml b/courses/scr403/quizz/009/en.yml
new file mode 100644
index 00000000000..5fddc7ca972
--- /dev/null
+++ b/courses/scr403/quizz/009/en.yml
@@ -0,0 +1,12 @@
+question: What does a half-adder compute?
+answer: The carry (AND) and sum (XOR) of two input bits.
+wrong_answers:
+ - The sum of two multi-bit integers with carry propagation.
+ - The average of two bits rounded down.
+ - The bitwise OR and AND of two input bits.
+explanation: >-
+ A half-adder takes two single bits and produces two outputs using
+ parallel composition: the carry bit (AND of inputs) and the sum bit
+ (XOR of inputs). In Simplicity it's defined as and ▵ xor, running
+ both operations on the same input pair.
+reviewed: false
diff --git a/courses/scr403/quizz/009/question.yml b/courses/scr403/quizz/009/question.yml
new file mode 100644
index 00000000000..23aa5f63627
--- /dev/null
+++ b/courses/scr403/quizz/009/question.yml
@@ -0,0 +1,14 @@
+id: 6d167e33-3e10-4e7a-8919-6565f929eb8d
+chapterId: 9981ae62-ae50-4770-adf2-b253d1e08de3
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/010/en.yml b/courses/scr403/quizz/010/en.yml
new file mode 100644
index 00000000000..afda0a95c6c
--- /dev/null
+++ b/courses/scr403/quizz/010/en.yml
@@ -0,0 +1,12 @@
+question: How are fixed-length vectors built in Simplicity's type system?
+answer: Through nested product types of power-of-two length (e.g. A⁴ = A² × A²).
+wrong_answers:
+ - Using a special array type constructor built into the language.
+ - Through recursive sum types that chain the elements together in a list.
+ - Using variable-length buffers that have a fixed maximum size.
+explanation: >-
+ Simplicity builds vectors from nested product types. A² is A × A,
+ A⁴ is A² × A², A⁸ is A⁴ × A⁴, and so on. This gives power-of-two
+ sized collections. For example, 𝟚²⁵⁶ (a 256-bit hash) is built by
+ nesting products 8 levels deep from the boolean type.
+reviewed: false
diff --git a/courses/scr403/quizz/010/question.yml b/courses/scr403/quizz/010/question.yml
new file mode 100644
index 00000000000..dd5b6c7e9dd
--- /dev/null
+++ b/courses/scr403/quizz/010/question.yml
@@ -0,0 +1,14 @@
+id: 582e5a78-71f9-4dca-87f0-bdcc65c5179b
+chapterId: 9981ae62-ae50-4770-adf2-b253d1e08de3
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/011/en.yml b/courses/scr403/quizz/011/en.yml
new file mode 100644
index 00000000000..0584fbd1890
--- /dev/null
+++ b/courses/scr403/quizz/011/en.yml
@@ -0,0 +1,13 @@
+question: What is the role of jets in Simplicity?
+answer: Jets are native implementations replacing given Simplicity expressions for speed.
+wrong_answers:
+ - Jets are a compilation step that converts Simplicity into Bitcoin Script.
+ - Jets are network messages that broadcast Simplicity programs to all nodes.
+ - Jets are debugging tools for testing and tracing Simplicity expressions.
+explanation: >-
+ A jet is a native implementation that the network agrees to substitute
+ for a particular Simplicity expression (identified by its Merkle root).
+ The Simplicity expression serves as a formal specification of what the
+ jet computes, while the native code provides practical execution speed.
+ Common jets handle arithmetic and cryptographic operations like SHA-256.
+reviewed: false
diff --git a/courses/scr403/quizz/011/question.yml b/courses/scr403/quizz/011/question.yml
new file mode 100644
index 00000000000..ef03108dc77
--- /dev/null
+++ b/courses/scr403/quizz/011/question.yml
@@ -0,0 +1,14 @@
+id: 1a8a9923-3600-446e-afd9-299c3bff7f9d
+chapterId: 9981ae62-ae50-4770-adf2-b253d1e08de3
+difficulty: easy
+duration: 15
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/012/en.yml b/courses/scr403/quizz/012/en.yml
new file mode 100644
index 00000000000..0e27d03edd8
--- /dev/null
+++ b/courses/scr403/quizz/012/en.yml
@@ -0,0 +1,13 @@
+question: Why are Simplicity expressions serialized as DAGs rather than trees?
+answer: To prevent exponential growth, since shared sub-expressions are stored just once.
+wrong_answers:
+ - Because plain tree structures cannot represent conditional branching at all.
+ - To enable parallel execution across many separate multi-core processors.
+ - Because the Liquid Network protocol strictly mandates the DAG format here.
+explanation: >-
+ Simplicity expressions naturally form trees that could grow exponentially
+ as complexity increases. By serializing as directed acyclic graphs (DAGs),
+ sub-expressions that appear multiple times are stored once and referenced
+ by multiple parents. This keeps actual program sizes growing linearly
+ rather than exponentially.
+reviewed: false
diff --git a/courses/scr403/quizz/012/question.yml b/courses/scr403/quizz/012/question.yml
new file mode 100644
index 00000000000..26fdae5a581
--- /dev/null
+++ b/courses/scr403/quizz/012/question.yml
@@ -0,0 +1,14 @@
+id: b5e01b45-f621-429b-abee-c748b73739fd
+chapterId: 9981ae62-ae50-4770-adf2-b253d1e08de3
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/013/en.yml b/courses/scr403/quizz/013/en.yml
new file mode 100644
index 00000000000..bd2d9979ee2
--- /dev/null
+++ b/courses/scr403/quizz/013/en.yml
@@ -0,0 +1,13 @@
+question: Why does Simplicity use static analysis instead of a dynamic gas model like Ethereum?
+answer: To determine resource bounds before execution begins, giving predictable costs.
+wrong_answers:
+ - Because static analysis is simply much faster to implement for developers.
+ - Because Ethereum's own gas model was patented and therefore unavailable.
+ - Because Simplicity programs are far too short to ever really need metering.
+explanation: >-
+ Simplicity's static analysis allows the network to know exactly how
+ much computation a program requires before it runs. This eliminates
+ the unpredictability of dynamic metering, prevents denial-of-service
+ via resource exhaustion, and enables nodes to reject programs that
+ exceed limits without wasting computation.
+reviewed: false
diff --git a/courses/scr403/quizz/013/question.yml b/courses/scr403/quizz/013/question.yml
new file mode 100644
index 00000000000..755f3f12f24
--- /dev/null
+++ b/courses/scr403/quizz/013/question.yml
@@ -0,0 +1,14 @@
+id: 0c2c49a2-3766-467a-8ab4-c16c15a5dd60
+chapterId: 6d46e77a-7e60-473b-b230-418da5ae44eb
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/014/en.yml b/courses/scr403/quizz/014/en.yml
new file mode 100644
index 00000000000..a2dca5764b3
--- /dev/null
+++ b/courses/scr403/quizz/014/en.yml
@@ -0,0 +1,13 @@
+question: What is the unit type (𝟙) and why is it useful despite carrying no information?
+answer: It holds one value (the empty tuple) and is the base for all other types.
+wrong_answers:
+ - It represents the number 1 and is used directly for arithmetic operations.
+ - It is a special debugging type that logs execution traces out to a file.
+ - It stores exactly a single bit of data used for boolean operations.
+explanation: >-
+ The unit type 𝟙 has exactly one value — the empty tuple ⟨⟩. While
+ it carries zero bits of information, it is essential as the seed
+ from which sum and product types build up all useful data types.
+ For example, the boolean type 𝟚 is 𝟙 + 𝟙, constructed entirely
+ from unit types.
+reviewed: false
diff --git a/courses/scr403/quizz/014/question.yml b/courses/scr403/quizz/014/question.yml
new file mode 100644
index 00000000000..c59d500f6b2
--- /dev/null
+++ b/courses/scr403/quizz/014/question.yml
@@ -0,0 +1,14 @@
+id: d92a0b52-981d-4a4b-b245-4a6b0c0ac328
+chapterId: 2a10a6ba-fada-4556-a673-3ae8c0794bf0
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/015/en.yml b/courses/scr403/quizz/015/en.yml
new file mode 100644
index 00000000000..1ab13354476
--- /dev/null
+++ b/courses/scr403/quizz/015/en.yml
@@ -0,0 +1,13 @@
+question: Why does the 'case' combinator include a shared environment type C in its signature?
+answer: So both branches can read shared context data alongside the tagged input.
+wrong_answers:
+ - To limit the size of the input in order to prevent stack overflows.
+ - To enable recursive calls back and forth between the two branches.
+ - To store the output of the previous combinator earlier in the chain.
+explanation: >-
+ The case combinator has signature (A + B) × C ⊢ D. The extra type C
+ acts as a shared environment that both the left branch (f : A × C ⊢ D)
+ and right branch (g : B × C ⊢ D) can access. This is more powerful
+ than a simple if-then-else because branches receive both their specific
+ data and contextual information needed for computation.
+reviewed: false
diff --git a/courses/scr403/quizz/015/question.yml b/courses/scr403/quizz/015/question.yml
new file mode 100644
index 00000000000..41c8258408e
--- /dev/null
+++ b/courses/scr403/quizz/015/question.yml
@@ -0,0 +1,14 @@
+id: 8b4ee208-b723-41c4-af9c-0d30b10132fb
+chapterId: 2a10a6ba-fada-4556-a673-3ae8c0794bf0
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/016/en.yml b/courses/scr403/quizz/016/en.yml
new file mode 100644
index 00000000000..5b4a55e3bdf
--- /dev/null
+++ b/courses/scr403/quizz/016/en.yml
@@ -0,0 +1,13 @@
+question: What is the relationship between Simplicity and Gentzen's sequent calculus?
+answer: Its nine combinators mirror the conjunctive-disjunctive fragment of the sequent calculus.
+wrong_answers:
+ - Simplicity was directly translated from sequent calculus proofs into working code.
+ - Gentzen's sequent calculus is used at runtime to type-check Simplicity programs.
+ - They are entirely unrelated, and the surface similarity is purely coincidental.
+explanation: >-
+ The nine core rules of Simplicity closely resemble rules in Gentzen's
+ sequent calculus, analogous to the Curry-Howard correspondence between
+ lambda calculus and natural deduction. This connection ensures that
+ types in the premises are smaller than in conclusions, which the Bit
+ Machine exploits for efficient execution with minimal data copying.
+reviewed: false
diff --git a/courses/scr403/quizz/016/question.yml b/courses/scr403/quizz/016/question.yml
new file mode 100644
index 00000000000..63aa620e904
--- /dev/null
+++ b/courses/scr403/quizz/016/question.yml
@@ -0,0 +1,14 @@
+id: c4df1bd0-8d1c-4f71-ac5a-ebf3be1f4a51
+chapterId: 2a10a6ba-fada-4556-a673-3ae8c0794bf0
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/017/en.yml b/courses/scr403/quizz/017/en.yml
new file mode 100644
index 00000000000..c245af6ec3d
--- /dev/null
+++ b/courses/scr403/quizz/017/en.yml
@@ -0,0 +1,13 @@
+question: How does the access notation (O, I, H) work in Simplicity?
+answer: O means 'take' (left), I means 'drop' (right), and H means 'iden' (whole value).
+wrong_answers:
+ - O means output, I means input, and H means halt the program's execution.
+ - They are variable names that the compiler assigns to values automatically.
+ - O selects odd-indexed elements, I selects even-indexed elements, H selects the head.
+explanation: >-
+ The O/I/H shorthand provides a compact way to navigate nested pairs.
+ O f is take f (extract left), I f is drop f (extract right), and H is
+ iden (the whole value). Sequences like I O H mean drop(take(iden)),
+ extracting the first element of the second element. This resembles
+ De Bruijn indices with binary digits as tree positions.
+reviewed: false
diff --git a/courses/scr403/quizz/017/question.yml b/courses/scr403/quizz/017/question.yml
new file mode 100644
index 00000000000..d168c75ebfa
--- /dev/null
+++ b/courses/scr403/quizz/017/question.yml
@@ -0,0 +1,14 @@
+id: f88741e5-8019-427f-80d4-de0616a2bd9a
+chapterId: 9981ae62-ae50-4770-adf2-b253d1e08de3
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/018/en.yml b/courses/scr403/quizz/018/en.yml
new file mode 100644
index 00000000000..b331f7056a2
--- /dev/null
+++ b/courses/scr403/quizz/018/en.yml
@@ -0,0 +1,13 @@
+question: How are variable-length buffers represented in Simplicity's type system?
+answer: As nested option-type products, each layer flagging a power-of-two block.
+wrong_answers:
+ - Using a special dynamic array type built directly into the language.
+ - Through recursive sum types that grow larger on each function call.
+ - As fixed-size vectors that are padded out with trailing zero values.
+explanation: >-
+ Buffers use nested option types. For example, Xᑉ⁸ expands to
+ (1 + X⁴) × ((1 + X²) × (1 + X)), which as a polynomial yields
+ 1 + X + X² + ... + X⁷ — representing collections of 0 to 7 elements.
+ Each option layer indicates whether a power-of-two block is present,
+ effectively encoding the length in binary.
+reviewed: false
diff --git a/courses/scr403/quizz/018/question.yml b/courses/scr403/quizz/018/question.yml
new file mode 100644
index 00000000000..7f41cef5a3b
--- /dev/null
+++ b/courses/scr403/quizz/018/question.yml
@@ -0,0 +1,14 @@
+id: 8ecab257-d521-437a-ad11-bb6d2020b0f1
+chapterId: 9981ae62-ae50-4770-adf2-b253d1e08de3
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/019/en.yml b/courses/scr403/quizz/019/en.yml
new file mode 100644
index 00000000000..70eea425845
--- /dev/null
+++ b/courses/scr403/quizz/019/en.yml
@@ -0,0 +1,14 @@
+question: What is SimplicityHL and why is it needed?
+answer: A higher-level language compiling to Simplicity that manages naming and scope.
+wrong_answers:
+ - A hardware description language for mining the ASICs that run Simplicity.
+ - A graphical drag-and-drop IDE for wiring together Simplicity combinators.
+ - A testing framework for running Simplicity programs inside a safe sandbox.
+explanation: >-
+ Raw Simplicity becomes inscrutable at production complexity levels because
+ all data access must be done through nested take/drop combinators. SimplicityHL
+ provides familiar programming constructs — named variables, scoping, library
+ imports, and control flow — that compile down to Simplicity combinator
+ expressions. End users write SimplicityHL while Simplicity serves as
+ the formally verified compilation target.
+reviewed: false
diff --git a/courses/scr403/quizz/019/question.yml b/courses/scr403/quizz/019/question.yml
new file mode 100644
index 00000000000..56a1e9eb35b
--- /dev/null
+++ b/courses/scr403/quizz/019/question.yml
@@ -0,0 +1,14 @@
+id: b4130b1d-4f08-4543-948c-3c2095cd110f
+chapterId: 9981ae62-ae50-4770-adf2-b253d1e08de3
+difficulty: easy
+duration: 15
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/020/en.yml b/courses/scr403/quizz/020/en.yml
new file mode 100644
index 00000000000..39053db5baf
--- /dev/null
+++ b/courses/scr403/quizz/020/en.yml
@@ -0,0 +1,12 @@
+question: "What are the two side effects used in Simplicity for Bitcoin and Liquid applications?"
+answer: "The Failure effect (an exception of type 1) and the Reader effect (access to transaction environment data)."
+wrong_answers:
+ - "The State effect (mutable variables) and the Writer effect (logging to a transaction log)."
+ - "The IO effect (network communication) and the Memory effect (dynamic memory allocation)."
+ - "The Continuation effect (callbacks) and the Nondeterminism effect (multiple execution paths)."
+explanation: >-
+ Simplicity uses exactly two side effects for blockchain applications. The Failure effect allows
+ computations to abort (e.g., when a signature check fails), and the Reader effect allows
+ expressions to read data from the transaction environment. The core combinators remain pure —
+ side effects are introduced through jets.
+reviewed: true
diff --git a/courses/scr403/quizz/020/question.yml b/courses/scr403/quizz/020/question.yml
new file mode 100644
index 00000000000..1eb6ebdf80c
--- /dev/null
+++ b/courses/scr403/quizz/020/question.yml
@@ -0,0 +1,14 @@
+id: db95b84e-6529-4422-aae2-3d6f8a789013
+chapterId: 9eafe498-0765-419a-a69d-a74a9cdf3713
+difficulty: easy
+duration: 15
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/021/en.yml b/courses/scr403/quizz/021/en.yml
new file mode 100644
index 00000000000..3cde1cab1a3
--- /dev/null
+++ b/courses/scr403/quizz/021/en.yml
@@ -0,0 +1,12 @@
+question: "Why is the Failure effect commutative in Simplicity, even though exceptions are generally not commutative?"
+answer: Because the exception type is unit (1) with only one value, so the throwing order does not matter.
+wrong_answers:
+ - Because Simplicity executes all expressions in a deterministic order defined by the combinator tree.
+ - Because the Failure effect is always caught and then re-thrown by the case combinator.
+ - Because Simplicity uses batch verification, which makes all thrown exceptions equivalent.
+explanation: >-
+ In general, exceptions are not commutative because different expressions may throw different
+ exception values. However, Simplicity restricts exceptions to unit type (only one possible value),
+ so swapping the order of two potentially-failing expressions produces the same exception regardless
+ of which one actually fails. This commutativity property enables important program optimizations.
+reviewed: true
diff --git a/courses/scr403/quizz/021/question.yml b/courses/scr403/quizz/021/question.yml
new file mode 100644
index 00000000000..acd3a9b3066
--- /dev/null
+++ b/courses/scr403/quizz/021/question.yml
@@ -0,0 +1,14 @@
+id: b5e36dfe-d941-4041-ba23-dc1643d7abc9
+chapterId: 9eafe498-0765-419a-a69d-a74a9cdf3713
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/022/en.yml b/courses/scr403/quizz/022/en.yml
new file mode 100644
index 00000000000..19f735016cd
--- /dev/null
+++ b/courses/scr403/quizz/022/en.yml
@@ -0,0 +1,12 @@
+question: "Why does bip0340-verify use the Failure effect instead of returning a boolean (true/false)?"
+answer: To enable batch verification of Schnorr signatures, where one failed check fails the batch.
+wrong_answers:
+ - Because boolean types are too expensive in terms of block space compared to the unit type.
+ - Because Simplicity's type system cannot represent boolean return values coming from jets.
+ - Because returning a plain boolean value would directly violate the completeness theorem.
+explanation: >-
+ If bip0340-verify returned a boolean, a failing signature check could still lead to a branch where
+ the script succeeds. In that case, the verifier would need to know which specific signature
+ failed, preventing batch verification. By using the Failure effect, a failed check always aborts
+ the entire computation, enabling efficient batch verification where many signatures are pooled together.
+reviewed: true
diff --git a/courses/scr403/quizz/022/question.yml b/courses/scr403/quizz/022/question.yml
new file mode 100644
index 00000000000..38869bdb217
--- /dev/null
+++ b/courses/scr403/quizz/022/question.yml
@@ -0,0 +1,14 @@
+id: 04d17f4c-1e95-4c2e-8e40-c9b84cf75b2f
+chapterId: 9eafe498-0765-419a-a69d-a74a9cdf3713
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/023/en.yml b/courses/scr403/quizz/023/en.yml
new file mode 100644
index 00000000000..86152612da3
--- /dev/null
+++ b/courses/scr403/quizz/023/en.yml
@@ -0,0 +1,13 @@
+question: "Why does sig-all-hash use the Reader effect instead of taking the transaction data as a typed input?"
+answer: So the jet can use PrecomputedTransactionData and run in constant time on a fixed environment.
+wrong_answers:
+ - Because Simplicity's type system fundamentally cannot represent transaction data as a type.
+ - Because the Reader effect is faster than passing that data through the combinator tree.
+ - Because transaction data is far too large to fit in Simplicity's fixed-size type system.
+explanation: >-
+ If sig-all-hash took a TxEnv input type, programs could pass modified copies of transaction data
+ to the jet, preventing it from using precomputed hashes. With the Reader effect, the jet only
+ accesses a fixed, immutable transaction environment, so its implementation can safely use
+ PrecomputedTransactionData and run in constant time per signature check, avoiding the quadratic
+ hashing problem that plagued early Bitcoin Script.
+reviewed: true
diff --git a/courses/scr403/quizz/023/question.yml b/courses/scr403/quizz/023/question.yml
new file mode 100644
index 00000000000..c537ab45dc8
--- /dev/null
+++ b/courses/scr403/quizz/023/question.yml
@@ -0,0 +1,14 @@
+id: 0b2a2848-cb65-46e2-be56-e98513794786
+chapterId: 9eafe498-0765-419a-a69d-a74a9cdf3713
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/024/en.yml b/courses/scr403/quizz/024/en.yml
new file mode 100644
index 00000000000..eb0b4ace5a2
--- /dev/null
+++ b/courses/scr403/quizz/024/en.yml
@@ -0,0 +1,11 @@
+question: "What is the type of a Simplicity program?"
+answer: 1 ⊢ 1 (unit to unit) — no meaningful input or output; side effects do the I/O.
+wrong_answers:
+ - TxEnv ⊢ Bool — it takes transaction data and returns a validity boolean.
+ - 2^256 ⊢ 2^256 — it takes a hash input and returns a new hash output value.
+ - Any type A ⊢ B — programs may have completely arbitrary input and output types.
+explanation: >-
+ A Simplicity program is defined as an expression of type 1 ⊢ 1. The Reader effect captures
+ the transaction environment input, while the Failure effect determines success or failure.
+ These side effects handle all the I/O rather than the Simplicity types themselves.
+reviewed: true
diff --git a/courses/scr403/quizz/024/question.yml b/courses/scr403/quizz/024/question.yml
new file mode 100644
index 00000000000..0231c7f2bab
--- /dev/null
+++ b/courses/scr403/quizz/024/question.yml
@@ -0,0 +1,14 @@
+id: bbc1725b-94ae-42ea-85cc-4e40087a985a
+chapterId: 961652e3-8f7d-4c2a-8b55-9a990b91a0dd
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/025/en.yml b/courses/scr403/quizz/025/en.yml
new file mode 100644
index 00000000000..48e227d1005
--- /dev/null
+++ b/courses/scr403/quizz/025/en.yml
@@ -0,0 +1,12 @@
+question: "What is a Commitment Merkle Root (CMR) in Simplicity?"
+answer: A 256-bit hash committing to a Simplicity program's structure with tagged SHA-256.
+wrong_answers:
+ - A binary tree containing all possible execution paths of a Simplicity program.
+ - A hash of the program's types and witness values used for address verification.
+ - A Merkle root of the transaction data that the program is authorized to access.
+explanation: >-
+ Each Simplicity combinator has a unique SHA-256 tag (e.g., Simplicity␟Commitment␟iden), and the
+ CMR is computed by recursively hashing the program's combinator tree using these tagged midstates.
+ Importantly, the CMR does not commit to the types of expressions, relying on type inference
+ during redemption. CMRs are used to commit programs into Taproot addresses.
+reviewed: true
diff --git a/courses/scr403/quizz/025/question.yml b/courses/scr403/quizz/025/question.yml
new file mode 100644
index 00000000000..f07f311b18e
--- /dev/null
+++ b/courses/scr403/quizz/025/question.yml
@@ -0,0 +1,14 @@
+id: e9f7f36d-e07d-4ad2-9d12-845c0b5f63bb
+chapterId: 961652e3-8f7d-4c2a-8b55-9a990b91a0dd
+difficulty: intermediate
+duration: 30
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/026/en.yml b/courses/scr403/quizz/026/en.yml
new file mode 100644
index 00000000000..2e12a506cb6
--- /dev/null
+++ b/courses/scr403/quizz/026/en.yml
@@ -0,0 +1,11 @@
+question: "What TapLeaf version does Simplicity use when committed under BIP-0341 Taproot?"
+answer: Version 0xbe, which is the byte value 190 in decimal.
+wrong_answers:
+ - Version 0xc0, the same as Bitcoin Script Tapscript.
+ - Version 0x00, the default Taproot leaf version.
+ - Version 0xff, a reserved version for experimental scripts.
+explanation: >-
+ Simplicity programs are committed into Taproot addresses using TapLeaf version 0xbe. This
+ distinguishes Simplicity scripts from Bitcoin Tapscript (which uses version 0xc0) and allows
+ the network to identify and validate Simplicity programs correctly when they appear on-chain.
+reviewed: true
diff --git a/courses/scr403/quizz/026/question.yml b/courses/scr403/quizz/026/question.yml
new file mode 100644
index 00000000000..e8d76205fee
--- /dev/null
+++ b/courses/scr403/quizz/026/question.yml
@@ -0,0 +1,14 @@
+id: 55d95b1b-18e0-4ac0-b5d2-e5f18ea365a0
+chapterId: 961652e3-8f7d-4c2a-8b55-9a990b91a0dd
+difficulty: easy
+duration: 15
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/027/en.yml b/courses/scr403/quizz/027/en.yml
new file mode 100644
index 00000000000..d05627cdf06
--- /dev/null
+++ b/courses/scr403/quizz/027/en.yml
@@ -0,0 +1,12 @@
+question: "Why are witness values excluded from the Commitment Merkle Root (CMR)?"
+answer: So addresses form before witnesses are known, and unused branches prune privately.
+wrong_answers:
+ - Because witness values are simply far too large to include in a 256-bit hash.
+ - Because witness values are validated entirely separately by the Failure effect.
+ - Because including the witness values would make the CMR non-deterministic.
+explanation: >-
+ Witness expressions (like signatures) are provided at spending time, not at address creation time.
+ Excluding them from the CMR enables two important properties: addresses can be generated before
+ the spending transaction exists, and unexecuted conditional branches can be pruned from the
+ on-chain data without revealing their associated witness values.
+reviewed: true
diff --git a/courses/scr403/quizz/027/question.yml b/courses/scr403/quizz/027/question.yml
new file mode 100644
index 00000000000..1e45a1ded95
--- /dev/null
+++ b/courses/scr403/quizz/027/question.yml
@@ -0,0 +1,14 @@
+id: a81a36bd-d3da-4205-886b-3b66bc82fa1f
+chapterId: 961652e3-8f7d-4c2a-8b55-9a990b91a0dd
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/028/en.yml b/courses/scr403/quizz/028/en.yml
new file mode 100644
index 00000000000..f2eb2660506
--- /dev/null
+++ b/courses/scr403/quizz/028/en.yml
@@ -0,0 +1,16 @@
+question: In what sense is conditional composition the dual of parallel composition?
+answer: Parallel feeds both operations one input and pairs their outputs (a product); conditional takes a sum of inputs and both branches share one output type.
+wrong_answers:
+ - Parallel must run its two operations simultaneously; conditional runs them in sequence and returns only the branch the tag selects.
+ - Both run on one shared input; parallel keeps the output pair, while conditional runs both branches and discards the unselected one.
+ - Parallel duplicates its input beforehand while conditional duplicates its output afterward, swapping where the copying happens.
+explanation: >-
+ The duality is a product/sum exchange with the shared type switching
+ sides: parallel composition gives both operations the same input type
+ and pairs their outputs into a product, whereas conditional composition
+ takes a sum (tagged union) of the two input types and both branches must
+ yield the same output type. Simultaneity is irrelevant — the article
+ stresses parallel composition may be implemented sequentially — and
+ conditional composition executes exactly one branch, chosen by the tag,
+ rather than running both and discarding one.
+reviewed: false
diff --git a/courses/scr403/quizz/028/question.yml b/courses/scr403/quizz/028/question.yml
new file mode 100644
index 00000000000..12ff7fa4e9e
--- /dev/null
+++ b/courses/scr403/quizz/028/question.yml
@@ -0,0 +1,14 @@
+id: 000a686f-b43a-4685-b014-e4b82fa6a9e7
+chapterId: 6d46e77a-7e60-473b-b230-418da5ae44eb
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/029/en.yml b/courses/scr403/quizz/029/en.yml
new file mode 100644
index 00000000000..d699b825622
--- /dev/null
+++ b/courses/scr403/quizz/029/en.yml
@@ -0,0 +1,15 @@
+question: Simplicity excludes unbounded recursion. What is its intended substitute for unbounded iteration?
+answer: Recursive covenants that spread the computation across multiple transactions, keeping each transaction's cost predictable.
+wrong_answers:
+ - The delegation feature, purpose-built to give a metered form of unbounded recursion inside a single transaction.
+ - The nine core combinators, whose completeness lets a fixed-point construction encode any recursive function.
+ - Compile-time loop unrolling, where static analysis infers the maximum iteration count and duplicates the body.
+explanation: >-
+ The article's thesis is that unbounded iteration is better implemented
+ as recursive covenants computing over multiple transactions, which
+ avoids block-space and standardness constraints and makes transaction
+ costs predictable. Delegation can only be abused to produce something
+ resembling unbounded recursion — it is not the intended mechanism — and
+ the nine core combinators are complete only for finite computations, so
+ no fixed-point construction exists within a single program.
+reviewed: false
diff --git a/courses/scr403/quizz/029/question.yml b/courses/scr403/quizz/029/question.yml
new file mode 100644
index 00000000000..83241e11150
--- /dev/null
+++ b/courses/scr403/quizz/029/question.yml
@@ -0,0 +1,14 @@
+id: ff0808d2-6b22-49a1-ab04-7b861df475a5
+chapterId: 6d46e77a-7e60-473b-b230-418da5ae44eb
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/030/en.yml b/courses/scr403/quizz/030/en.yml
new file mode 100644
index 00000000000..bac3278714b
--- /dev/null
+++ b/courses/scr403/quizz/030/en.yml
@@ -0,0 +1,15 @@
+question: "Which core-combinator expression implements the distribution function dist : (A + B) × C ⊢ A × C + B × C?"
+answer: case (injl iden) (injr iden)
+wrong_answers:
+ - case (injl (take iden)) (injr (drop iden))
+ - pair (injl iden) (injr iden)
+ - copair (injl iden) (injr iden)
+explanation: >-
+ Inside each branch of case, the environment is already paired with the
+ untagged value, so f = injl iden and g = injr iden give ⟨σᴸ(a), c⟩ ↦
+ σᴸ⟨a, c⟩ and ⟨σᴿ(b), c⟩ ↦ σᴿ⟨b, c⟩ — exactly dist. The take/drop variant
+ type-checks but discards the pairing, denoting a function of type (A +
+ B) × C ⊢ A + C instead. pair produces a product rather than a sum, and
+ copair is not a Simplicity combinator at all — dist is precisely what
+ copair alone cannot express.
+reviewed: false
diff --git a/courses/scr403/quizz/030/question.yml b/courses/scr403/quizz/030/question.yml
new file mode 100644
index 00000000000..e521b410853
--- /dev/null
+++ b/courses/scr403/quizz/030/question.yml
@@ -0,0 +1,14 @@
+id: 7c9dd892-1724-4c25-89cb-d24c0bc88097
+chapterId: 2a10a6ba-fada-4556-a673-3ae8c0794bf0
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/031/en.yml b/courses/scr403/quizz/031/en.yml
new file mode 100644
index 00000000000..513419d8b03
--- /dev/null
+++ b/courses/scr403/quizz/031/en.yml
@@ -0,0 +1,13 @@
+question: What is the type of pair (drop iden) (take iden), and what function does it denote?
+answer: A × B ⊢ B × A — it swaps the two components of a pair.
+wrong_answers:
+ - A × B ⊢ A × B — it passes both components through unchanged (the identity).
+ - "Ill-typed: take iden and drop iden have different output types, which pair cannot merge."
+ - (A × B) × (A × B) ⊢ B × A — pair merges its two subexpressions' input types.
+explanation: >-
+ drop iden : A × B ⊢ B extracts the second component and take iden : A ×
+ B ⊢ A extracts the first. The pair combinator requires only that its two
+ subexpressions share the same input type (here A × B); their outputs may
+ differ, and are returned as a pair. On input ⟨a, b⟩ the expression
+ therefore yields ⟨b, a⟩: the swap function, of type A × B ⊢ B × A.
+reviewed: false
diff --git a/courses/scr403/quizz/031/question.yml b/courses/scr403/quizz/031/question.yml
new file mode 100644
index 00000000000..c614c527ae9
--- /dev/null
+++ b/courses/scr403/quizz/031/question.yml
@@ -0,0 +1,14 @@
+id: 9a086b63-059e-4573-bd34-266ad74d5016
+chapterId: 2a10a6ba-fada-4556-a673-3ae8c0794bf0
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/032/en.yml b/courses/scr403/quizz/032/en.yml
new file mode 100644
index 00000000000..05cab8e1797
--- /dev/null
+++ b/courses/scr403/quizz/032/en.yml
@@ -0,0 +1,16 @@
+question: The completeness proof builds any function by nesting case to decompose the input and scribe for each output. Why is it only a theoretical tool?
+answer: The resulting expression is a giant lookup table whose size grows exponentially — a 256-bit input would need about 2²⁵⁶ entries.
+wrong_answers:
+ - scribe is a macro, not a core combinator, so the expression falls outside the formally verified language.
+ - The Bit Machine evaluates it in exponential time, even though the expression itself stays compact via sharing.
+ - Nested case can only decompose sum types, so the construction fails on any product-typed input.
+explanation: >-
+ The construction enumerates every possible input via nested case
+ decomposition and hard-codes each output with scribe, so expression size
+ explodes exponentially — astronomical for realistic types like 256-bit
+ words. The blowup is in the expression's size, not in an otherwise-
+ compact expression's runtime. scribe expands into genuine core
+ combinators (unit, injl, injr, pair), so the result stays inside the
+ core language, whose completeness theorem is formally verified in Rocq;
+ and the decomposition handles inputs of any type, products included.
+reviewed: false
diff --git a/courses/scr403/quizz/032/question.yml b/courses/scr403/quizz/032/question.yml
new file mode 100644
index 00000000000..36d3148bc80
--- /dev/null
+++ b/courses/scr403/quizz/032/question.yml
@@ -0,0 +1,14 @@
+id: 8d7f9c10-c453-463b-830b-98d6cf6638b5
+chapterId: 2a10a6ba-fada-4556-a673-3ae8c0794bf0
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/033/en.yml b/courses/scr403/quizz/033/en.yml
new file mode 100644
index 00000000000..dfc89bb95cb
--- /dev/null
+++ b/courses/scr403/quizz/033/en.yml
@@ -0,0 +1,14 @@
+question: Given the 'smaller types in the premises' typing rules, which core combinators actually move data during execution?
+answer: Only iden and comp; the other seven are implemented with nothing more than bookkeeping.
+wrong_answers:
+ - Only take and drop; extracting one component forces the machine to copy it out of the product.
+ - Only pair and case; duplicating the input for two branches and dispatching on a tag shuffle data.
+ - Only injl and injr; adding a tag rewrites the value into a larger sum-type representation.
+explanation: >-
+ Counterintuitively, the combinators that look like data access (take,
+ drop, pair, case, injl, injr) need no copying: because premises in the
+ typing rules involve smaller types than their conclusions, the Bit
+ Machine can implement them with bookkeeping alone. Only iden, which
+ copies its entire input to its output, and comp, which materializes an
+ intermediate value passed from f to g, genuinely move data around.
+reviewed: false
diff --git a/courses/scr403/quizz/033/question.yml b/courses/scr403/quizz/033/question.yml
new file mode 100644
index 00000000000..8b7161c5494
--- /dev/null
+++ b/courses/scr403/quizz/033/question.yml
@@ -0,0 +1,14 @@
+id: 31df83c3-972d-46ec-aefb-249154f541fc
+chapterId: 2a10a6ba-fada-4556-a673-3ae8c0794bf0
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/034/en.yml b/courses/scr403/quizz/034/en.yml
new file mode 100644
index 00000000000..470f91995eb
--- /dev/null
+++ b/courses/scr403/quizz/034/en.yml
@@ -0,0 +1,14 @@
+question: The full-adder ORs the carry bits of its two half-adders instead of XORing them. Why is OR correct?
+answer: At most one half-adder can carry for any input, so OR merges two mutually exclusive cases exactly.
+wrong_answers:
+ - The two carry bits must be added, and OR is how single-bit binary addition is done in Simplicity.
+ - After the branching, OR is the only Boolean operator whose type still matches the environment.
+ - OR over-approximates the carry; any spurious carries are dropped by the final projection afterwards.
+explanation: >-
+ If the first half-adder carries, both of its input bits were 1, so its
+ sum bit is 0 — and a half-adder fed a 0 can never carry. The two carry
+ bits are therefore never simultaneously 1, and OR merges them exactly
+ (on the reachable inputs it even coincides with XOR). This mutual
+ exclusivity is precisely what makes the two-half-adder decomposition of
+ a full-adder correct.
+reviewed: false
diff --git a/courses/scr403/quizz/034/question.yml b/courses/scr403/quizz/034/question.yml
new file mode 100644
index 00000000000..39abc707af7
--- /dev/null
+++ b/courses/scr403/quizz/034/question.yml
@@ -0,0 +1,14 @@
+id: 0e911244-f764-4df7-a12a-0d09195e97d5
+chapterId: 9981ae62-ae50-4770-adf2-b253d1e08de3
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/035/en.yml b/courses/scr403/quizz/035/en.yml
new file mode 100644
index 00000000000..40de6c4cdc9
--- /dev/null
+++ b/courses/scr403/quizz/035/en.yml
@@ -0,0 +1,14 @@
+question: Trace the full-adder on ⟨⟨1,1⟩,1⟩ (1+1+1). What value does stage two, O O H ▵ (O I H ▵ I H ⨾ half-adder), hand to the final stage?
+answer: ⟨1, ⟨0, 1⟩⟩ — the first half-adder's carry, then the second's carry and sum.
+wrong_answers:
+ - ⟨1, ⟨1, 0⟩⟩ — the first half-adder's carry, then the second's sum and carry.
+ - ⟨0, ⟨0, 1⟩⟩ — the first half-adder's sum bit, then the second's carry and sum.
+ - ⟨1, ⟨1, 1⟩⟩ — the first half-adder's carry, then the second's OR and XOR bits.
+explanation: >-
+ Stage one computes half-adder⟨1,1⟩ = ⟨1, 0⟩ (carry 1, sum 0) and saves
+ the carry-in, giving ⟨⟨1,0⟩, 1⟩. In stage two, O O H extracts the first
+ carry (1), while O I H ▵ I H feeds ⟨0, 1⟩ — the first sum and the carry-
+ in — into the second half-adder, yielding ⟨0, 1⟩ since and(0,1)=0 and
+ xor(0,1)=1. The final stage then ORs the two carries and keeps the sum,
+ producing ⟨1, 1⟩: binary 3, as expected.
+reviewed: false
diff --git a/courses/scr403/quizz/035/question.yml b/courses/scr403/quizz/035/question.yml
new file mode 100644
index 00000000000..e68a3f2de07
--- /dev/null
+++ b/courses/scr403/quizz/035/question.yml
@@ -0,0 +1,14 @@
+id: c6f4fb69-40d0-45d7-9d45-4f6f0f9e65d6
+chapterId: 9981ae62-ae50-4770-adf2-b253d1e08de3
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/036/en.yml b/courses/scr403/quizz/036/en.yml
new file mode 100644
index 00000000000..a0fe03d068d
--- /dev/null
+++ b/courses/scr403/quizz/036/en.yml
@@ -0,0 +1,14 @@
+question: push--
+ Aᑉⁿ is exactly the type of lists whose length is strictly less than n,
+ so a buffer at maximum capacity holds n−1 elements. Pushing one more
+ produces exactly n elements, which Aᑉⁿ cannot represent; the Aⁿ summand
+ returns that overflowed result as a full vector. Encoding overflow in
+ the output type keeps push--
+ A jet is a native replacement for one specific, fully-formed Simplicity
+ expression, which nodes can substitute while preserving its exact
+ semantics. fold-right-n, map, zip and their variants are not single
+ expressions but construction schemes: each choice of the inner function
+ f yields a structurally different expression, so no single jet can stand
+ in for the whole family. That is why these iteration patterns appear as
+ genuine combinator code in real programs, typically generated by higher-
+ level languages like SimplicityHL.
+reviewed: false
diff --git a/courses/scr403/quizz/037/question.yml b/courses/scr403/quizz/037/question.yml
new file mode 100644
index 00000000000..0ddc79996b4
--- /dev/null
+++ b/courses/scr403/quizz/037/question.yml
@@ -0,0 +1,14 @@
+id: 485d8e95-c687-4825-8fcd-dadcd4a54edf
+chapterId: 9981ae62-ae50-4770-adf2-b253d1e08de3
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/038/en.yml b/courses/scr403/quizz/038/en.yml
new file mode 100644
index 00000000000..67284e9d0bb
--- /dev/null
+++ b/courses/scr403/quizz/038/en.yml
@@ -0,0 +1,16 @@
+question: A half-agg-verify jet logs a set of tuples as a Writer effect. Under the commutative/idempotent/unitary test, what does the set design achieve, and what is still missing?
+answer: "Commutative and idempotent (as Simplicity requires), but not unitary: discarding a call would drop its tuple and skip a signature."
+wrong_answers:
+ - Idempotent and unitary, but not commutative, since the aggregate must combine r-components in signing order.
+ - All three, so an optimizer may freely duplicate, reorder, or discard the calls with no risk.
+ - Commutative but not idempotent, since logging the same tuple twice would demand two aggregate s-components.
+explanation: >-
+ Treating the writer log as a set makes the effect idempotent and
+ commutative, because set insertion itself has both properties — exactly
+ the two Simplicity demands of every effect. Unitarity is still out of
+ reach: like Failure, the write influences transaction validity, since
+ the transaction is only valid when an aggregate s-component covers every
+ logged tuple. An expression performing the write therefore cannot be
+ discarded merely because its unit output is unused, as its tuple would
+ silently vanish from the half-aggregation verification.
+reviewed: false
diff --git a/courses/scr403/quizz/038/question.yml b/courses/scr403/quizz/038/question.yml
new file mode 100644
index 00000000000..89bbac284da
--- /dev/null
+++ b/courses/scr403/quizz/038/question.yml
@@ -0,0 +1,14 @@
+id: c3aefa22-3865-4a6c-8afd-ab30df8b5cbf
+chapterId: 9eafe498-0765-419a-a69d-a74a9cdf3713
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/039/en.yml b/courses/scr403/quizz/039/en.yml
new file mode 100644
index 00000000000..f27a8ca3755
--- /dev/null
+++ b/courses/scr403/quizz/039/en.yml
@@ -0,0 +1,17 @@
+question: Simplicity's effects are commutative and idempotent but not unitary. Which optimizer transformation must therefore be refused in general?
+answer: Replacing a seemingly-dead expression with unit — Failure isn't unitary, so it could hide a failing check that must abort.
+wrong_answers:
+ - Swapping two independent subexpressions, since a sig-all-hash could observe a different environment state.
+ - Merging two identical verify calls, since a duplicated Failure would throw twice and abort wrongly.
+ - Reordering expressions that may throw, since the propagated exception depends on which side runs first.
+explanation: >-
+ Because Simplicity's effects are guaranteed commutative and idempotent,
+ swapping independent subexpressions and duplicating or merging identical
+ ones are always safe; the Reader environment is fixed, and Failure's
+ unit-typed exception is identical no matter which side throws first or
+ how many times. The discard transformation `f ⨾ unit = unit`, however,
+ requires unitarity, which Failure lacks: if `f` contains a
+ `bip0340-verify` on an invalid signature, eliminating the 'dead' code
+ would optimize away the abort and validate a transaction that should
+ fail.
+reviewed: false
diff --git a/courses/scr403/quizz/039/question.yml b/courses/scr403/quizz/039/question.yml
new file mode 100644
index 00000000000..2405c9b5f45
--- /dev/null
+++ b/courses/scr403/quizz/039/question.yml
@@ -0,0 +1,14 @@
+id: beb048dc-bcc3-43ed-804d-1cbda2a7d9b7
+chapterId: 9eafe498-0765-419a-a69d-a74a9cdf3713
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/040/en.yml b/courses/scr403/quizz/040/en.yml
new file mode 100644
index 00000000000..e760956bce5
--- /dev/null
+++ b/courses/scr403/quizz/040/en.yml
@@ -0,0 +1,16 @@
+question: "Computing #ᶜ(comp f g) hashes 128 bytes: the comp tag twice, then both child CMRs. Why is that still at most one SHA-256 compression call?"
+answer: The first 64-byte block is the constant tag∥tag, whose midstate is precomputed once; only the block holding the child CMRs is compressed.
+wrong_answers:
+ - Dropping SHA-256's final length-padding block alone lets the whole 128 bytes fit in one call.
+ - The two child CMRs are XORed into one 32-byte digest, shrinking the input to a single block.
+ - SHA-256-midstate is a wide-block variant that absorbs 128-byte message blocks in one pass.
+explanation: >-
+ SHA-256's compression function processes fixed 64-byte blocks, so a
+ 128-byte input normally needs two calls (plus one more for the length
+ padding in full SHA-256). Because every combinator's first block is the
+ constant tag∥tag, its midstate can be precomputed once and cached; each
+ expression then only needs one fresh compression of the block holding
+ its children's CMRs. Midstates also drop the final padding block, but
+ that alone would still leave two compressions — the precomputed tag
+ midstate is what brings it down to at most one.
+reviewed: false
diff --git a/courses/scr403/quizz/040/question.yml b/courses/scr403/quizz/040/question.yml
new file mode 100644
index 00000000000..a073aa822a5
--- /dev/null
+++ b/courses/scr403/quizz/040/question.yml
@@ -0,0 +1,14 @@
+id: 1371db28-5256-4d6f-adb0-2e275ea7feba
+chapterId: 961652e3-8f7d-4c2a-8b55-9a990b91a0dd
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/041/en.yml b/courses/scr403/quizz/041/en.yml
new file mode 100644
index 00000000000..d2b972a8804
--- /dev/null
+++ b/courses/scr403/quizz/041/en.yml
@@ -0,0 +1,17 @@
+question: A Simplicity output uses the fixed BIP-0341 NUMS point as its internal key. Why is key-spend provably impossible, and what does randomizing the NUMS point add?
+answer: Nobody knows the NUMS point's discrete log, so no key-path signature can exist; randomizing only adds privacy.
+wrong_answers:
+ - The NUMS point lies off the curve so key-path signatures fail; randomizing brings it back on-curve.
+ - The NUMS point's private key is zero, which consensus rejects; randomizing guards the tweak against side channels.
+ - Tweaking a NUMS point yields an out-of-range key, making key-spend non-standard; randomizing avoids address reuse.
+explanation: >-
+ A NUMS ('Nothing-Up-My-Sleeve') point is a perfectly valid curve point
+ constructed so that no one knows a corresponding private key — its
+ discrete logarithm is unknown. Since a key-path spend requires a Schnorr
+ signature under the internal key, and no such signature can be produced
+ without the private key, the key-spend path is provably unusable and
+ funds can only move through the committed script path. Randomizing the
+ NUMS point changes none of this; it merely hides the fact that key-spend
+ is disabled, so the output looks like any other Taproot output — a
+ privacy benefit.
+reviewed: false
diff --git a/courses/scr403/quizz/041/question.yml b/courses/scr403/quizz/041/question.yml
new file mode 100644
index 00000000000..d4d6df48080
--- /dev/null
+++ b/courses/scr403/quizz/041/question.yml
@@ -0,0 +1,14 @@
+id: d2d4b610-c2b4-4e1c-9409-d8adba929785
+chapterId: 961652e3-8f7d-4c2a-8b55-9a990b91a0dd
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/courses/scr403/quizz/042/en.yml b/courses/scr403/quizz/042/en.yml
new file mode 100644
index 00000000000..b7ecf1b2b2f
--- /dev/null
+++ b/courses/scr403/quizz/042/en.yml
@@ -0,0 +1,16 @@
+question: At spending time a case branch is pruned away. How can the verifier still match the revealed program to the committed CMR?
+answer: The CMR is a Merkle root, so the spender supplies just the pruned branch's CMR and the verifier folds it in to recompute the root.
+wrong_answers:
+ - The verifier uses only the executed branch, since unexecuted case branches were never in the CMR.
+ - Pruned branches become a canonical placeholder whose fixed CMR stands in when recomputing the root.
+ - The pruned branch's full code stays in the witness, where the verifier hashes but does not execute it.
+explanation: >-
+ The CMR of case f g is a tagged hash over both children's CMRs, so every
+ branch — executed or not — is committed at address time. Because the
+ construction is a Merkle tree, a pruned branch can be summarized by its
+ 32-byte CMR alone: the verifier plugs that hash into the recursive
+ computation and checks that the root matches the UTXO's commitment,
+ without ever seeing the pruned code. This is exactly why a Merkle root
+ is used for the commitment, and why any witness expressions inside the
+ pruned branch never appear on-chain.
+reviewed: false
diff --git a/courses/scr403/quizz/042/question.yml b/courses/scr403/quizz/042/question.yml
new file mode 100644
index 00000000000..b72d0b72d18
--- /dev/null
+++ b/courses/scr403/quizz/042/question.yml
@@ -0,0 +1,14 @@
+id: ebd70d78-8294-4e17-b9bd-c08ed7c62b30
+chapterId: 961652e3-8f7d-4c2a-8b55-9a990b91a0dd
+difficulty: hard
+duration: 45
+author: 2e1b5182-567e-453a-af29-36009340ff02
+original_language: en
+
+proofreading:
+ - language: en
+ last_contribution_date: 2026-03-02
+ urgency: 1
+ contributor_names:
+ - rogzy
+ reward: 0
diff --git a/docs/PBN-template-repo/professors/professor-scheme.json b/docs/PBN-template-repo/professors/professor-scheme.json
index 08f4dc5526d..32c9ec60b28 100644
--- a/docs/PBN-template-repo/professors/professor-scheme.json
+++ b/docs/PBN-template-repo/professors/professor-scheme.json
@@ -3,6 +3,11 @@
"title": "Professor",
"type": "object",
"properties": {
+ "id": {
+ "type": "string",
+ "description": "Unique identifier for the professor (UUID format)",
+ "pattern": "^[0-9a-f]{8}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{12}$"
+ },
"name": {
"type": "string",
"description": "Full name of the professor"
@@ -16,13 +21,18 @@
"description": "Online presence of the professor",
"properties": {
"twitter": {
- "type": "string",
- "format": "url",
+ "type": ["string", "null"],
+ "format": "uri",
"description": "Twitter URL of the professor"
},
+ "github": {
+ "type": "string",
+ "format": "uri",
+ "description": "GitHub URL of the professor"
+ },
"website": {
"type": "string",
- "format": "url",
+ "format": "uri",
"description": "Personal or professional website of the professor"
}
},
@@ -103,7 +113,7 @@
}
}
},
- "required": ["name", "contributor_id", "links", "tags", "tips", "company", "affiliations"],
+ "required": ["id", "name", "contributor_id", "links", "tags", "company"],
"additionalProperties": false
}
diff --git a/professors/russell-oconnor/assets/profile.webp b/professors/russell-oconnor/assets/profile.webp
new file mode 100644
index 00000000000..80773f4c8a8
Binary files /dev/null and b/professors/russell-oconnor/assets/profile.webp differ
diff --git a/professors/russell-oconnor/en.yml b/professors/russell-oconnor/en.yml
new file mode 100644
index 00000000000..5bcbe05b3e2
--- /dev/null
+++ b/professors/russell-oconnor/en.yml
@@ -0,0 +1,4 @@
+bio: |
+ Dr. Russell O'Connor is an Infrastructure Tech Developer at Blockstream and the creator of Simplicity, a next-generation smart contract language for Bitcoin. He holds a Ph.D. in Science from Radboud University Nijmegen and a bachelor's degree in Pure Mathematics and Computer Science from the University of Waterloo. His work at Blockstream Research has contributed to landmark Bitcoin innovations including Taproot. Simplicity, which he designed from scratch starting in 2017, was activated on the Liquid Network in July 2025 after years of formal verification and development.
+
+short_bio: Creator of Simplicity at Blockstream Research
diff --git a/professors/russell-oconnor/professor.yml b/professors/russell-oconnor/professor.yml
new file mode 100644
index 00000000000..495ad38131e
--- /dev/null
+++ b/professors/russell-oconnor/professor.yml
@@ -0,0 +1,15 @@
+id: a3b29adb-43ee-49f4-9582-b37e9cf72858
+name: "Russell O'Connor"
+contributor_id: rocket-turtle
+
+links:
+ website: http://r6.ca/
+ github: https://github.com/oconnorr
+
+company: Blockstream
+
+tags:
+ - simplicity
+ - development
+ - protocol
+ - research