Failure("Impossible: missing universe instantiation on unroll")

[msprotz]

Steps to reproduce:

jonathan@absinthe:/tmp $ fstar.exe --codegen OCaml --extract Unroll Unroll.fst --include ~/Code/kremlin/kremlib && cat Unroll.ml
proof-state: State dump @ depth 0 (at the time of failure):
Location: Unroll.fst(19,4-21,64)
Goal 1/1:
 |- _ : Prims.squash ((fun b ->
        C.Loops.for (FStar.UInt32.__uint_to_t 0)
          (FStar.UInt32.__uint_to_t 16)
          (fun h _ -> LowStar.Monotonic.Buffer.live h b)
          (fun i ->
              let _ =
                let _ = LowStar.Monotonic.Buffer.index b i in
                FStar.UInt8.add_mod _ (FStar.UInt8.__uint_to_t 1)
              in
              LowStar.Monotonic.Buffer.upd b i _)
        <:
        FStar.HyperStack.ST.Stack Prims.unit
          (fun h0 -> LowStar.Monotonic.Buffer.live h0 b)
          (fun _ _ _ -> Prims.l_True)) ==
    (*?u0*)
    _)

the testcase:

module Unroll

module B = LowStar.Buffer
module T = FStar.Tactics

open FStar.Tactics
open FStar.HyperStack.ST

let unroll t () : Tac unit =
  T.norm [primops; zeta_full; delta(*_only [t]*); iota];
  T.trefl()

[@@(postprocess_for_extraction_with (unroll (`%C.Loops.for)))]
let test (b: B.buffer UInt8.t { B.length b == 16 }): Stack unit
  (requires (fun h0 -> B.live h0 b))
  (ensures (fun _ _ _ -> True))
=
  (* norm [ primops; iota; zeta_full; delta_only [ `%C.Loops.for ] ] ( *)
    C.Loops.for 0ul 16ul
  (* ) *) (fun h _ -> B.live h b)
    (fun i -> B.upd b i (B.index b i `FStar.UInt8.add_mod` 1uy))

thanks!

Jonathan

[mtzguido]

This works by annotating (t:string) in unroll, which gets rids of the (implicit) universe polymorphism. Definitely a bug though.

[mtzguido]

(Sorry Zoe.. missed a few keystrokes from my terminal into here and somehow assigned you.)

Argh so this is an oversight on my part, these attributes are not typechecked and hence not elaborated, so the tactics crash. I've made them check at typechecking time, and the postprocess_for_extraction_with variant can then just run the tactic as-is at extraction. However, this requires to call deep_compress on the tactic term before passing it along or it will explode when it reaches a uvar node. That almost works, except that we would also need default unconstrained variables to zero, just as we do for top-levels, which begs the question of whether attributes should just always be elaborated... any opinion @nikswamy @aseemr ?

In any case, pushing the current status into master which should cover most uses. See the file below, the last example crashes but I wouldn't expect it to be common.

let unroll t1 t2 () : Tac unit =
  T.trefl()

[@@ expect_failure [12];
    postprocess_with (unroll (`%int))]
let test0 () : int = 42

[@@ expect_failure [12];
    postprocess_for_extraction_with (unroll (`%int))]
let test1 () : int = 42

[@@ postprocess_with (unroll () (`%int))]
let test2 () : int = 42

[@@ postprocess_for_extraction_with (unroll () (`%int))]
let test3 () : int = 42

[@@ postprocess_for_extraction_with (unroll (raise_val ()) (`%int))]
let test4 () : int = 42