Skip to content

Readme.md

Latest commit

 

History

History
154 lines (127 loc) · 5.14 KB

Readme.md

File metadata and controls

154 lines (127 loc) · 5.14 KB

FROG logo

Reference Lowering-to-LLVM Rule Families

Bounded lowered-unit-kind LLVM proof emitters used by the non-normative reference workspace
FROG — Free Open Graphical Language

Purpose

This directory documents the bounded lowering-to-LLVM rule families currently recognized by the reference LLVM-oriented path. The purpose is to keep the lowering -> LLVM corridor explicit while preserving the architectural rule that LLVM consumes lowering artifacts, not FIR or canonical source directly.

These documents are non-normative reference-implementation material. They do not replace IR/Lowering.md, IR/Backend contract.md, or any future production compiler backend specification.

Current Emission Posture

lowering artifact
  -> artifact_kind == frog_lowered_unit
  -> exactly one lowered unit
  -> lowered_units[0].kind
  -> bounded LLVM emitter
  -> module.ll
  -> optional native build proof
  -> expected-output.json

The reference LLVM emitter dispatches by lowered_units[0].kind. The source example identifier remains preserved in source_ref, but it is not the LLVM-emitter authority.

Current LLVM Emitter Families

Emitter family Lowered unit kind Published example Native proof posture Current limitation
Pure floating-point addition pure_addition_kernel 01_pure_addition Emits a native proof function that computes f64 a + b and prints result/status. Only the published two-input addition shape is supported.
Widget-value arithmetic proof ui_value_roundtrip_kernel 02_ui_value_roundtrip Emits a native proof that treats widget values as proof inputs and prints the indicator value/status. No native UI host is emitted; widget participation is represented as proof payload.
UI property-effect proof ui_property_write_effect_unit 03_ui_property_write Emits a native proof that prints the affected widget, member, value, and status. No native UI mutation host is emitted; the effect is represented as proof payload.
Explicit delay step proof stateful_feedback_delay_kernel 04_stateful_feedback_delay Emits a native proof for one explicit delay-backed state step. Only the published delay_1 shape is supported.
Bounded accumulator proof bounded_accumulator_kernel_with_ui_bindings 05_bounded_ui_accumulator Emits a native bounded accumulator proof with u16 overflow rejection. UI binding is proof payload; no native front-panel renderer is emitted.

Shared LLVM Emission Invariants

  • The input artifact must declare artifact_kind = frog_lowered_unit.
  • The input artifact must contain exactly one lowered unit.
  • The lowered unit must expose a string kind.
  • The lowered unit kind must match a registered LLVM emitter.
  • The emitted module is a proof artifact, not a production backend artifact.
  • The emitted module must be reproducible against the published module.ll for the corresponding example.
  • The optional native build must be checked against expected-output.json when the build toolchain is available.

Boundary

The LLVM-oriented path is downstream from lowering. It must not consume canonical source or FIR directly, must not redefine FROG semantics, and must not claim general production compiler coverage. 

.frog
  -> FIR
  -> lowering
  -> LLVM proof

Out of Scope

  • general LLVM backend completeness,
  • general graph scheduling,
  • native UI host generation,
  • widget realization rendering,
  • arbitrary type lowering,
  • production ABI definition,
  • optimization passes,
  • multi-unit linking.

Next Stabilization Direction

The next safe improvement is to keep the current emitters but progressively separate reusable proof-emission helpers from example-shaped emitter functions: 

lowered_unit.kind
  -> shared lowered-kernel validation
  -> shared LLVM text construction helpers
  -> family-specific proof module emission