feat: add RCOQ proofs for WG05.

Signed-off-by: Amlal El Mahrouss <amlal@nekernel.org>

5 files changed, 491 insertions, 0 deletions

diff --git a/proofs/Makefile b/proofs/Makefile
new file mode 100644
index 0000000..2391e6d
--- /dev/null
+++ b/proofs/Makefile
@@ -0,0 +1,13 @@
+COQMAKEFILE ?= Makefile.coq
+
+all: $(COQMAKEFILE)
+	$(MAKE) -f $(COQMAKEFILE)
+
+$(COQMAKEFILE): _CoqProject
+	coq_makefile -f _CoqProject -o $(COQMAKEFILE)
+
+clean: $(COQMAKEFILE)
+	$(MAKE) -f $(COQMAKEFILE) clean
+	rm -f $(COQMAKEFILE) $(COQMAKEFILE).conf
+
+.PHONY: all clean
diff --git a/proofs/WG05/ExecutionAuthority.v b/proofs/WG05/ExecutionAuthority.v
new file mode 100644
index 0000000..f4cb5e2
--- /dev/null
+++ b/proofs/WG05/ExecutionAuthority.v
@@ -0,0 +1,169 @@
+(*
+  WG05: Execution Authority Theory
+
+  An execution authority is responsible for defining whose semantics
+  may be used for an execution context.
+
+  Author: Amlal El Mahrouss
+  Formalization: January 2026
+*)
+
+Require Import Stdlib.Logic.Classical_Prop.
+Require Import WG05.ExecutionDomains.
+
+(** * Traits *)
+
+(** A trait is a set of formal rules defining the semantic concepts
+    of an execution context *)
+Record Trait : Type := mkTrait {
+  Rules : Type;
+  valid : Rules -> Prop;
+  trait_compose : Rules -> Rules -> Rules;
+  compose_preserves_valid :
+    forall r1 r2, valid r1 -> valid r2 -> valid (trait_compose r1 r2)
+}.
+
+(** * Execution Authority *)
+
+(** An execution authority of type T, where T is a trait *)
+Record ExecutionAuthority (T : Trait) : Type := mkExecutionAuthority {
+  governs : Rules T -> Prop;
+  authority_valid : forall r, governs r -> valid T r
+}.
+
+Arguments governs {T}.
+Arguments authority_valid {T}.
+
+(** * Semantic Substitutability *)
+
+(** Two execution contexts are semantically substitutable if one can
+    be used in place of the other while preserving semantic properties *)
+Record SemanticSubstitutability (EC1 EC2 : ExecutionContext) : Type :=
+  mkSemanticSubstitutability {
+    subst_forward : Context EC1 -> Context EC2;
+    subst_backward : Context EC2 -> Context EC1;
+    subst_roundtrip : forall c, subst_backward (subst_forward c) = c
+  }.
+
+(** Propositional version: contexts are substitutable if there exists
+    a substitutability witness *)
+Definition Substitutable (EC1 EC2 : ExecutionContext) : Prop :=
+  inhabited (SemanticSubstitutability EC1 EC2).
+
+(** * Core Theorems *)
+
+Section AuthorityTheorems.
+
+(** Property 1: If X does not equal or is not semantically substitutable
+    with E (or vice versa), then C shall not equal Z *)
+
+(** The domain separation theorem states that without context equality
+    or semantic substitutability, domains cannot be meaningfully equivalent.
+
+    This is stated as an axiom because the proof requires additional
+    axioms about context identity that are domain-specific. *)
+
+Axiom domain_separation_by_context :
+  forall (EC1 EC2 : ExecutionContext)
+         (C : ExecutionDomain EC1)
+         (Z : ExecutionDomain EC2),
+    EC1 <> EC2 ->
+    ~ Substitutable EC1 EC2 ->
+    (* Conclusion: The domains cannot be semantically equivalent *)
+    ~ (exists (f : Domain C -> Domain Z) (g : Domain Z -> Domain C),
+         (forall x, g (f x) = x) /\ (forall y, f (g y) = y)).
+
+(** Property 2: Null execution context theory
+    If Z or C are defined as a null execution context,
+    then N <> not N (a context is not equal to its negation) *)
+
+(** First, define what a null context means *)
+Record NullContext (EC : ExecutionContext) : Type := mkNullContext {
+  null : Context EC;
+  is_null : forall c : Context EC, {c = null} + {c <> null}
+}.
+
+(** The negation of a context (in the semantic sense) *)
+Record ContextNegation (EC : ExecutionContext) : Type := mkContextNegation {
+  negate : Context EC -> Context EC;
+  negate_involutive : forall c, negate (negate c) = c;
+  context_not_negation : forall c, c <> negate c
+}.
+
+(** Theorem: N <> not N *)
+Theorem null_not_negation :
+  forall (EC : ExecutionContext)
+         (NC : NullContext EC)
+         (CN : ContextNegation EC),
+    null EC NC <> negate EC CN (null EC NC).
+Proof.
+  intros EC NC CN.
+  apply context_not_negation.
+Qed.
+
+End AuthorityTheorems.
+
+(** * Authority Composition *)
+
+Section AuthorityComposition.
+
+Record CompatibleAuthorities (T1 T2 : Trait) : Type := mkCompatibleAuthorities {
+  A1 : ExecutionAuthority T1;
+  A2 : ExecutionAuthority T2;
+  rule_compat : Rules T1 -> Rules T2
+}.
+
+(** When authorities are compatible, they can be combined *)
+Theorem compose_authorities :
+  forall (T1 T2 : Trait)
+         (compat : CompatibleAuthorities T1 T2)
+         (r : Rules T1),
+    governs (A1 T1 T2 compat) r ->
+    exists r', r' = rule_compat T1 T2 compat r.
+Proof.
+  intros T1 T2 compat r Hgov.
+  exists (rule_compat T1 T2 compat r).
+  reflexivity.
+Qed.
+
+End AuthorityComposition.
+
+(** * Additional Properties *)
+
+Section AdditionalProperties.
+
+(** Two authorities over the same trait are compatible if they
+    agree on what they govern *)
+Definition authorities_agree {T : Trait} (A1 A2 : ExecutionAuthority T) : Prop :=
+  forall r, governs A1 r <-> governs A2 r.
+
+(** Agreement is an equivalence relation *)
+Lemma authorities_agree_refl :
+  forall (T : Trait) (A : ExecutionAuthority T),
+    authorities_agree A A.
+Proof.
+  intros T A r.
+  split; auto.
+Qed.
+
+Lemma authorities_agree_sym :
+  forall (T : Trait) (A1 A2 : ExecutionAuthority T),
+    authorities_agree A1 A2 -> authorities_agree A2 A1.
+Proof.
+  intros T A1 A2 H r.
+  split; apply H.
+Qed.
+
+Lemma authorities_agree_trans :
+  forall (T : Trait) (A1 A2 A3 : ExecutionAuthority T),
+    authorities_agree A1 A2 ->
+    authorities_agree A2 A3 ->
+    authorities_agree A1 A3.
+Proof.
+  intros T A1 A2 A3 H12 H23 r.
+  split; intro H.
+  - apply H23. apply H12. exact H.
+  - apply H12. apply H23. exact H.
+Qed.
+
+End AdditionalProperties.
diff --git a/proofs/WG05/ExecutionDomains.v b/proofs/WG05/ExecutionDomains.v
new file mode 100644
index 0000000..534840a
--- /dev/null
+++ b/proofs/WG05/ExecutionDomains.v
@@ -0,0 +1,110 @@
+(*
+  WG05: Execution Domains Theory
+
+  An execution domain defines a boundary for execution semantics,
+  resource visibility, and control flow.
+
+  Author: Amlal El Mahrouss
+  Formalization: January 2026
+*)
+
+Require Import Stdlib.Logic.Classical_Prop.
+Require Import Stdlib.Logic.FunctionalExtensionality.
+
+(** * Execution Contexts *)
+
+(** Execution contexts are abstract semantic parameters *)
+Record ExecutionContext : Type := mkExecutionContext {
+  Context : Type;
+  context_eq_dec : forall (c1 c2 : Context), {c1 = c2} + {c1 <> c2}
+}.
+
+(** * Execution Domains *)
+
+(** An execution domain is indexed by an execution context *)
+Record ExecutionDomain (EC : ExecutionContext) : Type := mkExecutionDomain {
+  Domain : Type;
+  domain_context : Context EC;
+  SubProgram : Type;
+  compose : SubProgram -> Domain
+}.
+
+Arguments Domain {EC}.
+Arguments domain_context {EC}.
+Arguments SubProgram {EC}.
+Arguments compose {EC}.
+
+(** * Core Theorem: Domains with Different Contexts are Distinct *)
+
+Section DomainSeparation.
+
+Variable EC : ExecutionContext.
+
+(** Two domains with provably different contexts cannot be equal
+    in any meaningful semantic sense *)
+Record DomainEquivalence (D1 D2 : ExecutionDomain EC) : Prop := mkDomainEquivalence {
+  context_eq : domain_context D1 = domain_context D2;
+  domain_iso : exists (f : Domain D1 -> Domain D2), True
+}.
+
+(** The separation theorem: different contexts imply distinct domains *)
+Theorem separation_theorem :
+  forall (D1 D2 : ExecutionDomain EC),
+    domain_context D1 <> domain_context D2 ->
+    ~ DomainEquivalence D1 D2.
+Proof.
+  intros D1 D2 Hneq Heq.
+  destruct Heq as [Hctx _].
+  contradiction.
+Qed.
+
+End DomainSeparation.
+
+(** * Composition Property *)
+
+(** Domains may be composed of sub-programs within the execution context *)
+Record ComposableDomain (EC : ExecutionContext) : Type := mkComposableDomain {
+  base : ExecutionDomain EC;
+  composition_preserves_context :
+    forall (sp : SubProgram base),
+      exists d, d = compose base sp
+}.
+
+(** * Context Abstraction *)
+
+(** Execution contexts are treated as abstract semantic parameters.
+    This section provides the abstraction barrier. *)
+
+Section ContextAbstraction.
+
+(** A context family abstracts over specific context implementations *)
+Record ContextFamily : Type := mkContextFamily {
+  Contexts : Type;
+  mkContext : Contexts -> ExecutionContext
+}.
+
+(** Domains can be parameterized by context families *)
+Definition DomainFamily (cf : ContextFamily) : Type :=
+  forall (c : Contexts cf), ExecutionDomain (mkContext cf c).
+
+End ContextAbstraction.
+
+(** * Properties about Domain Inequality *)
+
+Section DomainInequality.
+
+(** If two domains belong to different execution contexts,
+    they cannot be structurally equal *)
+Lemma domains_different_contexts_not_equal :
+  forall (EC1 EC2 : ExecutionContext)
+         (D1 : ExecutionDomain EC1)
+         (D2 : ExecutionDomain EC2),
+    EC1 <> EC2 ->
+    ~ (exists (H : EC1 = EC2),
+         eq_rect EC1 ExecutionDomain D1 EC2 H = D2).
+Proof.
+  intros EC1 EC2 D1 D2 Hneq [H _].
+  contradiction.
+Qed.
+
+End DomainInequality.
diff --git a/proofs/WG05/HarvardSeparation.v b/proofs/WG05/HarvardSeparation.v
new file mode 100644
index 0000000..127b57d
--- /dev/null
+++ b/proofs/WG05/HarvardSeparation.v
@@ -0,0 +1,194 @@
+(*
+  WG05: The General Harvard Separation Axiom
+
+  This module formalizes the axiom that execution semantics (G) are
+  primitive and cannot be derived from computational behavior theories (O).
+
+  Key insight: Any theory O that models computation requires execution
+  to occur, thus implicitly depending on G's primitives. Attempting to
+  derive G from O creates circular dependency.
+
+  Author: Amlal El Mahrouss
+  Formalization: January 2026
+*)
+
+Require Import Stdlib.Logic.Classical_Prop.
+
+(** * Theory Structure *)
+
+(** A theory is characterized by its primitives and derivable statements *)
+Record Theory : Type := mkTheory {
+  Primitive : Type;
+  Statement : Type;
+  derives : Primitive -> Statement -> Prop;
+  consistent : exists s, forall p, ~ derives p s
+}.
+
+Notation "p ⊢ s" := (derives _ p s) (at level 70).
+
+(** * Theory Dependencies *)
+
+(** One theory depends on another if it requires the other's primitives.
+    The dependency is witnessed by a mapping from T1's primitives to T2's
+    primitives, along with evidence that T2 has primitives (is non-empty). *)
+Record DependsOn (T1 T2 : Theory) : Type := mkDependsOn {
+  primitive_requirement : Primitive T1 -> Primitive T2;
+  target_inhabited : Primitive T2
+}.
+
+Arguments primitive_requirement {T1 T2}.
+Arguments target_inhabited {T1 T2}.
+
+Notation "T1 ⇒ T2" := (DependsOn T1 T2) (at level 80).
+
+(** Propositional version for use in negations *)
+Definition Depends (T1 T2 : Theory) : Prop := inhabited (DependsOn T1 T2).
+
+(** * Execution Semantics Theory (G) *)
+
+(** G formally defines execution semantics: domains, contexts, authority *)
+Record ExecutionSemanticsTheory : Type := mkExecutionSemanticsTheory {
+  G_theory : Theory;
+  has_domains : Primitive G_theory;
+  has_contexts : Primitive G_theory;
+  has_authority : Primitive G_theory;
+  domains_neq_contexts : has_domains <> has_contexts;
+  contexts_neq_authority : has_contexts <> has_authority
+}.
+
+(** * Computational Behavior Theory (O) *)
+
+(** O is any theory of computational behavior *)
+Record ComputationalTheory : Type := mkComputationalTheory {
+  O_theory : Theory;
+  models_computation : Statement O_theory;
+  requires_execution : Prop
+}.
+
+(** * The General Harvard Separation Axiom *)
+
+Section HarvardSeparationAxiom.
+
+(** Property 1: If O models computation, then O requires execution to occur *)
+Axiom computation_requires_execution :
+  forall (O : ComputationalTheory), requires_execution O.
+
+(** Property 2: O implicitly depends on G's primitives
+    (execution must be defined for computation to be theorized) *)
+Definition implicit_dependency (G : ExecutionSemanticsTheory) (O : ComputationalTheory)
+    (H : requires_execution O) : DependsOn (O_theory O) (G_theory G) :=
+  {| primitive_requirement := fun _ => has_domains G
+   ; target_inhabited := has_domains G
+   |}.
+
+(** Property 3: G does not depend on O
+    (execution semantics are primitive, not derived from computational models) *)
+
+(** Circular dependency is when A depends on B and B depends on A *)
+Definition CircularDependency (T1 T2 : Theory) : Prop :=
+  Depends T1 T2 /\ Depends T2 T1.
+
+(** Axiom: Circular dependencies in foundational theories are impossible.
+    This captures the intuition that we cannot have A defined in terms of B
+    while B is simultaneously defined in terms of A. *)
+Axiom no_circular_foundations :
+  forall (T1 T2 : Theory), ~ CircularDependency T1 T2.
+
+(** Main Theorem: G cannot be derived from O
+    If G were derivable from O, this would create circular dependency *)
+Theorem G_not_derivable_from_O :
+  forall (G : ExecutionSemanticsTheory) (O : ComputationalTheory),
+    DependsOn (G_theory G) (O_theory O) -> False.
+Proof.
+  intros G O H_G_dep_O.
+  apply (no_circular_foundations (G_theory G) (O_theory O)).
+  split.
+  - exact (inhabits H_G_dep_O).
+  - exact (inhabits (implicit_dependency G O (computation_requires_execution O))).
+Qed.
+
+(** Corollary: G must be axiomatic.
+    G is a foundational primitive that cannot be reduced to
+    other computational theories. *)
+Record Axiomatic (T : Theory) : Prop := mkAxiomatic {
+  not_derivable : forall (O : ComputationalTheory), DependsOn T (O_theory O) -> False
+}.
+
+Theorem G_is_axiomatic :
+  forall (G : ExecutionSemanticsTheory),
+    Axiomatic (G_theory G).
+Proof.
+  intro G.
+  apply mkAxiomatic.
+  intros O.
+  apply G_not_derivable_from_O.
+Qed.
+
+End HarvardSeparationAxiom.
+
+(** * Impossibility of G = O or G ⊆ O *)
+
+Section ImpossibilityResults.
+
+(** Theory equality (both derive from each other) *)
+Definition theory_equiv (T1 T2 : Theory) : Prop :=
+  Depends T1 T2 /\ Depends T2 T1.
+
+Notation "T1 ≈ T2" := (theory_equiv T1 T2) (at level 70).
+
+(** Theory subsumption (one is contained in the other) *)
+Definition theory_subsumes (T1 T2 : Theory) : Prop :=
+  Depends T1 T2.
+
+Notation "T1 ⊆ T2" := (theory_subsumes T1 T2) (at level 70).
+
+(** Theorem: G ≠ O (G cannot equal O) *)
+Theorem G_not_equiv_O :
+  forall (G : ExecutionSemanticsTheory) (O : ComputationalTheory),
+    ~ theory_equiv (G_theory G) (O_theory O).
+Proof.
+  intros G O [[H_G_dep_O] _].
+  apply (G_not_derivable_from_O G O).
+  exact H_G_dep_O.
+Qed.
+
+(** Theorem: G ⊄ O (G cannot be subsumed by O) *)
+Theorem G_not_subsumed_by_O :
+  forall (G : ExecutionSemanticsTheory) (O : ComputationalTheory),
+    ~ theory_subsumes (G_theory G) (O_theory O).
+Proof.
+  intros G O [H].
+  apply (G_not_derivable_from_O G O).
+  exact H.
+Qed.
+
+End ImpossibilityResults.
+
+(** * Additional Meta-Theoretic Properties *)
+
+Section MetaTheory.
+
+(** The dependency relation is transitive *)
+Lemma depends_on_trans :
+  forall (T1 T2 T3 : Theory),
+    DependsOn T1 T2 -> DependsOn T2 T3 -> DependsOn T1 T3.
+Proof.
+  intros T1 T2 T3 H12 H23.
+  exact {| primitive_requirement := fun p => primitive_requirement H23 (primitive_requirement H12 p)
+         ; target_inhabited := target_inhabited H23
+         |}.
+Qed.
+
+(** If G is axiomatic and O depends on G, then O cannot be axiomatic
+    with respect to theories that G depends on *)
+Lemma axiomatic_asymmetry :
+  forall (G : ExecutionSemanticsTheory) (O : ComputationalTheory),
+    DependsOn (O_theory O) (G_theory G) ->
+    Axiomatic (G_theory G) ->
+    DependsOn (G_theory G) (O_theory O) -> False.
+Proof.
+  intros G O H_O_dep_G H_G_ax.
+  apply (not_derivable _ H_G_ax).
+Qed.
+
+End MetaTheory.
diff --git a/proofs/_CoqProject b/proofs/_CoqProject
new file mode 100644
index 0000000..ffb5f3e
--- /dev/null
+++ b/proofs/_CoqProject
@@ -0,0 +1,5 @@
+-R WG05 WG05
+
+WG05/ExecutionDomains.v
+WG05/ExecutionAuthority.v
+WG05/HarvardSeparation.v