LOAF — Logic Objects As Facts

LOAF is a language of declarative manifests. A manifest is made of blocks, facts and rules, and a set of LOAF files denotes a logic program whose meaning is its model. Rules are written in the notation of ASP (answer set programming).

loaf 0.1.

block team {
  lead person.
  size? int.
}

block person {
  team* team.
  email? text.
}

team infra { lead alice. }

person alice {
  team infra.
  email "alice@example.org".
}

% The lead of a team is a member of it.
error(lead_not_member, T) :- T.lead(P), not P.team(T).

The language guarantees:

• a single semantics: validation, deductions and constraints are rules over the same facts;
• termination: the evaluation of an accepted manifest always terminates;
• a declared vocabulary: every predicate and every enumerated value is declared, anything else is refused;
• a canonical form: a line-by-line JSON export, described by a schema;
• checked versions: language version at the head of each file, versioned modules, and a tool-checked version bump required by each change.

The loaf tool

loaf is the reference implementation of the language, in OCaml. It reads the files, applies the checks of the specification, computes the model and exports it in the interchange format.

loaf check records.loaf rules.loaf      # reports refusals and errors
loaf export records.loaf rules.loaf     # the model, one JSON line per atom
loaf export --document records.loaf     # the blocks, as one JSON document
loaf export --asp records.loaf rules.loaf > p.lp   # the program, for an ASP solver
loaf diff rbac-1.2.0.loaf rbac-1.3.0.loaf   # required version bump (L010)
loaf fmt -i records.loaf                # rewrites into the canonical form
loaf lock records.loaf rules.loaf       # writes the module checksums (loaf.sum)

A directory given on the command line stands for the .loaf files it contains, at any depth. Modules loaded by use are searched for in the directories given by -L or by the LOAF_PATH variable. When a loaf.sum file is present, check and export verify that each loaded module matches its checksum.

The model is computed without an external solver: a LOAF program is stratified and choice-free, and its unique model is computed stratum by stratum.

Repository contents

Directory	Contents
spec/	The specification (loaf.typ, Typst), which is authoritative.
schema/	The JSON schema of the canonical export.
src/	The loaf library: lexer (ocamllex), grammar (Menhir), elaboration, checks, evaluation, export.
bin/	The loaf command.
models/	LOAF modules of classic security models (RBAC, Bell-LaPadula, Biba…).
examples/	The examples of the specification and their reference export.
test/	The cram tests: cases, refusals before evaluation, versions, examples.

Build and test

opam install . --deps-only --with-test
dune build                  # the loaf command
dune runtest                # the tests
make check                  # checks the specification (fails on any warning)
make                        # builds spec/loaf.pdf

The PDF is not versioned. The specification of main is published as a PDF at https://forge.ocamlpro.com/api/packages/OSS/generic/loaf-spec/latest/loaf.pdf, and each release carries the PDF of its version.

Licenses

The repository follows the REUSE specification:

• the specification, the schema and the documentation are under CC-BY-4.0;
• the code is under Apache-2.0;
• the funders' logos (spec/assets/) remain trademarks of their owners.

See REUSE.toml for per-file details, and CONTRIBUTING.md to contribute.

Funding

« Ce projet a été financé par le Gouvernement dans le cadre du plan France 2030 opéré par Cap Digital et financé par l'Union européenne – NextGeneration EU. »

This project was funded by the French Government as part of the France 2030 plan, operated by Cap Digital and funded by the European Union – NextGenerationEU. The notice above is the wording that the grant agreement requires.