With #32, the smt tactic is becoming robust enough that I can translate some fairly complex expressions (e.g. exponentiation by squaring in $GF(2^8)$ with internals declared). Unfortunately, the current preprocessing approach (concretize) is lacking and falls over on these expressions, so I cannot define the entire circuit. This is to record the problems and propose a general approach. The approach is basically that of Blot et al. in snipe, with some new ideas.
Problems in concretize:
It leaves behind let-bindings. For example, if the goal is @List.foldl Nat .. = .. and the user decides to concretize foldl, we add let List.foldl.Nat := whnf(@List.foldl Nat) to the local context and change the goal to List.foldl.Nat .. = ... While convenient, let-bindings are not well supported by Lean's builtin tactics, for example there is no way to rewrite inside the body of one. Maybe this should be fixed in Lean but otherwise, we need a workaround. There is a good reason to prefer equations, namely that they do not need to justify termination. So we can have foo n = foo (n+1) as an equation, but not as a definition. Lean uses this fact to hide well-foundedness encodings behind its unfold equations.
It does a bit too much. It combines steps 3.1 and 3.5 of snipe, which they separate for a good reason. For example, we may want to first create a local copy of a recursive definition foo using 3.1 so that we can transform it later, but without also monomorphising foo. And then we may want to monomorphise something in the body of foo.
For the snipe approach, we need a representation of "local copies" of definitions which can be transformed and eventually consumed by smt. The equational variant foo.def : ∀ x y z, foo x y z = foo_body x y z that snipe uses seems quite workable. We should ensure it is fully abstract, i.e. that the equality is not over a function, by adding as many binders as possible (3.2 in snipe). This is roughly like the unfold equational theorems that Lean core uses.
We can then use certifying transformations which operate on this representation. The starting set I am going to implement is:
definition extraction (3.1/3.2 - I think the two can be merged) which creates a local copy of a definition to manipulate further
monomorphization (3.5), by making concretize more modular
a custom partial evaluation tactic, stay tuned :)
Other ones (that I will not do unless I find them necessary) include #27, ADTs, pattern matching, etc.
One thing to note is that having a bunch of blah.def equations which are expected to be of a certain form is a bit hacky. Fundamentally, the issue is how to transfer information between tactics. It might be nice to eventually provide an smt tactic mode which stores this information instead of relying on the local context. The syntax could be
smt =>
extract_def foo
monomorphize [blah] at foo
extract_def [bar] at foo
solve
With #32, the
smttactic is becoming robust enough that I can translate some fairly complex expressions (e.g. exponentiation by squaring in $GF(2^8)$ with internalsdeclared). Unfortunately, the current preprocessing approach (concretize) is lacking and falls over on these expressions, so I cannotdefinethe entire circuit. This is to record the problems and propose a general approach. The approach is basically that of Blot et al. insnipe, with some new ideas.Problems in
concretize:let-bindings. For example, if the goal is@List.foldl Nat .. = ..and the user decides to concretizefoldl, we addlet List.foldl.Nat := whnf(@List.foldl Nat)to the local context and change the goal toList.foldl.Nat .. = ... While convenient,let-bindings are not well supported by Lean's builtin tactics, for example there is no way to rewrite inside the body of one.Maybe this should be fixed in Lean but otherwise, we need a workaround.There is a good reason to prefer equations, namely that they do not need to justify termination. So we can havefoo n = foo (n+1)as an equation, but not as a definition. Lean uses this fact to hide well-foundedness encodings behind itsunfoldequations.snipe, which they separate for a good reason. For example, we may want to first create a local copy of a recursive definitionfoousing 3.1 so that we can transform it later, but without also monomorphisingfoo. And then we may want to monomorphise something in the body offoo.For the
snipeapproach, we need a representation of "local copies" of definitions which can be transformed and eventually consumed bysmt. The equational variantfoo.def : ∀ x y z, foo x y z = foo_body x y zthatsnipeuses seems quite workable. We should ensure it is fully abstract, i.e. that the equality is not over a function, by adding as many binders as possible (3.2 insnipe). This is roughly like theunfoldequational theorems that Lean core uses.We can then use certifying transformations which operate on this representation. The starting set I am going to implement is:
concretizemore modularOther ones (that I will not do unless I find them necessary) include #27, ADTs, pattern matching, etc.
One thing to note is that having a bunch of
blah.defequations which are expected to be of a certain form is a bit hacky. Fundamentally, the issue is how to transfer information between tactics. It might be nice to eventually provide ansmttactic mode which stores this information instead of relying on the local context. The syntax could be