The kernel

MODEL.md says what a Beloch program talks about. This document says how the kernel in packages/core holds that in memory and which of the model's statements each part realizes. It refers to the model by the ids of its statements; the model does not refer back. When the two disagree, the model wins and the kernel has a bug, or the model has a gap and gets a new statement.

Entries name OCaml modules and functions as they exist today and are updated with the code. Anything the kernel cannot represent is stated as a ceiling with the issue that tracks it.

Sheet

The language offers one sheet, paper square, the unit square with the four corners bound as .a to .d. The model's sheet (def-sheet) allows any simple polygon. Faces are convex polygons in counter-clockwise order because Geom clips against half-planes and tests overlap on convex polygons only; a non-convex sheet would enter as several convex faces joined by hinges of angle $0$.

State

Fold_state.t is abstract and Fold_state.make is its only constructor, so every operation builds a candidate and passes it through make: no value of type Fold_state.t exists that is not a legal state. make returns Error violation for anything outside the definition of the state and its non-crossing conditions (def-noncrossing); the violation constructors and the conditions they check are listed under Violations.

type t

Realizes: Definition 2.1

val make :
  ?base:Isometry3.t ->
  ?marks:mark array ->
  faces:face array ->
  hinges:hinge array ->
  root:int ->
  rank:int array ->
  unit ->
  (t, violation) result

The only constructor. rank.(i) is face i's stacking height (higher = above), a permutation of 0..n-1. base is the root face's placement — ONE whole-sheet rigid motion (default identity); needed because after a pleat (fold, then fold moving the previously-stationary side) no face keeps an identity placement, and flip moves everything. No per-face freedom, so tears stay unrepresentable, and the closure/non-crossing checks are unaffected (a rigid motion of everything). marks is a paper-space, fold-invariant array of reference/pinch records (default empty). The trailing unit anchors the two leading optional arguments — OCaml cannot erase omitted optionals followed only by labelled arguments. Checks in order: structure (indices, rank, angle domain, line non-degeneracy), connectivity, hinge adjacency (half-plane + shared edge), cycle closure, then the non-crossing conditions (taco-tortilla, taco-taco) over the flat projection. Input arrays are copied.

Realizes: Definition 2.1, Definition 3.6

Faces are convex polygons in paper coordinates, one exact 2D isometry each (Isometry.t), the restriction of $f$ to that face. A hinge names the two faces it joins, its line and its angle in $\{0, \pm 1\}$ units of $\pi$:

type hinge = {
  fa : int;
  fb : int;
  line : Geom.line;
  angle : Num.t;
  crease_id : int;
  prov : State.provenance option;
}

Crease between adjacent faces fa and fb. angle = dihedral/π. The sign does not affect a flat placement (±π half-turns coincide); M/V is derived from the rank, never stored.

crease_id : int

internal identity; unique within a state, never serialized

Refinement equivalence (def-refinement) is not quotiented in the representation: mark adds faces and hinges of angle $0$, and two states equal up to refinement are two different values. Comparisons across programs are made pointwise on the folded geometry, as in the test that checks the two preliminary-base routes against each other.

Rank

The kernel does not store $\lambda$. Fold_state.rank is a total order of all faces, and Fold_state.rel reads above/below for a pair off the rank only when the two table polygons overlap in positive area; otherwise the pair is Apart. The rank is therefore a linear extension of $\lambda$ in the sense of the model's remark on linear extensions (rem-linear-extension), and two ranks with the same restriction to overlapping pairs represent the same state.

Ceiling: a linear extension exists only for acyclic layerings, so states with cyclic layering, the square twist among them, cannot be represented. Tracked as issue #83. Nothing on the crane path needs such a state.

History

The model's state does not remember how it was reached. The kernel keeps the history for output: the FOLD file carries one frame per statement in file_frames, and per edge the statement that scored it in beloch:edges and beloch:source_line (SPECIFICATION.md §7). No operation reads this record.

Violations

One constructor per check Fold_state.make runs, each carrying the model statement it enforces. Bad_index and Bad_line reject a malformed representation and answer to no statement of the model.

type violation =
  | Bad_index of string
  | Bad_rank
  | Bad_angle of int
  | Bad_line of int
  | Disconnected of int
  | Hinge_not_shared of int
  | Hinge_not_closed of int
  | Taco_tortilla of { tortilla : int; hinge : int }
  | Taco_taco of int * int

| Bad_index of string

root or a hinge's face index out of range, or fa = fb. A check on the representation; the model has no statement behind it.

| Bad_rank

rank is not a permutation of 0..n-1

Realizes: Remark 2.8

| Bad_angle of int

hinge i: angle outside {0, ±1} (flat-first)

Realizes: Definition 2.1

| Bad_line of int

hinge i: line is degenerate (a = b = 0). A check on the representation; the model has no statement behind it.

| Disconnected of int

face i unreachable from the root via hinges

Realizes: Condition 3.5

| Hinge_not_shared of int

hinge i: its line is not a positive-length shared boundary edge between faces lying in opposite half-planes

Realizes: Condition 3.4

| Hinge_not_closed of int

hinge i (a cycle edge): the derived placements contradict its motion — folding would tear the sheet

Realizes: Condition 3.4

| Taco_tortilla of { tortilla : int; hinge : int }

face tortilla is stacked inside folded hinge hinge's taco but crosses its crease hullzakharevich2023 §2.1

Realizes: Condition 3.2

| Taco_taco of int * int

hinges i and j: creases coincide on the table and their face pairs interleave in the stack hullzakharevich2023 §2.1

Realizes: Condition 3.3