arena-handle

The densest single file here for language features: class records, a discretio sum type with variant payloads, match matching over it, and a test suite in the same file. Stale handles are rejected by a generation check rather than by a runtime guard.

Source: examples/arena-handle

`src/main.fab`#

230 lines — the whole file, unabridged.

reader locale

faber format --locale en — English reader surface

# =============================================================================
# arena-handle — generational arena-handle contract via pure value updates
# =============================================================================
#
# What this example teaches:
#   • Generational arena pattern — stable identity via (index, generation) handle
#     pair; stale handles rejected on lookup via generation check
#   • genus (struct) definitions — Manus, Loculus, Area, AreaCumManus, Nodus
#   • Pure functional updates — no lista[i] mutation, all operations return new
#     Area values to keep generated Rust sound
#   • dum loop — explicit iteration over list indices (lines 42-46, 75-90)
#   • si/sin/secus — conditional logic (lines 58, 60, 62, 78-89)
#   • discerne/casu — pattern matching on enum variants (lines 117-133)
#   • probandum/proba/adfirma — test framework with multi-case assertions
#   • discretio — sum type (enum) with variant payloads (lines 93-96)
#   • gingimus (finge) — enum variant construction with named fields (lines 113-116)
#
# Syntaxes used:
#   • genus — struct definition (lines 8, 12, 18, 22)
#   • discretio — enum/sum type (line 93)
#   • functio — function definition (lines 28, 32, 36, 57, 70, 73)
#   • fixum — immutable binding (lines 33, 43, etc.)
#   • varia — mutable binding (lines 40, 41, etc.)
#   • dum — while loop (lines 42, 75)
#   • si/sin/secus — conditionals (lines 58, 60, 62, 78-89)
#   • discerne/casu — match/pattern match (lines 117-133)
#   • redde — return (lines 30, etc.)
#   • finge — construct enum variant (lines 113-116)
#   • adfirma — test assertion (lines 109-112, etc.)
#   • proba — test case (lines 101, 134, 155)
#   • probandum — test suite (line 100)
#   • ≡ — equality comparison (lines 29, 61, etc.)
#   • lista<T> — list type (lines 20, 93, 96)
#   • textus, numerus, bivalens — primitive types
#   • vacua — empty list literal
#   • .longitudo() — list length method
#   • .appende() — list append method
#
# Alternate approaches (not shown):
#   • Mutable arena with unsafe interior for performance — a mutable lista<Loculus> with in-place updates avoids copying on every insert/take
#   • Reusing free slots (via free list) instead of always appending — maintain a list of freed indices to recycle slots without growing the arena
#
# Anti-patterns (avoid these):
#   • Using lista[i] assignment in generated Rust contexts — in-place list mutation breaks Rust's borrow-checker soundness; use pure value updates (return new Area) instead
#   • Assuming stale handle reuse after removal without generation check — always verify generatio matches before using a handle; stale handles must be rejected on lookup
#
# Learning path:
#   Before: Stage 3: genus, lista, nihil → Stage 3: discerne/casu (structs, collections, and pattern matching)
#   After:  Stage 6: advanced applications (vivilite — real-world resource management)
#
# Stage: arena-handle, complete contract with tests, all language constructs demonstrated
# Backend: Rust, stepper
# =============================================================================

# Reusable generational arena-handle contract (language surface).
#
# Semantics mirror faber-runtime::Arena / ArenaHandle (see arena.rs):
# stable identity independent of list order; stale handles reject on lookup.
# This package uses pure value updates (no lista[i] assignment) so generated
# Rust stays sound; the runtime crate is the authoritative store implementation.

class Manus {
    int index
    int generatio
}

class Loculus {
    int generatio
    bool vivus
    string valor
}

class Area {
    list<Loculus> loculi
}

class AreaCumManus {
    Area area
    Manus manus
}

fn manus_aequat(ref Manus a, ref Manus b) → bool {
    return a.index ≡ b.index and a.generatio ≡ b.generatio
}

fn area_nova() → Area {
    const list<Loculus> loculi ← vacua
    return Area {loculi = loculi}
}

fn area_inserit(Area area, string valor) → AreaCumManus {
    # Always append a new live slot. Free slots from tollit stay dead so the
    # old handle generation remains invalid; reuse is optional for this proof.
    var list<Loculus> out ← vacua
    var int i ← 0
    while i ≺ area.loculi.longitudo() {
        out.appende(area.loculi[i])
        i ← i + 1
    }
    const int index ← out.longitudo()
    out.appende(Loculus {generatio = 0, vivus = true, valor = valor})
    return AreaCumManus {area = Area {loculi = out}, manus = Manus {index = index, generatio = 0}}
}

# Lookup returns the payload, or "" when the handle is stale / out of range.
# Proof resources never use empty text, so "" is the explicit reject signal.
fn area_accipe(ref Area area, ref Manus manus) → string {
    if manus.index ≥ area.loculi.longitudo() then return ""
    const Loculus slot ← area.loculi[manus.index]
    if slot.vivus ≡ false then return ""
    if slot.generatio ≠ manus.generatio then return ""
    return slot.valor
}

fn area_continet(ref Area area, ref Manus manus) → bool {
    return area_accipe(area, manus) ≠ ""
}

fn area_tollit(Area area, ref Manus manus) → Area {
    var list<Loculus> out ← vacua
    var int i ← 0
    while i ≺ area.loculi.longitudo() {
        const Loculus slot ← area.loculi[i]
        if (i ≡ manus.index and slot.vivus ≡ true) and slot.generatio ≡ manus.generatio {
            out.appende(Loculus {generatio = slot.generatio + 1, vivus = false, valor = ""})
        }
        else {
            out.appende(slot)
        }
        i ← i + 1
    }
    return Area {loculi = out}
}

# Heterogeneous node: stores Manus, never deep-copies the resource payload.
union Nodus {
    Groupus {
        list<Manus> filii
    },
    Tessera {
        Manus geometria
    },
}

test "two nodes share one resource identity" tag "identity" {
    const AreaCumManus step ← area_inserit(area_nova(), "shared-mesh")
    const Area res ← step.area
    const Manus geo ← step.manus
    # Reconstruct handle values so each node owns a copy of the identity bits
    # without cloning the resource payload (still one live slot in `res`).
    const Manus left_geo ← Manus {index = geo.index, generatio = geo.generatio}
    const Manus right_geo ← Manus {index = geo.index, generatio = geo.generatio}
    assert manus_aequat(left_geo, right_geo)
    assert area_accipe(res, left_geo) ≡ "shared-mesh"
    assert area_accipe(res, right_geo) ≡ "shared-mesh"
    const Nodus left ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    const Nodus right ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    match left {
        case Tessera const geometria {
            assert manus_aequat(geometria, left_geo)
        }
        case Groupus const filii {
            assert filii.longitudo() ≡ 0
        }
    }
    match right {
        case Tessera const geometria {
            assert manus_aequat(geometria, right_geo)
        }
        case Groupus const filii {
            assert filii.longitudo() ≡ 0
        }
    }
}

test "reparent reorder preserves handle identity" tag "identity" {
    const AreaCumManus s0 ← area_inserit(area_nova(), "child-a")
    const AreaCumManus s1 ← area_inserit(s0.area, "child-b")
    const Area nodi ← s1.area
    const Manus a ← s0.manus
    const Manus b ← s1.manus
    var list<Manus> filii ← vacua
    filii.appende(Manus {index = a.index, generatio = a.generatio})
    filii.appende(Manus {index = b.index, generatio = b.generatio})
    # swap order without changing handle identities
    const Manus first ← filii[0]
    const Manus second ← filii[1]
    var list<Manus> reord ← vacua
    reord.appende(Manus {index = second.index, generatio = second.generatio})
    reord.appende(Manus {index = first.index, generatio = first.generatio})
    assert area_accipe(nodi, reord[0]) ≡ "child-b"
    assert area_accipe(nodi, reord[1]) ≡ "child-a"
    assert area_accipe(nodi, a) ≡ "child-a"
    assert area_accipe(nodi, b) ≡ "child-b"
}

test "stale handle rejects after remove" tag "identity" {
    const AreaCumManus s0 ← area_inserit(area_nova(), "gone")
    const Manus h ← s0.manus
    const Manus h_bits ← Manus {index = h.index, generatio = h.generatio}
    assert area_continet(s0.area, h_bits)
    const Area after ← area_tollit(s0.area, h_bits)
    assert area_continet(after, h_bits) ≡ false
    assert area_accipe(after, h_bits) ≡ ""
    const AreaCumManus s1 ← area_inserit(after, "fresh")
    const Manus h2 ← s1.manus
    # New live slot (append); old handle still rejected by generation/vivus.
    assert manus_aequat(h_bits, h2) ≡ false
    assert area_accipe(s1.area, h_bits) ≡ ""
    assert area_accipe(s1.area, h2) ≡ "fresh"
    assert area_continet(s1.area, h2)
}

main {
}

faber format --locale la — canonical Faber

# =============================================================================
# arena-handle — generational arena-handle contract via pure value updates
# =============================================================================
#
# What this example teaches:
#   • Generational arena pattern — stable identity via (index, generation) handle
#     pair; stale handles rejected on lookup via generation check
#   • genus (struct) definitions — Manus, Loculus, Area, AreaCumManus, Nodus
#   • Pure functional updates — no lista[i] mutation, all operations return new
#     Area values to keep generated Rust sound
#   • dum loop — explicit iteration over list indices (lines 42-46, 75-90)
#   • si/sin/secus — conditional logic (lines 58, 60, 62, 78-89)
#   • discerne/casu — pattern matching on enum variants (lines 117-133)
#   • probandum/proba/adfirma — test framework with multi-case assertions
#   • discretio — sum type (enum) with variant payloads (lines 93-96)
#   • gingimus (finge) — enum variant construction with named fields (lines 113-116)
#
# Syntaxes used:
#   • genus — struct definition (lines 8, 12, 18, 22)
#   • discretio — enum/sum type (line 93)
#   • functio — function definition (lines 28, 32, 36, 57, 70, 73)
#   • fixum — immutable binding (lines 33, 43, etc.)
#   • varia — mutable binding (lines 40, 41, etc.)
#   • dum — while loop (lines 42, 75)
#   • si/sin/secus — conditionals (lines 58, 60, 62, 78-89)
#   • discerne/casu — match/pattern match (lines 117-133)
#   • redde — return (lines 30, etc.)
#   • finge — construct enum variant (lines 113-116)
#   • adfirma — test assertion (lines 109-112, etc.)
#   • proba — test case (lines 101, 134, 155)
#   • probandum — test suite (line 100)
#   • ≡ — equality comparison (lines 29, 61, etc.)
#   • lista<T> — list type (lines 20, 93, 96)
#   • textus, numerus, bivalens — primitive types
#   • vacua — empty list literal
#   • .longitudo() — list length method
#   • .appende() — list append method
#
# Alternate approaches (not shown):
#   • Mutable arena with unsafe interior for performance — a mutable lista<Loculus> with in-place updates avoids copying on every insert/take
#   • Reusing free slots (via free list) instead of always appending — maintain a list of freed indices to recycle slots without growing the arena
#
# Anti-patterns (avoid these):
#   • Using lista[i] assignment in generated Rust contexts — in-place list mutation breaks Rust's borrow-checker soundness; use pure value updates (return new Area) instead
#   • Assuming stale handle reuse after removal without generation check — always verify generatio matches before using a handle; stale handles must be rejected on lookup
#
# Learning path:
#   Before: Stage 3: genus, lista, nihil → Stage 3: discerne/casu (structs, collections, and pattern matching)
#   After:  Stage 6: advanced applications (vivilite — real-world resource management)
#
# Stage: arena-handle, complete contract with tests, all language constructs demonstrated
# Backend: Rust, stepper
# =============================================================================

# Reusable generational arena-handle contract (language surface).
#
# Semantics mirror faber-runtime::Arena / ArenaHandle (see arena.rs):
# stable identity independent of list order; stale handles reject on lookup.
# This package uses pure value updates (no lista[i] assignment) so generated
# Rust stays sound; the runtime crate is the authoritative store implementation.

genus Manus {
    numerus index
    numerus generatio
}

genus Loculus {
    numerus generatio
    bivalens vivus
    textus valor
}

genus Area {
    lista<Loculus> loculi
}

genus AreaCumManus {
    Area area
    Manus manus
}

functio manus_aequat(de Manus a, de Manus b) → bivalens {
    redde a.index ≡ b.index et a.generatio ≡ b.generatio
}

functio area_nova() → Area {
    fixum lista<Loculus> loculi ← vacua
    redde Area {loculi = loculi}
}

functio area_inserit(Area area, textus valor) → AreaCumManus {
    # Always append a new live slot. Free slots from tollit stay dead so the
    # old handle generation remains invalid; reuse is optional for this proof.
    varia lista<Loculus> out ← vacua
    varia numerus i ← 0
    dum i ≺ area.loculi.longitudo() {
        out.appende(area.loculi[i])
        i ← i + 1
    }
    fixum numerus index ← out.longitudo()
    out.appende(Loculus {generatio = 0, vivus = verum, valor = valor})
    redde AreaCumManus {area = Area {loculi = out}, manus = Manus {index = index, generatio = 0}}
}

# Lookup returns the payload, or "" when the handle is stale / out of range.
# Proof resources never use empty text, so "" is the explicit reject signal.
functio area_accipe(de Area area, de Manus manus) → textus {
    si manus.index ≥ area.loculi.longitudo() ergo redde ""
    fixum Loculus slot ← area.loculi[manus.index]
    si slot.vivus ≡ falsum ergo redde ""
    si slot.generatio ≠ manus.generatio ergo redde ""
    redde slot.valor
}

functio area_continet(de Area area, de Manus manus) → bivalens {
    redde area_accipe(area, manus) ≠ ""
}

functio area_tollit(Area area, de Manus manus) → Area {
    varia lista<Loculus> out ← vacua
    varia numerus i ← 0
    dum i ≺ area.loculi.longitudo() {
        fixum Loculus slot ← area.loculi[i]
        si (i ≡ manus.index et slot.vivus ≡ verum) et slot.generatio ≡ manus.generatio {
            out.appende(Loculus {generatio = slot.generatio + 1, vivus = falsum, valor = ""})
        }
        secus {
            out.appende(slot)
        }
        i ← i + 1
    }
    redde Area {loculi = out}
}

# Heterogeneous node: stores Manus, never deep-copies the resource payload.
discretio Nodus {
    Groupus {
        lista<Manus> filii
    },
    Tessera {
        Manus geometria
    },
}

proba "two nodes share one resource identity" tag "identity" {
    fixum AreaCumManus step ← area_inserit(area_nova(), "shared-mesh")
    fixum Area res ← step.area
    fixum Manus geo ← step.manus
    # Reconstruct handle values so each node owns a copy of the identity bits
    # without cloning the resource payload (still one live slot in `res`).
    fixum Manus left_geo ← Manus {index = geo.index, generatio = geo.generatio}
    fixum Manus right_geo ← Manus {index = geo.index, generatio = geo.generatio}
    adfirma manus_aequat(left_geo, right_geo)
    adfirma area_accipe(res, left_geo) ≡ "shared-mesh"
    adfirma area_accipe(res, right_geo) ≡ "shared-mesh"
    fixum Nodus left ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    fixum Nodus right ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    discerne left {
        casu Tessera fixum geometria {
            adfirma manus_aequat(geometria, left_geo)
        }
        casu Groupus fixum filii {
            adfirma filii.longitudo() ≡ 0
        }
    }
    discerne right {
        casu Tessera fixum geometria {
            adfirma manus_aequat(geometria, right_geo)
        }
        casu Groupus fixum filii {
            adfirma filii.longitudo() ≡ 0
        }
    }
}

proba "reparent reorder preserves handle identity" tag "identity" {
    fixum AreaCumManus s0 ← area_inserit(area_nova(), "child-a")
    fixum AreaCumManus s1 ← area_inserit(s0.area, "child-b")
    fixum Area nodi ← s1.area
    fixum Manus a ← s0.manus
    fixum Manus b ← s1.manus
    varia lista<Manus> filii ← vacua
    filii.appende(Manus {index = a.index, generatio = a.generatio})
    filii.appende(Manus {index = b.index, generatio = b.generatio})
    # swap order without changing handle identities
    fixum Manus first ← filii[0]
    fixum Manus second ← filii[1]
    varia lista<Manus> reord ← vacua
    reord.appende(Manus {index = second.index, generatio = second.generatio})
    reord.appende(Manus {index = first.index, generatio = first.generatio})
    adfirma area_accipe(nodi, reord[0]) ≡ "child-b"
    adfirma area_accipe(nodi, reord[1]) ≡ "child-a"
    adfirma area_accipe(nodi, a) ≡ "child-a"
    adfirma area_accipe(nodi, b) ≡ "child-b"
}

proba "stale handle rejects after remove" tag "identity" {
    fixum AreaCumManus s0 ← area_inserit(area_nova(), "gone")
    fixum Manus h ← s0.manus
    fixum Manus h_bits ← Manus {index = h.index, generatio = h.generatio}
    adfirma area_continet(s0.area, h_bits)
    fixum Area after ← area_tollit(s0.area, h_bits)
    adfirma area_continet(after, h_bits) ≡ falsum
    adfirma area_accipe(after, h_bits) ≡ ""
    fixum AreaCumManus s1 ← area_inserit(after, "fresh")
    fixum Manus h2 ← s1.manus
    # New live slot (append); old handle still rejected by generation/vivus.
    adfirma manus_aequat(h_bits, h2) ≡ falsum
    adfirma area_accipe(s1.area, h_bits) ≡ ""
    adfirma area_accipe(s1.area, h2) ≡ "fresh"
    adfirma area_continet(s1.area, h2)
}

incipit {
}

faber format --locale th-TH — Thai

# =============================================================================
# arena-handle — generational arena-handle contract via pure value updates
# =============================================================================
#
# What this example teaches:
#   • Generational arena pattern — stable identity via (index, generation) handle
#     pair; stale handles rejected on lookup via generation check
#   • genus (struct) definitions — Manus, Loculus, Area, AreaCumManus, Nodus
#   • Pure functional updates — no lista[i] mutation, all operations return new
#     Area values to keep generated Rust sound
#   • dum loop — explicit iteration over list indices (lines 42-46, 75-90)
#   • si/sin/secus — conditional logic (lines 58, 60, 62, 78-89)
#   • discerne/casu — pattern matching on enum variants (lines 117-133)
#   • probandum/proba/adfirma — test framework with multi-case assertions
#   • discretio — sum type (enum) with variant payloads (lines 93-96)
#   • gingimus (finge) — enum variant construction with named fields (lines 113-116)
#
# Syntaxes used:
#   • genus — struct definition (lines 8, 12, 18, 22)
#   • discretio — enum/sum type (line 93)
#   • functio — function definition (lines 28, 32, 36, 57, 70, 73)
#   • fixum — immutable binding (lines 33, 43, etc.)
#   • varia — mutable binding (lines 40, 41, etc.)
#   • dum — while loop (lines 42, 75)
#   • si/sin/secus — conditionals (lines 58, 60, 62, 78-89)
#   • discerne/casu — match/pattern match (lines 117-133)
#   • redde — return (lines 30, etc.)
#   • finge — construct enum variant (lines 113-116)
#   • adfirma — test assertion (lines 109-112, etc.)
#   • proba — test case (lines 101, 134, 155)
#   • probandum — test suite (line 100)
#   • ≡ — equality comparison (lines 29, 61, etc.)
#   • lista<T> — list type (lines 20, 93, 96)
#   • textus, numerus, bivalens — primitive types
#   • vacua — empty list literal
#   • .longitudo() — list length method
#   • .appende() — list append method
#
# Alternate approaches (not shown):
#   • Mutable arena with unsafe interior for performance — a mutable lista<Loculus> with in-place updates avoids copying on every insert/take
#   • Reusing free slots (via free list) instead of always appending — maintain a list of freed indices to recycle slots without growing the arena
#
# Anti-patterns (avoid these):
#   • Using lista[i] assignment in generated Rust contexts — in-place list mutation breaks Rust's borrow-checker soundness; use pure value updates (return new Area) instead
#   • Assuming stale handle reuse after removal without generation check — always verify generatio matches before using a handle; stale handles must be rejected on lookup
#
# Learning path:
#   Before: Stage 3: genus, lista, nihil → Stage 3: discerne/casu (structs, collections, and pattern matching)
#   After:  Stage 6: advanced applications (vivilite — real-world resource management)
#
# Stage: arena-handle, complete contract with tests, all language constructs demonstrated
# Backend: Rust, stepper
# =============================================================================

# Reusable generational arena-handle contract (language surface).
#
# Semantics mirror faber-runtime::Arena / ArenaHandle (see arena.rs):
# stable identity independent of list order; stale handles reject on lookup.
# This package uses pure value updates (no lista[i] assignment) so generated
# Rust stays sound; the runtime crate is the authoritative store implementation.

ชนิด Manus {
    จำนวน index
    จำนวน generatio
}

ชนิด Loculus {
    จำนวน generatio
    ตรรกะ vivus
    ข้อความ valor
}

ชนิด Area {
    รายการ<Loculus> loculi
}

ชนิด AreaCumManus {
    Area area
    Manus manus
}

ฟังก์ชัน manus_aequat(จาก Manus a, จาก Manus b) → ตรรกะ {
    คืน a.index ≡ b.index และ a.generatio ≡ b.generatio
}

ฟังก์ชัน area_nova() → Area {
    คงที่ รายการ<Loculus> loculi ← เซตว่าง
    คืน Area {loculi = loculi}
}

ฟังก์ชัน area_inserit(Area area, ข้อความ valor) → AreaCumManus {
    # Always append a new live slot. Free slots from tollit stay dead so the
    # old handle generation remains invalid; reuse is optional for this proof.
    แปร รายการ<Loculus> out ← เซตว่าง
    แปร จำนวน i ← 0
    ขณะ i ≺ area.loculi.longitudo() {
        out.appende(area.loculi[i])
        i ← i + 1
    }
    คงที่ จำนวน index ← out.longitudo()
    out.appende(Loculus {generatio = 0, vivus = จริง, valor = valor})
    คืน AreaCumManus {area = Area {loculi = out}, manus = Manus {index = index, generatio = 0}}
}

# Lookup returns the payload, or "" when the handle is stale / out of range.
# Proof resources never use empty text, so "" is the explicit reject signal.
ฟังก์ชัน area_accipe(จาก Area area, จาก Manus manus) → ข้อความ {
    ถ้า manus.index ≥ area.loculi.longitudo() ดังนั้น คืน ""
    คงที่ Loculus slot ← area.loculi[manus.index]
    ถ้า slot.vivus ≡ เท็จ ดังนั้น คืน ""
    ถ้า slot.generatio ≠ manus.generatio ดังนั้น คืน ""
    คืน slot.valor
}

ฟังก์ชัน area_continet(จาก Area area, จาก Manus manus) → ตรรกะ {
    คืน area_accipe(area, manus) ≠ ""
}

ฟังก์ชัน area_tollit(Area area, จาก Manus manus) → Area {
    แปร รายการ<Loculus> out ← เซตว่าง
    แปร จำนวน i ← 0
    ขณะ i ≺ area.loculi.longitudo() {
        คงที่ Loculus slot ← area.loculi[i]
        ถ้า (i ≡ manus.index และ slot.vivus ≡ จริง) และ slot.generatio ≡ manus.generatio {
            out.appende(Loculus {generatio = slot.generatio + 1, vivus = เท็จ, valor = ""})
        }
        มิฉะนั้น {
            out.appende(slot)
        }
        i ← i + 1
    }
    คืน Area {loculi = out}
}

# Heterogeneous node: stores Manus, never deep-copies the resource payload.
สหภาพแยก Nodus {
    Groupus {
        รายการ<Manus> filii
    },
    Tessera {
        Manus geometria
    },
}

ทดสอบ "two nodes share one resource identity" แท็ก "identity" {
    คงที่ AreaCumManus step ← area_inserit(area_nova(), "shared-mesh")
    คงที่ Area res ← step.area
    คงที่ Manus geo ← step.manus
    # Reconstruct handle values so each node owns a copy of the identity bits
    # without cloning the resource payload (still one live slot in `res`).
    คงที่ Manus left_geo ← Manus {index = geo.index, generatio = geo.generatio}
    คงที่ Manus right_geo ← Manus {index = geo.index, generatio = geo.generatio}
    ยืนยัน manus_aequat(left_geo, right_geo)
    ยืนยัน area_accipe(res, left_geo) ≡ "shared-mesh"
    ยืนยัน area_accipe(res, right_geo) ≡ "shared-mesh"
    คงที่ Nodus left ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    คงที่ Nodus right ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    แยก left {
        กรณี Tessera คงที่ geometria {
            ยืนยัน manus_aequat(geometria, left_geo)
        }
        กรณี Groupus คงที่ filii {
            ยืนยัน filii.longitudo() ≡ 0
        }
    }
    แยก right {
        กรณี Tessera คงที่ geometria {
            ยืนยัน manus_aequat(geometria, right_geo)
        }
        กรณี Groupus คงที่ filii {
            ยืนยัน filii.longitudo() ≡ 0
        }
    }
}

ทดสอบ "reparent reorder preserves handle identity" แท็ก "identity" {
    คงที่ AreaCumManus s0 ← area_inserit(area_nova(), "child-a")
    คงที่ AreaCumManus s1 ← area_inserit(s0.area, "child-b")
    คงที่ Area nodi ← s1.area
    คงที่ Manus a ← s0.manus
    คงที่ Manus b ← s1.manus
    แปร รายการ<Manus> filii ← เซตว่าง
    filii.appende(Manus {index = a.index, generatio = a.generatio})
    filii.appende(Manus {index = b.index, generatio = b.generatio})
    # swap order without changing handle identities
    คงที่ Manus first ← filii[0]
    คงที่ Manus second ← filii[1]
    แปร รายการ<Manus> reord ← เซตว่าง
    reord.appende(Manus {index = second.index, generatio = second.generatio})
    reord.appende(Manus {index = first.index, generatio = first.generatio})
    ยืนยัน area_accipe(nodi, reord[0]) ≡ "child-b"
    ยืนยัน area_accipe(nodi, reord[1]) ≡ "child-a"
    ยืนยัน area_accipe(nodi, a) ≡ "child-a"
    ยืนยัน area_accipe(nodi, b) ≡ "child-b"
}

ทดสอบ "stale handle rejects after remove" แท็ก "identity" {
    คงที่ AreaCumManus s0 ← area_inserit(area_nova(), "gone")
    คงที่ Manus h ← s0.manus
    คงที่ Manus h_bits ← Manus {index = h.index, generatio = h.generatio}
    ยืนยัน area_continet(s0.area, h_bits)
    คงที่ Area after ← area_tollit(s0.area, h_bits)
    ยืนยัน area_continet(after, h_bits) ≡ เท็จ
    ยืนยัน area_accipe(after, h_bits) ≡ ""
    คงที่ AreaCumManus s1 ← area_inserit(after, "fresh")
    คงที่ Manus h2 ← s1.manus
    # New live slot (append); old handle still rejected by generation/vivus.
    ยืนยัน manus_aequat(h_bits, h2) ≡ เท็จ
    ยืนยัน area_accipe(s1.area, h_bits) ≡ ""
    ยืนยัน area_accipe(s1.area, h2) ≡ "fresh"
    ยืนยัน area_continet(s1.area, h2)
}

เริ่ม {
}

faber format --locale zh-Hans — Simplified Chinese

# =============================================================================
# arena-handle — generational arena-handle contract via pure value updates
# =============================================================================
#
# What this example teaches:
#   • Generational arena pattern — stable identity via (index, generation) handle
#     pair; stale handles rejected on lookup via generation check
#   • genus (struct) definitions — Manus, Loculus, Area, AreaCumManus, Nodus
#   • Pure functional updates — no lista[i] mutation, all operations return new
#     Area values to keep generated Rust sound
#   • dum loop — explicit iteration over list indices (lines 42-46, 75-90)
#   • si/sin/secus — conditional logic (lines 58, 60, 62, 78-89)
#   • discerne/casu — pattern matching on enum variants (lines 117-133)
#   • probandum/proba/adfirma — test framework with multi-case assertions
#   • discretio — sum type (enum) with variant payloads (lines 93-96)
#   • gingimus (finge) — enum variant construction with named fields (lines 113-116)
#
# Syntaxes used:
#   • genus — struct definition (lines 8, 12, 18, 22)
#   • discretio — enum/sum type (line 93)
#   • functio — function definition (lines 28, 32, 36, 57, 70, 73)
#   • fixum — immutable binding (lines 33, 43, etc.)
#   • varia — mutable binding (lines 40, 41, etc.)
#   • dum — while loop (lines 42, 75)
#   • si/sin/secus — conditionals (lines 58, 60, 62, 78-89)
#   • discerne/casu — match/pattern match (lines 117-133)
#   • redde — return (lines 30, etc.)
#   • finge — construct enum variant (lines 113-116)
#   • adfirma — test assertion (lines 109-112, etc.)
#   • proba — test case (lines 101, 134, 155)
#   • probandum — test suite (line 100)
#   • ≡ — equality comparison (lines 29, 61, etc.)
#   • lista<T> — list type (lines 20, 93, 96)
#   • textus, numerus, bivalens — primitive types
#   • vacua — empty list literal
#   • .longitudo() — list length method
#   • .appende() — list append method
#
# Alternate approaches (not shown):
#   • Mutable arena with unsafe interior for performance — a mutable lista<Loculus> with in-place updates avoids copying on every insert/take
#   • Reusing free slots (via free list) instead of always appending — maintain a list of freed indices to recycle slots without growing the arena
#
# Anti-patterns (avoid these):
#   • Using lista[i] assignment in generated Rust contexts — in-place list mutation breaks Rust's borrow-checker soundness; use pure value updates (return new Area) instead
#   • Assuming stale handle reuse after removal without generation check — always verify generatio matches before using a handle; stale handles must be rejected on lookup
#
# Learning path:
#   Before: Stage 3: genus, lista, nihil → Stage 3: discerne/casu (structs, collections, and pattern matching)
#   After:  Stage 6: advanced applications (vivilite — real-world resource management)
#
# Stage: arena-handle, complete contract with tests, all language constructs demonstrated
# Backend: Rust, stepper
# =============================================================================

# Reusable generational arena-handle contract (language surface).
#
# Semantics mirror faber-runtime::Arena / ArenaHandle (see arena.rs):
# stable identity independent of list order; stale handles reject on lookup.
# This package uses pure value updates (no lista[i] assignment) so generated
# Rust stays sound; the runtime crate is the authoritative store implementation.

类 Manus {
    整数 index
    整数 generatio
}

类 Loculus {
    整数 generatio
    布尔 vivus
    文本 valor
}

类 Area {
    列表<Loculus> loculi
}

类 AreaCumManus {
    Area area
    Manus manus
}

函数 manus_aequat(借自 Manus a, 借自 Manus b) → 布尔 {
    返回 a.index ≡ b.index 且 a.generatio ≡ b.generatio
}

函数 area_nova() → Area {
    常量 列表<Loculus> loculi ← 空集
    返回 Area {loculi = loculi}
}

函数 area_inserit(Area area, 文本 valor) → AreaCumManus {
    # Always append a new live slot. Free slots from tollit stay dead so the
    # old handle generation remains invalid; reuse is optional for this proof.
    变量 列表<Loculus> out ← 空集
    变量 整数 i ← 0
    当 i ≺ area.loculi.longitudo() {
        out.appende(area.loculi[i])
        i ← i + 1
    }
    常量 整数 index ← out.longitudo()
    out.appende(Loculus {generatio = 0, vivus = 真, valor = valor})
    返回 AreaCumManus {area = Area {loculi = out}, manus = Manus {index = index, generatio = 0}}
}

# Lookup returns the payload, or "" when the handle is stale / out of range.
# Proof resources never use empty text, so "" is the explicit reject signal.
函数 area_accipe(借自 Area area, 借自 Manus manus) → 文本 {
    如果 manus.index ≥ area.loculi.longitudo() 则 返回 ""
    常量 Loculus slot ← area.loculi[manus.index]
    如果 slot.vivus ≡ 假 则 返回 ""
    如果 slot.generatio ≠ manus.generatio 则 返回 ""
    返回 slot.valor
}

函数 area_continet(借自 Area area, 借自 Manus manus) → 布尔 {
    返回 area_accipe(area, manus) ≠ ""
}

函数 area_tollit(Area area, 借自 Manus manus) → Area {
    变量 列表<Loculus> out ← 空集
    变量 整数 i ← 0
    当 i ≺ area.loculi.longitudo() {
        常量 Loculus slot ← area.loculi[i]
        如果 (i ≡ manus.index 且 slot.vivus ≡ 真) 且 slot.generatio ≡ manus.generatio {
            out.appende(Loculus {generatio = slot.generatio + 1, vivus = 假, valor = ""})
        }
        否则 {
            out.appende(slot)
        }
        i ← i + 1
    }
    返回 Area {loculi = out}
}

# Heterogeneous node: stores Manus, never deep-copies the resource payload.
判别 Nodus {
    Groupus {
        列表<Manus> filii
    },
    Tessera {
        Manus geometria
    },
}

测试 "two nodes share one resource identity" 标签 "identity" {
    常量 AreaCumManus step ← area_inserit(area_nova(), "shared-mesh")
    常量 Area res ← step.area
    常量 Manus geo ← step.manus
    # Reconstruct handle values so each node owns a copy of the identity bits
    # without cloning the resource payload (still one live slot in `res`).
    常量 Manus left_geo ← Manus {index = geo.index, generatio = geo.generatio}
    常量 Manus right_geo ← Manus {index = geo.index, generatio = geo.generatio}
    断言 manus_aequat(left_geo, right_geo)
    断言 area_accipe(res, left_geo) ≡ "shared-mesh"
    断言 area_accipe(res, right_geo) ≡ "shared-mesh"
    常量 Nodus left ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    常量 Nodus right ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    匹配 left {
        情况 Tessera 常量 geometria {
            断言 manus_aequat(geometria, left_geo)
        }
        情况 Groupus 常量 filii {
            断言 filii.longitudo() ≡ 0
        }
    }
    匹配 right {
        情况 Tessera 常量 geometria {
            断言 manus_aequat(geometria, right_geo)
        }
        情况 Groupus 常量 filii {
            断言 filii.longitudo() ≡ 0
        }
    }
}

测试 "reparent reorder preserves handle identity" 标签 "identity" {
    常量 AreaCumManus s0 ← area_inserit(area_nova(), "child-a")
    常量 AreaCumManus s1 ← area_inserit(s0.area, "child-b")
    常量 Area nodi ← s1.area
    常量 Manus a ← s0.manus
    常量 Manus b ← s1.manus
    变量 列表<Manus> filii ← 空集
    filii.appende(Manus {index = a.index, generatio = a.generatio})
    filii.appende(Manus {index = b.index, generatio = b.generatio})
    # swap order without changing handle identities
    常量 Manus first ← filii[0]
    常量 Manus second ← filii[1]
    变量 列表<Manus> reord ← 空集
    reord.appende(Manus {index = second.index, generatio = second.generatio})
    reord.appende(Manus {index = first.index, generatio = first.generatio})
    断言 area_accipe(nodi, reord[0]) ≡ "child-b"
    断言 area_accipe(nodi, reord[1]) ≡ "child-a"
    断言 area_accipe(nodi, a) ≡ "child-a"
    断言 area_accipe(nodi, b) ≡ "child-b"
}

测试 "stale handle rejects after remove" 标签 "identity" {
    常量 AreaCumManus s0 ← area_inserit(area_nova(), "gone")
    常量 Manus h ← s0.manus
    常量 Manus h_bits ← Manus {index = h.index, generatio = h.generatio}
    断言 area_continet(s0.area, h_bits)
    常量 Area after ← area_tollit(s0.area, h_bits)
    断言 area_continet(after, h_bits) ≡ 假
    断言 area_accipe(after, h_bits) ≡ ""
    常量 AreaCumManus s1 ← area_inserit(after, "fresh")
    常量 Manus h2 ← s1.manus
    # New live slot (append); old handle still rejected by generation/vivus.
    断言 manus_aequat(h_bits, h2) ≡ 假
    断言 area_accipe(s1.area, h_bits) ≡ ""
    断言 area_accipe(s1.area, h2) ≡ "fresh"
    断言 area_continet(s1.area, h2)
}

入口 {
}

faber format --locale zh-Hant — Traditional Chinese

# =============================================================================
# arena-handle — generational arena-handle contract via pure value updates
# =============================================================================
#
# What this example teaches:
#   • Generational arena pattern — stable identity via (index, generation) handle
#     pair; stale handles rejected on lookup via generation check
#   • genus (struct) definitions — Manus, Loculus, Area, AreaCumManus, Nodus
#   • Pure functional updates — no lista[i] mutation, all operations return new
#     Area values to keep generated Rust sound
#   • dum loop — explicit iteration over list indices (lines 42-46, 75-90)
#   • si/sin/secus — conditional logic (lines 58, 60, 62, 78-89)
#   • discerne/casu — pattern matching on enum variants (lines 117-133)
#   • probandum/proba/adfirma — test framework with multi-case assertions
#   • discretio — sum type (enum) with variant payloads (lines 93-96)
#   • gingimus (finge) — enum variant construction with named fields (lines 113-116)
#
# Syntaxes used:
#   • genus — struct definition (lines 8, 12, 18, 22)
#   • discretio — enum/sum type (line 93)
#   • functio — function definition (lines 28, 32, 36, 57, 70, 73)
#   • fixum — immutable binding (lines 33, 43, etc.)
#   • varia — mutable binding (lines 40, 41, etc.)
#   • dum — while loop (lines 42, 75)
#   • si/sin/secus — conditionals (lines 58, 60, 62, 78-89)
#   • discerne/casu — match/pattern match (lines 117-133)
#   • redde — return (lines 30, etc.)
#   • finge — construct enum variant (lines 113-116)
#   • adfirma — test assertion (lines 109-112, etc.)
#   • proba — test case (lines 101, 134, 155)
#   • probandum — test suite (line 100)
#   • ≡ — equality comparison (lines 29, 61, etc.)
#   • lista<T> — list type (lines 20, 93, 96)
#   • textus, numerus, bivalens — primitive types
#   • vacua — empty list literal
#   • .longitudo() — list length method
#   • .appende() — list append method
#
# Alternate approaches (not shown):
#   • Mutable arena with unsafe interior for performance — a mutable lista<Loculus> with in-place updates avoids copying on every insert/take
#   • Reusing free slots (via free list) instead of always appending — maintain a list of freed indices to recycle slots without growing the arena
#
# Anti-patterns (avoid these):
#   • Using lista[i] assignment in generated Rust contexts — in-place list mutation breaks Rust's borrow-checker soundness; use pure value updates (return new Area) instead
#   • Assuming stale handle reuse after removal without generation check — always verify generatio matches before using a handle; stale handles must be rejected on lookup
#
# Learning path:
#   Before: Stage 3: genus, lista, nihil → Stage 3: discerne/casu (structs, collections, and pattern matching)
#   After:  Stage 6: advanced applications (vivilite — real-world resource management)
#
# Stage: arena-handle, complete contract with tests, all language constructs demonstrated
# Backend: Rust, stepper
# =============================================================================

# Reusable generational arena-handle contract (language surface).
#
# Semantics mirror faber-runtime::Arena / ArenaHandle (see arena.rs):
# stable identity independent of list order; stale handles reject on lookup.
# This package uses pure value updates (no lista[i] assignment) so generated
# Rust stays sound; the runtime crate is the authoritative store implementation.

類型 Manus {
    整數 index
    整數 generatio
}

類型 Loculus {
    整數 generatio
    布林 vivus
    文字 valor
}

類型 Area {
    列表<Loculus> loculi
}

類型 AreaCumManus {
    Area area
    Manus manus
}

函式 manus_aequat(從 Manus a, 從 Manus b) → 布林 {
    傳回 a.index ≡ b.index 且 a.generatio ≡ b.generatio
}

函式 area_nova() → Area {
    定值 列表<Loculus> loculi ← 空集
    傳回 Area {loculi = loculi}
}

函式 area_inserit(Area area, 文字 valor) → AreaCumManus {
    # Always append a new live slot. Free slots from tollit stay dead so the
    # old handle generation remains invalid; reuse is optional for this proof.
    變值 列表<Loculus> out ← 空集
    變值 整數 i ← 0
    當 i ≺ area.loculi.longitudo() {
        out.appende(area.loculi[i])
        i ← i + 1
    }
    定值 整數 index ← out.longitudo()
    out.appende(Loculus {generatio = 0, vivus = 真, valor = valor})
    傳回 AreaCumManus {area = Area {loculi = out}, manus = Manus {index = index, generatio = 0}}
}

# Lookup returns the payload, or "" when the handle is stale / out of range.
# Proof resources never use empty text, so "" is the explicit reject signal.
函式 area_accipe(從 Area area, 從 Manus manus) → 文字 {
    若 manus.index ≥ area.loculi.longitudo() 則 傳回 ""
    定值 Loculus slot ← area.loculi[manus.index]
    若 slot.vivus ≡ 假 則 傳回 ""
    若 slot.generatio ≠ manus.generatio 則 傳回 ""
    傳回 slot.valor
}

函式 area_continet(從 Area area, 從 Manus manus) → 布林 {
    傳回 area_accipe(area, manus) ≠ ""
}

函式 area_tollit(Area area, 從 Manus manus) → Area {
    變值 列表<Loculus> out ← 空集
    變值 整數 i ← 0
    當 i ≺ area.loculi.longitudo() {
        定值 Loculus slot ← area.loculi[i]
        若 (i ≡ manus.index 且 slot.vivus ≡ 真) 且 slot.generatio ≡ manus.generatio {
            out.appende(Loculus {generatio = slot.generatio + 1, vivus = 假, valor = ""})
        }
        否則 {
            out.appende(slot)
        }
        i ← i + 1
    }
    傳回 Area {loculi = out}
}

# Heterogeneous node: stores Manus, never deep-copies the resource payload.
分支聯集 Nodus {
    Groupus {
        列表<Manus> filii
    },
    Tessera {
        Manus geometria
    },
}

測試 "two nodes share one resource identity" 標籤 "identity" {
    定值 AreaCumManus step ← area_inserit(area_nova(), "shared-mesh")
    定值 Area res ← step.area
    定值 Manus geo ← step.manus
    # Reconstruct handle values so each node owns a copy of the identity bits
    # without cloning the resource payload (still one live slot in `res`).
    定值 Manus left_geo ← Manus {index = geo.index, generatio = geo.generatio}
    定值 Manus right_geo ← Manus {index = geo.index, generatio = geo.generatio}
    斷言 manus_aequat(left_geo, right_geo)
    斷言 area_accipe(res, left_geo) ≡ "shared-mesh"
    斷言 area_accipe(res, right_geo) ≡ "shared-mesh"
    定值 Nodus left ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    定值 Nodus right ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    比對 left {
        分支 Tessera 定值 geometria {
            斷言 manus_aequat(geometria, left_geo)
        }
        分支 Groupus 定值 filii {
            斷言 filii.longitudo() ≡ 0
        }
    }
    比對 right {
        分支 Tessera 定值 geometria {
            斷言 manus_aequat(geometria, right_geo)
        }
        分支 Groupus 定值 filii {
            斷言 filii.longitudo() ≡ 0
        }
    }
}

測試 "reparent reorder preserves handle identity" 標籤 "identity" {
    定值 AreaCumManus s0 ← area_inserit(area_nova(), "child-a")
    定值 AreaCumManus s1 ← area_inserit(s0.area, "child-b")
    定值 Area nodi ← s1.area
    定值 Manus a ← s0.manus
    定值 Manus b ← s1.manus
    變值 列表<Manus> filii ← 空集
    filii.appende(Manus {index = a.index, generatio = a.generatio})
    filii.appende(Manus {index = b.index, generatio = b.generatio})
    # swap order without changing handle identities
    定值 Manus first ← filii[0]
    定值 Manus second ← filii[1]
    變值 列表<Manus> reord ← 空集
    reord.appende(Manus {index = second.index, generatio = second.generatio})
    reord.appende(Manus {index = first.index, generatio = first.generatio})
    斷言 area_accipe(nodi, reord[0]) ≡ "child-b"
    斷言 area_accipe(nodi, reord[1]) ≡ "child-a"
    斷言 area_accipe(nodi, a) ≡ "child-a"
    斷言 area_accipe(nodi, b) ≡ "child-b"
}

測試 "stale handle rejects after remove" 標籤 "identity" {
    定值 AreaCumManus s0 ← area_inserit(area_nova(), "gone")
    定值 Manus h ← s0.manus
    定值 Manus h_bits ← Manus {index = h.index, generatio = h.generatio}
    斷言 area_continet(s0.area, h_bits)
    定值 Area after ← area_tollit(s0.area, h_bits)
    斷言 area_continet(after, h_bits) ≡ 假
    斷言 area_accipe(after, h_bits) ≡ ""
    定值 AreaCumManus s1 ← area_inserit(after, "fresh")
    定值 Manus h2 ← s1.manus
    # New live slot (append); old handle still rejected by generation/vivus.
    斷言 manus_aequat(h_bits, h2) ≡ 假
    斷言 area_accipe(s1.area, h_bits) ≡ ""
    斷言 area_accipe(s1.area, h2) ≡ "fresh"
    斷言 area_continet(s1.area, h2)
}

入口 {
}

faber format --locale vi — Vietnamese

# =============================================================================
# arena-handle — generational arena-handle contract via pure value updates
# =============================================================================
#
# What this example teaches:
#   • Generational arena pattern — stable identity via (index, generation) handle
#     pair; stale handles rejected on lookup via generation check
#   • genus (struct) definitions — Manus, Loculus, Area, AreaCumManus, Nodus
#   • Pure functional updates — no lista[i] mutation, all operations return new
#     Area values to keep generated Rust sound
#   • dum loop — explicit iteration over list indices (lines 42-46, 75-90)
#   • si/sin/secus — conditional logic (lines 58, 60, 62, 78-89)
#   • discerne/casu — pattern matching on enum variants (lines 117-133)
#   • probandum/proba/adfirma — test framework with multi-case assertions
#   • discretio — sum type (enum) with variant payloads (lines 93-96)
#   • gingimus (finge) — enum variant construction with named fields (lines 113-116)
#
# Syntaxes used:
#   • genus — struct definition (lines 8, 12, 18, 22)
#   • discretio — enum/sum type (line 93)
#   • functio — function definition (lines 28, 32, 36, 57, 70, 73)
#   • fixum — immutable binding (lines 33, 43, etc.)
#   • varia — mutable binding (lines 40, 41, etc.)
#   • dum — while loop (lines 42, 75)
#   • si/sin/secus — conditionals (lines 58, 60, 62, 78-89)
#   • discerne/casu — match/pattern match (lines 117-133)
#   • redde — return (lines 30, etc.)
#   • finge — construct enum variant (lines 113-116)
#   • adfirma — test assertion (lines 109-112, etc.)
#   • proba — test case (lines 101, 134, 155)
#   • probandum — test suite (line 100)
#   • ≡ — equality comparison (lines 29, 61, etc.)
#   • lista<T> — list type (lines 20, 93, 96)
#   • textus, numerus, bivalens — primitive types
#   • vacua — empty list literal
#   • .longitudo() — list length method
#   • .appende() — list append method
#
# Alternate approaches (not shown):
#   • Mutable arena with unsafe interior for performance — a mutable lista<Loculus> with in-place updates avoids copying on every insert/take
#   • Reusing free slots (via free list) instead of always appending — maintain a list of freed indices to recycle slots without growing the arena
#
# Anti-patterns (avoid these):
#   • Using lista[i] assignment in generated Rust contexts — in-place list mutation breaks Rust's borrow-checker soundness; use pure value updates (return new Area) instead
#   • Assuming stale handle reuse after removal without generation check — always verify generatio matches before using a handle; stale handles must be rejected on lookup
#
# Learning path:
#   Before: Stage 3: genus, lista, nihil → Stage 3: discerne/casu (structs, collections, and pattern matching)
#   After:  Stage 6: advanced applications (vivilite — real-world resource management)
#
# Stage: arena-handle, complete contract with tests, all language constructs demonstrated
# Backend: Rust, stepper
# =============================================================================

# Reusable generational arena-handle contract (language surface).
#
# Semantics mirror faber-runtime::Arena / ArenaHandle (see arena.rs):
# stable identity independent of list order; stale handles reject on lookup.
# This package uses pure value updates (no lista[i] assignment) so generated
# Rust stays sound; the runtime crate is the authoritative store implementation.

kiểu Manus {
    số index
    số generatio
}

kiểu Loculus {
    số generatio
    logic vivus
    văn_bản valor
}

kiểu Area {
    danh_sách<Loculus> loculi
}

kiểu AreaCumManus {
    Area area
    Manus manus
}

hàm manus_aequat(ra Manus a, ra Manus b) → logic {
    trả a.index ≡ b.index và a.generatio ≡ b.generatio
}

hàm area_nova() → Area {
    hằng danh_sách<Loculus> loculi ← tập_rỗng
    trả Area {loculi = loculi}
}

hàm area_inserit(Area area, văn_bản valor) → AreaCumManus {
    # Always append a new live slot. Free slots from tollit stay dead so the
    # old handle generation remains invalid; reuse is optional for this proof.
    biến danh_sách<Loculus> out ← tập_rỗng
    biến số i ← 0
    trong_khi i ≺ area.loculi.longitudo() {
        out.appende(area.loculi[i])
        i ← i + 1
    }
    hằng số index ← out.longitudo()
    out.appende(Loculus {generatio = 0, vivus = đúng, valor = valor})
    trả AreaCumManus {area = Area {loculi = out}, manus = Manus {index = index, generatio = 0}}
}

# Lookup returns the payload, or "" when the handle is stale / out of range.
# Proof resources never use empty text, so "" is the explicit reject signal.
hàm area_accipe(ra Area area, ra Manus manus) → văn_bản {
    nếu manus.index ≥ area.loculi.longitudo() do_đó trả ""
    hằng Loculus slot ← area.loculi[manus.index]
    nếu slot.vivus ≡ sai do_đó trả ""
    nếu slot.generatio ≠ manus.generatio do_đó trả ""
    trả slot.valor
}

hàm area_continet(ra Area area, ra Manus manus) → logic {
    trả area_accipe(area, manus) ≠ ""
}

hàm area_tollit(Area area, ra Manus manus) → Area {
    biến danh_sách<Loculus> out ← tập_rỗng
    biến số i ← 0
    trong_khi i ≺ area.loculi.longitudo() {
        hằng Loculus slot ← area.loculi[i]
        nếu (i ≡ manus.index và slot.vivus ≡ đúng) và slot.generatio ≡ manus.generatio {
            out.appende(Loculus {generatio = slot.generatio + 1, vivus = sai, valor = ""})
        }
        khác {
            out.appende(slot)
        }
        i ← i + 1
    }
    trả Area {loculi = out}
}

# Heterogeneous node: stores Manus, never deep-copies the resource payload.
hợp_nhất Nodus {
    Groupus {
        danh_sách<Manus> filii
    },
    Tessera {
        Manus geometria
    },
}

kiểm_thử "two nodes share one resource identity" nhãn "identity" {
    hằng AreaCumManus step ← area_inserit(area_nova(), "shared-mesh")
    hằng Area res ← step.area
    hằng Manus geo ← step.manus
    # Reconstruct handle values so each node owns a copy of the identity bits
    # without cloning the resource payload (still one live slot in `res`).
    hằng Manus left_geo ← Manus {index = geo.index, generatio = geo.generatio}
    hằng Manus right_geo ← Manus {index = geo.index, generatio = geo.generatio}
    khẳng_định manus_aequat(left_geo, right_geo)
    khẳng_định area_accipe(res, left_geo) ≡ "shared-mesh"
    khẳng_định area_accipe(res, right_geo) ≡ "shared-mesh"
    hằng Nodus left ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    hằng Nodus right ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    phân_tích left {
        trường_hợp Tessera hằng geometria {
            khẳng_định manus_aequat(geometria, left_geo)
        }
        trường_hợp Groupus hằng filii {
            khẳng_định filii.longitudo() ≡ 0
        }
    }
    phân_tích right {
        trường_hợp Tessera hằng geometria {
            khẳng_định manus_aequat(geometria, right_geo)
        }
        trường_hợp Groupus hằng filii {
            khẳng_định filii.longitudo() ≡ 0
        }
    }
}

kiểm_thử "reparent reorder preserves handle identity" nhãn "identity" {
    hằng AreaCumManus s0 ← area_inserit(area_nova(), "child-a")
    hằng AreaCumManus s1 ← area_inserit(s0.area, "child-b")
    hằng Area nodi ← s1.area
    hằng Manus a ← s0.manus
    hằng Manus b ← s1.manus
    biến danh_sách<Manus> filii ← tập_rỗng
    filii.appende(Manus {index = a.index, generatio = a.generatio})
    filii.appende(Manus {index = b.index, generatio = b.generatio})
    # swap order without changing handle identities
    hằng Manus first ← filii[0]
    hằng Manus second ← filii[1]
    biến danh_sách<Manus> reord ← tập_rỗng
    reord.appende(Manus {index = second.index, generatio = second.generatio})
    reord.appende(Manus {index = first.index, generatio = first.generatio})
    khẳng_định area_accipe(nodi, reord[0]) ≡ "child-b"
    khẳng_định area_accipe(nodi, reord[1]) ≡ "child-a"
    khẳng_định area_accipe(nodi, a) ≡ "child-a"
    khẳng_định area_accipe(nodi, b) ≡ "child-b"
}

kiểm_thử "stale handle rejects after remove" nhãn "identity" {
    hằng AreaCumManus s0 ← area_inserit(area_nova(), "gone")
    hằng Manus h ← s0.manus
    hằng Manus h_bits ← Manus {index = h.index, generatio = h.generatio}
    khẳng_định area_continet(s0.area, h_bits)
    hằng Area after ← area_tollit(s0.area, h_bits)
    khẳng_định area_continet(after, h_bits) ≡ sai
    khẳng_định area_accipe(after, h_bits) ≡ ""
    hằng AreaCumManus s1 ← area_inserit(after, "fresh")
    hằng Manus h2 ← s1.manus
    # New live slot (append); old handle still rejected by generation/vivus.
    khẳng_định manus_aequat(h_bits, h2) ≡ sai
    khẳng_định area_accipe(s1.area, h_bits) ≡ ""
    khẳng_định area_accipe(s1.area, h2) ≡ "fresh"
    khẳng_định area_continet(s1.area, h2)
}

bắt_đầu {
}

faber format --locale ar — Arabic

# =============================================================================
# arena-handle — generational arena-handle contract via pure value updates
# =============================================================================
#
# What this example teaches:
#   • Generational arena pattern — stable identity via (index, generation) handle
#     pair; stale handles rejected on lookup via generation check
#   • genus (struct) definitions — Manus, Loculus, Area, AreaCumManus, Nodus
#   • Pure functional updates — no lista[i] mutation, all operations return new
#     Area values to keep generated Rust sound
#   • dum loop — explicit iteration over list indices (lines 42-46, 75-90)
#   • si/sin/secus — conditional logic (lines 58, 60, 62, 78-89)
#   • discerne/casu — pattern matching on enum variants (lines 117-133)
#   • probandum/proba/adfirma — test framework with multi-case assertions
#   • discretio — sum type (enum) with variant payloads (lines 93-96)
#   • gingimus (finge) — enum variant construction with named fields (lines 113-116)
#
# Syntaxes used:
#   • genus — struct definition (lines 8, 12, 18, 22)
#   • discretio — enum/sum type (line 93)
#   • functio — function definition (lines 28, 32, 36, 57, 70, 73)
#   • fixum — immutable binding (lines 33, 43, etc.)
#   • varia — mutable binding (lines 40, 41, etc.)
#   • dum — while loop (lines 42, 75)
#   • si/sin/secus — conditionals (lines 58, 60, 62, 78-89)
#   • discerne/casu — match/pattern match (lines 117-133)
#   • redde — return (lines 30, etc.)
#   • finge — construct enum variant (lines 113-116)
#   • adfirma — test assertion (lines 109-112, etc.)
#   • proba — test case (lines 101, 134, 155)
#   • probandum — test suite (line 100)
#   • ≡ — equality comparison (lines 29, 61, etc.)
#   • lista<T> — list type (lines 20, 93, 96)
#   • textus, numerus, bivalens — primitive types
#   • vacua — empty list literal
#   • .longitudo() — list length method
#   • .appende() — list append method
#
# Alternate approaches (not shown):
#   • Mutable arena with unsafe interior for performance — a mutable lista<Loculus> with in-place updates avoids copying on every insert/take
#   • Reusing free slots (via free list) instead of always appending — maintain a list of freed indices to recycle slots without growing the arena
#
# Anti-patterns (avoid these):
#   • Using lista[i] assignment in generated Rust contexts — in-place list mutation breaks Rust's borrow-checker soundness; use pure value updates (return new Area) instead
#   • Assuming stale handle reuse after removal without generation check — always verify generatio matches before using a handle; stale handles must be rejected on lookup
#
# Learning path:
#   Before: Stage 3: genus, lista, nihil → Stage 3: discerne/casu (structs, collections, and pattern matching)
#   After:  Stage 6: advanced applications (vivilite — real-world resource management)
#
# Stage: arena-handle, complete contract with tests, all language constructs demonstrated
# Backend: Rust, stepper
# =============================================================================

# Reusable generational arena-handle contract (language surface).
#
# Semantics mirror faber-runtime::Arena / ArenaHandle (see arena.rs):
# stable identity independent of list order; stale handles reject on lookup.
# This package uses pure value updates (no lista[i] assignment) so generated
# Rust stays sound; the runtime crate is the authoritative store implementation.

صنف Manus {
    عدد index
    عدد generatio
}

صنف Loculus {
    عدد generatio
    منطقي vivus
    نص valor
}

صنف Area {
    قائمة<Loculus> loculi
}

صنف AreaCumManus {
    Area area
    Manus manus
}

دالة manus_aequat(عن Manus a, عن Manus b) → منطقي {
    أعد a.index ≡ b.index و a.generatio ≡ b.generatio
}

دالة area_nova() → Area {
    ثابت قائمة<Loculus> loculi ← فارغ
    أعد Area {loculi = loculi}
}

دالة area_inserit(Area area, نص valor) → AreaCumManus {
    # Always append a new live slot. Free slots from tollit stay dead so the
    # old handle generation remains invalid; reuse is optional for this proof.
    متغير قائمة<Loculus> out ← فارغ
    متغير عدد i ← 0
    طالما i ≺ area.loculi.longitudo() {
        out.appende(area.loculi[i])
        i ← i + 1
    }
    ثابت عدد index ← out.longitudo()
    out.appende(Loculus {generatio = 0, vivus = صواب, valor = valor})
    أعد AreaCumManus {area = Area {loculi = out}, manus = Manus {index = index, generatio = 0}}
}

# Lookup returns the payload, or "" when the handle is stale / out of range.
# Proof resources never use empty text, so "" is the explicit reject signal.
دالة area_accipe(عن Area area, عن Manus manus) → نص {
    إذا manus.index ≥ area.loculi.longitudo() إذن أعد ""
    ثابت Loculus slot ← area.loculi[manus.index]
    إذا slot.vivus ≡ خطأ إذن أعد ""
    إذا slot.generatio ≠ manus.generatio إذن أعد ""
    أعد slot.valor
}

دالة area_continet(عن Area area, عن Manus manus) → منطقي {
    أعد area_accipe(area, manus) ≠ ""
}

دالة area_tollit(Area area, عن Manus manus) → Area {
    متغير قائمة<Loculus> out ← فارغ
    متغير عدد i ← 0
    طالما i ≺ area.loculi.longitudo() {
        ثابت Loculus slot ← area.loculi[i]
        إذا (i ≡ manus.index و slot.vivus ≡ صواب) و slot.generatio ≡ manus.generatio {
            out.appende(Loculus {generatio = slot.generatio + 1, vivus = خطأ, valor = ""})
        }
        وإلا {
            out.appende(slot)
        }
        i ← i + 1
    }
    أعد Area {loculi = out}
}

# Heterogeneous node: stores Manus, never deep-copies the resource payload.
تمايز Nodus {
    Groupus {
        قائمة<Manus> filii
    },
    Tessera {
        Manus geometria
    },
}

اختبر "two nodes share one resource identity" وسم "identity" {
    ثابت AreaCumManus step ← area_inserit(area_nova(), "shared-mesh")
    ثابت Area res ← step.area
    ثابت Manus geo ← step.manus
    # Reconstruct handle values so each node owns a copy of the identity bits
    # without cloning the resource payload (still one live slot in `res`).
    ثابت Manus left_geo ← Manus {index = geo.index, generatio = geo.generatio}
    ثابت Manus right_geo ← Manus {index = geo.index, generatio = geo.generatio}
    أكد manus_aequat(left_geo, right_geo)
    أكد area_accipe(res, left_geo) ≡ "shared-mesh"
    أكد area_accipe(res, right_geo) ≡ "shared-mesh"
    ثابت Nodus left ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    ثابت Nodus right ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    طابق left {
        حالة Tessera ثابت geometria {
            أكد manus_aequat(geometria, left_geo)
        }
        حالة Groupus ثابت filii {
            أكد filii.longitudo() ≡ 0
        }
    }
    طابق right {
        حالة Tessera ثابت geometria {
            أكد manus_aequat(geometria, right_geo)
        }
        حالة Groupus ثابت filii {
            أكد filii.longitudo() ≡ 0
        }
    }
}

اختبر "reparent reorder preserves handle identity" وسم "identity" {
    ثابت AreaCumManus s0 ← area_inserit(area_nova(), "child-a")
    ثابت AreaCumManus s1 ← area_inserit(s0.area, "child-b")
    ثابت Area nodi ← s1.area
    ثابت Manus a ← s0.manus
    ثابت Manus b ← s1.manus
    متغير قائمة<Manus> filii ← فارغ
    filii.appende(Manus {index = a.index, generatio = a.generatio})
    filii.appende(Manus {index = b.index, generatio = b.generatio})
    # swap order without changing handle identities
    ثابت Manus first ← filii[0]
    ثابت Manus second ← filii[1]
    متغير قائمة<Manus> reord ← فارغ
    reord.appende(Manus {index = second.index, generatio = second.generatio})
    reord.appende(Manus {index = first.index, generatio = first.generatio})
    أكد area_accipe(nodi, reord[0]) ≡ "child-b"
    أكد area_accipe(nodi, reord[1]) ≡ "child-a"
    أكد area_accipe(nodi, a) ≡ "child-a"
    أكد area_accipe(nodi, b) ≡ "child-b"
}

اختبر "stale handle rejects after remove" وسم "identity" {
    ثابت AreaCumManus s0 ← area_inserit(area_nova(), "gone")
    ثابت Manus h ← s0.manus
    ثابت Manus h_bits ← Manus {index = h.index, generatio = h.generatio}
    أكد area_continet(s0.area, h_bits)
    ثابت Area after ← area_tollit(s0.area, h_bits)
    أكد area_continet(after, h_bits) ≡ خطأ
    أكد area_accipe(after, h_bits) ≡ ""
    ثابت AreaCumManus s1 ← area_inserit(after, "fresh")
    ثابت Manus h2 ← s1.manus
    # New live slot (append); old handle still rejected by generation/vivus.
    أكد manus_aequat(h_bits, h2) ≡ خطأ
    أكد area_accipe(s1.area, h_bits) ≡ ""
    أكد area_accipe(s1.area, h2) ≡ "fresh"
    أكد area_continet(s1.area, h2)
}

بداية {
}

faber format --locale hi — Hindi

# =============================================================================
# arena-handle — generational arena-handle contract via pure value updates
# =============================================================================
#
# What this example teaches:
#   • Generational arena pattern — stable identity via (index, generation) handle
#     pair; stale handles rejected on lookup via generation check
#   • genus (struct) definitions — Manus, Loculus, Area, AreaCumManus, Nodus
#   • Pure functional updates — no lista[i] mutation, all operations return new
#     Area values to keep generated Rust sound
#   • dum loop — explicit iteration over list indices (lines 42-46, 75-90)
#   • si/sin/secus — conditional logic (lines 58, 60, 62, 78-89)
#   • discerne/casu — pattern matching on enum variants (lines 117-133)
#   • probandum/proba/adfirma — test framework with multi-case assertions
#   • discretio — sum type (enum) with variant payloads (lines 93-96)
#   • gingimus (finge) — enum variant construction with named fields (lines 113-116)
#
# Syntaxes used:
#   • genus — struct definition (lines 8, 12, 18, 22)
#   • discretio — enum/sum type (line 93)
#   • functio — function definition (lines 28, 32, 36, 57, 70, 73)
#   • fixum — immutable binding (lines 33, 43, etc.)
#   • varia — mutable binding (lines 40, 41, etc.)
#   • dum — while loop (lines 42, 75)
#   • si/sin/secus — conditionals (lines 58, 60, 62, 78-89)
#   • discerne/casu — match/pattern match (lines 117-133)
#   • redde — return (lines 30, etc.)
#   • finge — construct enum variant (lines 113-116)
#   • adfirma — test assertion (lines 109-112, etc.)
#   • proba — test case (lines 101, 134, 155)
#   • probandum — test suite (line 100)
#   • ≡ — equality comparison (lines 29, 61, etc.)
#   • lista<T> — list type (lines 20, 93, 96)
#   • textus, numerus, bivalens — primitive types
#   • vacua — empty list literal
#   • .longitudo() — list length method
#   • .appende() — list append method
#
# Alternate approaches (not shown):
#   • Mutable arena with unsafe interior for performance — a mutable lista<Loculus> with in-place updates avoids copying on every insert/take
#   • Reusing free slots (via free list) instead of always appending — maintain a list of freed indices to recycle slots without growing the arena
#
# Anti-patterns (avoid these):
#   • Using lista[i] assignment in generated Rust contexts — in-place list mutation breaks Rust's borrow-checker soundness; use pure value updates (return new Area) instead
#   • Assuming stale handle reuse after removal without generation check — always verify generatio matches before using a handle; stale handles must be rejected on lookup
#
# Learning path:
#   Before: Stage 3: genus, lista, nihil → Stage 3: discerne/casu (structs, collections, and pattern matching)
#   After:  Stage 6: advanced applications (vivilite — real-world resource management)
#
# Stage: arena-handle, complete contract with tests, all language constructs demonstrated
# Backend: Rust, stepper
# =============================================================================

# Reusable generational arena-handle contract (language surface).
#
# Semantics mirror faber-runtime::Arena / ArenaHandle (see arena.rs):
# stable identity independent of list order; stale handles reject on lookup.
# This package uses pure value updates (no lista[i] assignment) so generated
# Rust stays sound; the runtime crate is the authoritative store implementation.

वर्ग Manus {
    संख्या index
    संख्या generatio
}

वर्ग Loculus {
    संख्या generatio
    तार्किक vivus
    पाठ valor
}

वर्ग Area {
    सूची<Loculus> loculi
}

वर्ग AreaCumManus {
    Area area
    Manus manus
}

फलन manus_aequat(से Manus a, से Manus b) → तार्किक {
    लौटाओ a.index ≡ b.index और a.generatio ≡ b.generatio
}

फलन area_nova() → Area {
    स्थिर सूची<Loculus> loculi ← खाली
    लौटाओ Area {loculi = loculi}
}

फलन area_inserit(Area area, पाठ valor) → AreaCumManus {
    # Always append a new live slot. Free slots from tollit stay dead so the
    # old handle generation remains invalid; reuse is optional for this proof.
    चर सूची<Loculus> out ← खाली
    चर संख्या i ← 0
    जबतक i ≺ area.loculi.longitudo() {
        out.appende(area.loculi[i])
        i ← i + 1
    }
    स्थिर संख्या index ← out.longitudo()
    out.appende(Loculus {generatio = 0, vivus = सत्य, valor = valor})
    लौटाओ AreaCumManus {area = Area {loculi = out}, manus = Manus {index = index, generatio = 0}}
}

# Lookup returns the payload, or "" when the handle is stale / out of range.
# Proof resources never use empty text, so "" is the explicit reject signal.
फलन area_accipe(से Area area, से Manus manus) → पाठ {
    यदि manus.index ≥ area.loculi.longitudo() अतः लौटाओ ""
    स्थिर Loculus slot ← area.loculi[manus.index]
    यदि slot.vivus ≡ असत्य अतः लौटाओ ""
    यदि slot.generatio ≠ manus.generatio अतः लौटाओ ""
    लौटाओ slot.valor
}

फलन area_continet(से Area area, से Manus manus) → तार्किक {
    लौटाओ area_accipe(area, manus) ≠ ""
}

फलन area_tollit(Area area, से Manus manus) → Area {
    चर सूची<Loculus> out ← खाली
    चर संख्या i ← 0
    जबतक i ≺ area.loculi.longitudo() {
        स्थिर Loculus slot ← area.loculi[i]
        यदि (i ≡ manus.index और slot.vivus ≡ सत्य) और slot.generatio ≡ manus.generatio {
            out.appende(Loculus {generatio = slot.generatio + 1, vivus = असत्य, valor = ""})
        }
        अन्यथा {
            out.appende(slot)
        }
        i ← i + 1
    }
    लौटाओ Area {loculi = out}
}

# Heterogeneous node: stores Manus, never deep-copies the resource payload.
विभेद Nodus {
    Groupus {
        सूची<Manus> filii
    },
    Tessera {
        Manus geometria
    },
}

परीक्षण "two nodes share one resource identity" टैग "identity" {
    स्थिर AreaCumManus step ← area_inserit(area_nova(), "shared-mesh")
    स्थिर Area res ← step.area
    स्थिर Manus geo ← step.manus
    # Reconstruct handle values so each node owns a copy of the identity bits
    # without cloning the resource payload (still one live slot in `res`).
    स्थिर Manus left_geo ← Manus {index = geo.index, generatio = geo.generatio}
    स्थिर Manus right_geo ← Manus {index = geo.index, generatio = geo.generatio}
    पुष्टि manus_aequat(left_geo, right_geo)
    पुष्टि area_accipe(res, left_geo) ≡ "shared-mesh"
    पुष्टि area_accipe(res, right_geo) ≡ "shared-mesh"
    स्थिर Nodus left ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    स्थिर Nodus right ← Tessera(Manus {index = geo.index, generatio = geo.generatio})
    मिलाओ left {
        स्थिति Tessera स्थिर geometria {
            पुष्टि manus_aequat(geometria, left_geo)
        }
        स्थिति Groupus स्थिर filii {
            पुष्टि filii.longitudo() ≡ 0
        }
    }
    मिलाओ right {
        स्थिति Tessera स्थिर geometria {
            पुष्टि manus_aequat(geometria, right_geo)
        }
        स्थिति Groupus स्थिर filii {
            पुष्टि filii.longitudo() ≡ 0
        }
    }
}

परीक्षण "reparent reorder preserves handle identity" टैग "identity" {
    स्थिर AreaCumManus s0 ← area_inserit(area_nova(), "child-a")
    स्थिर AreaCumManus s1 ← area_inserit(s0.area, "child-b")
    स्थिर Area nodi ← s1.area
    स्थिर Manus a ← s0.manus
    स्थिर Manus b ← s1.manus
    चर सूची<Manus> filii ← खाली
    filii.appende(Manus {index = a.index, generatio = a.generatio})
    filii.appende(Manus {index = b.index, generatio = b.generatio})
    # swap order without changing handle identities
    स्थिर Manus first ← filii[0]
    स्थिर Manus second ← filii[1]
    चर सूची<Manus> reord ← खाली
    reord.appende(Manus {index = second.index, generatio = second.generatio})
    reord.appende(Manus {index = first.index, generatio = first.generatio})
    पुष्टि area_accipe(nodi, reord[0]) ≡ "child-b"
    पुष्टि area_accipe(nodi, reord[1]) ≡ "child-a"
    पुष्टि area_accipe(nodi, a) ≡ "child-a"
    पुष्टि area_accipe(nodi, b) ≡ "child-b"
}

परीक्षण "stale handle rejects after remove" टैग "identity" {
    स्थिर AreaCumManus s0 ← area_inserit(area_nova(), "gone")
    स्थिर Manus h ← s0.manus
    स्थिर Manus h_bits ← Manus {index = h.index, generatio = h.generatio}
    पुष्टि area_continet(s0.area, h_bits)
    स्थिर Area after ← area_tollit(s0.area, h_bits)
    पुष्टि area_continet(after, h_bits) ≡ असत्य
    पुष्टि area_accipe(after, h_bits) ≡ ""
    स्थिर AreaCumManus s1 ← area_inserit(after, "fresh")
    स्थिर Manus h2 ← s1.manus
    # New live slot (append); old handle still rejected by generation/vivus.
    पुष्टि manus_aequat(h_bits, h2) ≡ असत्य
    पुष्टि area_accipe(s1.area, h_bits) ≡ ""
    पुष्टि area_accipe(s1.area, h2) ≡ "fresh"
    पुष्टि area_continet(s1.area, h2)
}

आरंभ {
}

---

All examples · Install · Cheat sheet

arena-handle

src/main.fab#

`src/main.fab`#