Dhall expressions for building Sigil OS configurations.

These expressions are for generating configuration from the top-down, which is the inverse of how configuration is parsed at runtime, from the bottom up. At runtime it must not be possible for higher systems to affect lower systems without explicit pathways. During composition-time however, the maintainer should be aided by tools to infer as much configuration as possible.

These expressions serve multiple purposes, they formalize the concepts of Sigil configuration, they infer strict configurations from simple declarations, and they protect maintainers from the perils of manual XML manipulation.

#Conceptual description

#ROM

The lowest and coarsest level of configuration is the map of ROM (read only memory) modules burned into the bootable images. At this level configuration is a key-value collection of raw data. The type is at BootModules and is transformed into linker directives that are used to link the core binary. This map is the only configuration of core and is static at runtime.

#Init

The Genode init component is the child component of core. The init component can host an any number of children, which may be additional instances of init nested at arbitrary height. The type is Init and is present in the Boot type as the root of system configuration, which is transformed to the "config" ROM at core. This is where the XML begins. When init is nested it must become Init/Child, the Init type contains a map of named Init/Child instances.

#Init/Child

A child of Init has the type Init/Child. The implementation of the type is awkward because Dhall does not support recursive types, but the functions provided should be intuitive. A tree of Init/Child can be traversed but an Init/Child cannot be transformed back to its origin type.

#Init/Config

Init configuration is parsed as XML at runtime, and the configuration ROM passed to children is implicitly enclosed in config XML tags when the child configuration is inlined. The Init/Config type models the configuration ROM passed to init or a child of init.

#Init/Resources

Init/Resources models resources that are managed by init and accounted by core. A parents resources is the sum of the resources of its children.

#Init/LabelSelector

The LabelSelector type is used to model the label matching employed by init when routing service session requests.