search

FStarLang / steel

The Steel separation logic library for F*
Apache License 2.0
31 stars 5 forks source link

Losing precision when encoding function literal #19

Closed nikswamy closed 1 year ago

nikswamy commented 1 year ago

Pulse functions needlessly get encoded to the SMT solver producing warnings like so:

(Warning 249) Losing precision when encoding a function literal: fun _ ->
  Steel.ST.Array.pts_to a
    Steel.FractionalPermission.full_perm
    (FStar.Seq.Base.upd (FStar.Ghost.reveal s) (FStar.SizeT.v i) v)
(Unnannotated abstraction in the compiler ?)
ArrayTests.fst(250,13-251,29): (Warning 249) Losing precision when encoding a function literal: fun _ ->
  Steel.ST.Util.exists_ (fun s' ->
        Steel.Effect.Common.star (Steel.ST.Array.pts_to a Steel.FractionalPermission.full_perm s')
          (Steel.ST.Util.pure (ArrayTests.sorted (FStar.Ghost.reveal s) s')))
(Unnannotated abstraction in the compiler ?) (see also ArrayTests.fst(246,18-251,29))

The pulse plugin generates an attribute to instruct F to not encode this to the SMT solver, but F does not respect that attribute.

This F PR tries to fix it, https://github.com/FStarLang/FStar/pull/2940 ... but that leads to other F regressions

nikswamy commented 1 year ago

Fixed in F*