Introduction

This is the documentation for [QED Smart Contract Language], a new programming language designed for ["safe and efficient smart contract development"]. This book serves as a comprehensive guide for developers interested in learning the language and building applications with it.

[QED Smart Contract Language] is in active development and a work in progress. If you have feedback or suggestions, feel free to contribute via the GitHub repository.

This book covers the core features of [QED Smart Contract Language], including its syntax, module system, structs, traits, and storage capabilities.

Before We Begin

[QED Smart Contract Language] requires a development environment to write and run programs. This chapter covers the prerequisites: setting up your IDE, installing the compiler, and understanding the basic tools.

If you already have the compiler installed (via git or another method), you can skip to the next chapter.

Installing the Compiler

Download the latest compiler binary from [https://github.com/QEDProtocol/qed-lang]. Binaries are available for macOS, Linux, and Windows.

Using a Package Manager

• Homebrew (macOS): brew install [dargo]
• Chocolatey (Windows): choco install [dargo]
• Cargo (Rust-based, if applicable): cargo install --git https://github.com/QEDProtocol/qed-lang dargo

Setting up environment

set -gx DARGO_STD_PATH "/path-to-qed-lang/qed-std/std.qed"

Setting Up Your IDE

Recommended IDEs:

• VSCode: Install the [QED Smart Contract Language] extension for syntax highlighting.
• IntelliJ IDEA: Use the [QED Smart Contract Language] plugin by [QEDProtocol].

QED LSP Developer Tutorial

QED is a custom language with a dedicated Language Server Protocol (LSP) service, providing basic features such as hover, goto definition, find references, and formatting.

This document introduces how to use the QED language server qed-lsp-server for a better development experience in VSCode, Neovim, and RustRover.

🛠️ Preparation

1. Clone repository:

  git clone https://github.com/QEDProtocol/qedlang-rust.git
  cd qed-lang

2. Compile qed-lsp-server：

  cd qed-lsp-server
  cargo build --release

⚠️ Note: Regardless of which IDE you are using, the qed-lsp-server binary is required for the language features to work properly.
Please make sure you have built it and remember its path.

💻 VSCode Usage Tutorial

Developer debugging mode (recommended for developers)

1. Start VSCode:

  cd qed-lsp-server/qed-lsp-vscode
  code .

2. Press F5 to enter plugin debugging mode. VSCode will start a new VSCode window and load the local plugin.
3. In the new window, open a QED project containing Dargo.toml to enable plugin features, such as:
   • Mouse hover → Show type information
   • Right click → Goto Definition / Find References / Format

💡 Note: In the file qed-lsp-vscode/src/extension.ts, the path to the qed-lsp-server binary is currently hardcoded:

const serverExecutable = path.join(
    // Warning: this path is hardcoded and may not be portable across systems.
    context.extensionPath, '..', '..', 'target', 'release', 'qed-lsp-server'
);

If you need to change the path (for example, to use a different build directory or binary location), please modify this line accordingly and then rebuild the extension by running:

  npm run build

🧑‍💻 Neovim usage tutorial (based on Lazy.nvim)

This guide demonstrates how to set up the QED language server (qed-lsp-server) in Neovim using the lazy.nvim plugin manager.

⚠️ Note: The qed-lsp-server binary must be compiled first and accessible in your system. Ensure the path to the binary is correct.

1️⃣ Plugin Installation

In your init.lua, make sure to install the necessary plugins:

require("lazy").setup({
  { "neovim/nvim-lspconfig" },             -- LSP support
  { "nvim-treesitter/nvim-treesitter", build = ":TSUpdate" }, -- syntax highlighting
  { "hrsh7th/nvim-cmp" },                  -- completion
  { "hrsh7th/cmp-nvim-lsp" },              -- LSP completion source
})

2️⃣ QED LSP Setup via Lazy

local lspconfig = require("lspconfig")
local configs = require("lspconfig.configs")

-- Register custom LSP
if not configs.qed_lsp then
configs.qed_lsp = {
   default_config = {
      cmd = {"/full path/to/qed-lsp-server" }, -- ⚠️ Note to fill in the full path
      filetypes = {"qed"},
      root_dir = lspconfig.util.root_pattern("Dargo.toml"),
      settings = {},
   },
}
end

lspconfig.qed_lsp.setup({})

-- Let Neovim recognize the `.qed` file type
vim.filetype.add({
   extension = {
      qed = "qed",
   },
})

Instead of manually configuring LSP in init.lua, you can configure it via Lazy plugin opts. Create a file like ~/.config/nvim/lua/plugins/lsp.lua and write:

return {
  "neovim/nvim-lspconfig",
  opts = function(_, opts)
    -- Tell Neovim `.qed` files are of type `qed`
    vim.filetype.add({ extension = { qed = "qed" } })

    -- Reuse Rust Tree-sitter highlighting for `.qed` files
    vim.treesitter.language.register("rust", "qed")

    -- Load LSP config
    local lspconfig = require("lspconfig")
    local configs = require("lspconfig.configs")

    -- Register qed_lsp_server only once
    if not configs.qed_lsp_server then
      configs.qed_lsp_server = {
        default_config = {
          cmd = { "/full/path/to/qed-lsp-server" }, -- 🔧 Replace with your built binary
          filetypes = { "qed" },
          root_dir = lspconfig.util.root_pattern("Dargo.toml", ".qed"),
          settings = {},
        },
      }
    end

    -- Attach server config to Lazy's LSP handler
    opts.servers.qed_lsp_server = {}
    return opts
  end,
}

✅ Once you’ve saved this config, reopen Neovim and run :Lazy sync to apply it.

✅ Additional Notes

• vim.filetype.add(...) tells Neovim that .qed files should be handled as the qed filetype.
• vim.treesitter.language.register("rust", "qed") means .qedfiles will reuse Rust’s highlighting engine via Tree-sitter.
• Make sure the qed-lsp-server binary is either in your PATH or referenced using the full path.

3️⃣ Navigation & Reference Lookup in Neovim

Once your qed-lsp-server is properly registered and running in Neovim, you can use the following built-in LSP keybindings to navigate your QED code efficiently.

-- Place these in your init.lua or keymap config file if not already present
vim.keymap.set("n", "gd", vim.lsp.buf.definition, { noremap = true, desc = "Go to Definition" })
vim.keymap.set("n", "gr", vim.lsp.buf.references, { noremap = true, desc = "Find References" })
vim.keymap.set("n", "K", vim.lsp.buf.hover, { noremap = true, desc = "Hover Documentation" })
vim.keymap.set("n", "<leader>rn", vim.lsp.buf.rename, { noremap = true, desc = "Rename Symbol" })
vim.keymap.set("n", "<leader>f", vim.lsp.buf.format, { noremap = true, desc = "Format Document" })

📚 Common shortcut keys description

⚙️ RustRover usage tutorial (based on LSP4IJ plugin)

This tutorial assumes that you have already completed the configuration of Rust in RustRover.

We will use the LSP plugin LSP Support (lsp4ij) provided by RedHat to enable custom LSP support for .qed files, realizing functions such as jump, hover, reference lookup, code formatting, etc.

📦 Step 1: Install the LSP4IJ plugin

1. Open RustRover and click RustRover > Settings in the upper left corner (or use the shortcut Cmd + ,).
2. Go to Plugins > Marketplace.
3. Search for lsp4ij .
4. Click Install and restart the IDE after the installation is complete.

✅ Step 2: Create a QED file type

1. Open Settings → Editor → File Types

2. Click "+" Add at the top to create a new File Type

3. Name: QED

4. Description: QED language

5. Configure highlighting (optional) fill in the following fields:

Then click Save.

🧠 Step 3: Configure the Language Server of QED language

Open Settings > Languages && Frameworks > Language Servers, we need to add a new configuration, click the plus sign ➕, there are three tabs in the new interface: Server, Mapping and Configuration.

▶️ Server tab

Used to register a new LSP service.

• Name: Fill in QED language server.
• Environment Variables: Leave it blank (optional, if you need to set DARGO_STD_PATH, you can fill it in here).
• Command: Fill in the path of your compiled LSP executable file, for example: /Users/UserName/bin/qed-lsp-server

▶️ Mapping tab

Used to map file types to language services.

• Language: Leave it blank.
• FileType: Click ➕, select QED on the left, and enter qed on the right
  • Note: If there is no QED option, please go back to step 2 and add the file type again.
• Filename Patterns: Click ➕, enter *.qed on the left, and enter qed on the right

📌 Note:

• The left side is the file type inside the IDE .
• The right side is the Language ID of the LSP Server, which needs to match your textDocument.languageId

▶️ Configuration (optional)

You can set:

• Server Trace Level: Set to Verbose to view more debugging information

• Client Trace Level: Set to Verbose or Info

• To view LSP communication logs, it is recommended to open the LSP Console view

✅ Step 4: Verify if it works

1. Open a QED project with Dargo.toml
2. Open the .qed file
3. You can try:

• Hover to view the type
• Go to Definition
• Find References
• Format Document

You can check the debug log in View > Tool Windows > LSP Console to confirm whether LSP is started correctly.

Setting up Shell Completions

Shell completions allow you to use the Tab key to autocomplete commands, options, and arguments when working with the QED CLI tools. This makes development faster and more convenient.

This guide will help you set up shell completions for the Dargo CLI.

Zsh Completions

You can add the completions script to your Zsh completions directory:

# Create the completions directory if it doesn't exist
mkdir -p ~/.zsh/completions

# Generate and save the completion script
dargo complete zsh > ~/.zsh/completions/_dargo

# Add the directory to your fpath in ~/.zshrc if you haven't already
echo 'fpath=(~/.zsh/completions $fpath)' >> ~/.zshrc
echo 'autoload -U compinit && compinit' >> ~/.zshrc

# Reload your shell
source ~/.zshrc

Bash Completions

You can add the completions script to your Bash environment in a few ways:

If you have bash-completion installed:

# Generate and save the completion script to the bash-completion directory
dargo complete bash > /usr/local/etc/bash_completion.d/dargo

Without bash-completion, you can add it to your profile:

# Create a completions directory if you don't have one
mkdir -p ~/.bash_completions

# Generate and save the completion script
dargo complete bash > ~/.bash_completions/dargo.bash

# Add the following line to your ~/.bash_profile or ~/.bashrc
echo 'source ~/.bash_completions/dargo.bash' >> ~/.bashrc

# Reload your shell
source ~/.bashrc

Fish Completions

For Fish shell users, you can easily set up completions:

# Generate and save the completion script to the Fish completions directory
dargo complete fish > ~/.config/fish/completions/dargo.fish

No additional steps are needed as Fish automatically loads completions from this directory.

Verifying Completions

To verify that completions are working correctly, type dargo followed by a space and press Tab. You should see a list of available commands.

Try:

dargo <TAB>

You should see a list of commands like new, build, compile, etc.

Troubleshooting

If completions aren't working:

1. Make sure you've restarted your terminal or sourced your .zshrc file
2. Check that the dargo complete zsh command works and produces output
3. Verify that the path to the completion script is correct
4. Ensure that Zsh completions are enabled in your shell configuration

Hello, World!

This chapter walks you through creating your first [QED Smart Contract Language] program.

Creating a New Program

Create a new project:

dargo new hello_world

fn main(x: Felt, y: Felt) {
    assert(x == y, "x != y");
}

#[test]
fn test_main() {
    main(1, 1);

    // Uncomment to make test fail
    // main(1, 2);
}

Compiling

run the program using the compiler:

dargo compile

You will see a target directory. Open the hello_world.json inside and you'll be able to see the target code for qed. The qed smart contract language generates this code for each function in the contract and deploys it to the blockchain.

[
    {
        "name": "main",
        "method_id": 680917438,
        "circuit_inputs": [
            0,
            1
        ],
        "circuit_outputs": [],
        "state_commands": [],
        "state_command_resolution_indices": [],
        "assertions": [
            {
                "left": 4294967296,
                "right": 4294967297,
                "message": "x != y"
            }
        ],
        "definitions": [
            {
                "data_type": 0,
                "index": 0,
                "op_type": 0,
                "inputs": [
                    0
                ]
            },
            {
                "data_type": 0,
                "index": 1,
                "op_type": 0,
                "inputs": [
                    1
                ]
            },
            {
                "data_type": 1,
                "index": 0,
                "op_type": 13,
                "inputs": [
                    0,
                    1
                ]
            },
            {
                "data_type": 1,
                "index": 1,
                "op_type": 2,
                "inputs": [
                    1
                ]
            }
        ]
    }
]

Running

Basic Syntax

[QED Smart Contract Language] uses a syntax inspired by [Rust]. Here are the basics:

Variables

Variables are declared with let and can be mutable with mut:

#![allow(unused)]
fn main() {
let a: Felt = 1;
let mut b: Felt = 2;
b += 1;

}

Comments

Use // for single-line comments: Use /* */ for single-line comments:

#![allow(unused)]
fn main() {
// This is a comment
let a: Felt = 1;
}

Types

• Felt: A goldilocks field type.
• bool: Boolean type.
• u32: 32-bit unsigned integer.
• Array
• Tuple
• Struct

Modules and Visibility

Modules organize code and control visibility.

Defining a Module

#![allow(unused)]
fn main() {
mod math {
    pub fn max(a: Felt, b: Felt) -> Felt {
        return a * ((a > b) as Felt) + b * ((a <= b) as Felt);
    }
}
}

Using Modules

use math::*;
fn main() -> Felt {
    max(1, 2)
}

Visibility

pub: Makes an item public.
No modifier: Private to the module.

Structs and Implementations

Structs define custom data types, and impl blocks add methods.

Defining a Struct

#![allow(unused)]
fn main() {
struct Person {
    pub age: Felt,
    male: bool,
}

}

Implementing Methods

#![allow(unused)]
fn main() {
impl Person {
    pub fn get_age(self: Person) -> Felt {
        return self.age;
    }
}
}

Usage

fn main() -> Felt {
    let p: Person = new Person { age: 20, male: true };
    p.get_age()
}

Traits and Generics

Traits define shared behavior, and generics allow type flexibility.

Defining a Trait

#![allow(unused)]
fn main() {
pub trait Value {
    pub fn value() -> Felt;
}
}

Implementing a Trait

#![allow(unused)]
fn main() {
struct Two {}
impl Value for Two {
    pub fn value() -> Felt {
        2
    }
}

fn get_value<T: Value>(value: T) -> Felt {
    T::value()
}
}

Storage and Contracts

[QED Smart Contract Language] supports storage for persistent state, useful for blockchain applications.

Defining a Contract

#[storage]
struct Contract {
}

impl Contract {
    pub fn simple_mint(amount: Felt) -> Felt {
        let self_user_leaf: Hash = get_state_hash_at(get_user_id());
        let current_balance: Felt = self_user_leaf[0];
        let new_balance: Felt = current_balance + amount;
        cset_state_hash_at(get_user_id(), [new_balance, self_user_leaf[1], self_user_leaf[2], self_user_leaf[3]]);
        new_balance
    }
}

Explanation

#[storage]: Marks a struct for persistent storage. get_state_hash_at: Retrieves state. cset_state_hash_at: Updates state.

Control Flow

If Statements

#![allow(unused)]
fn main() {
fn min(a: Felt, b: Felt) -> Felt {
    if a < b {
        a
    } else {
        b
    }
}
}

While Loops

fn main() -> Felt {
    let mut res: Felt = 0;
    let mut i: Felt = 0;
    while i < 10 {
        res += i;
        i += 1;
    }
    res
}

Match Expressions

#![allow(unused)]
fn main() {
fn match_test_case(input: Felt) -> Felt {
    match input {
        0 => 10,
        1 => 20,
        _ => 30,
    }
}
}

Functions and Closures

Functions

#![allow(unused)]
fn main() {
fn add(a: Felt, b: Felt) -> Felt {
    a + b
}
}

Closures

fn main() -> Felt {
    let max = |a: Felt, b: Felt| -> Felt {
        a * ((a > b) as Felt) + b * ((a <= b) as Felt)
    };
    max(1, 2)
}

Arrays and Tuples

Arrays

fn main() -> Felt {
    let arr: [Felt; 2] = [1, 2];
    arr[0]
}

Tuples

fn main() -> Felt {
    let t: (Felt, Felt) = (1, 2);
    t.0 + t.1
}

Testing

Tests are written within modules using the #[test] attribute.

#![allow(unused)]
fn main() {
mod math {
    pub fn min(a: Felt, b: Felt) -> Felt {
        a * ((a < b) as Felt) + b * ((a >= b) as Felt)
    }
    mod math_tests {
        use super::*;
        #[test]
        fn test_min() {
            assert(min(2, 3) == 2, "min(2, 3) == 2");
        }
    }
}
}

run tests with [dargo] test.

Appendix A: Glossary

• Felt: A numeric type, likely an integer.
• Hash: A fixed-size array used for state storage.
• Storage: Persistent state management for contracts.

Appendix B: Reserved Keywords

• fn, pub, mod, use, struct, impl, trait, let, mut, if, else, while, match, return, assert, assert_eq

Appendix C: Publications

Appendix D: Contributing

To contribute, submit a pull request to the [GitHub repository]. The source files are in mdBook format.

Appendix E: Acknowledgements