Fully normalising recursive functions applied to literals

[amosr]

This is a rough transcription of a discussion on Slack with @nikswamy

I have a recursive datatype exp, which represents an expression in a small language, and a recursive function translate : exp -> system which describes the semantics of the expression as a transition system. When I try to prove something about a specific expression, I expect the translation to a transition system to fully normalise away, leaving just the resulting transition system. However, when I apply FStar.Tactics.compute and inspect the proof state, there are some remaining calls to translate applied to literal expressions inside pattern matches.

How do I fully evaluate my translate function, even inside matches?

[amosr]

Here is a full example, which may be a little long, but it shows the issue concretely. Nik's solution is to apply normalisation-by-evaluation with FStar.Tactics.norm [primops; iota; delta; zeta; nbe], which fully reduces all instances of the translate function.

module MinSystem
module T = FStar.Tactics

(* Say we have a small streaming language *)
type value = nat

type exp =
  // Read the input value
  | XRead: exp
  // Add two expressions together
  | XAdd2: exp -> exp -> exp
  // Delay a stream, initialising it with `value`
  | XDelay: value -> exp -> exp

(* I have a recursive type that describes the state needed to execute such an expression... *)
let rec state_of_exp (e: exp): Type =
  match e with
  // Reads require no internal state
  | XRead -> unit
  // Addition requires the state of both subexpressions
  | XAdd2 e1 e2 -> state_of_exp e1 * state_of_exp e2
  // Delay needs to store the delayed value and the subexpression's state
  | XDelay v e1 -> value * state_of_exp e1

(* Define the type of labelled transition systems: a function that takes an input value and a state (None for initial) and returns the updated state and output result. *)
let system (state: Type) =
  (input: value) -> (s: option state) -> (state * value)

(* We can translate expressions to transition systems *)
let rec translate (e: exp): system (state_of_exp e) =
  match e with
  // Read returns the input value as-is
  | XRead -> (fun i s -> ((), i))
  // Add translates both subexpressions and adds them
  | XAdd2 e1 e2 ->
    let t1 = translate e1 in
    let t2 = translate e2 in
    (fun i s ->
        let ss: option (state_of_exp e1 * state_of_exp e2) = s in
        let (s1, s2) = match ss with
          | None -> (None, None)
          | Some (s1, s2) -> (Some s1, Some s2)
        in
        let (s1', v1) = t1 i s1 in
        let (s2', v2) = t2 i s2 in
        ((s1', s2'), v1 + v2)
    )
  // Delay translates the subexpression and delays the value
  | XDelay v e1 ->
    let t1 = translate e1 in
    (fun i s ->
        let ss: option (value * state_of_exp e1) = s in
        match ss with
        | None ->
          let (s', v') = t1 i None in
          (((v',s') <: state_of_exp e), v)
        | Some (vx, sx) ->
          let (s', v') = t1 i (Some sx) in
          ((v', s'), vx)
    )


(* A concrete example program *)
let example = XAdd2 XRead (XDelay 0 XRead)

(* Example of non-normalisation *)
let translate_with_compute (): unit =
  // Prove that the result is always larger than the input.
  // The proof goes through, but the dumped proof state still includes
  // calls such as `translate XRead` that could be normalised.
  assert
    (forall (i: nat) (s: state_of_exp example). snd (translate example i (Some s)) >= i) by
    (T.compute (); T.dump "translate_compute");
  ()

(* Example of full normalisation suggested by Nik *)
let translate_with_nbe (): unit =
  // The normalisation-by-evaluation strategy reduces all of the calls to
  // translate:
  assert
    (forall (i: nat) (s: state_of_exp example). snd (translate example i (Some s)) >= i) by
    (T.norm [primops; iota; delta; zeta; nbe]; T.dump "translate_nbe");
  ()