Agent-Skills.md

Agent Skills: Move-Narya Bridge Skill

Observational bridge between Move smart contracts and Narya proof verification.

UncategorizedID: plurigrid/asi/move-narya-bridge

Repository

plurigrid/asi
plurigridLicense: MIT
165

Install this agent skill to your local

pnpm dlx add-skill https://github.com/plurigrid/asi/tree/HEAD/skills/move-narya-bridge

Skill Files

Browse the full folder contents for move-narya-bridge.

Download Skill

Loading file tree…

skills/move-narya-bridge/SKILL.md

Skill Metadata

Name
move-narya-bridge
Description
Observational bridge between Move smart contracts and Narya proof verification.

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

| Role | Trit | Function | |------|------|----------| | COORDINATOR | 0 | Bridges Move semantics to Narya verification |

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

| Move Concept | Narya Concept | Notes | |--------------|---------------|-------| | struct | sig (record) | Direct mapping | | has store | Linear annotation | Resource tracking | | public fun | def with arrow type | Morphism | | assert! | Proof obligation | Must prove | | #[test] | Example checking | Automatic | | Module | Namespace | Direct |

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

| Field | Definition | |-------|------------| | before | Move module source | | after | Narya translation + proofs | | delta | Proof obligations (holes) | | birth | Empty module stub | | impact | 1 if all proofs complete |

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

| Operation | Expected Time | |-----------|---------------| | Translation (small module) | < 1s | | Type checking | < 1s for small proofs | | Proof search | Seconds to minutes | | Full verification | Depends on proof complexity |

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

Cross-References (Signed Skill Interleaving)

Triad Partners

| Skill | Trit | Role | Color | |-------|------|------|-------| | aptos-gf3-society | +1 | GENERATOR | #8A60CB | | move-narya-bridge | 0 | COORDINATOR | #3A86AF | | move-smith-fuzzer | -1 | VALIDATOR | #BDCA5B |

Conservation: +1 + 0 + (-1) = 0

Move 2.3 Type Translation

| Move Type | Narya Type | Bridge Pattern | |-----------|------------|----------------| | i8 | I8 | Direct mapping | | i32 | I32 | Conservation sums | | Trit | Trit : Type | Structural equality | | vector<Trit> | List Trit | Collection mapping |

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 Seed: 4354685564936970510

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.