An example of my thinking on proving timing equivalence using dependent types.

timing.idr

-- Program analysis and types are just views of the same problem. I encode my possible analysis here in the types and rely on the
-- type checker to ensure the correctness of my implementation instead of leaving it to pen and paper proof.
-- In this case we encode a langauge that is ideally correct by construction and then prove that translation of such a language
-- into ISA's is possible each indexed by the same time (which must be statically known, i.e reflected into the type). 
-- If we can prove equvalence between our higher level language to the ISA's and equivalence to the ISA then we have the desired
-- analysis, it only requires that you encode the cost model in the constructors of the ISAs

-- We simply use Nat's for the time being.
Time : Type
Time = Nat

Name : Type
Name = String

data Value : Type -> Type where
  MkValue : {a : Type} -> {x : a} -> Value a

-- A Term in our language is indexed by a time step it takes.
data Term : Time -> Type where
  Assign : Name -> Value t -> Term 1 -- Let's say we assume there is a cost model of our high level language.
  -- While : Value Bool -> Term t -> Term -- This isn't right
  -- Loops are more complicated we need to be able to statically compute the number of times a loop body can execute.
  -- I believe we can do this easily by restricting our guard conditions and reflecting the values into the types.
  --
  -- Conditional require some thought as you need to compute a upper bound on the time either takes to execute and pad
  -- it.

-- Each ISA is also parametrized by time (I use dummy implementations here).
data ISA1 : Time -> Type where
  MkOne : {t : Time} -> ISA1 t

data ISA2 : Time -> Type where
  MkTwo : {t : Time} -> ISA2 t

-- We assume an implementation of compileOne, and compileTwo.
-- We also need a proof of equivalence between the two ISA's

-- Isomorphism is a bijective function that shows we can go either way given one of the types.
data Iso : Type -> Type -> Type where
  mkIso : {a : Type} -> {b : Type} -> (a -> b) -> (b -> a) -> Iso a b
  
isoProof : {t : Time} -> (ISA1 t -> ISA2 t) -> Iso (ISA1 t) (ISA2 t)
isoProof = ?an_exercise_for_the_reader

-- Our compiler is just a function that interprets our term language as each ISA and is able to show time equivalence between
-- the two.
theISO : Iso (ISA1 t) (ISA2 t)
theISO = ?foryou

-- We also assume implementations for both individual compilation functions.
compile : {t : Time} -> Iso (ISA1 t, ISA2 t) -> t -> (ISA1 t, ISA2 t)
compile t = (compileOne t, compileTwo t)