Skip to content

Compiler optimizer v0 — semantics-preserving transformations with witnesses #70

Description

@juv4uk

Goal

Add the first optimization pass only after compiled execution has a parity witness.

An optimization is admitted only as a transformation with an explicit applicability condition and executable evidence that observable semantics are preserved. The backend must not silently 'know better' than Lisp.

Required work

  • Choose one narrow optimization whose safety conditions can be stated precisely.
  • Represent the transformation and its witness/provenance in inspectable data.
  • Preserve exact integers/rationals exactly; never introduce float approximation.
  • Preserve observable evaluation/error behavior under the stated preconditions.
  • Keep the transformation rule at the Lisp/semantic layer where practical; Rust may perform mechanical execution of an already-admitted transform but not define its meaning.

Acceptance evidence

For a corpus containing both eligible and deliberately ineligible cases:

  • optimized compiled result == unoptimized compiled result == meta/native oracle;
  • ineligible cases are left unchanged or rejected, never guessed;
  • the test can identify which transformation fired and why.

Dependencies

Non-goals

  • No optimizer grab-bag.
  • No optimization accepted on benchmark speed alone.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions