Skip to main content

Module address

kernel

Module address 

Source
Expand description

Address: canonical relative path inside a city, and the WriteDomain primitive is_within. The part crates/kernel/spec/Address.lean specifies this module.

Invariants owned here:

  • one constructor: Address::parse; whatever it accepts is already canonical (no normalization happens, non-canonical spellings are rejected), so as_str is a byte-exact round trip.
  • identity is byte-wise on every platform: Eq, Ord and is_within never fold case; is_reserved alone does, and it only refuses more.
  • symlink resolution is an effect-layer concern; this type only judges already-canonical relative paths.
  • is_reserved answers C17: a protected-metadata subtree (PROTECTED_METADATA) can never enter a WriteDomain, at whatever depth it sits, and every WriteDomain constructor must ask first.
  • may_read answers the read bound: what a resident of one building may read by a path it chose (crates/city/Spec.lean §8-2).

Structs§

Address
Canonical relative path; invariants enforced at the sole constructor.
SessionName
What a person calls one session: one address segment, and therefore one directory under a building.

Enums§

ReadVerdict
What the read bound answers about one address.

Constants§

GIT_METADATA
git’s own metadata directory (crates/kernel/spec/Address.lean §8-73). Writing it is privilege escalation: a hook is code that runs at the next git operation, a config key can start a program, and the checkpoint references and the restoration objects a file_discarded names all live in there.
PROTECTED_METADATA
Every directory name that is protected metadata, and therefore reserved at whatever depth it sits: what governs a scope, and what keeps a repository itself. The one list - Address::is_reserved judges it, and no caller re-spells these names.
RESERVED_PREFIX
The directory name whose subtree never enters any WriteDomain (C17).

Functions§

may_read
The read bound: whether a resident of reader_building may read target. Its own building is open whole; any other is open unless its rules say it is confidential or cannot be read.