Compiler Traces

A compiler trace is the structure that the compiler outputs and the certifier operates on. It contains all the ASTs of the performed passes together with some information about that pass.

module VerifiedCompilation.Trace where

open import RawU using (Untyped)
open import Data.List using (List ; _∷_ ; [])
open import Utils using (_×_ ; Maybe ; _,_)
open Maybe

Pass tags

We enumerate the known passes:

data SimplifierTag : Set where
  floatDelayT : SimplifierTag
  forceDelayT : SimplifierTag
  forceCaseDelayT : SimplifierTag
  caseOfCaseT : SimplifierTag
  caseReduceT : SimplifierTag
  inlineT : SimplifierTag
  cseT : SimplifierTag
  applyToCaseT : SimplifierTag
  unknown : SimplifierTag -- a placeholder for passes that we don't yet know of, so the certifier doesn't break if a pass was added

{-# FOREIGN GHC import UntypedPlutusCore.Transform.Simplifier #-}
{-# COMPILE GHC SimplifierTag = data SimplifierStage (FloatDelay | ForceDelay | ForceCaseDelay | CaseOfCase | CaseReduce | Inline | CSE | ApplyToCase | Unknown) #-}

Hints

Some passes produce hints that help the certifier to perform a faster search.

data InlineHints : Set where
  var     : InlineHints
  expand  : InlineHints → InlineHints
  ƛ       : InlineHints → InlineHints
  ƛ↓      : InlineHints → InlineHints
  _·_     : InlineHints → InlineHints → InlineHints
  _·↓     : InlineHints → InlineHints
  force   : InlineHints → InlineHints
  delay   : InlineHints → InlineHints
  con     : InlineHints
  builtin : InlineHints
  error   : InlineHints
  constr  : List InlineHints → InlineHints
  case    : InlineHints → List InlineHints → InlineHints

data Hints : Set where
  inline : InlineHints → Hints
  none : Hints

{-# FOREIGN GHC import UntypedPlutusCore.Transform.Certify.Trace #-}
{-# FOREIGN GHC import qualified UntypedPlutusCore.Transform.Certify.Hints as Hints #-}
{-# COMPILE GHC InlineHints = data Hints.Inline (Hints.InlVar | Hints.InlExpand | Hints.InlLam | Hints.InlLamDrop | Hints.InlApply | Hints.InlDrop | Hints.InlForce | Hints.InlDelay | Hints.InlCon | Hints.InlBuiltin | Hints.InlError | Hints.InlConstr | Hints.InlCase) #-}
{-# COMPILE GHC Hints = data Hints.Hints (Hints.Inline | Hints.NoHints) #-}

Compiler traces

A Trace A is a sequence of optimisation transformations applied to terms of type A. Each transition is labeled with a SimplifierTag that contains information about which pass was performed.

data Trace (A : Set) : Set where
  -- One step in the pipeline, with its pass and input term
  step : SimplifierTag → Hints → A → Trace A → Trace A
  -- Final AST in the trace
  done : A → Trace A

-- Get the first term in the trace
head : ∀{A} → Trace A → A
head (done x) = x
head (step _ _ x _) = x

Dump is the structure that is currently dumped on the Haskell side. We can convert it in a Trace using toTrace

-- The current trace structure dumped from Haskell
Dump : Set
Dump = List (SimplifierTag × Hints × Untyped × Untyped)

--
-- Since there is duplication in the dump, i.e. it is of the form
--
--     [(_ , x , y) ; (_ , y , z) ; (_ , z , w) ...]
--
-- This conversion entirely ignores the duplicated terms.
-- FIXME: just dump the Trace structure directly from
-- Haskell, this function won't be necessary
toTrace : Dump → Maybe (Trace Untyped)
toTrace [] = nothing
toTrace (x ∷ xs) = just (go x xs)
  where
    go : SimplifierTag × Hints × Untyped × Untyped → Dump → Trace Untyped
    go (pass , hints , x , y) [] = step pass hints x (done y)
    go (pass , hints , x , y) ((pass' , hints' , _ , z) ∷ xs) = step pass hints x (go (pass' , hints' , y , z) xs)