Peano encoding probably bad

[workingjubilee]

The Rust compiler is unlikely to successfully compile anything that requires explosively recursive expressions. Even after rust-lang/rust#122717 for example, it will still have to actually finish trait resolving, borrow checking, and codegen. Also, it will be obviously slow. Use of an intermediate encoding that is amenable to applying a rewrite rule to eliminate the redexes, and actually applying such a rule during extraction, would be preferable. That way you don't have to assume that rustc will put up with being force-fed an infinite amount of abstract nonsense.

The more general cases regarding inefficient implementation work are already discussed by other authors such as Jansen, Koopman, and Plasmeijer, i.e. https://repository.ubn.ru.nl/bitstream/handle/2066/151174/151174.pdf?sequence=1&isAllowed=y

[spitters]

There is now better support for primitive types, like the integers, in metacoq/certicoq. We should probably be using it in rust extraction too. @womeier has also been looking at it recently

…

On Tue, Mar 19, 2024 at 6:18 PM Jubilee ***@***.***> wrote: The Rust compiler is unlikely to successfully compile anything that requires explosively recursive expressions. Even after rust-lang/rust#122717 <rust-lang/rust#122717> for example, it will still have to actually finish trait resolving, borrow checking, and codegen. Also, it will be obviously slow. Use of an intermediate encoding that is amenable to applying a rewrite rule to eliminate the redexes, and actually applying such a rule during extraction, would be preferable. That way you don't have to assume that rustc will put up with being force-fed an infinite amount of abstract nonsense. The more general cases regarding inefficient implementation work are already discussed by other authors such as Jansen, Koopman, and Plasmeijer, i.e. https://repository.ubn.ru.nl/bitstream/handle/2066/151174/151174.pdf?sequence=1&isAllowed=y — Reply to this email directly, view it on GitHub <#17>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABTNTVCOOEFVK76RE73RETYZBXOLAVCNFSM6AAAAABE572EYSVHI2DSMVQWIX3LMV43ASLTON2WKOZSGE4TKNJUGI2DGMY> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[spitters]

Actually, the natural numbers are already remapped:
https://github.com/AU-COBRA/coq-rust-extraction/blob/master/plugin/theories/ExtrRustCheckedArith.v

@workingjubilee which Peano numbers were you referring too ?

[workingjubilee]

@Spitter: I mean the extraction of this:

Fixpoint insert_list (l : list nat) (q : priqueue) :=
match l with
| [] => q
| x :: l => insert_list l (insert x q)
end.


Fixpoint make_list (n : nat) (l : list nat) :=
match n with
| 0 => 0 :: l
| S 0 => 1 :: l
| S (S n) => make_list n (S (S n) :: l)
end.

Definition main :=
let a := insert_list (make_list 2000 []) empty in

to this:

fn CertiCoq_Benchmarks_lib_Binom_main(&'a self) -> CertiCoq_Benchmarks_lib_Binom_key<'a> {
let a =
self.CertiCoq_Benchmarks_lib_Binom_insert_list(
self.CertiCoq_Benchmarks_lib_Binom_make_list(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
__nat_succ(
0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
self.alloc(
Coq_Init_Datatypes_list::nil(
PhantomData))),
self.CertiCoq_Benchmarks_lib_Binom_empty());

[workingjubilee]

The following extraction would be equally valid:

let a = self.CertiCoq_Benchmarks_lib_Binom_insert_list(
    self.CertiCoq_Benchmarks_lib_Binom_make_list({
        let mut n = 0;
        for _ in 0..2000 = {
            n = __nat_succ(n);
        }
        n
    },
    self.alloc(Coq_Init_Datatypes_list::nil(PhantomData))),
    self.CertiCoq_Benchmarks_lib_Binom_empty()
);

You could even just use iter::successors and then simply make it

iter::successors(initial_value, |n| some_fn(n)).nth(2000)

It's basically a function made with things like this in mind.

[4ever2]

@spitters This is about natural number literals, we do remap functions on natural numbers to their efficient Rust counterparts. However, literals are not translated directly to Rust literals, so 3 which in Coq is S (S (S O)) will become __nat_succ(__nat_succ(__nat_succ(0)) in Rust, where __nat_succ is defined as

fn __nat_succ(x: u64) -> u64 {
  x.checked_add(1).unwrap()
}

This works fine for small numbers but the CertiCoq Binom example uses a larger literal which Rust struggles with.

@workingjubilee Your suggestions are valid but they would be hard to produce in our verified extraction with how the pipeline works at the moment.

We could probably produce the Rust literals directly on the Coq side, but I don't have time to look into this at the moment. However, it is something that we would want to improve at some point in the future.

[workingjubilee]

@4ever2 Curious as to why that is. Is the extraction too rigid to reduce?

[womeier]

There is now better support for primitive types, like the integers, in metacoq/certicoq. We should probably be using it in rust extraction too. @womeier has also been looking at it recently

We may try to add support for primitives to the rust extraction, but it's currently not a priority.

[4ever2]

Curious as to why that is. Is the extraction too rigid to reduce?

It is not so much producing the code that is problematic, the problem is proving such a translation correct.

We could spend time trying to prove that, but on the other hand people wishing to extract code from Coq to efficient implementations should not use the nat datatype. There are already more efficient data types in Coq that are better for extraction and primitives which could easily be supported.

@womeier Adding support for primitives to the rust extraction should be quite easy. The MetaCoq typed erasure should already support primitives, so it is probably as simple as adding support in the final printing step.

[4ever2]

@workingjubilee We could naturally reduce such literals in an unverified step, we already do that for some of the other extraction languages that we support https://github.com/AU-COBRA/ConCert/blob/8433cdeb62c37974c53a5fa6fec0dc8318271fe2/extraction/theories/CameLIGOPretty.v#L471

I don't recall why we didn't do it for Rust.

[workingjubilee]

"should not" but evidently a benchmark is how well the extraction supports Nat.

[workingjubilee]

I suppose an alternative is to PR a change to the upstream examples/benchmarks so that they use a data type more reflective of what you would deem a "real world" usage.

[spitters]

@womeier I'm curious what happens with this code in the other backends. Do we see a similar unfolding in the C and wasm backends. We're still figuring out why they are so huge, this may be one of the reasons??

[womeier]

@spitters
I'm fairly certain this is the main reason why our binaries are so large.

The lambdaANF looks like this, which we translate one-by-one to Wasm:

let y_334 := O() in 
let y_335 := S(y_334) in 
let y_336 := S(y_335) in 
let y_337 := S(y_336) in 
let y_338 := S(y_337) in 
let y_339 := S(y_338) in 
let y_340 := S(y_339) in 
let y_341 := S(y_340) in 
let y_342 := S(y_341) in 
let y_343 := S(y_342) in 
let y_344 := S(y_343) in
...

Just reusing the common part of somewhat big Nats would reduce binary size quite a bit, I guess, but perhaps you shouldn't use a Nat in that case anyway.
(Zoe lists common subexpression elimination on lambdaANF under future work.)

Hoping for binaryen/clang to optimize operations on the boxed values also seems quite optimistic.
At least binaryen's optimizations are quite conservative around store instructions, it certainly doesn't take advantage of the fact that we never overwrite existing values, and it could thus optimize loads more aggressively.
(perhaps using WasmGC's structs to box constructors will allow binaryen to perform more advanced dataflow analyses, at least that's what I hope)

[spitters]

Great! So, should we just remove the unary natural 2000 to the binary 2000 in the sources then? The subexpressions can maybe be done by using some extra lets in the source code?

…

On Mon, Mar 25, 2024 at 8:41 PM Wolfgang Meier ***@***.***> wrote: @spitters <https://github.com/spitters> I'm fairly certain this is the main reason why our binaries are so large. The lambdaANF looks like this, which we translate one-by-one to Wasm: let y_334 := O() in let y_335 := S(y_334) in let y_336 := S(y_335) in let y_337 := S(y_336) in let y_338 := S(y_337) in let y_339 := S(y_338) in let y_340 := S(y_339) in let y_341 := S(y_340) in let y_342 := S(y_341) in let y_343 := S(y_342) in let y_344 := S(y_343) in ... Just reusing the common part of somewhat big Nats would reduce binary size quite a bit, I guess, but perhaps you shouldn't use a Nat in that case anyway. (Zoe lists common subexpression elimination on lambdaANF under future work.) Hoping for binaryen/clang to optimize operations on the boxed values also seems quite optimistic. At least binaryen's optimizations are quite conservative around store instructions, it certainly doesn't take advantage of the fact that we never overwrite existing values, and it could thus optimize loads more aggressively. (perhaps using WasmGC's structs to box constructors will allow binaryen to perform more advanced dataflow analyses) — Reply to this email directly, view it on GitHub <#17 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABTNTSVOS7FKIVCNIMBLA3Y2B4XJAVCNFSM6AAAAABE572EYSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDAMJYG43TIMZSGQ> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[womeier]

Great! So, should we just remove the unary natural 2000 to the binary 2000 in the sources then?

Yes, ideal would be this though:
One could replace Nats by primitives on lambdaANF then clang/binaryen should be able to do constant folding for applications of S.
Proving such a transformation correct could be tricky, not sure how that would work in detail. (It's probably fair to assume that all nats < i63.max, but there are probably other considerations.)

The subexpressions can maybe be done by using some extra lets in the source code?

yes