Documentation

LeanPool.PureNock.ModularEval

Modular (field-noun) evaluation #

The paper's nouns are field-valued: leaves carry elements of a field ๐”ฝ (main.tex:345โ€“349, 1023) and the increment operator reduces modulo the characteristic, +(n) = (1 + n) mod p (main.tex:1531โ€“1534). The Nat-level reference evalN (Nock/Reference.lean) instead uses the unbounded successor n โ†ฆ n + 1.

This module makes the modulus-generic embedding precise over Nat-atom nouns, parameterized by an arbitrary modulus q (so it never needs a concrete prime and never declares a project axiom). It defines:

Everything is q-generic; the ZMod injectivity fact zmod_natCast_inj_of_lt requires no primality assumption. Axioms stay within {propext, Classical.choice, Quot.sound}.

Field nouns: bounded leaf labels #

source
def Nock.FieldEmbedding.BoundedBy (q : โ„•) :
Noun โ†’ Prop

BoundedBy q n means that every atom (leaf) of n is in the numeric range [0,q). This is the bound needed when the operative modulus varies with a security parameter.

Equations
Instances For
    source
    @[simp]
    theorem Nock.FieldEmbedding.BoundedBy_atom {q n : โ„•} :
    BoundedBy q (Noun.atom n) โ†” n < q
    source
    @[simp]
    theorem Nock.FieldEmbedding.BoundedBy_cell {q : โ„•} {l r : Noun} :
    BoundedBy q (l.cell r) โ†” BoundedBy q l โˆง BoundedBy q r

    The field increment +(n) = (1 + n) mod q (main.tex:1531โ€“1534) #

    source
    def Nock.FieldEmbedding.lusFBy (q : โ„•) :
    Noun โ†’ Option Noun

    Increment modulo q on an atom, crash on a cell.

    Equations
    Instances For
      source
      def Nock.FieldEmbedding.lusGBy (q : โ„•) :
      Noun โ†’ Option Noun

      Guarded Nat increment: like Noun.lus (n โ†ฆ n+1) but crashes instead of overflowing the selected range, i.e. it refuses to produce an atom โ‰ฅ q. A successful guarded run witnesses that no increment reached q โ€” this is how the no-overflow side condition is encoded honestly.

      Equations
      Instances For

        The field-valued evaluator evalFBy #

        evalFBy q is Nock.evalN verbatim EXCEPT that OPโ‚„ (+) uses increment modulo q. All other operators are structural (they only rearrange existing leaves) or produce the constants 0/1, so over field nouns they coincide with the Nat versions; hence evalFBy reuses Noun.slot, Noun.edit, Noun.wut, Noun.tis from Nock/Reference.lean. Equality (OPโ‚…, main.tex:1525) compares nouns structurally; over q-bounded nouns this is field equality (distinct < q atoms are distinct in ZMod q).

        source
        def Nock.FieldEmbedding.evalFBy (q : โ„•) :
        โ„• โ†’ Noun โ†’ Noun โ†’ Option Noun

        Fuel-indexed Nock evaluation with increment reduced modulo the supplied modulus.

        Equations
        Instances For

          The guarded (no-overflow) evaluator evalGBy #

          evalGBy q is Nock.evalN verbatim EXCEPT that OPโ‚„ uses lusGBy q, which crashes on overflow.

          source
          def Nock.FieldEmbedding.evalGBy (q : โ„•) :
          โ„• โ†’ Noun โ†’ Noun โ†’ Option Noun

          Fuel-indexed Nock evaluation that rejects increments reaching the supplied modulus.

          Equations
          Instances For

            BoundedBy is preserved by the structural operators #

            source
            theorem Nock.FieldEmbedding.slot_boundedBy (q ax : โ„•) (n : Noun) :
            BoundedBy q n โ†’ โˆ€ {m : Noun}, Noun.slot ax n = some m โ†’ BoundedBy q m

            slot returns a subtree of n, so it preserves every numeric leaf bound.

            source
            theorem Nock.FieldEmbedding.edit_boundedBy (q ax : โ„•) (new old : Noun) :
            BoundedBy q new โ†’ BoundedBy q old โ†’ โˆ€ {m : Noun}, Noun.edit ax new old = some m โ†’ BoundedBy q m

            edit grafts new into old, so it preserves every numeric leaf bound.

            source
            theorem Nock.FieldEmbedding.lusFBy_bounded {q : โ„•} (hq : 0 < q) {x m : Noun} (h : lusFBy q x = some m) :
            BoundedBy q m

            Increment modulo a positive q always produces an atom < q.

            source
            theorem Nock.FieldEmbedding.wut_boundedBy {q : โ„•} (hq : 1 < q) (x : Noun) :
            BoundedBy q x.wut
            source
            theorem Nock.FieldEmbedding.tis_boundedBy {q : โ„•} (hq : 1 < q) (a b : Noun) :
            BoundedBy q (a.tis b)

            Main agreement lemma (the no-overflow simulation) #

            agreeBy is proved by induction on fuel. Its conclusion bundles the three facts that must be carried through the recursion simultaneously:

            The ONLY place the three evaluators differ is OPโ‚„ (+): there evalGBy q succeeds exactly when n + 1 < q, and under that guard the Nat increment (n+1) and the modular increment ((n+1) mod q) coincide โ€” this is where no-overflow discharges the divergence.

            source
            theorem Nock.FieldEmbedding.agreeBy (q : โ„•) (hq : 1 < q) (fuel : โ„•) (s f r : Noun) :
            BoundedBy q s โ†’ BoundedBy q f โ†’ evalGBy q fuel s f = some r โ†’ evalN fuel s f = some r โˆง evalFBy q fuel s f = some r โˆง BoundedBy q r

            The guarded evaluator refines evalN: the guard only removes behaviours #

            source
            theorem Nock.FieldEmbedding.evalGBy_le_evalN {q : โ„•} (hq : 1 < q) {fuel : โ„•} {s f r : Noun} (hs : BoundedBy q s) (hf : BoundedBy q f) (h : evalGBy q fuel s f = some r) :
            evalN fuel s f = some r

            The no-overflow agreement theorem #

            source
            theorem Nock.FieldEmbedding.noOverflow_agreeBy {q : โ„•} (hq : 1 < q) {fuel : โ„•} {s f r : Noun} (hs : BoundedBy q s) (hf : BoundedBy q f) (hno : evalGBy q fuel s f = some r) :
            evalN fuel s f = some r โˆง evalFBy q fuel s f = some r โˆง BoundedBy q r

            No-overflow agreement. For q-bounded inputs, a successful guarded run contains no modular wrap at q, so the Nat and modulo-q evaluators return the same q-bounded noun.

            The modular evaluator is a field-noun endomorphism #

            Unconditionally (no guard): on q-bounded inputs, every successful modular run returns a q-bounded noun. evalFBy q maps canonical field nouns to canonical field nouns โ€” its OPโ‚„ increment is (n+1) mod q < q, and every other opcode only rearranges existing (bounded) leaves or produces 0/1.

            source
            theorem Nock.FieldEmbedding.evalFBy_boundedBy {q : โ„•} (hq : 1 < q) (fuel : โ„•) (s f r : Noun) :
            BoundedBy q s โ†’ BoundedBy q f โ†’ evalFBy q fuel s f = some r โ†’ BoundedBy q r

            ZMod q representative-level injectivity #

            On q-bounded nouns the structural Nock equality used by OPโ‚… (main.tex:1525) coincides with field equality in ZMod q: distinct canonical residues < q stay distinct. Primality is not needed for this representative-level fact.

            source
            theorem Nock.FieldEmbedding.zmod_natCast_inj_of_lt {q m n : โ„•} (hm : m < q) (hn : n < q) (h : โ†‘m = โ†‘n) :
            m = n

            The Nat cast into ZMod q is injective on canonical representatives [0,q).