Metadata-Version: 2.4
Name: adva
Version: 0.1.0
Classifier: Development Status :: 2 - Pre-Alpha
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Rust
Classifier: Typing :: Typed
Requires-Dist: numpy>=1.26 ; extra == 'scientific'
Requires-Dist: scipy>=1.12 ; extra == 'scientific'
Requires-Dist: sympy>=1.12 ; extra == 'scientific'
Requires-Dist: blake3>=1,<2 ; extra == 'test'
Requires-Dist: numpy>=1.26 ; extra == 'test'
Requires-Dist: pytest>=8 ; extra == 'test'
Requires-Dist: scipy>=1.12 ; extra == 'test'
Requires-Dist: sympy>=1.12 ; extra == 'test'
Provides-Extra: scientific
Provides-Extra: test
License-File: LICENSE
License-File: Unknown-LICENSE-v0.3.md
License-File: LICENSING.md
Summary: A typed Lisp engine and interoperable IR for program geometry
Author: Adva contributors
License-Expression: LicenseRef-Unknown-0.3
Requires-Python: >=3.11
Description-Content-Type: text/markdown; charset=UTF-8; variant=GFM

# Adva

This repository is evolving toward knowledge and executable research, using
the specification and toolchains maintained in
[`adva-machine`](https://github.com/mountain/adva-machine).
The [dependency continuity plan](docs/KNOWLEDGE_MACHINE_BOUNDARY.md) and its
[fixed machine version](dependencies/adva-machine.lock.json) 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](knowledge/exchanges/party-naming-layer-2026-09-16-v1/README.md)
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](knowledge/exchanges/iota-process-knowledge-2026-09-17-v1/README.md)
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](knowledge/exchanges/iota-frame-knowledge-2026-09-17-v1/README.md)
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?**

[中文入口](README.zh-CN.md) · [Run an example](#run-an-example) ·
[Bring a stalled problem](#bring-a-stalled-problem) · [Development](docs/DEVELOPMENT.md)

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](Unknown-LICENSE-v0.3.md)
dedicates the first-party work to the public domain, with a voluntary philosophical
statement. See [LICENSE](LICENSE) and [licensing scope](LICENSING.md).

## 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](docs/research/0166-interpretation-obligation.md)
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](docs/research/0183-zhang-finite-example-verification.md)
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](docs/research/0123-arithmetic-universality-and-hypothesized-truth.md)
  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](docs/philosophy/README.md),
[ontology](ontology/README.md), and [research agenda](docs/RESEARCH_ENGINEERING_AGENDA.md)
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](docs/claims.toml) records scoped claims and their evidence;
the [semantic scope](docs/SEMANTIC_SCOPE.md) 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:

```sh
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:

```sh
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](programs/bounded-interpreter/README.md):
stop after 17 steps, recheck the prefix, and continue without resetting the
original lifetime fuel. Replay work is recorded separately. The
[research report](docs/research/bounded-native-data-interpreter.md) explains
what the retained calibration establishes and what remains open.

The newer [compilation calibration](docs/research/futamura-projections-in-adva-terms.md)
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](experiments/bounded_self_compiler/README.md)
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](docs/research/bounded-self-compiler-and-futamura.md) 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](experiments/bounded_mix/README.md)
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](docs/research/bounded-mix-and-three-projections.md).

### A collaboration record, without building Rust

With Python 3.11 or later:

```sh
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](experiments/bounded_observation_exchange/README.md).

## 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](docs/TOOLING_WORKFLOW.md) 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 | [中文入口](README.zh-CN.md) |
| See how finite examples can become a proof | [Finite-example verification](docs/research/0183-zhang-finite-example-verification.md) |
| Distinguish nontermination evidence from timeout | [Finite cycle certificates](docs/research/keraia-cycle-certificates-and-halting-mass-bounds.md) |
| Write or extend native programs | [Development guide](docs/DEVELOPMENT.md), then [AGENTS.md](AGENTS.md) |
| Understand the programme's larger questions | [Philosophy](docs/philosophy/README.md) and [research agenda](docs/RESEARCH_ENGINEERING_AGENDA.md) |
| Explore the library | [Library](adva-library/README.md) and [mathematical growth obligation](adva-library/math/README.md) |
| Exchange knowledge across interfaces | [Formal communication vocabulary and receiving contracts](docs/COMMUNICATION_FRAMEWORK.md) |
| Trace results, corrections and remaining questions | [Research index](docs/research/README.md), [claims](docs/claims.toml), 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](docs/DEVELOPMENT.md#replaying-historical-library-epochs).
The [AI attribution policy](docs/AI_ATTRIBUTION.md) records contributions and
checks separately from account ownership.

