Standpoint visibility: the DEFAULT layer vs scoped facts

Area: Standpoints & federation Teaches: how a fact’s scope decides which views can see it. A DEFAULT-layer (unscoped, module-level) fact restricts into every view; a standpoint-scoped fact is local to its standpoint. This is the sheaf reading of visibility — a global section restricts to every open set; a local section does not. Prerequisites: concepts, and pub query (see first-class relations). Run: ox build examples/standpoint_visibility && ox query examples/standpoint_visibility --with-truth4

A standpoint is a named viewpoint — a place from which facts are asserted and read. Standpoints sit in a <: lattice, and the unscoped DEFAULT layer is the shared base every standpoint extends. The question this example answers: when you assert a fact, who can see it? The answer turns entirely on whether the fact is scoped.

What to read in visibility.ar

Two standpoints and one concept:

pub type Widget;

pub standpoint s1;
pub standpoint s2;

A DEFAULT-layer fact is unscoped — declared at module level, outside any standpoint block. It restricts into every view:

// DEFAULT-layer (unscoped) fact — visible in every view.
pub fact Widget(dfl);

A scoped fact lives inside a standpoint block and is local to it:

pub standpoint s1 {
    pub fact Widget(only_s1);
}

pub standpoint s2 {
    pub fact Widget(only_s2);
}

Four queries read from four vantage points. The base query is unfederated (DEFAULT only); across [...] selects which standpoints join the view:

pub query base() -> Widget;                       // DEFAULT only
pub query in_s1() -> Widget across [s1];           // DEFAULT ∪ s1
pub query in_s2() -> Widget across [s2];           // DEFAULT ∪ s2
pub query fed() -> Widget across [s1, s2];         // DEFAULT ∪ s1 ∪ s2

Running it

The four views form a visibility matrix — dfl is the DEFAULT-layer individual, only_s1/only_s2 are scoped:

base   (unfederated):   { dfl }                    — DEFAULT only
in_s1  (across [s1]):    { dfl, only_s1 }           — DEFAULT ∪ s1
in_s2  (across [s2]):    { dfl, only_s2 }           — DEFAULT ∪ s2
fed    (across [s1, s2]): { dfl, only_s1, only_s2 } — DEFAULT ∪ s1 ∪ s2

The decisive cell is only_s1 against base and in_s2: it is invisible to both. A standpoint-scoped fact does not leak into the unfederated base view, and it does not leak into a different standpoint’s view. Seeing it requires explicitly selecting s1 (or federating over a list that includes it). Meanwhile dfl appears in all four rows — the DEFAULT layer is the floor every view stands on.

Every row reads [Is] here: there is no disagreement in this example, so the four-valued status is uniform. (For where [Both] arises, see federation: standpoints disagree and federation: the DEFAULT layer joins as a constituent.)

Honest caveats (what runs today)

• The query output identifies rows by individual id; the named mapping above (dfl, only_s1, only_s2) is how the package declares them.
• --with-truth4 surfaces the per-row four-valued tag. Unfederated queries always read Is; the federated views here also read Is because nothing refutes a Widget.

This example is compiled and run in CI; the four-quadrant visibility matrix is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so a leak across standpoints breaks the build rather than the docs.

Source

The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.

root.ar

//! Standpoint visibility composition (rsn-05).

mod visibility;

visibility.ar

//! Standpoint visibility composition (audit rsn-05).
//!
//! Demonstrates the sheaf reading of standpoint visibility (§10.4):
//!
//!   * A DEFAULT-layer (unscoped, file/module-level) `pub fact`
//!     restricts into EVERY view — the base/unfederated query AND
//!     every standpoint's federated view (a global section restricts
//!     to every open set).
//!   * A standpoint-scoped `pub fact` is LOCAL to its standpoint: it
//!     is invisible to the base/unfederated query and to a query
//!     scoped to a DIFFERENT standpoint. Cross-standpoint reads
//!     require explicit federation (`across [...]`), `box`/`diamond`,
//!     or selecting that standpoint.
//!
//! Expected runtime behavior (four-quadrant matrix):
//!
//!   base()   (unfederated):       { dfl }                    — DEFAULT only
//!   in_s1()  (across [s1]):       { dfl, only_s1 }           — DEFAULT ∪ s1
//!   in_s2()  (across [s2]):       { dfl, only_s2 }           — DEFAULT ∪ s2
//!   fed()    (across [s1, s2]):   { dfl, only_s1, only_s2 }  — DEFAULT ∪ s1 ∪ s2
//!
//! In particular `only_s1` is invisible to `base()` and to `in_s2()`;
//! `dfl` is visible everywhere.
//!
//! Soundness: `Argon.Visibility.view_of_base_eq_default_layer`
//! (base = DEFAULT layer), `Argon.Visibility.scoped_view_eq_default_union_own`
//! (scoped = DEFAULT ∪ own standpoint), `default_visible_everywhere`,
//! `scoped_invisible_to_base`, `scoped_invisible_to_other`.

// ANCHOR: visibility
pub type Widget;

pub standpoint s1;
pub standpoint s2;

// DEFAULT-layer (unscoped) fact — visible in every view.
pub fact Widget(dfl);

pub standpoint s1 {
    pub fact Widget(only_s1);
}

pub standpoint s2 {
    pub fact Widget(only_s2);
}

// Unfederated / base view: sees the DEFAULT layer only.
pub query base() -> Widget;
// Scoped views: DEFAULT layer ∪ own standpoint.
pub query in_s1() -> Widget across [s1];
pub query in_s2() -> Widget across [s2];
// Federated across both: DEFAULT layer ∪ s1 ∪ s2.
pub query fed() -> Widget across [s1, s2];
// ANCHOR_END: visibility