move @iajhff comments over (from BlockstreamResearch/SimplicityHL@0ecec39)

imaginator · imaginator · commit 09ef349f52c5 · 2025-09-08T17:39:49.000Z
diff --git a/docs/simplicityhl-reference/context.md b/docs/simplicityhl-reference/context.md
@@ -0,0 +1,137 @@
+# Context
+
+A context Γ maps variable names to Simplicity types:
+
+Γ = [ `foo` ↦ 𝟙, `bar` ↦ 𝟚^32?, `baz` ↦ 𝟚^32 × 𝟙 ]
+
+We write Γ(`v`) = A to denote that variable `v` has type A in context Γ.
+
+We handle free variables inside SimplicityHL expressions via contexts.
+
+If all free variables are defined in a context, then the context assigns a type to the expression.
+
+We write Γ ⊩ `a`: A to denote that expression `a` has type A in context Γ.
+
+Note that contexts handle only the **target type** of an expression!
+
+Source types are handled by environments and the translation of SimplicityHL to Simplicity.
+
+We write Γ ⊎ Δ to denote the **disjoint union** of Γ and Δ.
+
+We write Γ // Δ to denote the **update** of Γ with Δ. The update contains mappings from both contexts. If a variable is present in both, then the mapping from Δ is taken.
+
+## Unit literal
+
+Γ ⊩ `()`: 𝟙
+
+## Product constructor
+
+If Γ ⊩ `b`: B
+
+If Γ ⊩ `c`: C
+
+Then Γ ⊩ `(b, c)`: B × C
+
+## Left constructor
+
+If Γ ⊩ `b`: B
+
+Then Γ ⊩ `Left(b)`: B + C
+
+For any C
+
+## Right constructor
+
+If Γ ⊩ `c`: c
+
+Then Γ ⊩ `Right(c)`: B + C
+
+For any B
+
+## Bit string literal
+
+If `s` is a bit string of 2^n bits
+
+Then Γ ⊩ `0bs`: 𝟚^(2^n)
+
+## Byte string literal
+
+If `s` is a hex string of 2^n digits
+
+Then Γ ⊩ `0xs`: 𝟚^(4 * 2^n)
+
+## Variable
+
+If Γ(`v`) = B
+
+Then Γ ⊩ `v`: B
+
+## Witness value
+
+Γ ⊩ `witness(name)`: B
+
+For any B
+
+## Jet
+
+If `j` is the name of a jet of type B → C
+
+If Γ ⊩ `b`: B
+
+Then Γ ⊩ `jet::j b`: C
+
+## Chaining
+
+If Γ ⊩ `b`: 𝟙
+
+If Γ ⊩ `c`: C
+
+Then Γ ⊩ `b; c`: C
+
+## Patterns
+
+Type A and pattern `p` create a context denoted by PCtx(A, `p`)
+
+PCtx(A, `v`) := [`v` ↦ A]
+
+PCtx(A, `_`) := []
+
+If `p1` and `p2` map disjoint sets of variables
+
+Then PCtx(A × B, `(p1, p2)`) := PCtx(A, `p1`) ⊎ PCtx(B, `p2`)
+
+## Let statement
+
+If Γ ⊩ `b`: B
+
+If Γ // PCtx(B, `p`) ⊩ `c`: C
+
+Then Γ ⊩ `let p: B = b; c`: C
+
+With alternative syntax
+
+Then Γ ⊩ `let p = b; c`: C
+
+## Match statement
+
+If Γ ⊩ `a`: B + C
+
+If Γ // [`x` ↦ B] ⊩ `b`: D
+
+If Γ // [`y` ↦ C] ⊩ `c`: D
+
+Then Γ ⊩ `match a { Left(x) => b, Right(y) => c, }`: D
+
+_(We do not enforce that `x` is used inside `b` or `y` inside `c`. Writing stupid programs is allowed, although there will be a compiler warning at some point.)_
+
+## Left unwrap
+
+If Γ ⊩ `b`: B + C
+
+Then Γ ⊩ `b.unwrap_left()`: B
+
+## Right unwrap
+
+If Γ ⊩ `c`: B + C
+
+Then Γ ⊩ `c.unwrap_right()`: C
diff --git a/docs/simplicityhl-reference/environment.md b/docs/simplicityhl-reference/environment.md
@@ -0,0 +1,82 @@
+# Environment
+
+An environment Ξ maps variable names to Simplicity expressions.
+
+All expressions inside an environment share the same source type A. We say the environment is "from type A".
+
+```
+Ξ =
+[ foo ↦ unit:      (𝟚^32? × 2^32) → 𝟙
+, bar ↦ take iden: (𝟚^32? × 𝟚^32) → 𝟚^32?
+, baz ↦ drop iden: (𝟚^32? × 𝟚^32) → 𝟚^32
+]
+```
+
+We use environments to translate variables inside SimplicityHL expressions to Simplicity.
+
+The environment tells us the Simplicity expression that returns the value of each variable.
+
+We translate a SimplicityHL program "top to bottom". Each time a variable is defined, we update the environment to reflect this change.
+
+During the translation, we can ignore the source type of Simplicity expressions (translated SimplicityHL expressions) entirely. We can focus on producing a Simplicity value of the expected target type. Environments ensure that we get input values for each variable that is in scope.
+
+Target types are handled by contexts.
+
+We obtain context Ctx(Ξ) from environment Ξ by mapping each variable `x` from Ξ to the target type of Ξ(`x`):
+
+Ctx(Ξ)(`x`) = B if Ξ(`x`) = a: A → B
+
+## Patterns
+
+
+Patterns occur in let statements `let p := s`.
+
+Pattern `p` binds the output of SimplicityHL expression `s` to variables.
+
+As we translate `s` to Simplicity, we need an environment that maps the variables from `p` to Simplicity expressions.
+
+If `p` is just a variable `p = a`, then the environment is simply [`a` ↦ iden: A → A].
+
+If `p` is a product of two variables `p = (a, b)`, then the environment is [`a` ↦ take iden: A × B → A, `b` ↦ drop iden: A × B → B].
+
+"take" and "drop" are added as we go deeper in the product hierarchy. The pattern `_` is ignored.
+
+PEnv'(t: A → B, `v`) := [`v` ↦ t]
+
+PEnv'(t: A → B, `_`) := []
+
+If `p1` and `p2` contain disjoint sets of variables
+
+Then PEnv'(t: A → B × C, `(p1, p2)`) := PEnv'(take t: A → B, p1) ⊎ PEnv'(drop t: A → C, p2)
+
+PEnv(A, `p`) := PEnv'(iden: A → A, `p`)
+
+Pattern environments are compatible with pattern contexts:
+
+Ctx(PEnv(A, `p`)) = PCtx(A, `p`)
+
+## Product
+
+We write Product(ΞA, ΞB) to denote the **product** of environment ΞA from A and environment ΞB from B.
+
+The product is an environment from type A × B.
+
+When two Simplicity expressions with environments are joined using the "pair" combinator, then the product of both environments gives us updated bindings for all variables.
+
+If the same variable is bound in both environments, then the binding from the first environment is taken.
+
+If ΞA maps `v` to Simplicity expression a: A → C
+
+Then Product(ΞA, ΞB) maps `v` to take a: A × B → C
+
+If ΞB maps `v` to Simplicity expression b: B → C
+
+If ΞA doesn't map `v`
+
+Then Product(ΞA, ΞB) maps `v` to drop b: A × B → C
+
+Environment products are compatible with context updates:
+
+Ctx(Product(ΞA, ΞB)) = Ctx(ΞB) // Ctx(ΞA)
+
+The order of B and A is reversed: The context of ΞB is updated with the dominant context of ΞA.
diff --git a/docs/simplicityhl-reference/function.md b/docs/simplicityhl-reference/function.md
@@ -22,7 +22,7 @@ The function then checks if the carry is true, signaling an overflow, in which c
 On the last line, the value of `sum` is returned.
 
 The above function is called by writing its name `add` followed by a list of arguments `(40, 2)`.
-Each parameter needs an argument, so the list of arguments is as long as the list of arguments.
+Each parameter needs an argument, so the list of arguments is as long as the list of parameters.
 Here, `x` is assigned the value `40` and `y` is assigned the value `2`.
 
 ```rust
@@ -54,7 +54,7 @@ fn level_1() -> u32 {
 }
 
 fn level_2() -> u32 {
-    let (_, next) = jet::increment_32(level_1));
+    let (_, next) = jet::increment_32(level_1());
     next
 }
 ```
@@ -91,7 +91,7 @@ There is no support for "libraries".
 
 ## Jets
 
-Jets are predefined and optimized functions for common usecases.
+Jets are predefined and optimized functions for common use cases.
 
 ```rust
 jet::add_32(40, 2)
diff --git a/docs/simplicityhl-reference/let_statement.md b/docs/simplicityhl-reference/let_statement.md
@@ -48,7 +48,7 @@ let z: u32 = {
     assert!(jet::eq_32(y, 2)); // y == 2
     x
 };
-assert!(jet::eq_32(x, 3)); // z == 3
+assert!(jet::eq_32(z, 3)); // z == 3
 ```
 
 ## Pattern matching
diff --git a/docs/simplicityhl-reference/translation.md b/docs/simplicityhl-reference/translation.md
@@ -0,0 +1,105 @@
+# Translation
+
+We write ⟦`e`⟧Ξ to denote the translation of SimplicityHL expression `e` using environment Ξ from A.
+
+The translation produces a Simplicity expression with source type A.
+
+The target type depends on the SimplicityHL expression `e`.
+
+## Unit literal
+
+⟦`()`⟧Ξ = unit: A → 𝟙
+
+## Product constructor
+
+If Ctx(Ξ) ⊩ `b`: B
+
+If Ctx(Ξ) ⊩ `c`: C
+
+Then ⟦`(b, c)`⟧Ξ = pair ⟦`b`⟧Ξ ⟦`c`⟧Ξ: A → B × C
+
+## Left constructor
+
+If Ctx(Ξ) ⊩ `b`: B
+
+Then ⟦`Left(b)`⟧Ξ = injl ⟦`b`⟧Ξ: A → B + C
+
+For any C
+
+## Right constructor
+
+If Ctx(Ξ) ⊩ `c`: C
+
+Then ⟦`Right(c)`⟧Ξ = injr ⟦`c`⟧Ξ: A → B + C
+
+For any B
+
+## Bit string literal
+
+If `s` is a bit string of 2^n bits
+
+Then ⟦`0bs`⟧Ξ = comp unit const 0bs: A → 𝟚^(2^n)
+
+## Byte string literal
+
+If `s` is a hex string of 2^n digits
+
+Then ⟦`0xs`⟧Ξ = comp unit const 0xs: A → 𝟚^(4 * 2^n)
+
+## Variable
+
+If Ctx(Ξ)(`v`) = B
+
+Then ⟦`v`⟧Ξ = Ξ(`v`): A → B
+
+## Witness value
+
+Ctx(Ξ) ⊩ `witness(name)`: B
+
+Then ⟦`witness(name)`⟧Ξ = witness: A → B
+
+## Jet
+
+If `j` is the name of a jet of type B → C
+
+If Ctx(Ξ) ⊩ `b`: B
+
+Then ⟦`jet::j b`⟧Ξ = comp ⟦`b`⟧Ξ j: A → C
+
+## Chaining
+
+If Ctx(Ξ) ⊩ `b`: 𝟙
+
+If Ctx(Ξ) ⊩ `c`: C
+
+Then ⟦`b; c`⟧Ξ = comp (pair ⟦`b`⟧Ξ ⟦`c`⟧Ξ) (drop iden): A → C
+
+## Let statement
+
+If Ctx(Ξ) ⊩ `b`: B
+
+If Product(PEnv(B, `p`), Ξ) ⊩ `c`: C
+
+Then ⟦`let p: B = b; c`⟧Ξ = comp (pair ⟦`b`⟧Ξ iden) ⟦`c`⟧Product(PEnv(B, `p`), Ξ): A → C
+
+## Match statement
+
+If Ctx(Ξ) ⊩ `a`: B + C
+
+If Product(PEnv(B, `x`), Ξ) ⊩ `b`: D
+
+If Product(PEnv(C, `y`), Ξ) ⊩ `c`: D
+
+Then ⟦`match a { Left(x) => b, Right(y) => c, }`⟧Ξ = comp (pair ⟦`a`⟧Ξ iden) (case ⟦`b`⟧Product(PEnv(B, `x`), Ξ) ⟦`c`⟧Product(PEnv(C, `y`), Ξ)): A → D
+
+## Left unwrap
+
+If Ctx(Ξ) ⊩ `b`: B + C
+
+Then ⟦`b.unwrap_left()`⟧Ξ = comp (pair ⟦`b`⟧Ξ unit) (assertl iden #{fail 0}): A → B
+
+## Right unwrap
+
+If Ctx(Ξ) ⊩ `c`: B + C
+
+Then ⟦`c.unwrap_right()`⟧Ξ = comp (pair ⟦`c`⟧Ξ unit) (assertr #{fail 0} iden): A → C
diff --git a/docs/simplicityhl-reference/type.md b/docs/simplicityhl-reference/type.md
@@ -100,11 +100,11 @@ Arrays are always of finite length.
 | `List<A, 256>`            | <256-list           | `list![]`, …, `list![a1, …, a255]`                   |
 | `List<A, 512>`            | <512-list           | `list![]`, …, `list![a1, …, a511]`                   |
 | …                         | …                   | …                                                    |
-| `List<A,`2<sup>N</sup>`>` | <2<sup>N</sup>-list | `list![]`, …, `list![a1, …, a`(2<sup>N</sup> - 1)`]` |
+| `List<A, 2^N>`           | <2^N-list           | `list![]`, …, `list![a1, …, a_{2^N - 1}]`          |
 
 Lists hold a variable number of elements of the same type.
 This is similar to [Rust vectors](https://doc.rust-lang.org/std/vec/struct.Vec.html), but SimplicityHL doesn't have a heap.
-In SimplicityHL, lists exists on the stack, which is why the maximum list length is bounded.
+In SimplicityHL, lists exist on the stack, which is why the maximum list length is bounded.
 
 <2-lists hold fewer than 2 elements, so zero or one element.
 <4-lists hold fewer than 4 elements, so zero to three elements.
@@ -156,7 +156,7 @@ Sum types represent values that are of some "left" type in some cases and that a
 [They work just like in the either crate](https://docs.rs/either/latest/either/enum.Either.html).
 [The Result type from Rust is very similar, too](https://doc.rust-lang.org/std/result/index.html).
 
-A sum type type is generic over two types, `A` and `B`.
+A sum type is generic over two types, `A` and `B`.
 The value `Left(a)` contains an inner value `a` of type `A`.
 The value `Right(b)` contains an inner value `b` of type `B`.
 
diff --git a/docs/simplicityhl-reference/type_casting.md b/docs/simplicityhl-reference/type_casting.md
diff --git a/mkdocs.yml b/mkdocs.yml

Original file line number	Diff line number	Diff line change
`@@ -48,7 +48,7 @@ let z: u32 = {`
`48`	`48`	`assert!(jet::eq_32(y, 2)); // y == 2`
`49`	`49`	`x`
`50`	`50`	`};`
`51`		`-assert!(jet::eq_32(x, 3)); // z == 3`
	`51`	`+assert!(jet::eq_32(z, 3)); // z == 3`
`52`	`52`	```
`53`	`53`
`54`	`54`	`## Pattern matching`