# Scope Resolution Proof Sandbox

This package is an experimental proof sandbox for one `mold` scope-resolution
rule: a local scope binding wins over the root context for the first path
segment.

The proof lives in `src/proof_scope/` and intentionally uses a small model:

- keys are `Int`, not `String`
- objects/scopes are recursive key-value bindings, not `Map[String, Value]`
- results are explicit model enums, not `MoldError`

This keeps the proof focused on the semantic rule rather than the production
runtime representation. It does not prove `src/context.mbt` directly. Production
behavior is still covered by ordinary tests.

Run the proof manually on platforms with a native Why3 server available:

```text
moon prove src/proof_scope
```

Windows contributors can use Ubuntu WSL rather than a native Windows Why3
wrapper. One known working setup is:

```text
sudo apt install -y build-essential curl git m4 pkg-config unzip opam z3
curl -fsSL https://cli.moonbitlang.com/install/unix.sh | bash
opam init -y
opam switch create mold-verify 5.2.1 -y
opam install --switch=mold-verify -y why3.1.7.2
opam exec --switch=mold-verify -- why3 config detect

cd /path/to/mold
export PATH="$HOME/.moon/bin:$PATH"
opam exec --switch=mold-verify -- moon prove src/proof_scope
```

If `_build/verif/why3.conf` was generated by a different platform, remove
`_build/verif/` before proving so MoonBit regenerates a local Why3 config.

The first targeted property is:

```text
if lookup(scope, key) == Hit(value), then resolve_head(ctx, scope, key)
returns Resolved(value), regardless of ctx.
```

Future proof extensions can model missing keys, non-object path traversal, empty
paths, and deterministic resolution.