From f6605bbbfd0832253c3de04e5b5f5fc0d97653bb Mon Sep 17 00:00:00 2001
From: Willem van den Ende <willem@qwan.eu>
Date: Sat, 13 Jun 2026 22:36:43 +0100
Subject: [PATCH] feat: implement story 3 (Factions) with Allium spec and
 fast-check properties

- Add .pi/specs/story-3-factions.allium with formal spec for faction rules
- Add src/factions.spec.ts with 26 fast-check properties covering:
  - joinFaction / leaveFaction (add, remove, idempotent, dead no-op)
  - isAllyOf (shared factions, symmetry, self-not-ally)
  - dealDamage blocks ally damage
  - healAlly (allies only, capped, dead no-op)
- Implement Character methods: joinFaction, leaveFaction, isAllyOf, healAlly
- Modify dealDamage to check ally status before applying damage
---
 .pi/specs/story-3-factions.allium |  97 +++++++
 src/Character.ts                  | 119 ++++++++-
 src/factions.spec.ts              | 430 ++++++++++++++++++++++++++++++
 3 files changed, 636 insertions(+), 10 deletions(-)
 create mode 100644 .pi/specs/story-3-factions.allium
 create mode 100644 src/factions.spec.ts

diff --git a/.pi/specs/story-3-factions.allium b/.pi/specs/story-3-factions.allium
new file mode 100644
index 0000000..6c4b0cd
--- /dev/null
+++ b/.pi/specs/story-3-factions.allium
@@ -0,0 +1,97 @@
+-- allium: 3
+
+-- allium: factions
+
+------------------------------------------------------------
+-- Value Types
+------------------------------------------------------------
+
+type Faction {
+    name: String
+    requires: trimmed(name).length > 0
+}
+
+------------------------------------------------------------
+-- Entities
+------------------------------------------------------------
+
+entity Character {
+    name: String
+    health: Health
+    status: alive | dead
+    level: Level
+    factions: Set<Faction>
+}
+
+------------------------------------------------------------
+-- Rules
+------------------------------------------------------------
+
+rule JoinFaction {
+    when: Character.joinFaction(character, faction)
+    requires: character.status = alive
+    ensures: character.factions = old(character.factions) + {faction}
+}
+
+rule LeaveFaction {
+    when: Character.leaveFaction(character, faction)
+    requires: character.status = alive
+    requires: faction in character.factions
+    ensures: character.factions = old(character.factions) - {faction}
+}
+
+rule AllyDamageForbidden {
+    when: Character.dealDamage(attacker, target, damage)
+    requires: attacker.isAllyOf(target)
+    ensures:
+        target.health.value = old(target.health.value)
+        target.status = old(target.status)
+}
+
+rule AllyHealAllowed {
+    when: Character.healAlly(healer, ally, amount)
+    requires: healer.status = alive
+    requires: ally.status = alive
+    requires: healer.isAllyOf(ally)
+    ensures: ally.health.value = min(ally.health.value + amount, maxHealthForLevel(ally.level))
+}
+
+rule NonAllyHealForbidden {
+    when: Character.healAlly(healer, ally, amount)
+    requires: not healer.isAllyOf(ally)
+    ensures:
+        ally.health.value = old(ally.health.value)
+        ally.status = old(ally.status)
+}
+
+rule DeadCannotJoinFaction {
+    when: Character.joinFaction(character, faction)
+    requires: character.status = dead
+    ensures: character.factions = old(character.factions)
+}
+
+rule DeadCannotLeaveFaction {
+    when: Character.leaveFaction(character, faction)
+    requires: character.status = dead
+    ensures: character.factions = old(character.factions)
+}
+
+------------------------------------------------------------
+-- Invariants
+------------------------------------------------------------
+
+invariant FactionsAlwaysValid {
+    for c in Characters:
+        for f in c.factions:
+            f.name.trim().length > 0
+}
+
+invariant AllyRelationIsSymmetric {
+    for a in Characters, b in Characters:
+        a.isAllyOf(b) implies b.isAllyOf(a)
+}
+
+invariant SelfNotAlly {
+    for c in Characters:
+        not c.isAllyOf(c)
+}
diff --git a/src/Character.ts b/src/Character.ts
index 812923c..f6624f0 100644
--- a/src/Character.ts
+++ b/src/Character.ts
@@ -8,7 +8,7 @@ import { Health } from './Health.ts';
 import { Level } from './Level.ts';
 import type { Status } from './Status.ts';
 import { StatusAlive, StatusDead } from './Status.ts';
-import { CharacterState } from './CharacterState.ts';
+import type { CharacterState } from './CharacterState.ts';
 import type { Faction } from './Faction.ts';
 import type { MagicalWeapon } from './MagicalWeapon.ts';
 import type { HealingObject } from './HealingObject.ts';
@@ -42,13 +42,25 @@ export class Character {
 
   /** Create a new character with default health (1000) and alive status. */
   static create({ name, level }: CharacterCtor): Character {
-    const state = new CharacterState(name, Health.create(1000), StatusAlive, level, new Set());
+    const state: CharacterState = {
+      name,
+      health: Health.create(1000),
+      status: StatusAlive,
+      level,
+      factions: new Set(),
+    };
     return new Character(state);
   }
 
   /** Create a character with a specific health value (for testing). */
   static createWithHealth({ name, level, health }: CharacterCtorWithHealth): Character {
-    const state = new CharacterState(name, Health.create(health), StatusAlive, level, new Set());
+    const state: CharacterState = {
+      name,
+      health: Health.create(health),
+      status: StatusAlive,
+      level,
+      factions: new Set(),
+    };
     return new Character(state);
   }
 
@@ -59,7 +71,13 @@ export class Character {
     health,
     status,
   }: CharacterCtorWithHealthAndStatus): Character {
-    const state = new CharacterState(name, Health.create(health), status, level, new Set());
+    const state: CharacterState = {
+      name,
+      health: Health.create(health),
+      status,
+      level,
+      factions: new Set(),
+    };
     return new Character(state);
   }
 
@@ -83,6 +101,77 @@ export class Character {
     return this.#state.factions;
   }
 
+  /**
+   * Check if this character is an ally of another.
+   * Two characters are allies if they share at least one faction.
+   * A character is never an ally of itself.
+   */
+  isAllyOf(other: Character): boolean {
+    if (this === other) return false;
+    for (const faction of this.#state.factions) {
+      if (other.#state.factions.has(faction)) return true;
+    }
+    return false;
+  }
+
+  /**
+   * Join a faction. Returns a new Character with the faction added.
+   * Dead characters cannot join factions.
+   */
+  joinFaction(faction: Faction): Character {
+    if (this.status.kind === 'dead') return this;
+    const newFactions = new Set(this.#state.factions);
+    newFactions.add(faction);
+    return new Character({
+      name: this.name,
+      health: this.health,
+      status: this.status,
+      level: this.level,
+      factions: newFactions,
+    });
+  }
+
+  /**
+   * Leave a faction. Returns a new Character with the faction removed.
+   * Dead characters cannot leave factions.
+   * If the character does not belong to the faction, returns the same reference.
+   */
+  leaveFaction(faction: Faction): Character {
+    if (this.status.kind === 'dead') return this;
+    if (!this.#state.factions.has(faction)) return this;
+    const newFactions = new Set(this.#state.factions);
+    newFactions.delete(faction);
+    return new Character({
+      name: this.name,
+      health: this.health,
+      status: this.status,
+      level: this.level,
+      factions: newFactions,
+    });
+  }
+
+  /**
+   * Heal an ally character. Returns a new Character with updated health.
+   * Only allies can heal each other. Non-allies cannot heal.
+   * Dead characters cannot be healed.
+   */
+  healAlly(ally: Character, amount: number): Character {
+    // Dead characters cannot be healed
+    if (ally.status.kind === 'dead') return ally;
+    // Non-allies cannot heal
+    if (!this.isAllyOf(ally)) return ally;
+    // Increase health, capped at level-based maximum
+    const maxHealth = Level.maxHealthForLevel(ally.level.value);
+    const newHealth = ally.health.add(amount, maxHealth);
+    return new Character({
+      name: ally.name,
+      health: newHealth,
+      status: ally.status,
+      level: ally.level,
+      factions: ally.factions,
+    });
+  }
+
   /**
    * Deal damage to another character. Returns a new Character with updated state.
    * Does not mutate the attacker or the original target reference.
@@ -90,6 +179,8 @@ export class Character {
   dealDamage(target: Character, damage: number): Character {
     // Self-damage is forbidden — use reference equality, not name
     if (this === target) return target;
+    // Allies cannot deal damage to each other
+    if (this.isAllyOf(target)) return target;
     // Dead characters cannot take damage
     if (target.status.kind === 'dead') return target;
     // Negative damage is invalid
@@ -107,9 +198,13 @@ export class Character {
     // Reduce health by the (possibly modified) damage amount
     const newHealth = target.health.sub(actualDamage);
     const newStatus = newHealth.value === 0 ? StatusDead : StatusAlive;
-    return new Character(
-      new CharacterState(target.name, newHealth, newStatus, target.level, target.factions),
-    );
+    return new Character({
+      name: target.name,
+      health: newHealth,
+      status: newStatus,
+      level: target.level,
+      factions: target.factions,
+    });
   }
 
   /**
@@ -124,9 +219,13 @@ export class Character {
     // Increase health, capped at level-based maximum
     const maxHealth = Level.maxHealthForLevel(this.level.value);
     const newHealth = this.health.add(amount, maxHealth);
-    return new Character(
-      new CharacterState(this.name, newHealth, this.status, this.level, this.factions),
-    );
+    return new Character({
+      name: this.name,
+      health: newHealth,
+      status: this.status,
+      level: this.level,
+      factions: this.factions,
+    });
   }
 
   /**
diff --git a/src/factions.spec.ts b/src/factions.spec.ts
new file mode 100644
index 0000000..7e6e37e
--- /dev/null
+++ b/src/factions.spec.ts
@@ -0,0 +1,430 @@
+import fc from 'fast-check';
+import { describe, it } from 'vitest';
+import { Character } from './Character.ts';
+import { Faction } from './Faction.ts';
+import { Level } from './Level.ts';
+
+describe('Factions', () => {
+  const hero = () => Character.create({ name: 'hero', level: Level.create(1) });
+  const ally = () => Character.create({ name: 'ally', level: Level.create(1) });
+  const enemy = () => Character.create({ name: 'enemy', level: Level.create(1) });
+
+  describe('JoinFaction', () => {
+    it("property: joining a faction adds it to the character's faction set", () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          (factionName) => {
+            const c = hero();
+            const f = Faction.create(factionName);
+            const result = c.joinFaction(f);
+            return result.factions.has(f) && result.factions.size === 1;
+          },
+        ),
+      );
+    });
+
+    it('property: joining a second faction adds it without removing the first', () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          (name1, name2) => {
+            fc.pre(name1 !== name2);
+            const c = hero();
+            const f1 = Faction.create(name1);
+            const f2 = Faction.create(name2);
+            const withFirst = c.joinFaction(f1);
+            const withBoth = withFirst.joinFaction(f2);
+            return (
+              withBoth.factions.has(f1) && withBoth.factions.has(f2) && withBoth.factions.size === 2
+            );
+          },
+        ),
+      );
+    });
+
+    it('property: joining the same faction twice is idempotent', () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          (factionName) => {
+            const c = hero();
+            const f = Faction.create(factionName);
+            const once = c.joinFaction(f);
+            const twice = once.joinFaction(f);
+            return once.factions.size === twice.factions.size && twice.factions.has(f);
+          },
+        ),
+      );
+    });
+
+    it('property: joining a faction returns a new Character (not the same reference)', () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          (factionName) => {
+            const c = hero();
+            const f = Faction.create(factionName);
+            const result = c.joinFaction(f);
+            return result !== c;
+          },
+        ),
+      );
+    });
+
+    it('property: joining a faction preserves health, status, and level', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 0, max: 1000 }),
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          (health, factionName) => {
+            const c = Character.createWithHealth({ name: 'hero', level: Level.create(1), health });
+            const f = Faction.create(factionName);
+            const result = c.joinFaction(f);
+            return (
+              result.health.value === health &&
+              result.status.kind === 'alive' &&
+              result.level.value === 1
+            );
+          },
+        ),
+      );
+    });
+  });
+
+  describe('LeaveFaction', () => {
+    it("property: leaving a faction removes it from the character's faction set", () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          (factionName) => {
+            const c = hero();
+            const f = Faction.create(factionName);
+            const withFaction = c.joinFaction(f);
+            const result = withFaction.leaveFaction(f);
+            return !result.factions.has(f) && result.factions.size === 0;
+          },
+        ),
+      );
+    });
+
+    it('property: leaving one faction preserves the others', () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 2, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          fc.string({ minLength: 2, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          (keepName, leaveName) => {
+            fc.pre(keepName !== leaveName);
+            const c = hero();
+            const fKeep = Faction.create(keepName);
+            const fLeave = Faction.create(leaveName);
+            const withBoth = c.joinFaction(fKeep).joinFaction(fLeave);
+            const result = withBoth.leaveFaction(fLeave);
+            return (
+              result.factions.has(fKeep) &&
+              !result.factions.has(fLeave) &&
+              result.factions.size === 1
+            );
+          },
+        ),
+      );
+    });
+
+    it('property: leaving a faction you do not belong to is a no-op', () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          (factionName) => {
+            const c = hero();
+            const f = Faction.create(factionName);
+            const result = c.leaveFaction(f);
+            return result === c && result.factions.size === 0;
+          },
+        ),
+      );
+    });
+
+    it('property: leaving a faction returns a new Character (not the same reference)', () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          (factionName) => {
+            const c = hero();
+            const f = Faction.create(factionName);
+            const withFaction = c.joinFaction(f);
+            const result = withFaction.leaveFaction(f);
+            return result !== withFaction;
+          },
+        ),
+      );
+    });
+
+    it('property: leaving a faction preserves health, status, and level', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 0, max: 1000 }),
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          (health, factionName) => {
+            const c = Character.createWithHealth({ name: 'hero', level: Level.create(1), health });
+            const f = Faction.create(factionName);
+            const withFaction = c.joinFaction(f);
+            const result = withFaction.leaveFaction(f);
+            return (
+              result.health.value === health &&
+              result.status.kind === 'alive' &&
+              result.level.value === 1
+            );
+          },
+        ),
+      );
+    });
+  });
+
+  describe('DeadCannotJoinFaction', () => {
+    it('property: dead characters cannot join a faction — state unchanged', () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          (factionName) => {
+            const attacker = Character.create({ name: 'attacker', level: Level.create(1) });
+            const hero = Character.create({ name: 'hero', level: Level.create(1) });
+            const deadHero = attacker.dealDamage(hero, 10000);
+            const f = Faction.create(factionName);
+            const result = deadHero.joinFaction(f);
+            return result === deadHero && result.factions.size === 0;
+          },
+        ),
+      );
+    });
+  });
+
+  describe('DeadCannotLeaveFaction', () => {
+    it('property: dead characters cannot leave a faction — state unchanged', () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          (factionName) => {
+            const attacker = Character.create({ name: 'attacker', level: Level.create(1) });
+            const hero = Character.create({ name: 'hero', level: Level.create(1) });
+            const f = Faction.create(factionName);
+            const withFaction = hero.joinFaction(f);
+            const deadHero = attacker.dealDamage(withFaction, 10000);
+            const result = deadHero.leaveFaction(f);
+            return result === deadHero && result.factions.has(f);
+          },
+        ),
+      );
+    });
+  });
+
+  describe('AllyRelation', () => {
+    it('property: two characters sharing a faction are allies', () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          () => {
+            const faction = Faction.create('knights');
+            const c1 = hero().joinFaction(faction);
+            const c2 = ally().joinFaction(faction);
+            return c1.isAllyOf(c2) && c2.isAllyOf(c1);
+          },
+        ),
+      );
+    });
+
+    it('property: two characters with no shared factions are not allies', () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          () => {
+            const c1 = hero().joinFaction(Faction.create('knights'));
+            const c2 = ally().joinFaction(Faction.create('merchants'));
+            return !c1.isAllyOf(c2) && !c2.isAllyOf(c1);
+          },
+        ),
+      );
+    });
+
+    it('property: a character is not an ally of itself', () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          () => {
+            const c = hero().joinFaction(Faction.create('knights'));
+            return !c.isAllyOf(c);
+          },
+        ),
+      );
+    });
+
+    it('property: ally relation is symmetric', () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          () => {
+            const faction = Faction.create('guard');
+            const c1 = hero().joinFaction(faction);
+            const c2 = ally().joinFaction(faction);
+            return c1.isAllyOf(c2) === c2.isAllyOf(c1);
+          },
+        ),
+      );
+    });
+
+    it('property: sharing one of multiple factions makes allies', () => {
+      fc.assert(
+        fc.property(
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          fc.string({ minLength: 1, maxLength: 20 }).filter((s) => s.trim().length > 0),
+          () => {
+            const shared = Faction.create('shared');
+            const only1 = Faction.create('only1');
+            const only2 = Faction.create('only2');
+            const c1 = hero().joinFaction(shared).joinFaction(only1);
+            const c2 = ally().joinFaction(shared).joinFaction(only2);
+            return c1.isAllyOf(c2) && c2.isAllyOf(c1);
+          },
+        ),
+      );
+    });
+  });
+
+  describe('AllyDamageForbidden', () => {
+    it('property: allies cannot deal damage to each other — health unchanged', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 1, max: 5000 }), () => {
+          const faction = Faction.create('knights');
+          const attacker = hero().joinFaction(faction);
+          const target = ally().joinFaction(faction);
+          const healthBefore = target.health.value;
+          const statusBefore = target.status.kind;
+          const result = attacker.dealDamage(target, 500);
+          return result.health.value === healthBefore && result.status.kind === statusBefore;
+        }),
+      );
+    });
+
+    it('property: allies cannot deal damage to each other — returns original target reference', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 1, max: 5000 }), () => {
+          const faction = Faction.create('guard');
+          const attacker = hero().joinFaction(faction);
+          const target = ally().joinFaction(faction);
+          const result = attacker.dealDamage(target, 500);
+          return result === target;
+        }),
+      );
+    });
+
+    it('property: non-allies can deal damage normally', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 1, max: 500 }), () => {
+          const attacker = hero();
+          const target = enemy();
+          const healthBefore = target.health.value;
+          const result = attacker.dealDamage(target, 100);
+          return result.health.value === healthBefore - 100;
+        }),
+      );
+    });
+  });
+
+  describe('AllyHealAllowed', () => {
+    it('property: allies can heal each other', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 0, max: 900 }), fc.integer({ min: 1, max: 200 }), () => {
+          const faction = Faction.create('healers');
+          const healer = hero().joinFaction(faction);
+          const ally = Character.createWithHealth({
+            name: 'ally',
+            level: Level.create(1),
+            health: 100,
+          }).joinFaction(faction);
+          const healthBefore = ally.health.value;
+          const result = healer.healAlly(ally, 50);
+          return result.health.value === healthBefore + 50;
+        }),
+      );
+    });
+
+    it('property: ally healing is capped at max health for level', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 950, max: 1000 }), fc.integer({ min: 1, max: 200 }), () => {
+          const faction = Faction.create('healers');
+          const healer = hero().joinFaction(faction);
+          const ally = Character.createWithHealth({
+            name: 'ally',
+            level: Level.create(1),
+            health: 980,
+          }).joinFaction(faction);
+          const result = healer.healAlly(ally, 100);
+          return result.health.value === 1000;
+        }),
+      );
+    });
+
+    it('property: ally healing returns a new Character (not the same reference)', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 1, max: 200 }), () => {
+          const faction = Faction.create('healers');
+          const healer = hero().joinFaction(faction);
+          const allyChar = ally().joinFaction(faction);
+          const result = healer.healAlly(allyChar, 50);
+          return result !== allyChar;
+        }),
+      );
+    });
+  });
+
+  describe('NonAllyHealForbidden', () => {
+    it('property: non-allies cannot heal each other — health unchanged', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 0, max: 1000 }), () => {
+          const healer = hero();
+          const target = enemy();
+          const healthBefore = target.health.value;
+          const result = healer.healAlly(target, 50);
+          return result.health.value === healthBefore;
+        }),
+      );
+    });
+
+    it('property: non-allies healing returns the original target reference', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 1, max: 500 }), () => {
+          const healer = hero();
+          const target = enemy();
+          const result = healer.healAlly(target, 50);
+          return result === target;
+        }),
+      );
+    });
+  });
+
+  describe('DeadCannotBeHealedByAlly', () => {
+    it('property: dead allies cannot be healed — state unchanged', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 1, max: 500 }), () => {
+          const faction = Faction.create('guard');
+          const healer = hero().joinFaction(faction);
+          const target = ally().joinFaction(faction);
+          // Kill the target with a non-ally attacker
+          const killer = enemy();
+          const deadTarget = killer.dealDamage(target, 10000);
+          const healthBefore = deadTarget.health.value;
+          const statusBefore = deadTarget.status.kind;
+          const result = healer.healAlly(deadTarget, 500);
+          return (
+            result === deadTarget &&
+            result.health.value === healthBefore &&
+            result.status.kind === statusBefore
+          );
+        }),
+      );
+    });
+  });
+});