chore: merge remote changes from origin/main

Author: hyperpolymath

Cargo.lock

@@ -1042,29 +1042,36 @@ \subsection{Properties}
 for any consent effect in $e$.
 \end{theorem}
 
-\begin{proof}[Proof sketch]
+\begin{proof}
 By structural induction on the typing derivation.  The critical case
-is \textsc{T-Consent}: the typing rule ensures that consent-gated
-expressions occur within a handler context ($\Sigma$ is non-empty),
-and the handler $h$ is total (it returns either $\granted$ or
-$\denied$ for any string $s$), so one of \textsc{E-ConsentGranted} or
-\textsc{E-ConsentDenied} always applies.
+is \textsc{T-Consent}: we strengthen the paper rule to require
+$\Sigma \neq \varnothing$ (at least one handler in scope), closing a
+gap in the original sketch.  With this invariant, the top handler $h$
+is always available and total, so one of \textsc{E-ConsentGranted} or
+\textsc{E-ConsentDenied} fires.  The full machine-checked proof is in
+\texttt{src/abi/WokeLang/Safety.idr} (\texttt{progress});
+see the supplementary proof inventory
+(\texttt{docs/supplementary/safety-proofs.adoc}) for details.
 \end{proof}
 
 \begin{theorem}[Preservation]
 \label{thm:preservation}
 If $\Gamma; \Sigma \vdash e : \tau$ and $\langle e, H, A \rangle
-\step \langle e', H', A' \rangle$, then $\Gamma; \Sigma \vdash e' :
-\tau'$ where $\tau' = \tau$ or $\tau' = \mathsf{Consent}[\tau]$
-resolves to $\tau$ (in the granted case) or $\denied$ (in the denied
-case).
+\step \langle e', H', A' \rangle$, then there exists $\tau'$ with
+$\Gamma; \Sigma' \vdash e' : \tau'$, where $\tau' = \tau$ for most
+rules, $\tau' = \tau$ (body type) when \textsc{E-ConsentGranted}
+fires, and $\tau' = \mathsf{TyDenied}$ when \textsc{E-ConsentDenied}
+fires.
 \end{theorem}
 
-\begin{proof}[Proof sketch]
-By structural induction on the reduction.  The consent cases follow
-from the handler totality and the fact that the body of a consent gate
-is typed at $\tau$ while the gate as a whole is typed at
-$\mathsf{Consent}[\tau]$.
+\begin{proof}
+By structural induction on the reduction derivation.  The consent
+cases follow from handler totality: \textsc{E-ConsentGranted} returns
+$e$ (the body, typed at $\tau$), and \textsc{E-ConsentDenied} returns
+\texttt{EDenied} (typed at $\mathsf{TyDenied}$).  The E-Beta case
+uses a closed-value substitution lemma proved by induction with a
+context-exchange step for nested lambda binders.  Machine-checked in
+\texttt{src/abi/WokeLang/Safety.idr} (\texttt{preservation}).
 \end{proof}
 
 \begin{theorem}[Consent Non-Evasion]
@@ -1075,14 +1082,16 @@ \subsection{Properties}
 decision.
 \end{theorem}
 
-\begin{proof}[Proof sketch]
-The only reduction rules that step into a consent gate body are
-\textsc{E-ConsentGranted} and \textsc{E-ConsentDenied}, both of which
-require a handler response and produce a log entry in $A$.  The typing
-rule \textsc{T-Consent} ensures that the body is not directly
-accessible outside the gate construct.  Exhaustiveness of the handler
-(it must return $\granted$ or $\denied$) ensures a decision is always
-made.
+\begin{proof}
+By inversion on the \textsc{Step} derivation for $\mathbf{only\_if\_okay}\;s\;e$.
+The only constructors of \textsc{Step} whose head expression matches
+$\mathbf{only\_if\_okay}$ are \textsc{E-ConsentGranted} and
+\textsc{E-ConsentDenied}; all other constructors match different head
+forms and are structurally absent.  Both firing rules require
+$H = h :: H'$ (non-empty stack) and append
+$\mathsf{ConsentEntry}(d, s)$ to $A$.
+Machine-checked in \texttt{src/abi/WokeLang/Safety.idr}
+(\texttt{nonEvasion}, \texttt{consentBodyRequiresLog}).
 \end{proof}
 
 This theorem is the core safety property of the consent system: you
@@ -1448,11 +1457,16 @@ \section{Future Work}
 
 \paragraph{Formal Verification.}
 The $\lambda_{\consent}$ calculus presented here covers a simplified
-core language.  Extending the formal treatment to cover the full
-\WokeLang{} language---including higher-order functions, mutation,
-concurrency, and module systems---is ongoing work.  We are exploring
-mechanized proofs in Idris~2~\citep{brady2021idris2} to ensure the
-correctness of our compiler's consent tracking.
+core language.  Proofs of Progress, Preservation, and Non-Evasion have
+been mechanised in Idris~2~\citep{brady2021idris2} under
+\texttt{\%default total} with no uses of \texttt{believe\_me} or
+\texttt{postulate}; see \texttt{src/abi/WokeLang/Safety.idr} and
+\texttt{docs/supplementary/safety-proofs.adoc}.  The mechanisation
+strengthens \textsc{T-Consent} to require a non-empty handler context
+$\Sigma$, fixing a gap in the original proof sketch.  Extending the
+formal treatment to the full language---including higher-order
+functions, mutation, concurrency, and module systems---remains future
+work.
 
 \paragraph{Localization.}
 Exploring multilingual keyword support while maintaining semantic

arxiv-consent-aware-programming.tex

@@ -0,0 +1,96 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
+= WokeLang Safety Proofs — Supplementary Material
+:toc:
+:toc-placement: preamble
+
+Supplementary material for _A Consent-Aware Programming Language: WokeLang_
+(§7, Formal Semantics).  This document maps each paper theorem to the
+corresponding Idris 2 source file and explains the key proof strategies.
+
+== Source locations
+
+[cols="2,3,4"]
+|===
+| Theorem | Paper reference | Idris 2 source
+
+| Syntax (Definition 1)
+| §7.1
+| `src/abi/WokeLang/Calculus.idr`
+
+| Typing (Definition 2)
+| §7.2
+| `src/abi/WokeLang/Typing.idr`
+
+| Operational semantics (Definition 3)
+| §7.3
+| `src/abi/WokeLang/Reduction.idr`
+
+| Theorem 1 — Progress
+| §7.4, `thm:progress`
+| `src/abi/WokeLang/Safety.idr`, `progress`
+
+| Theorem 2 — Preservation
+| §7.4, `thm:preservation`
+| `src/abi/WokeLang/Safety.idr`, `preservation`
+
+| Theorem 3 — Non-Evasion
+| §7.4, `thm:non-evasion`
+| `src/abi/WokeLang/Safety.idr`, `nonEvasion`, `consentBodyRequiresLog`
+
+|===
+
+All four files use `%default total` and contain no `believe_me`, `assert_total`,
+`postulate`, or `sorry`.
+
+== Key proof strategies
+
+=== T-Consent invariant fix
+
+The paper's T-Consent rule (Definition 2) accepts an arbitrary consent context Σ,
+including the empty one.  However, the Progress proof sketch (§7.4) implicitly
+assumes Σ is non-empty so that `E-ConsentGranted` or `E-ConsentDenied` can fire.
+The mechanisation strengthens T-Consent to require `Σ = h :: hs` (at least one
+handler in scope).  This is the only deviation from the paper and closes a genuine
+gap in the original presentation.
+
+=== Context exchange for substitution
+
+The substitution lemma (`substLemma` in `Typing.idr`) is proved for *closed values*
+(values typed in the empty context `[]`).  This is sufficient for Preservation
+because the whole term is typed in `[]`, so every function argument at a beta-redex
+is itself typed in `[]`.
+
+The `TLam` case requires a *context exchange* lemma (`ctxExchange`): when the
+substitution variable `x` appears under a lambda binder `y ≠ x`, the two adjacent
+bindings `(y, τy) :: (x, τx) :: ctx` are swapped to `(x, τx) :: (y, τy) :: ctx`.
+This is justified by `exchangeLookup`, which shows that `decEq`-based lookup
+produces the same result in both orderings when `x ≠ y`.
+
+=== Type change in Preservation
+
+Consent gate steps change the static type:
+
+* `SConsentGranted`: `Consent[τ] → τ` (`TCGranted`)
+* `SConsentDenied`: `Consent[τ] → TyDenied` (`TCDenied`)
+
+All other rules preserve the type exactly (`TCRefl`).  The `TypeChange` GADT
+captures this, and `preservation` returns `(τ' : Ty ** TypeChange τ τ' ** Typed [] sigma' e' τ')`.
+
+=== Non-Evasion
+
+`nonEvasion` proves Theorem 3 by *inversion*: matching on
+`Step (EOnlyIfOkay s e) H A e' H' A'` exhaustively enumerates the Step
+constructors.  The only constructors whose `Step` head is `EOnlyIfOkay` are
+`SConsentGranted` and `SConsentDenied`; all others match different head forms
+and are therefore structurally absent.  Both firing constructors append
+`ConsentEntry d s` to `A`, so `DecisionLogged A' s` holds immediately.
+
+== Scope and limitations
+
+* The mechanisation covers the core λ_consent calculus as defined in the paper.
+* The `EAttr` and `EFeel` extensions are included (reduction rules + preservation
+  cases) but are not the focus of the three theorems.
+* Units-of-measure typing (§5) and gratitude blocks (§6) are not mechanised here;
+  they are independent extensions that do not affect the consent gate soundness
+  results.

docs/supplementary/safety-proofs.adoc

@@ -0,0 +1,23 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# wokelang package manifest — OPSM native.
+# This file makes wokelang a first-class OPSM/HFR package.
+
+[package]
+name = "wokelang"
+description = "Wokelang compiler — general-purpose BEAM-friendly application language"
+license = "PMPL-1.0-or-later"
+authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
+keywords = ["wokelang", "hyperpolymath", "nextgen-languages", "compiler"]
+homepage = "https://github.com/hyperpolymath/nextgen-languages"
+repository = "https://github.com/hyperpolymath/nextgen-languages"
+forth = "wokelang"
+
+[opsm]
+trust_level = "hyperpolymath"
+registry = "hf"
+
+[dependencies]
+proven = { git = "https://github.com/hyperpolymath/proven", registry = "hf" }
+groove = { git = "https://github.com/hyperpolymath/groove", registry = "hf" }

opsm.toml

@@ -0,0 +1,162 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
+-- Calculus.idr - λ_consent calculus: syntax, types, values, handler algebra
+--
+-- Mechanises Definition 1 (Syntax) from §7 of arxiv-consent-aware-programming.tex.
+-- The calculus extends the simply-typed lambda calculus with four consent-specific
+-- forms: only_if_okay, consent_handler, attr, and feel.
+
+module WokeLang.Calculus
+
+%default total
+
+-- ---------------------------------------------------------------------------
+-- Consent decisions
+-- ---------------------------------------------------------------------------
+
+||| The binary decision a consent handler produces for any given prompt.
+||| Handlers are required to be total — they always return one of these.
+public export
+data ConsentDecision : Type where
+  Granted : ConsentDecision
+  Denied  : ConsentDecision
+
+-- ---------------------------------------------------------------------------
+-- Consent handlers (Definition 1, handler forms)
+-- ---------------------------------------------------------------------------
+
+||| A consent handler maps a prompt string to a consent decision.
+||| Four canonical forms:
+|||   HInteractive      — defers to the user (modelled as Granted here)
+|||   HPolicy p         — applies a policy predicate
+|||   HAutoGranted      — always grants (auto(granted))
+|||   HAutoDenied       — always denies  (auto(denied))
+public export
+data Handler : Type where
+  HInteractive  : Handler
+  HPolicy       : (String -> ConsentDecision) -> Handler
+  HAutoGranted  : Handler
+  HAutoDenied   : Handler
+
+||| Apply a handler to a consent prompt string.
+||| This function is total by construction: every case returns a decision.
+public export
+applyHandler : Handler -> String -> ConsentDecision
+applyHandler HInteractive  _ = Granted
+applyHandler (HPolicy p)   s = p s
+applyHandler HAutoGranted  _ = Granted
+applyHandler HAutoDenied   _ = Denied
+
+-- ---------------------------------------------------------------------------
+-- Types (Definition 1, type syntax)
+-- ---------------------------------------------------------------------------
+
+||| λ_consent types.
+|||   TyConsent τ — result gated behind a consent decision
+|||   TyDenied    — type of the `denied` terminal value
+public export
+data Ty : Type where
+  TyInt     : Ty
+  TyStr     : Ty
+  TyBool    : Ty
+  TyFun     : Ty -> Ty -> Ty
+  TyConsent : Ty -> Ty
+  TyDenied  : Ty
+
+-- ---------------------------------------------------------------------------
+-- Variable names
+-- ---------------------------------------------------------------------------
+
+||| Variables are represented as natural numbers.
+public export
+Var : Type
+Var = Nat
+
+-- ---------------------------------------------------------------------------
+-- Expressions (Definition 1, expression syntax)
+-- ---------------------------------------------------------------------------
+
+||| λ_consent expression syntax.
+|||
+||| Core forms:
+|||   EVar x            — variable (de-Bruijn-named)
+|||   ELam x τ e        — lambda abstraction
+|||   EApp f a          — application
+|||   ELit n            — integer literal
+|||   EAdd e1 e2        — integer addition (representative binary op)
+|||
+||| Consent-specific forms:
+|||   EOnlyIfOkay s e   — consent gate: only_if_okay s e
+|||   EConsentHandler h e — handler install: consent_handler h e
+|||   EAttr p d e       — attribution annotation: attr p d e
+|||   EFeel f e         — empathy annotation: feel f e  (phantom at runtime)
+|||
+||| Terminal values:
+|||   EDenied           — the `denied` terminal produced by a denied consent gate
+public export
+data Expr : Type where
+  EVar          : Var -> Expr
+  ELam          : Var -> Ty -> Expr -> Expr
+  EApp          : Expr -> Expr -> Expr
+  ELit          : Int -> Expr
+  EAdd          : Expr -> Expr -> Expr
+  EOnlyIfOkay   : String -> Expr -> Expr
+  EConsentHandler : Handler -> Expr -> Expr
+  EAttr         : String -> String -> Expr -> Expr
+  EFeel         : String -> Expr -> Expr
+  EDenied       : Expr
+
+-- ---------------------------------------------------------------------------
+-- Values (Definition 1, value syntax)
+-- ---------------------------------------------------------------------------
+
+||| Values are fully-reduced expressions: lambdas, literals, and denied.
+||| `denied` is a value because E-ConsentDenied produces it as a terminal.
+public export
+data IsValue : Expr -> Type where
+  VLam    : IsValue (ELam x τ e)
+  VLit    : IsValue (ELit n)
+  VDenied : IsValue EDenied
+
+-- ---------------------------------------------------------------------------
+-- Capture-avoiding substitution
+-- ---------------------------------------------------------------------------
+
+||| e[v/x] — substitute v for x in e.
+||| Precondition (caller's responsibility): v is closed.
+||| Lambda bodies where the binder shadows x are left unchanged.
+public export
+subst : (x : Var) -> (v : Expr) -> (e : Expr) -> Expr
+subst x v (EVar y) =
+  case decEq x y of
+    Yes _ => v
+    No  _ => EVar y
+subst x v (ELam y τ body) =
+  case decEq x y of
+    Yes _ => ELam y τ body          -- x is shadowed; do not descend
+    No  _ => ELam y τ (subst x v body)
+subst x v (EApp f a)              = EApp (subst x v f) (subst x v a)
+subst _ _ (ELit n)                = ELit n
+subst x v (EAdd e1 e2)            = EAdd (subst x v e1) (subst x v e2)
+subst x v (EOnlyIfOkay s e)       = EOnlyIfOkay s (subst x v e)
+subst x v (EConsentHandler h e)   = EConsentHandler h (subst x v e)
+subst x v (EAttr p d e)           = EAttr p d (subst x v e)
+subst x v (EFeel f e)             = EFeel f (subst x v e)
+subst _ _ EDenied                 = EDenied
+
+-- ---------------------------------------------------------------------------
+-- Audit log
+-- ---------------------------------------------------------------------------
+
+||| A single entry in the audit accumulator A.
+||| ConsentEntry records a handler's decision for a given prompt.
+||| AttrEntry records attribution (person, description) when attr is evaluated.
+public export
+data LogEntry : Type where
+  ConsentEntry : ConsentDecision -> String -> LogEntry
+  AttrEntry    : String -> String -> LogEntry
+
+||| The audit accumulator A — an ordered sequence of log entries.
+public export
+AuditLog : Type
+AuditLog = List LogEntry