Skip to content

scope-proof.md

Latest commit

 

History

History
50 lines (37 loc) · 1.67 KB

scope-proof.md

File metadata and controls

50 lines (37 loc) · 1.67 KB
Raw

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:

moon prove src/proof_scope

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

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:

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.