Check a property on a finite domain

Intention

I want to check that every element of the presented domain gets the expected conclusion.

The check runs over a finite domain; act goals use the same property form.

Correct formFrozen execution sceneBoundary

Incorrect form and why it stays silent

A premise does not replace an expectation about the conclusion.

Incorrect form

property AllRegistered {
    forall p in collect x: Person where eligible(x);
    expect eligible(p);
}

This checks the selection condition and stays silent on whether registered was obtained. Another incorrect form is forall p in GeneratedPeople;: an arbitrary generator is not declared here and does not replace a finite collect; that is exactly the mutation pinned by teaches.

Correct form

The property reads the registered head. The collect domain is finite; there is no random generator and no seed here.

Arxo Law

language "law.core" version "0.2";
package recipes.n.r12 version "0.1.0";
namespace "urn:recipe:n-package:12";

entity Person;
relation eligible(p: Person);
relation complete(p: Person);
relation registered(p: Person);
rule Register strict {
    for p: Person;
    when eligible(p) and complete(p);
    then registered(p);
}

Frozen execution scene

Facts	Question	Answer
eligible(p), complete(p)	AllRegistered	PASS, domain 1
eligible(p), no complete(p)	MissingRegistered	FAIL, counterexample p
Same incomplete input	Incorrect VacuousRegistration with expect eligible(p)	PASS

full input sustains property

Arxo Law

test "full input sustains property" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert eligible(entity_ref("urn:recipe:n-package:12:p"));
        assert complete(entity_ref("urn:recipe:n-package:12:p"));
    }
    evaluate truth(registered(entity_ref("urn:recipe:n-package:12:p")));
    expect truth_status == TRUE_ONLY;
}

property AllRegistered {
    forall p in collect x: Person where eligible(x);
    expect registered(p);
}

missing output counts as counterexample

Arxo Law

test "missing output counts as counterexample" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert eligible(entity_ref("urn:recipe:n-package:12:p"));
    }
    evaluate truth(registered(entity_ref("urn:recipe:n-package:12:p")));
    expect truth_status == NEITHER;
}

property MissingRegistered {
    forall p in collect x: Person where eligible(x);
    expect registered(p);
}

broken property checks only premise

Arxo Law

test "broken property checks only premise" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert eligible(entity_ref("urn:recipe:n-package:12:p"));
    }
    evaluate truth(registered(entity_ref("urn:recipe:n-package:12:p")));
    expect truth_status == NEITHER;
}

property VacuousRegistration {
    forall p in collect x: Person where eligible(x);
    expect eligible(p);
}

Counterfactual

The second scene leaves an element in the domain without a registered conclusion: the correct property yields FAIL. teaches replaces the finite collect with an undefined generator and requires a lowering rejection, not a fictitious empty run.

Boundary

An act goal additionally carries a basis on a source fragment; across legal orders it is goals, not rules, that are checked. A seed is needed only by a generator, which this finite domain does not use. A property cannot be declared proven on an empty domain.

Pitfall

A property once wrongly reported success on a resident without an age, because negation did not see the unknown. The fix is a separate not_known branch; the second scene checks exactly the absence of a conclusion.