chore(licence): normalise to MPL-2.0 + CC-BY-SA-4.0 (canonical pair)#658
Merged
Merged
Conversation
- LICENSES/ = {MPL-2.0.txt, CC-BY-SA-4.0.txt}; root LICENSE = verbatim MPL-2.0 (GitHub display)
- SPDX: code -> MPL-2.0, docs (.md/.adoc) -> CC-BY-SA-4.0; metadata/badge fixes; vendored untouched
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jun 27, 2026
…xec) (#664) Third rung of the real lift (`formal/REAL-LIFT.adoc`). Adds **structured control** to the real target IR + source core, and shows the compiler-correctness simulation still holds across a conditional. Axiom-free throughout. ## What landed **Target IR (`formal/RealWasm.v`)** - New instruction `IfElse (thn els : list instr)` — `lib/wasm.ml`'s `If` minus the `block_type` validation annotation. - Because `instr` now nests `list instr`, a *structural* `wexec` is rejected by Coq's guard checker ("cannot guess decreasing argument" — the recursive call descends into a branch sub-list, not the tail). So `wexec` becomes **fuel-indexed** (decreasing on a `nat`), exactly as `REAL-LIFT.adoc` anticipated for R2. Fuel keeps *definitional* computation, so `cbn` / `reflexivity` / the demos still evaluate. - Fuel breaks the old one-line `wexec_seq` (per-cons decrement ⇒ `wexec (is1++is2) ≠ wexec is2 ∘ wexec is1`). Recovered with: - `wexec_le_S` / `wexec_mono` — more fuel never loses a `Some` result; - `wexec_app_some` — additive sequencing: run `is1` with `f1`, then `is2` with `f2`, get `is1++is2` with `f1+f2` (the fuel-world replacement for `wexec_seq`); - `wexec_S_cons` / `wexec_ifelse` — one-step unfold lemmas (by `reflexivity`) used via `rewrite` so `cbn` doesn't over-reduce the `IfElse` branch run. **Source core (`formal/RealCompile.v`)** - New `RIf (c thn els : rexpr)`; `eval` branches on `Z.eqb vc 0`; `compile` emits `compile c ++ [IfElse (compile thn) (compile els)]`. - `compile_correct` restated **existential-in-fuel**: `exists fuel locals', wexec fuel (compile d e) locals st = Some (locals', v :: st) /\ …` (env↔locals agreement + low-slot preservation unchanged). The `RIf` case opens with `change (compile d (RIf …)) with (… ++ [IfElse …])` to expose the `++` while keeping inner compiles named, then discharges via `wexec_app_some` + `wexec_le_S`. - `wexec_sound` retired in this fuel refactor — it was a convenience soundness restatement, not load-bearing for `compile_correct`. ## Verification `coqc` 8.18, whole `formal/` track re-audited after rebasing onto current `main` (incl. #648's now-wired `Rows.v`): - **18 files compile**, **31 `Print Assumptions` reports**, every one *"Closed under the global context"* — **zero axioms, no `Admitted`**. ## Docs `formal/REAL-LIFT.adoc` (R2 row + nested-control section), `formal/README.adoc` (RealWasm/RealCompile rows + "The real lift (R0 → R2)"), `docs/PROOF-NEEDS.adoc` (K-1 row) updated. Conflict-resolved cleanly against #648 (Rows.v / P-11) and #658 (licence normalisation). ## Next Sub-rung **R2-loops** (`Loop`/`Br` + while/for, reusing the fuel device; settles the value-returning-tail question behind #601), then R-mem / R-float / R-str / … per `formal/REAL-LIFT.adoc`. Refs `REAL-LIFT.adoc`, `docs/PROOF-NEEDS.adoc` (K-1 row). 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr --- _Generated by [Claude Code](https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr)_ Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Estate licence normalisation. LICENSES/={MPL-2.0,CC-BY-SA-4.0}; root LICENSE=verbatim MPL-2.0 (GitHub display); code->MPL-2.0, docs(.md/.adoc)->CC-BY-SA-4.0; vendored untouched. Residual mentions (mostly legitimate anti-AGPL rules): 159. Manual-review licence PR.