Format7 tooling

nonos-sync commented

2026-10-03 19:22:34 -04:00

Member

Opened on GitHub by eKisNonos as pull request 73. Review and merge happen there while this repository is kept in step from GitHub; this copy follows it, and is marked merged or closed when it is.

Opened on GitHub by eKisNonos as [pull request 73](https://github.com/NON-OS/zkolang/pull/73). Review and merge happen there while this repository is kept in step from GitHub; this copy follows it, and is marked merged or closed when it is.

nonos-sync added 15 commits

2026-10-03 19:22:34 -04:00

check a crate with no main as a library c1c1e1b8ee

zkolang check built the program, and building needs a main, so a
library crate was refused with E0900. The driver now has a check that
stops before lowering and says whether the root module has a main;
check of a crate without one checks its items, reports it as a
library and builds nothing, and run of it still reports E0900. The
CLI's edition 2026 commands share one loader and one way of printing
diagnostics.

add a changelog and a release workflow for tagged versions 8ff1f3f65b

CHANGELOG.md records 0.1.0, the first release of edition 2026. On a
tag v*, release.yml builds zkolang for Linux on x86_64 and aarch64 and
for macOS on aarch64 and x86_64, packs each with the licence, the
README and a SHA-256, and publishes a release whose notes are the
tag's section of the changelog. Only the publishing job may write. A
run started by hand builds the archives without publishing.

highlight edition 2026 in the TextMate grammar and VS Code bdd09074ee

The grammar knew the edition 2025 words and line comments only. It now
highlights both editions: nested block comments and the four doc
comment forms, attributes, strings with their escapes, integer literals
with a radix and a type suffix, every keyword and reserved word, the
primitive types, and declared names. The VS Code extension ships the
same file, with block comments and indentation rules. grammar_tests
holds both copies equal and every keyword of the lexer named by a rule.

add zkolang lsp, a language server for edition 2026 9f8952276a

zkolang lsp speaks the Language Server Protocol on standard input and
output. It holds each open document's text, checks the program rooted
at it as edition 2026 on every change, reading open documents in place
of the disk, and publishes the diagnostics of each file of the package
at the protocol's UTF-16 positions, clearing those now gone. It lays a
document out on request with the formatter. A file whose manifest is
edition 2025 is not checked. JSON is read and written by a small
reader of its own that bounds nesting and refuses malformed text, with
unit tests, and a test drives the server as an editor would.

build edition 2026 programs to C and Python, held to the reference run 1745801e3c

zkolang build --edition 2026 --target c|python emits the built program's SSA as a C file or a Python script. Each advice value is found by its hint and each constraint is checked as the run goes, so a run the proof would refuse exits with status 3. Inputs are one argument per leaf, public then secret, range checked against their types. The C declares only the values an output or a check reads, and compiles with -Wall -Wextra -Werror. A test runs every README program and a program with each kind of leaf, at and past the edges of its type, through both targets and holds them to the reference run.

name what pins each boundary of the step AIR, and lay a run out fc14aa1867

StepAir::boundary_pins gives boundary() in its order with what pins each cell: a value the program fixes, or public input or output slot k. The pins come from the instructions that read inputs and write outputs, so they are the same for every run of a program, which is what lets a verifier hold the circuit apart from the statement.

compiler::driver::traced runs an edition 2026 program beside the reference interpreter, as prove does, and returns the AIR, the trace and the public statement for a prover of another format. The prepare step of the driver moves to its own file.

record the step transition and write a program's STARKs image 472b8b850c

nonos_zkolang_format7 runs the step AIR's transition over a field element that records each addition, subtraction and multiplication on a per-thread tape. The transition never branches on a value and reads the program only through its periodic columns, so one tape serves every program; it is kept only if replaying it at a probe point gives what transition_ext gives, and an inversion refuses it.

image writes the program image a STARKs format 7 verifier parses: the counts, the exempt last row, the tape, the constraints, the rows as powers of the trace generator, and each boundary as a value or as the public word its pin names. The tests read each image back by the rules of that format, resolve its boundaries against a run's public words to the AIR's own, and check it is the same for every run of a program.

parse edition 2026 with the tree-sitter grammar, held to every program 23a28dbd5d

The grammar now reads edition 2026 as SPEC.md section 3 gives it: attributes, generic items, labelled and generic types, every expression at its precedence, struct literals kept out of conditions, match arms with guards, and every pattern form; and the top-level forms of edition 2025 beside it. The rules are split by part under grammar/, and src/scanner.c reads block comments, which nest.

scripts/check_grammar.py generates the parser, runs the pinned trees of test/corpus, compiles the highlight queries, and parses every .zkl file in the repository that marks no lexical or syntax error, and every program of the README, failing on any error node. The zkl workflow runs it with tree-sitter-cli 0.25.10.

build nonos-stark with fri8, the build of STARKs format 7 3892dcc15d

nonos-stark is built with its fri8 feature: radix 8 FRI and Merkle digests that keep all 32 bytes, the build the STARKs format 7 writer and nox_verify exist in. zKølang's own Poseidon proofs do not change; the keccak periodic root does, and with it every registration root and verifier key.

The golden test's root and key are back to the values it pinned before the move to the STARKs repository, 3f3379da... and 0b16d67a.... The shield circuits' keys in circuits/shield/README.md are repinned: spend_note 3b45aec5...b59ac338, note_root 50ce0eac...855e0ca3.

prove zKølang runs in STARKs format 7, verified by nox_verify b8e8e592f0

nonos_zkolang_format7::prove runs a built program beside the reference interpreter, commits the step AIR's trace in two rounds with stark_prove_ext_rounds, and writes the proof with serialize_rounds_shared after checking it against the statement. Every format 7 verifier needs a column in the second round; the step AIR reads no challenge, so Air7 commits its last column there and fills nothing between the rounds. The point is STARKs shape A, 19 queries after a 28-bit grind on the launch transcript, with five extra blowup bits. Every column is blinded to blinding_degree(19, 2, 8), which the composition admits from 2^10 rows, so traced takes a least trace size.

statement makes, from the program alone, what a gate pins: the image and its keccak256, the periodic root, the trace size and the parameter identity. verify checks a proof with nox_verify against it and public words a verifier computes with words. The test proves a run, has nox_verify accept it, and has it refuse another output, another input, a damaged proof and another program's statement; a failing run has no proof. The parallel feature spreads the prover's grind across cores.

add zkolang prove, verify and statement for STARKs format 7 68d171b53a

zkolang prove proves a run of an edition 2026 program in format 7 with a seed read from /dev/urandom, has nox_verify accept it, and writes proof.bin, program.bin and statement.txt. zkolang statement writes the image and statement from the program alone, the numbers a gate pins. zkolang verify makes the statement from the program and the public words from the claimed inputs and outputs, never from the prover, and checks the proof with nox_verify.

The parallel feature of the command passes through to the prover; CI lints that build. The test makes a statement, proves a run, checks the image prove wrote is the one statement wrote, and has verify accept the proof for the run's output and refuse another.

pin a format 7 fixture, and the words a statement fixes 0e9b2401b9

A statement now carries head, the five words every run of its program begins with: the commitment's limbs and the trace length. text writes a statement as statement.txt, for the command and for a page alike, and verify_pinned checks a proof against bare pins, the image, its hash, the periodic root, the parameter identity and the word count, for a verifier that holds no program.

fixture/ holds a proof of fixture/sum.zkl on public 12 and secret 5, with its image, statement and words; the example that writes it uses a fixed seed, and writing it twice gives the same bytes. tests/fixture.rs makes the statement and words again and has nox_verify accept the pinned proof and refuse it with a byte flipped or another output, so a change that moves the image, the format or the STARKs pin fails there.

verify format 7 proofs in a page with a WebAssembly module 35eacb9455

nonos_zkolang_wasm builds nox_verify, through verify_pinned, into a module a page instantiates with nothing but WebAssembly.instantiate: zk_alloc, zk_free, zk_verify and zk_reason, with the statement passed as its pins, its word count and its image end to end. js/zkolang-verify.mjs reads statement.txt and the slots a page expects and returns whether the proof verifies and why not.

CI builds the module for wasm32 and has Node verify the committed fixture with it, refusing it with a byte flipped and with another output; the release workflow packs the module and the interface beside the command. nonos_zkolang_format7 gets a README of what a verifier pins and how a run's words are made.

show how to verify a run anywhere, and state format 7's bounds 5afa24f933

The README's walkthrough gains a tenth section: a program the README test proves, the statement a verifier pins, a proof made with zkolang prove, and zkolang verify accepting it for the run's output and refusing another. SECURITY.md states the point format 7 proofs are made at, that their columns are blinded with the same boundary as edition 2026 proofs, and what the format 7 tests and the fixture enforce.

move the new CI and release jobs to the bumped action pins 62e85c1e49

main moved actions/checkout to v7.0.1, actions/upload-artifact to v7.0.1 and actions/cache to v6.1.0. The grammar job, the browser verifier job and the release workflow now pin the same commits.

This pull request can be merged automatically.

You are not authorized to merge this pull request.

View command line instructions

Checkout

From your project repository, check out a new branch and test the changes.

git fetch -u origin +refs/pull/16/head:nonos-sync/gh-73

git switch nonos-sync/gh-73

Rows
Columns

Format7 tooling #16

Checkout