Scope

ff-spartan6-unsafe is the host-execution companion layer for generated JSON terms in the Spartan6 namespace. Its three checked modules comprise an aggregate checking entry point, a narrow JSON-generation wrapper, and an executable generation example. The wrapper publicly exposes constructors for JSON scalar, array, and object syntax together with the macro that turns an external JSON node into an Agda term. The example applies that macro to an array containing a Boolean, a number, a string, and null. Library checking enables cubical features, guardedness, and host execution while relying on ff-json-unsafe as its sole in-scope dependency.

Most important results

The public wrapper keeps the generated helper names in scope while leaving the host-execution primitives and script-path binding hidden. The example establishes that a JSON literal can be generated as a value of the native JsonValue type during checking. A reflexivity proof confirms that the generated value reduces definitionally to the corresponding explicit array of JSON constructors. The Everything module brings both the wrapper and its reduction example under one library-level check.