Validity is a next-generation, deduction-based language for formally verified, context-aware, autonomous & reactive smart contracts.

Overview

Validity Language

Validity is a next-generation, deduction-based language for formally verified, context-aware, autonomous & reactive smart contracts.

Validity is designed for smart contracts over the generalized UTXOs (called "Cells") of Nervos Network's Common Knowledge Base (CKB).

Validity is a very early stage language under active development. Currently, there are three subdirectories of interest:

  1. validity-athena contains a formal specification of Validity's syntax and semantics using the Athena proof assistant.
  2. validity-proof provides a Rust implementation of Validity's natural deduction language.
  3. validity-compute provides a Rust implementation of Validity that extends the proof language with a higher order functional language for computing expressions.

Validity programs have two required sections: Spec and Contract.

  • Spec defines a set of "operations" that that the smart contract supports. It associates a textual label with a "forall-exists" style Horn clause. The set of operations define constraints over a transaction.
  • Contract defines a set of guarantees and useful invariants about the smart contract, in the form of deductive proofs. It provides a way for a smart contract developer to publish important properties about their contract, making it easier for other contracts to interact with it in a defensive and safe manner.

Formula in Validity can specify properties over a state change, which is a triple of the form $(Prev, Next, Meta)$ . This maps directly to the structure of transactions on UTXO-style chains.

Underlying Theory

The soundness guarantees of Validity's logic owes to the fact that it belongs to a class of languages called Denotational Proof Languages (DPL). DPL's are well suited for CKB because they can provide soundness guarantees without complicated type systems, which makes evaluation much faster. Further, due to the fact that DPL's include an Assumption Base in their execution context, code size can be kept small as well (which is important for contracts deployed on CKB, since storage size is the scarce resource as opposed to computation).

DPLs can produce and check proof certificates, which are fully static representations of deductions. These can be generated off-chain and embedded within a Cell-based transaction's witnesses field, enabling contracts to enforce sophisticated and relational properties at runtime without adding significant compute cycles to the on-chain execution.

Example: SUDT

Below is an example of a smart contract for a simple user defined fungible token. It is compliant with the SUDT token standard on Nervos Network.


// A function over a list of byte sequences 
fn tokens: [List(Bytes)] -> [List(Bytes)] {
    tokens(nil) := nil;
    (tokens(?x:Bytes :: rest) :=  (check? {
                (is_self_token(?x)) ==> ?x :: tokens(rest)
                | else ==> tokens(rest)
    });
}


fn balance: [Bytes] -> Nat {
    balance(?b:Bytes) := (check? {
        (length(?b:Bytes) >= 16) ==> uint128_le(?b[0..16]))
        | else ==> 0
    });
}

// a function over a list of byte sequences that returns a list of tuples of (hash_string, number)
// such for each token, hash_string is a lock_hash of a bag of tokens and number is the total sum of the balances
// of the bags in the list owned by that lock_hash

fn balances: [List(Bytes)] -> [(Bytes, Nat)] {
    
}

Spec {
    mint {
        (forall ?p:Prev ?n:Next .   sum(balance(?p)) < sum(balance(?n)) ==> exists ?o:Bytes . 
            and( 
                in(?o, ?p),
                lock_hash(?0) = slice(args(), 0, 32) 
            )
        )
    }

    transfer {
        (forall ?p:Prev ?n:Next .  
            and(
                balances(tokens(?p)) =/= balances(tokens(?n)),
                len(balances(tokens(?p))) = len(balances(tokens(?n))) 
            ) ==> sum(balance(?p)) = sum(balance(?n))
        )
    }

    burn {
        (forall ?p:Prev ?n:Next .  
            len(balances(tokens(?p))) < len(balances(tokens(?n))) ==> sum(balance(?p)) < sum(balance(?n))
        )
    }
}



Contract {

// Case analysis over Spec...
// When case analysis is performed over the Spec, the axioms of each operation (mint, transfer and burn in this case)
// are already added to the assumption base.
// The antecedent of each clause (i.e., the guard clause) must be assumed. Then, the stated conclusion must be proven from the
// assumption of each guard clause


// The below proof states that for any state change, the sum of the balances in the prev state is less than or equal to the sum of the
// balances in the next state. I.e., that a single step preserves this property.
// It does *not* prove that this is true for a possibly infinite *sequence* of state changes (many steps) preserves this property.
// Such a safety property can be proved by induction over a list of (Prev, Next) tuples 

    conclude conservation_of_tokens_in_single_step := (forall ?p:Prev ?n:Next . sum(balance(?p)) <= sum(balance(?n))) {
        pick-any ?p:Prev, ?n:Next {
            (!cases Spec
                (!chain [
                        (sum(balance(?p)) < sum(balance(?n))) 
                    ==> (sum(balance(?p)) <= sum(balance(?n)))                          [(forall ?n:Nat ?m:Nat . ?n < ?m ==> ?n <= ?m)]
                ]),

                (!chain [
                        (and
                            (balances(tokens(?p)) =/= balances(tokens(?n)), 
                            (len(balances(tokens(?p))) = len(balances(tokens(?n))))
                        ) 
                    ==> sum(balance(?p)) = sum(balance(?n))                             [transfer]
                    ==> sum(balance(?p)) <= sum(balance(?n))                            [(forall ?n:Nat ?m:Nat . ?n = ?m ==> ?n <= ?m)]
                ]),

                (!chain [
                        (len(balances(tokens(?p))) < len(balances(tokens(?n))))
                    ==> sum(balance(?p)) < sum(balance(?n))                             [burn]
                    ==> (sum(balance(?p)) <= sum(balance(?n)))                          [(forall ?n:Nat ?m:Nat . ?n < ?m ==> ?n <= ?m)]
                ])
                
            )
        } 
    }
    
}

You might also like...
A framework for creating PoC's for Solana Smart Contracts in a painless and intuitive way

Solana PoC Framework DISCLAIMER: any illegal usage of this framework is heavily discouraged. Most projects on Solana offer a more than generous bug bo

My code for the terra.academy course on CosmWasm smart contracts

CosmWasm Starter Pack This is a template to build smart contracts in Rust to run inside a Cosmos SDK module on all chains that enable it. To understan

Smart contracts powering Spectrum Protocol on Terra

Spectrum Core Contracts This monorepository contains the source code for the core smart contracts implementing Spectrum Protocol on the Terra blockcha

A template to build smart contracts in Rust to run inside a Cosmos SDK module on all chains that enable it.

CosmWasm Starter Pack This is a template to build smart contracts in Rust to run inside a Cosmos SDK module on all chains that enable it. To understan

Create your personal token with rust smart contracts

Solana Rust Token 💰 This application written Rust using Anchor ⚓

This is a node implementation of Thippy, a Substrate parachain for smart contracts

Thippy ‒- A Smart Contracts Parachain This is a node implementation of Thippy, a Substrate parachain for smart contracts. Developing Smart Contracts f

Rust library for build smart contracts on Internet Computer, by the Spinner.Cash team.

Spinner Rust library for building smart contracts on the Internet Computer. More specifically it is used by Spinner.Cash, a decentralized layer-2 prot

Rust implementation for Thippy -- a Substrate parachain for smart contracts.

Thippy ‒- A Smart Contracts Parachain This is a node implementation of Thippy, a Substrate parachain for smart contracts. Developing Smart Contracts f

Helpful functions and macros for developing smart contracts on NEAR Protocol.

near-contract-tools Helpful functions and macros for developing smart contracts on NEAR Protocol. This package is a collection of common tools and pat

Owner
Tempest Labs
Tempest Labs
Next-generation implementation of Ethereum protocol ("client") written in Rust, based on Erigon architecture.

?? Martinez ?? Next-generation implementation of Ethereum protocol ("client") written in Rust, based on Erigon architecture. Why run Martinez? Look at

Arthur·Thomas 23 Jul 3, 2022
L2 validity rollup combined with blind signatures over elliptic curves inside zkSNARK, to provide offchain anonymous voting with onchain binding execution on Ethereum

blind-ovote Blind-OVOTE is a L2 voting solution which combines the validity rollup ideas with blind signatures over elliptic curves inside zkSNARK, to

Aragon ZK Research 3 Nov 18, 2022
A "Type 0" zkEVM. Prove validity of Ethereum blocks using RISC Zero's zkVM

zeth NEW: Zeth now supports Optimism blocks! Just pass in --network=optimism! Zeth is an open-source ZK block prover for Ethereum built on the RISC Ze

RISC Zero 222 Oct 26, 2023
CYFS:Next Generation Protocol Family to Build Web3

CYFS is the next-generation technology to build real Web3 by upgrading the basic protocol of Web (TCP/IP+DNS+HTTP). It has a subversive architectural design that everyone brings their own OOD (Owner Online Device) to form a truly decentralized network.

CYFS Core Dev Team 2k Jul 6, 2023
A gRPC-based scripting library for interacting with CosmWasm smart-contracts.

Cosmos Rust Script Smart contract scripting library to ease CosmWasm smart contract development and deployment. cosm-script is inspired by terra-rust-

null 11 Nov 3, 2022
evm2near compiles Solidity contracts into NEAR WebAssembly contracts.

EVM → NEAR evm2near is a project for compiling EVM bytecode into wasm bytecode, with the particular goal of having that wasm artifact be executable on

Aurora 125 Dec 3, 2022
Ticketed Discreet Log Contracts (DLCs) to enable instant buy-in for wager-like contracts on Bitcoin.

dlctix Ticketed Discreet Log Contracts (DLCs) to enable instant buy-in for wager-like contracts on Bitcoin. This project is part of the Backdrop Build

null 7 Feb 29, 2024
Smart contracts for Ref Finance

Ref Finance Contracts This mono repo contains the source code for the smart contracts of Ref Finance on NEAR. Contracts Contract Reference Description

Ref Finance 92 Dec 7, 2022
Skyward Finance smart-contracts

Build and Init ./build.sh near dev-deploy res/skyward.was export CONTRACT_ID=skyward.testnet near call $CONTRACT_ID new --account_id=$CONTRACT_ID Regi

Skyward Finance 777 Jan 4, 2023
Rust client to Opensea's APIs and Ethereum smart contracts

opensea.rs Rust bindings & CLI to the Opensea API and Contracts CLI Usage Run cargo r -- --help to get the top level help menu: opensea-cli 0.1.0 Choo

Georgios Konstantopoulos 226 Dec 27, 2022