# Proof Spec: wokelang
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->

**Repo Path**: `/var/mnt/eclipse/repos/nextgen-languages/wokelang`
**Tier**: T1 — Critical
**Total Theorems**: 4
**Primary Prover(s)**: Lean4 (2), Coq (2)
**Existing Proof Coverage**: WokeLang.lean (747 LOC, **1 sorry**), WokeLang.v (1166 LOC, 0 Admitted)
**Dependencies**: None

## Status Tracker

| # | Theorem | Prover | Status | Verified |
|---|---------|--------|--------|----------|
| 1 | WL1 Close 1 sorry in WokeLang.lean | L4 | [ ] Pending | — |
| 2 | WL2 Consent tracking soundness | L4 | [ ] Pending | — |
| 3 | WL3 VOops error propagation | Cq | [ ] Pending | — |
| 4 | WL4 HM inference soundness | Cq | [ ] Pending | — |

## Context

Consent-aware programming language for human collaboration. HM inference, JavaScript expressiveness, consent/permission tracking, VOops (virtual objects) for error handling.

### Key files
- `docs/proofs/verification/WokeLang.lean` (747 LOC, 1 sorry)
- `docs/proofs/verification/WokeLang.v` (1166 LOC, 0 Admitted)
- `src/abi/*.idr` (3 files)

## Theorems to Prove

### WL1: Close sorry in WokeLang.lean

**Target file**: `docs/proofs/verification/WokeLang.lean` (EXISTING)
**Priority**: P0

**Obligations**:
- [ ] Identify and close 1 sorry

---

### WL2: Consent tracking soundness

**Target file**: `docs/proofs/verification/ConsentSound.lean` (NEW)
**Priority**: P0

**Statement**: Type system ensures permission checks precede protected operations.

**Obligations**:
- [ ] Model permission effects
- [ ] Prove precondition

---

### WL3: VOops error propagation

**Target file**: `docs/proofs/verification/VOops.v` (NEW)
**Priority**: P1

**Statement**: VOops type correctly models error propagation. Exceptions cannot be silently dropped.

**Obligations**:
- [ ] Define VOops type
- [ ] Prove error propagation

---

### WL4: HM inference soundness

**Target file**: `docs/proofs/verification/HMSound.v` (NEW)
**Priority**: P1

**Statement**: If HM inference returns type τ for expression e, then e has type τ.

**Obligations**:
- [ ] Formalise HM algorithm
- [ ] Prove soundness + completeness

---

## Verification Commands

```bash
cd /var/mnt/eclipse/repos/nextgen-languages/wokelang
lean docs/proofs/verification/*.lean
coqc docs/proofs/verification/*.v
```

## Handoff Checklist

- [ ] WL1 sorry closed
- [ ] WL2-WL4 complete
- [ ] Commit: `proof: complete wokelang proofs (4/4 theorems)`
