feat: Magical Objects story — weapons and healing items

- MagicalWeapon: fixed damage, owner-only, self-destructs at 0 HP
- HealingObject: heals characters up to both caps, self-destructs at 0 HP
- 18 fast-check properties covering rules and invariants
- Allium spec with entities, rules, and invariants
- Character.createWithHealthAndStatus factory method for status-aware creation

.pi/specs/story-4-magical-objects.allium

@@ -0,0 +1,174 @@
+-- allium: 3
+
+-- allium: magical-objects
+
+------------------------------------------------------------
+-- External Entities
+------------------------------------------------------------
+
+external entity Character {
+    name: String
+    health: Health
+    status: alive | dead
+    level: Level
+    factions: Set<Faction>
+}
+
+external entity Health {
+    value: Integer
+}
+
+external entity Level {
+    value: Integer
+}
+
+external entity Faction {
+    name: String
+}
+
+------------------------------------------------------------
+-- Entities and Variants
+------------------------------------------------------------
+
+entity MagicalWeapon {
+    health: Health
+    maxHealth: Integer
+    status: alive | destroyed
+    damage: Integer
+    owner: Character
+}
+
+entity HealingObject {
+    health: Health
+    maxHealth: Integer
+    status: alive | destroyed
+}
+
+------------------------------------------------------------
+-- Rules
+------------------------------------------------------------
+
+rule WeaponDealsDamage {
+    when: MagicalWeapon.dealsDamage(weapon, target, attacker)
+    requires: weapon.status = alive
+    requires: attacker = weapon.owner
+    requires: attacker.status = alive
+    ensures: target.health.value = max(0, target.health.value - weapon.damage)
+    ensures: weapon.health.value = weapon.health.value - 1
+    ensures:
+        if weapon.health.value - 1 = 0:
+            weapon.status = destroyed
+        else:
+            weapon.status = alive
+    ensures:
+        if max(0, target.health.value - weapon.damage) = 0:
+            target.status = dead
+        else:
+            target.status = alive
+}
+
+rule DeadCannotUseWeapon {
+    when: MagicalWeapon.dealsDamage(weapon, target, attacker)
+    requires: attacker.status = dead
+    ensures:
+        target.health.value = target.health.value
+        weapon.health.value = weapon.health.value
+        weapon.status = weapon.status
+        target.status = target.status
+}
+
+rule NonOwnerCannotUseWeapon {
+    when: MagicalWeapon.dealsDamage(weapon, target, attacker)
+    requires: attacker != weapon.owner
+    ensures:
+        target.health.value = target.health.value
+        weapon.health.value = weapon.health.value
+        weapon.status = weapon.status
+        target.status = target.status
+}
+
+rule DestroyedWeaponCannotDealDamage {
+    when: MagicalWeapon.dealsDamage(weapon, target, attacker)
+    requires: weapon.status = destroyed
+    ensures:
+        target.health.value = target.health.value
+        weapon.health.value = weapon.health.value
+        weapon.status = weapon.status
+        target.status = target.status
+}
+
+rule HealingObjectHealsCharacter {
+    when: HealingObject.healsCharacter(object, character, amount)
+    requires: object.status = alive
+    requires: character.status = alive
+    ensures: healAmount = min(amount, object.maxHealth - object.health.value)
+    ensures: character.health.value = character.health.value + healAmount
+    ensures: object.health.value = object.health.value - healAmount
+    ensures:
+        if object.health.value - healAmount = 0:
+            object.status = destroyed
+        else:
+            object.status = alive
+}
+
+rule DeadCannotUseHealingObject {
+    when: HealingObject.healsCharacter(object, character, amount)
+    requires: character.status = dead
+    ensures:
+        character.health.value = character.health.value
+        object.health.value = object.health.value
+        object.status = object.status
+}
+
+rule DestroyedHealingObjectCannotHeal {
+    when: HealingObject.healsCharacter(object, character, amount)
+    requires: object.status = destroyed
+    ensures:
+        character.health.value = character.health.value
+        object.health.value = object.health.value
+        object.status = object.status
+}
+
+------------------------------------------------------------
+-- Invariants
+------------------------------------------------------------
+
+invariant WeaponHealthNeverNegative {
+    for w in MagicalWeapons:
+        w.health.value >= 0
+}
+
+invariant WeaponDestroyedAtZeroHealth {
+    for w in MagicalWeapons:
+        w.health.value = 0 implies w.status = destroyed
+}
+
+invariant WeaponMaxHealthNeverExceeded {
+    for w in MagicalWeapons:
+        w.health.value <= w.maxHealth
+}
+
+invariant HealingObjectHealthNeverNegative {
+    for h in HealingObjects:
+        h.health.value >= 0
+}
+
+invariant HealingObjectDestroyedAtZeroHealth {
+    for h in HealingObjects:
+        h.health.value = 0 implies h.status = destroyed
+}
+
+invariant HealingObjectMaxHealthNeverExceeded {
+    for h in HealingObjects:
+        h.health.value <= h.maxHealth
+}
+
+invariant HealingObjectCannotDealDamage {
+    for h in HealingObjects:
+        not h.dealsDamage(_, _)
+}
+
+invariant WeaponCannotHeal {
+    for w in MagicalWeapons:
+        not w.healsCharacter(_, _)
+}

src/Character.ts

@@ -10,6 +10,8 @@ import type { Status } from './Status.ts';
 import { StatusAlive, StatusDead } from './Status.ts';
 import { CharacterState } from './CharacterState.ts';
 import type { Faction } from './Faction.ts';
+import type { MagicalWeapon } from './MagicalWeapon.ts';
+import type { HealingObject } from './HealingObject.ts';
 
 export interface CharacterCtor {
   name: string;
@@ -22,6 +24,13 @@ export interface CharacterCtorWithHealth {
   health: number;
 }
 
+export interface CharacterCtorWithHealthAndStatus {
+  name: string;
+  level: Level;
+  health: number;
+  status: Status;
+}
+
 export class Character {
   #state: CharacterState;
   readonly #name: string;
@@ -43,6 +52,17 @@ export class Character {
     return new Character(state);
   }
 
+  /** Create a character with specific health and status (for use by MagicalWeapon). */
+  static createWithHealthAndStatus({
+    name,
+    level,
+    health,
+    status,
+  }: CharacterCtorWithHealthAndStatus): Character {
+    const state = new CharacterState(name, Health.create(health), status, level, new Set());
+    return new Character(state);
+  }
+
   get name(): string {
     return this.#name;
   }
@@ -108,4 +128,34 @@ export class Character {
       new CharacterState(this.name, newHealth, this.status, this.level, this.factions),
     );
   }
+
+  /**
+   * Use a Magical Weapon to deal damage to a target.
+   * Dead characters cannot use weapons. Only the owner can use a weapon.
+   * Returns updated weapon and target.
+   */
+  useWeapon(
+    weapon: MagicalWeapon,
+    target: Character,
+  ): { weapon: MagicalWeapon; target: Character } {
+    // Dead characters cannot use weapons
+    if (this.status.kind === 'dead') return { weapon, target };
+    // Only the owner can use the weapon
+    if (weapon.owner !== this) return { weapon, target };
+    return weapon.use(target);
+  }
+
+  /**
+   * Use a Healing Object to gain health.
+   * Dead characters cannot use healing objects.
+   * Returns updated object and character.
+   */
+  useHealingObject(
+    object: HealingObject,
+    amount: number,
+  ): { object: HealingObject; character: Character } {
+    // Dead characters cannot use healing objects
+    if (this.status.kind === 'dead') return { object, character: this };
+    return object.heal(this, amount);
+  }
 }

src/HealingObject.ts

@@ -0,0 +1,84 @@
+/**
+ * Healing Object — a Magical Object that gives health to Characters.
+ *
+ * Invariants enforced at construction:
+ * - Health is non-negative
+ * - Health never exceeds maxHealth
+ */
+
+import { Character } from './Character.ts';
+
+export type ObjectStatus = { kind: 'alive' } | { kind: 'destroyed' };
+
+export class HealingObject {
+  readonly #health: number;
+  readonly #maxHealth: number;
+  readonly #status: ObjectStatus;
+
+  private constructor(health: number, maxHealth: number, status: ObjectStatus) {
+    this.#health = health;
+    this.#maxHealth = maxHealth;
+    this.#status = status;
+  }
+
+  static create({
+    maxHealth,
+    currentHealth,
+  }: {
+    maxHealth: number;
+    currentHealth: number;
+  }): HealingObject {
+    if (maxHealth < 0) throw new Error('MaxHealth cannot be negative');
+    if (currentHealth < 0) throw new Error('CurrentHealth cannot be negative');
+    if (currentHealth > maxHealth) throw new Error('CurrentHealth cannot exceed maxHealth');
+    const status =
+      currentHealth === 0 ? { kind: 'destroyed' as const } : { kind: 'alive' as const };
+    return new HealingObject(currentHealth, maxHealth, status);
+  }
+
+  get health(): number {
+    return this.#health;
+  }
+
+  get maxHealth(): number {
+    return this.#maxHealth;
+  }
+
+  get status(): ObjectStatus {
+    return this.#status;
+  }
+
+  /** Use this object to heal a character. Returns updated object and character. */
+  heal(character: Character, amount: number): { object: HealingObject; character: Character } {
+    // Destroyed objects can't heal
+    if (this.#status.kind === 'destroyed') {
+      return { object: this, character };
+    }
+    // Negative amount is invalid
+    if (amount < 0) throw new Error('Heal amount must be non-negative');
+    // Calculate actual heal amount: min of requested, object remaining, character headroom
+    const objectRemaining = this.#health;
+    const characterMax = character.level.value >= 6 ? 1500 : 1000;
+    const characterHeadroom = characterMax - character.health.value;
+    const actualHeal = Math.min(amount, objectRemaining, characterHeadroom);
+    // If actualHeal is 0, nothing changes
+    if (actualHeal === 0) {
+      return { object: this, character };
+    }
+    // Create updated object
+    const newObjectHealth = this.#health - actualHeal;
+    const newObjectStatus =
+      newObjectHealth === 0 ? { kind: 'destroyed' as const } : { kind: 'alive' as const };
+    // Create updated character
+    const newCharacterHealth = character.health.value + actualHeal;
+    const newCharacter = Character.createWithHealth({
+      name: character.name,
+      level: character.level,
+      health: newCharacterHealth,
+    });
+    return {
+      object: new HealingObject(newObjectHealth, this.#maxHealth, newObjectStatus),
+      character: newCharacter,
+    };
+  }
+}

src/MagicalWeapon.ts

@@ -0,0 +1,99 @@
+/**
+ * Magical Weapon — a Magical Object that deals fixed damage.
+ *
+ * Invariants enforced at construction:
+ * - Health is non-negative
+ * - Health never exceeds maxHealth
+ * - Damage is non-negative
+ */
+import { Character } from './Character.ts';
+
+export type WeaponStatus = { kind: 'alive' } | { kind: 'destroyed' };
+
+export class MagicalWeapon {
+  readonly #health: number;
+  readonly #maxHealth: number;
+  readonly #status: WeaponStatus;
+  readonly #damage: number;
+  readonly #owner: Character;
+
+  private constructor(
+    health: number,
+    maxHealth: number,
+    status: WeaponStatus,
+    damage: number,
+    owner: Character,
+  ) {
+    this.#health = health;
+    this.#maxHealth = maxHealth;
+    this.#status = status;
+    this.#damage = damage;
+    this.#owner = owner;
+  }
+
+  static create({
+    maxHealth,
+    damage,
+    owner,
+  }: {
+    maxHealth: number;
+    damage: number;
+    owner: Character;
+  }): MagicalWeapon {
+    if (maxHealth < 0) throw new Error('MaxHealth cannot be negative');
+    if (damage < 0) throw new Error('Damage cannot be negative');
+    return new MagicalWeapon(maxHealth, maxHealth, { kind: 'alive' }, damage, owner);
+  }
+
+  get health(): number {
+    return this.#health;
+  }
+
+  get maxHealth(): number {
+    return this.#maxHealth;
+  }
+
+  get status(): WeaponStatus {
+    return this.#status;
+  }
+
+  get damage(): number {
+    return this.#damage;
+  }
+
+  get owner(): Character {
+    return this.#owner;
+  }
+
+  /** Use this weapon to deal damage. Returns updated weapon and target. */
+  use(target: Character): { weapon: MagicalWeapon; target: Character } {
+    // Destroyed weapons can't be used
+    if (this.#status.kind === 'destroyed') {
+      return { weapon: this, target };
+    }
+    // Deal fixed damage
+    const newTargetHealth = Math.max(0, target.health.value - this.#damage);
+    const newTargetStatus = newTargetHealth === 0 ? { kind: 'dead' as const } : target.status;
+    const newTarget = Character.createWithHealthAndStatus({
+      name: target.name,
+      level: target.level,
+      health: newTargetHealth,
+      status: newTargetStatus,
+    });
+    // Reduce weapon health by 1
+    const newWeaponHealth = this.#health - 1;
+    const newWeaponStatus =
+      newWeaponHealth === 0 ? { kind: 'destroyed' as const } : { kind: 'alive' as const };
+    return {
+      weapon: new MagicalWeapon(
+        newWeaponHealth,
+        this.#maxHealth,
+        newWeaponStatus,
+        this.#damage,
+        this.#owner,
+      ),
+       
+      target: newTarget,
+    };
+  }
+}

src/magical-objects.spec.ts

@@ -0,0 +1,360 @@
+import fc from 'fast-check';
+import { describe, it } from 'vitest';
+import { Character } from './Character.ts';
+import { Level } from './Level.ts';
+import { MagicalWeapon } from './MagicalWeapon.ts';
+import { HealingObject } from './HealingObject.ts';
+
+describe('Magical Objects', () => {
+  describe('WeaponDealsDamage', () => {
+    it('property: weapon deals its fixed damage amount', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 1, max: 10 }),
+          (damage, weaponHP, level) => {
+            const attacker = Character.create({ name: 'hero', level: Level.create(level) });
+            const target = Character.create({ name: 'goblin', level: Level.create(level) });
+            const weapon = MagicalWeapon.create({
+              damage,
+              maxHealth: weaponHP,
+              owner: attacker,
+            });
+            const result = attacker.useWeapon(weapon, target);
+            return result.target.health.value === Math.max(0, 1000 - damage);
+          },
+        ),
+      );
+    });
+
+    it('property: weapon health decreases by 1 after use', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 2, max: 500 }),
+          fc.integer({ min: 1, max: 500 }),
+          (weaponHP, damage) => {
+            const attacker = Character.create({ name: 'hero', level: Level.create(1) });
+            const target = Character.create({ name: 'goblin', level: Level.create(1) });
+            const weapon = MagicalWeapon.create({ damage, maxHealth: weaponHP, owner: attacker });
+            const result = attacker.useWeapon(weapon, target);
+            return result.weapon.health === weaponHP - 1;
+          },
+        ),
+      );
+    });
+
+    it('property: weapon is destroyed when health reaches 0', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 1, max: 500 }), (damage) => {
+          const attacker = Character.create({ name: 'hero', level: Level.create(1) });
+          const target = Character.create({ name: 'goblin', level: Level.create(1) });
+          const weapon = MagicalWeapon.create({ damage, maxHealth: 1, owner: attacker });
+          const result = attacker.useWeapon(weapon, target);
+          return result.weapon.status.kind === 'destroyed';
+        }),
+      );
+    });
+
+    it('property: weapon remains alive when health > 0 after use', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 2, max: 500 }),
+          fc.integer({ min: 1, max: 500 }),
+          (weaponHP, damage) => {
+            const attacker = Character.create({ name: 'hero', level: Level.create(1) });
+            const target = Character.create({ name: 'goblin', level: Level.create(1) });
+            const weapon = MagicalWeapon.create({ damage, maxHealth: weaponHP, owner: attacker });
+            const result = attacker.useWeapon(weapon, target);
+            return result.weapon.status.kind === 'alive';
+          },
+        ),
+      );
+    });
+  });
+
+  describe('DeadCannotUseWeapon', () => {
+    it('property: dead character cannot use weapon — state unchanged', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 1, max: 500 }),
+          (damage, weaponHP) => {
+            const attacker = Character.create({ name: 'hero', level: Level.create(1) });
+            const target = Character.create({ name: 'goblin', level: Level.create(1) });
+            const weapon = MagicalWeapon.create({ damage, maxHealth: weaponHP, owner: attacker });
+            // Kill the attacker using a separate killer
+            const killer = Character.create({ name: 'boss', level: Level.create(1) });
+            const deadAttacker = killer.dealDamage(attacker, 10000);
+            const weaponHPBefore = weapon.health;
+            const targetHealthBefore = target.health.value;
+            const result = deadAttacker.useWeapon(weapon, target);
+            return (
+              result.weapon.health === weaponHPBefore &&
+              result.target.health.value === targetHealthBefore
+            );
+          },
+        ),
+      );
+    });
+  });
+
+  describe('NonOwnerCannotUseWeapon', () => {
+    it('property: non-owner cannot use weapon — state unchanged', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 1, max: 500 }),
+          (damage, weaponHP) => {
+            const owner = Character.create({ name: 'owner', level: Level.create(1) });
+            const thief = Character.create({ name: 'thief', level: Level.create(1) });
+            const target = Character.create({ name: 'goblin', level: Level.create(1) });
+            const weapon = MagicalWeapon.create({ damage, maxHealth: weaponHP, owner });
+            const weaponHPBefore = weapon.health;
+            const targetHealthBefore = target.health.value;
+            const result = thief.useWeapon(weapon, target);
+            return (
+              result.weapon.health === weaponHPBefore &&
+              result.target.health.value === targetHealthBefore
+            );
+          },
+        ),
+      );
+    });
+  });
+
+  describe('DestroyedWeaponCannotDealDamage', () => {
+    it('property: destroyed weapon cannot deal damage — state unchanged', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 1, max: 500 }), (damage) => {
+          const owner = Character.create({ name: 'owner', level: Level.create(1) });
+          const target = Character.create({ name: 'goblin', level: Level.create(1) });
+          const weapon = MagicalWeapon.create({ damage, maxHealth: 1, owner });
+          // Destroy the weapon first
+          const firstUse = owner.useWeapon(weapon, target);
+          const destroyedWeapon = firstUse.weapon;
+          const targetHealthBefore = firstUse.target.health.value;
+          // Try to use again on the destroyed weapon
+          const result = owner.useWeapon(destroyedWeapon, firstUse.target);
+          return result.weapon.health === 0 && result.target.health.value === targetHealthBefore;
+        }),
+      );
+    });
+  });
+
+  describe('HealingObjectHealsCharacter', () => {
+    it('property: healing object gives health up to its remaining health', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 1, max: 500 }),
+          (objectHP, healAmount, characterHealth) => {
+            fc.pre(healAmount >= objectHP);
+            fc.pre(characterHealth + objectHP <= 1000);
+            const character = Character.createWithHealth({
+              name: 'hero',
+              level: Level.create(1),
+              health: characterHealth,
+            });
+            const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP });
+            const result = character.useHealingObject(object, healAmount);
+            return result.character.health.value === characterHealth + objectHP;
+          },
+        ),
+      );
+    });
+
+    it('property: healing object gives health up to character max when object has more', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 900, max: 999 }),
+          (objectHP, healAmount, characterHealth) => {
+            fc.pre(objectHP >= healAmount);
+            fc.pre(characterHealth + healAmount > 1000);
+            const character = Character.createWithHealth({
+              name: 'hero',
+              level: Level.create(1),
+              health: characterHealth,
+            });
+            const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP });
+            const result = character.useHealingObject(object, healAmount);
+            return result.character.health.value === 1000;
+          },
+        ),
+      );
+    });
+
+    it('property: healing object health decreases by actual healed amount', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 1, max: 999 }),
+          (objectHP, healAmount, characterHealth) => {
+            fc.pre(characterHealth + healAmount <= 1000);
+            fc.pre(healAmount <= objectHP);
+            const character = Character.createWithHealth({
+              name: 'hero',
+              level: Level.create(1),
+              health: characterHealth,
+            });
+            const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP });
+            const result = character.useHealingObject(object, healAmount);
+            return result.object.health === objectHP - healAmount;
+          },
+        ),
+      );
+    });
+
+    it('property: healing object is destroyed when health reaches 0', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 1, max: 500 }), (objectHP) => {
+          // Character needs enough headroom to accept all object health
+          const characterHealth = Math.max(1, 1000 - objectHP);
+          const character = Character.createWithHealth({
+            name: 'hero',
+            level: Level.create(1),
+            health: characterHealth,
+          });
+          const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP });
+          const result = character.useHealingObject(object, objectHP);
+          return result.object.status.kind === 'destroyed';
+        }),
+      );
+    });
+
+    it('property: healing object remains alive when health > 0 after use', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 2, max: 500 }),
+          fc.integer({ min: 1, max: 999 }),
+          (objectHP, characterHealth) => {
+            const character = Character.createWithHealth({
+              name: 'hero',
+              level: Level.create(1),
+              health: characterHealth,
+            });
+            const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP });
+            const result = character.useHealingObject(object, 1);
+            return result.object.status.kind === 'alive';
+          },
+        ),
+      );
+    });
+  });
+
+  describe('DeadCannotUseHealingObject', () => {
+    it('property: dead character cannot use healing object — state unchanged', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 1, max: 500 }), (objectHP) => {
+          const character = Character.create({ name: 'hero', level: Level.create(1) });
+          const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP });
+          // Kill the character using a separate killer
+          const killer = Character.create({ name: 'boss', level: Level.create(1) });
+          const deadCharacter = killer.dealDamage(character, 10000);
+          const objectHPBefore = object.health;
+          const characterHealthBefore = deadCharacter.health.value;
+          const result = deadCharacter.useHealingObject(object, 100);
+          return (
+            result.object.health === objectHPBefore &&
+            result.character.health.value === characterHealthBefore
+          );
+        }),
+      );
+    });
+  });
+
+  describe('DestroyedHealingObjectCannotHeal', () => {
+    it('property: destroyed healing object cannot heal — state unchanged', () => {
+      fc.assert(
+        fc.property(fc.integer({ min: 1, max: 500 }), (objectHP) => {
+          // Character needs headroom to drain the object
+          const characterHealth = Math.max(1, 1000 - objectHP);
+          const character = Character.createWithHealth({
+            name: 'hero',
+            level: Level.create(1),
+            health: characterHealth,
+          });
+          const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP });
+          // Drain the object to 0
+          const firstUse = character.useHealingObject(object, objectHP);
+          const destroyedObject = firstUse.object;
+          const healedCharacter = firstUse.character;
+          const characterHealthBefore = healedCharacter.health.value;
+          // Try to use again on the destroyed object
+          const result = healedCharacter.useHealingObject(destroyedObject, 100);
+          return (
+            result.object.health === 0 && result.character.health.value === characterHealthBefore
+          );
+        }),
+      );
+    });
+  });
+
+  describe('Invariants', () => {
+    it('property: weapon health never goes negative', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 1, max: 10000 }),
+          (weaponHP, damage) => {
+            const attacker = Character.create({ name: 'hero', level: Level.create(1) });
+            const target = Character.create({ name: 'goblin', level: Level.create(1) });
+            const weapon = MagicalWeapon.create({ damage, maxHealth: weaponHP, owner: attacker });
+            const result = attacker.useWeapon(weapon, target);
+            return result.weapon.health >= 0;
+          },
+        ),
+      );
+    });
+
+    it('property: healing object health never goes negative', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 1, max: 10000 }),
+          (objectHP, healAmount) => {
+            const character = Character.create({ name: 'hero', level: Level.create(1) });
+            const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP });
+            const result = character.useHealingObject(object, healAmount);
+            return result.object.health >= 0;
+          },
+        ),
+      );
+    });
+
+    it('property: weapon health never exceeds maxHealth', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 1, max: 500 }),
+          (weaponHP, damage) => {
+            const attacker = Character.create({ name: 'hero', level: Level.create(1) });
+            const target = Character.create({ name: 'goblin', level: Level.create(1) });
+            const weapon = MagicalWeapon.create({ damage, maxHealth: weaponHP, owner: attacker });
+            const result = attacker.useWeapon(weapon, target);
+            return result.weapon.health <= weaponHP;
+          },
+        ),
+      );
+    });
+
+    it('property: healing object health never exceeds maxHealth', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 1, max: 500 }),
+          fc.integer({ min: 1, max: 10000 }),
+          (objectHP, healAmount) => {
+            const character = Character.create({ name: 'hero', level: Level.create(1) });
+            const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP });
+            const result = character.useHealingObject(object, healAmount);
+            return result.object.health <= objectHP;
+          },
+        ),
+      );
+    });
+  });
+});