Move-Narya Bridge Skill

"Observational equality turns axioms into theorems. Bridge types connect worlds."

Overview

The Move-Narya Bridge translates Move smart contract invariants into Narya's Higher Observational Type Theory (HOTT) for formal verification. Unlike traditional approaches that require axioms for function extensionality, Narya makes this definitional.

Key Insight: Move's resource type system maps naturally to Narya's linear-like resource tracking, while GF(3) conservation laws become observational equalities.

GF(3) Assignment

Denotation

This skill translates Move module specifications into Narya proof obligations, leveraging observational equality for automatic function extensionality.

Bridge : MoveSpec → NaryaTheorem
Verify : NaryaTheorem → Result
Invariant: ∀ spec ∈ MoveSpec: well_typed(spec) ⟹ provable(Bridge(spec))

The Three-Level Architecture

┌─────────────────────────────────────────────────────────────────┐
│ Level 3: Narya HOTT                                             │
│   - Observational equality (Id types per structure)             │
│   - Bridge types for parametricity                              │
│   - Definitional η-laws                                         │
├─────────────────────────────────────────────────────────────────┤
│ Level 2: Move-Narya Bridge (THIS SKILL)                         │
│   - Translate Move structs → Narya records                      │
│   - Translate Move functions → Narya morphisms                  │
│   - Translate invariants → proof obligations                    │
├─────────────────────────────────────────────────────────────────┤
│ Level 1: Move Smart Contracts                                   │
│   - Resource types (linear)                                     │
│   - Module specifications                                       │
│   - GF(3) trit annotations                                      │
└─────────────────────────────────────────────────────────────────┘

Translation Rules

Move Struct → Narya Record

// Move
struct Trit has store, copy, drop {
    value: i8,
}

-- Narya
def Trit : Type := sig (
  value : I8
)

-- Observational equality for Trit (automatic!)
-- Id(Trit)(t1, t2) ≡ Id(I8)(t1.value, t2.value)

Move Function → Narya Morphism

// Move
public fun add(a: Trit, b: Trit): Trit {
    Trit { value: normalize(a.value + b.value) }
}

-- Narya
def add : Trit → Trit → Trit :=
  λ a b. (value := normalize (a.value + b.value))

-- Function extensionality is DEFINITIONAL:
-- If ∀ x. f x = g x, then f = g (no axiom needed!)

GF(3) Conservation → Proof Obligation

// Move invariant
// assert!(sum % 3 == 0, E_CONSERVATION_VIOLATED);

-- Narya theorem
def conservation : (trits : List Trit) →
  Id(I32)(mod (sum (map value trits)) 3, 0) :=
  -- Proof term here

Bridge Types for GF(3)

Narya's bridge types provide "baby equality" without full symmetry/transitivity. This maps perfectly to GF(3) role relationships:

-- Bridge type: GENERATOR and VALIDATOR are related through COORDINATOR
def gf3_bridge : Br(Trit) plus minus :=
  -- Bridge through ergodic
  comp_bridge (bridge_to_ergodic plus) (bridge_from_ergodic minus)

-- The roles are related but not equal
-- This captures the asymmetry of the triad

Verification Workflow

# 1. Extract Move module specification
just move-spec-extract sources/gf3_move23.move > gf3.spec

# 2. Translate to Narya
just move-narya-translate gf3.spec > gf3.narya

# 3. Type-check in Narya
narya check gf3.narya

# 4. Generate proof obligations
narya holes gf3.narya

# 5. Fill proofs interactively
narya interactive gf3.narya

Key Translations

struct

sig

has store

public fun

def

assert!

#[test]

Example: GF(3) Module Translation

Input (Move)

module plurigrid::gf3 {
    struct Trit has store, copy, drop {
        value: i8,
    }

    const MINUS: i8 = -1;
    const ERGODIC: i8 = 0;
    const PLUS: i8 = 1;

    public fun add(a: Trit, b: Trit): Trit {
        Trit { value: normalize(a.value + b.value) }
    }

    public fun is_conserved(trits: &vector<Trit>): bool {
        let sum: i32 = 0;
        // ... compute sum
        sum % 3 == 0
    }
}

Output (Narya)

-- GF(3) Balanced Ternary in Narya HOTT
-- Auto-translated by move-narya-bridge

section GF3

def I8 : Type := -- primitive signed 8-bit

def Trit : Type := sig (
  value : I8,
  valid : Id(Bool)(and (leq (neg 1) value) (leq value 1), true)
)

def MINUS : Trit := (value := neg 1, valid := refl)
def ERGODIC : Trit := (value := 0, valid := refl)
def PLUS : Trit := (value := 1, valid := refl)

-- Addition with normalization
def normalize : I8 → I8 := λ v.
  if (gt v 1) then (sub v 3)
  else if (lt v (neg 1)) then (add v 3)
  else v

def add : Trit → Trit → Trit := λ a b.
  let raw := add_i8 a.value b.value in
  (value := normalize raw, valid := normalize_preserves_valid raw)

-- Conservation theorem (PROOF OBLIGATION)
def conservation : (trits : List Trit) →
  Id(I32)(mod (sum_trits trits) 3, 0) :=
  {? conservation_proof ?}  -- Hole to fill

-- Bridge types for role relationships
def generator_validator_bridge : Br(Trit) PLUS MINUS :=
  bridge_via ERGODIC

end GF3

Narya Compatibility Fields

before

after

delta

birth

impact

GF(3) Triad Integration

move-narya-bridge (0) ⊗ move-smith-fuzzer (-1) ⊗ aptos-governance (+1) = 0 ✓
move-narya-bridge (0) ⊗ narya-proofs (-1) ⊗ movemate-launchpad (+1) = 0 ✓
move-narya-bridge (0) ⊗ sheaf-cohomology (-1) ⊗ gf3-conservation (+1) = 0 ✓

Why Observational Equality Matters

Traditional (Axiom-based)

-- Agda: Need postulate
postulate
  funext : {A : Set} {B : A → Set} {f g : (x : A) → B x}
         → ((x : A) → f x ≡ g x) → f ≡ g

Narya (Observational)

-- Narya: Function extensionality is DEFINITIONAL
-- Id(A → B)(f, g) ≡ (x : A) → Id(B)(f x, g x)

-- So if we prove ∀ x. f x = g x, we immediately have f = g
-- No postulate, no axiom, no appeal to univalence

This matters for GF(3) because:

• add(a, b)

  and

  add(b, a)

  are equal if equal pointwise
• Conservation is preserved under function composition
• Bridge types give internal parametricity

Commands

# Translate Move module to Narya
just move-narya MODULE.move

# Check Narya translation
just narya-check MODULE.narya

# List proof obligations (holes)
just narya-holes MODULE.narya

# Interactive proof session
just narya-prove MODULE.narya

# Verify GF(3) conservation in Narya
just narya-verify-gf3 MODULE.narya

Performance Notes

Narya is research-grade, not production. Use for:

• Prototyping verification approaches
• Understanding observational equality
• Research into GF(3) formal semantics

For production verification, consider Lean 4 or Coq after prototyping in Narya.

References

• Narya Repository
• Towards an Implementation of HOTT
• Move Language Spec
• GF(3) Move 2.3 Module

Cross-References (Signed Skill Interleaving)

Triad Partners

aptos-gf3-society

#8A60CB

move-narya-bridge

#3A86AF

move-smith-fuzzer

#BDCA5B

Conservation:

+1 + 0 + (-1) = 0

Move 2.3 Type Translation

i8

I8

i32

I32

Trit

Trit : Type

vector<Trit>

List Trit

Related ERGODIC Skills

• datalog-fixpoint

  — Query coordination

• structured-decomp

  — Decomposition coordination

• acset-taxonomy

  — Schema coordination

• triadic-skill-orchestrator

  — Dispatch coordination

Interleaving Index

Position: Worker 2, Sweep 1 Hex:

#3A86AF

Skill Name: move-narya-bridge Type: Verification Bridge / Proof Translation Trit: 0 (ERGODIC - COORDINATOR) GF(3): Coordinates between Move execution (+1) and Narya verification (-1)

Autopoietic Marginalia

The interaction IS the skill improving itself.

Every use of this skill is an opportunity for worlding:

• MEMORY (-1): Record what was learned
• REMEMBERING (0): Connect patterns to other skills
• WORLDING (+1): Evolve the skill based on use

Add Interaction Exemplars here as the skill is used.