Adva

This repository is evolving toward knowledge and executable research, using the specification and toolchains maintained in adva-machine. The dependency continuity plan and its fixed machine version define the first external execution route. Existing implementation paths and historical evidence remain available while consumers migrate. English documentation is primary.

The first checked library exchange has received an original naming entry through the Rust communication profile, with its publication review, source home, obligations and receiver receipt retained.

The iota exchange now receives a focused iota package also delivered to adva-machine. Each side retains its own Rust receipt and executed comparison of terms, process cuts, observer clocks and three native object-language probes.

The iota frame companion now jointly carries iota, complex structure and exponential readings. Its post-arrival check preserves observations and clock groups under declared coordinate changes, with the same packet also checked by adva-machine.

How can a finite observer construct, check, and extend arithmetic knowledge?

中文入口 · Run an example · Bring a stalled problem · Development

Adva investigates this question through typed programs, explicit construction histories, bounded experiments, and reusable witnesses. The practical aim is to make a difficult problem easier to continue: establish what a particular observation tells us, preserve what it leaves undecided, and find the next construction or observation that could make a difference.

The implementation includes a Rust Lisp engine, a separately versioned bounded data language, a library of recorded constructions, and a substantial research record. Pre-alpha research software. Unknown v0.3 dedicates the first-party work to the public domain, with a voluntary philosophical statement. See LICENSE and licensing scope.

Start with one observation

Suppose two explanations of a program are f(x) = 2x and g(x) = x².

Observation	f(x)	g(x)	What it establishes
Evaluate at x = 2	4	4	Both explanations fit this observation.
Evaluate at x = 3	6	9	This observation distinguishes them.

Repeating the first observation does not resolve the ambiguity. A different observation does. Even agreement on many inputs would need a justification before becoming a claim about all inputs. Adva's interpretation experiment records this distinction with explicit questions, interpretations, and checks.

Finite observation can also support a proof. For example, two polynomials over the rationals, each of degree at most two, are identical if they agree at three distinct rational points: their difference has degree at most two and cannot have three distinct roots unless it is zero. The degree bound and the root argument make those observations sufficient. Three arbitrary tests do not. The finite-example research develops this kind of boundary between examples and proof.

Adva asks how to retain that whole relationship: the original question, the construction, the observer, the assumptions, the witness, and the unresolved remainder. A result can then be reused with its conditions attached.

What “finite observer” means here

An observer has a particular interface, a language of questions, and finite resources. It can distinguish some constructions and leave others unresolved. The research goal is to make these limits operational, including the possibility of changing the observer or extending its language.

Four distinctions guide the work:

• An observation is not the whole construction. Equal output values do not identify two programs, their sources, or their histories. The native core records explicit copying and distinct occurrences.
• An arithmetic check needs an interpretation. In a declared field, equality can be tested by A - B = 0, or by A / B = 1 when B ≠ 0. The domain and the correspondence to the original problem still need to be justified. The proposed arithmetic-universality and arithmetic-truth vocabulary remains a research hypothesis.
• A finite success has a scope. A complete finite check, together with an applicable theorem, may justify a larger conclusion. Running out of search time alone leaves the question Unknown.
• A useful next step changes what can be established. A new witness, counterexample, justified interpretation, or reusable construction can do this. Another run or another participant does not establish learning by itself.

The larger programme connects program geometry, arithmetic, learning, and language formation. Its philosophical questions, ontology, and research agenda explain that ambition. They are also part of the project; the runtime is one place where those ideas must meet concrete checks.

What you can inspect today

Layer	Existing work	Boundary
Native program core	Typed finite Lisp programs; explicit sources, occurrences and history; checked diagrams, graft traces and process slices; evaluation and forward differentiation	Finite, binder-free, linear PSC0 scope. Numerical evaluation uses floating point; structural certificates are not numerical error bounds.
Research data language	An arithmetic interpreter written in Adva instructions, executed by Rust; exact checked i64 arithmetic, bounded control, suspension and replay	A separate research profile. Overflow rejects. This example interprets arithmetic trees, not its own full instruction language.
Research library and experiments	Reusable witnesses, observer comparisons, closure and transport checks, retained failures and counterexamples	Each result has its own assumptions, checker, budget and residual. External checks do not confer native semantic authority.
Open programme	Observer-conditioned specialization, richer language formation, arithmetic universality and geometric representations	Construction targets and hypotheses, with dependencies in the agenda.

The claim registry records scoped claims and their evidence; the semantic scope defines the native boundary. Rust is the authority for native semantic identities and judgments. Python supplies adapters and external research tools. Decoding JSON alone never authorizes a semantic object.

Run an example

Clone with the library submodule:

git clone --recurse-submodules https://github.com/mountain/adva.git
cd adva

An interpreter that retains its execution

With a Rust toolchain installed, run these commands from the repository root in a POSIX shell:

cargo build --locked -p adva-witness --bin adva
adva_run_dir="$(mktemp -d)"
target/debug/adva data-run programs/bounded-interpreter/interpreter.adva \
  --input programs/bounded-interpreter/input.json \
  --fuel 2048 --quantum 2048 --output "$adva_run_dir/result.adva"

The supplied input is 2 + (3 * 4). The expected status is Returned, with integer result 14 after 134 instruction steps. Open the output to inspect the program, input, execution trace, final state and fuel accounting. Outputs must use fresh paths.

Then try the suspend-and-resume example: stop after 17 steps, recheck the prefix, and continue without resetting the original lifetime fuel. Replay work is recorded separately. The research report explains what the retained calibration establishes and what remains open.

The newer compilation calibration also compares interpretation with emitted three-instruction constant programs for 129 fully static arithmetic trees. Its recorded machine-step cost is higher for one use and lower after two uses, including compilation. This is a finite reuse result, with host-side program loading; it does not establish a general specializer or a wall-clock speedup.

A compiler that compiles itself

The structured self compiler compiles its own Adva source through two native generations with equal target bytes, independent block checks and execution controls. It uses the separately bounded adva data-run-v1 research profile. The report connects this bootstrap to the existing static and dynamic first-projection calibrations and states the remaining interpreter, mix and self-application contracts. This establishes self compilation for the declared subset.

The subsequent bounded mix experiment implements input binding in ordinary Adva instructions and checks actual emitted code across the three projection equations. Its separate data-run-v2 research profile preserves v1 and raises only instruction and node-arity capacities. This conservative baseline retains interpreter execution; a general optimizing specializer, interpreter elimination and unrestricted projection claims remain open. See the results and limits.

A collaboration record, without building Rust

With Python 3.11 or later:

python3 experiments/bounded_observation_exchange/check_exchange_chain.py

Expected result: DisclosedByteChainChecked, covering five recorded exchanges and four controls that reject an old reply as an answer to a new question. The checker compares disclosed fields and their byte bindings. It explicitly leaves source authenticity unverified and semantic acceptance withheld. This is a small, runnable example of retaining a question across handoffs; it does not establish the truth of the participants' statements. See the exchange experiment.

Bring a stalled problem

You can start with one failed attempt, without learning the whole mathematical framework. Keep the original problem and bring:

1. The result you need and the observations that would count as success.
2. A small reproducible attempt, with its inputs, assumptions and resource limit.
3. What passed, what failed, and the exact part that is still unresolved.
4. One proposed next step: a different observation, a counterexample, a stronger invariant, or a construction someone else could check.

For a coding challenge, this might mean finding a test that separates two plausible implementations, or exposing a mismatch between the written task and its tests. Human and AI attempts can both contribute. The useful comparison is what becomes checkable, reusable, or less costly under stated conditions.

The tooling work plan turns this into a proposed working session using existing tools. A unified problem-workbench interface is not implemented yet.

If you get stuck, come back with the attempt and the remaining question. If this approach helps you make progress, consider starring the project so you can find it again and follow its development.

Find your next reading

You want to…	Start here
Understand the idea in Chinese	中文入口
See how finite examples can become a proof	Finite-example verification
Distinguish nontermination evidence from timeout	Finite cycle certificates
Write or extend native programs	Development guide, then AGENTS.md
Understand the programme's larger questions	Philosophy and research agenda
Explore the library	Library and mathematical growth obligation
Exchange knowledge across interfaces	Formal communication vocabulary and receiving contracts
Trace results, corrections and remaining questions	Research index, claims, and each note's later corrections

Historical runs retain their original profiles. In particular, some stored library epochs need their pinned historical receiver; see the replay guidance. The AI attribution policy records contributions and checks separately from account ownership.