Stream: MetaCoq

Topic: Fueling the checker

Jason Gross (Nov 04 2022 at 13:14):

I'm interested in getting typing derivations that don't rely on the SN axiom (ideally that don't rely on axioms at all). Would it be reasonable to factor the checker into first a fueled version that returns a sum of either a typing derivation, or a function from Acc to typing derivations, with the idea being that it first uses fuel, and then used Acc when it runs out; and then a version that just plugs the axiom into this to merge the results?

Kenji Maillard (Nov 04 2022 at 13:17):

I thought that the acc-intro hack (pile n acc-intro on top of the axiom) was basically providing a fueled version (in the sense that if you obtain a complete derivation then the axiom won't be present). Am I missing something ?

Jason Gross (Nov 04 2022 at 14:56):

You need to reduce the derivation enough to make the axiom go away. If the derivation cannot be fully reduced in vm_compute (because, e.g., there are Qed-opaque intermediates, or functions present in the fully reduced term, or the fully reduced term is too big because inductives are quadratically-sized in their indices/parameters), then you have to very carefully reduce the right parts enough to see that the axiom goes away, but not so much that you blow up reduction

Jason Gross (Nov 04 2022 at 14:58):

It also means you can't use the hack where you get a thing of type T by having f args : option T, proving that g : (if f args then true else false) = true -> T and then getting a thing of type T by doing g (eq_refl true <: _), because g is still going to mention the axiom even if it's eventually computed away.

Jason Gross (Nov 04 2022 at 14:58):

(This doesn't matter for type inference, but it does matter for accessing the typing derivation, which does not seem to actually be vm_computable)

Théo Winterhalter (Nov 04 2022 at 15:10):

Why use vm_compute? I would use lazy precisely not to unfold stuff I don't need to.

Jason Gross (Nov 04 2022 at 16:05):

Because then I need to whitelist or blacklist the identifiers to be (not) unfolded, and this sort of stuff is in general near-impossible to debug when you're missing any identifier, because the intermediate terms are huge.

Meven Lennon-Bertrand (Nov 07 2022 at 14:26):

Can you do something like this and not implement the function twice? If so, I would say this is an improvement onto the acc-intro hack, by replacing the hidden, hardcoded fuel into a more transparent one

Jason Gross (Nov 07 2022 at 20:21):

Yes, it should be possible

Jason Gross (Nov 07 2022 at 21:09):

I'm not super-familiar with the infrastructure, and would appreciate some help figuring out where to start (somewhere around reduce_stack_full?) and how to interface with Equations, but the basic idea is like this:

Require Import Coq.Program.Program.
Require Import Coq.micromega.Lia.
Require Import Coq.Init.Wf.
Local Set Implicit Arguments.
Variant PartiallyFueled (R : Prop) A := finished (_ : A) | needs_acc (_ : R -> A).
Arguments finished {_ _} _.
Definition ret {R A} : A -> PartiallyFueled R A := finished.
Definition bind {R A A'} (v : PartiallyFueled R A) (k : A -> PartiallyFueled R A') : PartiallyFueled R A'
  := match v with
     | finished v => k v
     | needs_acc f
       => needs_acc (fun acc => match k (f acc) with
                                | finished v => v
                                | needs_acc f' => f' acc
                                end)
     end.
Definition fully_fuel {R : Prop} {A} (r : R) (v : PartiallyFueled R A) : A
  := match v with
     | finished v => v
     | needs_acc f => f r
     end.
Notation "x <- c1 ;; c2" := (@bind _ _ _ c1 (fun x => c2))
                              (at level 100, c1 at next level, right associativity).


Definition Fix_fueled_F {A} {R : A -> A -> Prop} (P : A -> Type)
           (F : forall x : A, (forall y : A, R y x -> PartiallyFueled (well_founded R) (P y)) -> PartiallyFueled (well_founded R) (P x))
  : forall (x : A) (fuel : nat), PartiallyFueled (well_founded R) (P x)
  := fix Fix_fueled_F (x : A) (fuel : nat) : PartiallyFueled (well_founded R) (P x)
    := F x (fun y _ => match fuel with
                       | O => needs_acc (fun rwf => @Fix A R rwf P (fun x f => fully_fuel rwf (F x (fun y h => finished (f y h)))) y)
                       | S fuel' => Fix_fueled_F y fuel'
                       end).

#[program]
Definition fib (n : nat) : PartiallyFueled (well_founded lt) nat
  := @Fix_fueled_F
       nat lt (fun _ => nat)
       (fun n fib => match n with
                     | 0 => ret 1
                     | 1 => ret 1
                     | S (S n) => (fn <- fib n _;; fsn <- fib (S n) _;; ret (fn + fsn))
                     end)
       n 100.
Axiom ltwf : well_founded lt.
Compute fully_fuel ltwf (fib 10). (* 89 *)

Jason Gross (Nov 07 2022 at 21:14):

The idea is that you do everything inside this monad that tracks whether or not you need the well-founded proof. When you're doing the computational work, you use the monad to abstract away whether you're in fuel-land or acc-land. When you're tying everything together, there's a general fixpoint combinator that basically says "use fuel until you're out; then switch to using well-founded". It's a little bit ugly in that everything happens inside this monad, and I don't really see a way to make the fuel go away in extraction, but I think that's a small price to pay for being able to make use of the proofs without needing to depend on the SN axiom.

Théo Winterhalter (Nov 07 2022 at 22:27):

The main motivation for this implementation was to have no fuel at extraction so I'm not sure we'd like that.

Jason Gross (Nov 07 2022 at 23:03):

Can you share a bit more of the design desires around extraction? What does avoiding fuel in extraction get you?

Jason Gross (Nov 07 2022 at 23:03):

(If it's just about having a function that doesn't error out if it runs out of fuel, this methodology achieves that)

Jason Gross (Nov 07 2022 at 23:04):

(And if matching on the fuel is too expensive, you can just pass in 0 for the fuel and the extracted code will behave the same except for an extra branch at the top level)

Théo Winterhalter (Nov 08 2022 at 12:53):

I think we wanted to handwave that we were basically producing the same we would write in ocaml. It's anyway false. But anything that might drag performance down for something already not fast is something I guess we would like to avoid.

On my side I'm also afraid it will complicate an already very complicated definition. But it may well be that all my fears are unfounded.

Jason Gross (Nov 09 2022 at 00:19):

I'm trying to code up an example change. How do I change

          | @exist (Some (args, c, ρ)) eq2 with inspect (reduce c (Fix_app mfix idx args :: ρ) _) := {
            | @exist (@exist (t, ρ') prf) eq3 with construct_viewc t := {

into something that does a monadic bind on reduce either before or after the inspect?

          | @exist (Some (args, c, ρ)) eq2 :=
            '(@exist (t, ρ') prf) <- reduce c (Fix_app mfix idx args :: ρ) _;;
              with construct_viewc t := {

is a syntax error...

Théo Winterhalter (Nov 10 2022 at 08:41):

I guess you need to basically reimplement bind manually…

Jason Gross (Nov 11 2022 at 15:05):

Is there no way to add syntactic sugar for it? The bind of this monad is non-trivial and implementing it manually duplicates code in a way that seems pretty terrible to inline:

Definition partially_fueled_bind {R A A'} (v : PartiallyFueled R A) (k : A -> PartiallyFueled R A') : PartiallyFueled R A'
  := match v with
     | finished v => k v
     | needs_acc f
       => needs_acc (fun acc => match k (f acc) with
                                | finished v => v
                                | needs_acc f' => f' acc
                                end)
     end.

Paolo Giarrusso (Nov 11 2022 at 20:07):

Is inlining even enough? It seems you'd need with inside a lambda, right? Since equations-based pattern-matching lambdas are not available in Coq, you probably need a named helper function using where?

Last updated: Sep 09 2024 at 06:02 UTC