Write KreMLin code to avoid some of bugs about postmortem

[master-q]

https://ocaml.org/releases/

KreMLin requires OCaml (>= 4.05.0, < 4.10.0)

$ opam switch create 4.05.0
$ opam switch
#  switch  compiler                    description
→  4.05.0  ocaml-base-compiler.4.05.0  4.05.0
$ opam install ppx_deriving_yojson zarith pprint menhir sedlex process fix wasm.1.0.1 visitors ctypes-foreign ctypes
--snip--
∗ installed wasm.1.0.1
[ERROR] The compilation of ocaml-secondary-compiler failed at "/home/kiwamu/.opam/opam-init/hooks/sandbox.sh build make -j3 world.opt".

#=== ERROR while compiling ocaml-secondary-compiler.4.08.1-1 ==================#
# context     2.0.5 | linux/x86_64 | ocaml-base-compiler.4.05.0 | https://opam.ocaml.org#fc695fe5
# path        ~/.opam/4.05.0/.opam-switch/build/ocaml-secondary-compiler.4.08.1-1
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j3 world.opt
# exit-code   2
# env-file    ~/.opam/log/ocaml-secondary-compiler-35975-14c197.env
# output-file ~/.opam/log/ocaml-secondary-compiler-35975-14c197.out
### output ###
# [...]
# echo '#!' | tr -d '\012' > camlheader_ur;
# ../boot/ocamlrun ../boot/ocamlc -use-prims ../runtime/primitives -strict-sequence -absname -w +a-4-9-41-42-44-45-48 -g -warn-error A -bin-annot -nostdlib -safe-string -strict-formats  -nopervasives -c camlinternalFormatBasics.ml
# ../boot/ocamlrun ../boot/ocamlc -use-prims ../runtime/primitives -strict-sequence -absname -w +a-4-9-41-42-44-45-48 -g -warn-error A -bin-annot -nostdlib -safe-string -strict-formats  -nopervasives -no-alias-deps -w -49  -pp "$AWK -f expand_module_aliases.awk" -c stdlib.mli
# gawk: fatal: can't open source file `expand_module_aliases.awk' for reading (No such file or directory)
# File "/home/kiwamu/.opam/4.05.0/.opam-switch/build/ocaml-secondary-compiler.4.08.1-1/stdlib/stdlib.mli", line 1:
# Error: Error while running external preprocessor
# Command line: gawk -f expand_module_aliases.awk 'stdlib.mli' > /tmp/ocamlpp253857
# 
# make[1]: *** [Makefile:251: stdlib.cmi] Error 2
# make[1]: *** Waiting for unfinished jobs....
# make[1]: Leaving directory '/home/kiwamu/.opam/4.05.0/.opam-switch/build/ocaml-secondary-compiler.4.08.1-1/stdlib'
# make: *** [Makefile:325: coldstart] Error 2

???

[master-q]

On Debian Buster:

$ sudo apt install libgmp-dev pkg-config libffi-dev z3
$ opam install fstar
$ export FSTAR_HOME=$HOME/.opam/default/.opam-switch/sources/fstar.0.9.3.0-beta1
$ make -C $FSTAR_HOME/ulib/ml
$ opam install ppx_deriving_yojson zarith pprint menhir sedlex process fix wasm.1.0.1 visitors ctypes-foreign ctypes
$ git clone https://github.com/FStarLang/kremlin.git
$ cd kremlin
$ make
$ ./krml | head -1
KreMLin: from a ML-like subset to C

Umm...

[master-q]

Ah, we should use Everest script.

[master-q]

On Debian Buster:

$ ./everest z3 opam
$ ./everest pull FStar make kremlin make
--snip--
================================================================================
Rebuilding FStar
Running: build_fstar
make: Entering directory '/home/vagrant/src/everest/FStar/src/ocaml-output'
Makefile:79: *** Correct version of menhir not found (needs a version newer than 20161115).  Stop.
make: Leaving directory '/home/vagrant/src/everest/FStar/src/ocaml-output'
================================================================================
FAILURE: build failed for FStar
$ opam install menhir
[NOTE] Package menhir is already installed (current version is 20200624).

???

[master-q]

Firstly we should read documents instead of building the tool chain.
https://fstarlang.github.io/lowstar/html/Core.html

[master-q]

Trying to use build_local.sh...

[master-q]

$ pwd
/home/kiwamu/src/everest
$ ./build_local.sh
--snip--
Step 29/29 : RUN rm .ssh/id_rsa
 ---> Running in 3d0a9ba1d49d
Removing intermediate container 3d0a9ba1d49d
 ---> ba91ed68ec19
Successfully built ba91ed68ec19
Successfully tagged everest:local
$ docker images|grep everest
everest                           local               ba91ed68ec19        About a minute ago   12.9GB
projecteverest/everest-ci-linux   5edd5df537d4        d9d5e20936ac        24 hours ago         5.36GB
projecteverest/fstar-linux        0032bcd7fbb7        6472ab2a9a8a        5 weeks ago          8.85GB

[master-q]

$ docker run -it everest:local /bin/bash
everest@263bc0a5d971:~$ cd ~/everest/kremlin/
everest@263bc0a5d971:~/everest/kremlin$ ./krml | head -3 
KreMLin: from a ML-like subset to C

Usage: ./Kremlin.native [OPTIONS] FILES

[master-q]

everest@263bc0a5d971:~$ eval $(opam env)
everest@263bc0a5d971:~$ export PATH=~/everest/z3/bin:$PATH
everest@263bc0a5d971:~$ export FSTAR_HOME=~/everest/FStar 
everest@263bc0a5d971:~$ export KREMLIN_HOME=~/everest/kremlin 
everest@263bc0a5d971:~$ cd ~/everest/kremlin/test/
everest@263bc0a5d971:~/everest/kremlin$ make
everest@263bc0a5d971:~/everest/kremlin/test$ cd ../book/
everest@263bc0a5d971:~/everest/kremlin/book$ make html
--snip--
writing output... [100%] tutorial/specs/Spec.Test                                                                                                                                                 

Warning, treated as error:
/home/everest/everest/kremlin/book/Toy.rst:13:toctree contains reference to document 'tutorial/specs/Spec.Bignum' that doesn't have a title: no link will be generated
make: *** [Makefile:37: html] Error 2

Umm...

[master-q]

everest@263bc0a5d971:~/src/practice-krml$ cat simple.krml 
module Intro

module P = LowStar.Printf
module C = LowStar.Comment
module B = LowStar.Buffer

open FStar.HyperStack.ST
open LowStar.BufferOps

let main (): St Int32.t =
  push_frame ();
  let b: B.buffer UInt32.t = B.alloca 0ul 8ul in
  b.(0ul) <- 255ul;
  C.comment "Calls to printf are desugared via meta-programming";
  let s = "from Low*!" in
  P.(printf "Hello from %s\nbuffer contents: %xul\n"
    s 8ul b done);
  pop_frame ();
  0l
everest@263bc0a5d971:~/src/practice-krml$ $KREMLIN_HOME/krml simple.krml
Fatal error: exception Failure("input_value: bad object")

???

[master-q]

$ docker images|grep everest
everest                           local          cefd03ba92cb   4 days ago      13.2GB
projecteverest/everest-ci-linux   32c49e325035   79fb46300371   5 days ago      5.38GB
projecteverest/everest-ci-linux   5edd5df537d4   d9d5e20936ac   2 months ago    5.36GB
projecteverest/fstar-linux        0032bcd7fbb7   6472ab2a9a8a   4 months ago    8.85GB
$ docker run -it everest:local /bin/bash
everest@c56edec11d3e:~$ eval $(opam env)
everest@c56edec11d3e:~$ export PATH=~/everest/z3/bin:$PATH
everest@c56edec11d3e:~$ export FSTAR_HOME=~/everest/FStar 
everest@c56edec11d3e:~$ export KREMLIN_HOME=~/everest/kremlin 
everest@c56edec11d3e:~$ cd ~/everest/kremlin/test/
everest@c56edec11d3e:~/everest/kremlin/test$ make
--snip--
All verification conditions discharged successfully
mkdir -p dist/
/home/everest/everest/kremlin/krml -tmpdir dist/ -skip-compilation \
  obj/FStar_Pervasives_Native.krml obj/FStar_Pervasives.krml obj/FStar_Mul.krml obj/FStar_Squash.krml obj/FStar_Classical.krml obj/FStar_Preorder.krml obj/FStar_Calc.krml obj/FStar_StrongExcludedMiddle.krml obj/FStar_List_Tot_Base.krml obj/FStar_List_Tot_Properties.krml o
bj/FStar_List_Tot.krml obj/FStar_Seq_Base.krml obj/FStar_FunctionalExtensionality.krml obj/FStar_Seq_Properties.krml obj/FStar_Seq.krml obj/FStar_Math_Lib.krml obj/FStar_Math_Lemmas.krml obj/FStar_BitVector.krml obj/FStar_UInt.krml obj/FStar_UInt32.krml obj/FStar_Int.krml
 obj/FStar_Int16.krml obj/FStar_Ghost.krml obj/FStar_ErasedLogic.krml obj/FStar_UInt64.krml obj/FStar_Monotonic_Witnessed.krml obj/FStar_Order.krml obj/FStar_Reflection_Const.krml obj/FStar_VConfig.krml obj/FStar_Reflection_Types.krml obj/FStar_Reflection_Data.krml obj/FS
tar_Reflection_Builtins.krml obj/FStar_Reflection_Derived.krml obj/FStar_Reflection_Derived_Lemmas.krml obj/FStar_Set.krml obj/FStar_PropositionalExtensionality.krml obj/FStar_PredicateExtensionality.krml obj/FStar_TSet.krml obj/FStar_Monotonic_Heap.krml obj/FStar_Heap.kr
ml obj/FStar_Map.krml obj/FStar_Monotonic_HyperHeap.krml obj/FStar_Monotonic_HyperStack.krml obj/FStar_HyperStack.krml obj/FStar_HyperStack_ST.krml obj/FStar_Universe.krml obj/FStar_GSet.krml obj/FStar_ModifiesGen.krml obj/FStar_Range.krml obj/FStar_Tactics_Common.krml ob
j/FStar_Tactics_Types.krml obj/FStar_Tactics_Result.krml obj/FStar_Tactics_Effect.krml obj/FStar_Tactics_Builtins.krml obj/FStar_Reflection.krml obj/FStar_Tactics_Print.krml obj/FStar_Tactics_SyntaxHelpers.krml obj/FStar_Tactics_Util.krml obj/FStar_Reflection_Formula.krml
 obj/FStar_Tactics_Derived.krml obj/FStar_Tactics_Logic.krml obj/FStar_Tactics.krml obj/FStar_BigOps.krml obj/LowStar_Monotonic_Buffer.krml obj/LowStar_Buffer.krml obj/FStar_Exn.krml obj/FStar_ST.krml obj/FStar_All.krml obj/FStar_List.krml obj/FStar_Int64.krml obj/FStar_I
nt32.krml obj/FStar_Int8.krml obj/FStar_UInt16.krml obj/FStar_UInt8.krml obj/FStar_Char.krml obj/FStar_String.krml obj/LowStar_Printf.krml obj/C.krml obj/A_Base.krml obj/A_Combinators.krml obj/A_Top.krml obj/FStar_Int_Cast.krml obj/B.krml obj/D.krml \
  -warn-error @4@5@18 \
  -fparentheses \
  -static-header A.Base \
  -library A.* \
  -bundle 'B=A.*,FStar.*,LowStar.*,Prims,C' \
  -bundle 'D=A.*,FStar.*,LowStar.*,Prims,C' \
  -bundle 'A.*[rename=A,rename-prefix]' \
  -no-prefix B \
  -minimal \
  -add-include '"A.h"' \
  -o B.exe
✔ [Monomorphization] ⏱️ 75ms
✔ [Inlining] ⏱️ 4ms
✔ [Pattern matches compilation] ⏱️ 5ms
Warning 7: : After inlining, D.main2 (going into D) calls C.exit_code (going into B) -- removing the static qualifier from C.exit_code
Warning 7: : After inlining, D.main2 (going into D) calls LowStar.Printf.print_u64 (going into B) -- removing the static qualifier from LowStar.Printf.print_u64
✔ [Structs + Simplify 2] ⏱️ 5ms
✔ [Drop] ⏱️ 4ms
✔ [AstToCStar] ⏱️ 3ms
✔ [CStarToC] ⏱️ <1ms
⚙ KreMLin auto-detecting tools. Here's what we found:
readlink is: readlink
KreMLin called via: /home/everest/everest/kremlin/krml
KreMLin home is: /home/everest/everest/kremlin
⚙ KreMLin will drive F*. Here's what we found:
read FSTAR_HOME via the environment
fstar is on branch master
fstar is: /home/everest/everest/FStar/bin/fstar.exe /home/everest/everest/kremlin/runtime/WasmSupport.fst /home/everest/everest/FStar/ulib/FStar.UInt128.fst --trace_error --cache_checked_modules --expose_interfaces --include /home/everest/everest/kremlin/kremlib --include /home/everest/everest/kremlin/include
✔ [PrettyPrinting] ⏱️ 6ms
KreMLin: wrote out .c files for B, D
KreMLin: wrote out .h files for B, D
! test -e dist/A.h
make -C dist/ -f Makefile.basic USER_CFLAGS=-I/home/everest/everest/kremlin/test/sepcomp/a/dist
make[3]: Entering directory '/home/everest/everest/kremlin/test/sepcomp/b/dist'
cc -I. -I /home/everest/everest/kremlin/include -I /home/everest/everest/kremlin/kremlib/dist/minimal -Wall -Wextra -Werror -std=c11 -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-parameter -Wno-infinite-recursion -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -fPIC -I/home/everest/everest/kremlin/test/sepcomp/a/dist   -c -o B.o B.c
cc -I. -I /home/everest/everest/kremlin/include -I /home/everest/everest/kremlin/kremlib/dist/minimal -Wall -Wextra -Werror -std=c11 -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-parameter -Wno-infinite-recursion -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -fPIC -I/home/everest/everest/kremlin/test/sepcomp/a/dist   -c -o D.o D.c
cc -I. -I /home/everest/everest/kremlin/include -I /home/everest/everest/kremlin/kremlib/dist/minimal -Wall -Wextra -Werror -std=c11 -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-parameter -Wno-infinite-recursion -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -fPIC -I/home/everest/everest/kremlin/test/sepcomp/a/dist -o B.exe B.o D.o /home/everest/everest/kremlin/kremlib/dist/generic/libkremlib.a
make[3]: Leaving directory '/home/everest/everest/kremlin/test/sepcomp/b/dist'
dist/B.exe
1729make[2]: Leaving directory '/home/everest/everest/kremlin/test/sepcomp/b'
make[1]: Leaving directory '/home/everest/everest/kremlin/test/sepcomp'
everest@c56edec11d3e:~/everest/kremlin/test$ cd ../book/
everest@c56edec11d3e:~/everest/kremlin/book$ make html
ocaml fst2rst.ml < tutorial/specs/Spec.Bignum.fst > tutorial/specs/Spec.Bignum.rst
ocaml fst2rst.ml < tutorial/specs/Spec.Test.fst > tutorial/specs/Spec.Test.rst
ocaml fst2rst.ml < tutorial/code/Impl.Bignum.fst > tutorial/code/Impl.Bignum.rst
ocaml fst2rst.ml < tutorial/code/Impl.Bignum.Lemmas.fst > tutorial/code/Impl.Bignum.Lemmas.rst
ocaml fst2rst.ml < RingBuffer.fst > RingBuffer.rst
ocaml fst2rst.ml < LinkedList4.fst > LinkedList4.rst
ocaml fst2rst.ml < tutorial/code/Impl.Bignum.Intrinsics.fsti > tutorial/code/Impl.Bignum.Intrinsics.rst
mkdir -p _static
Running Sphinx v1.7.2
making output directory...
loading pickled environment... not yet created
building [mo]: targets for 0 po files that are out of date
building [html]: targets for 22 source files that are out of date
updating environment: 22 added, 0 changed, 0 removed
reading sources... [100%] tutorial/specs/Spec.Test                                                                                                                                                
looking for now-outdated files... none found
pickling environment... done
checking consistency... done
preparing documents... done
writing output... [100%] tutorial/specs/Spec.Test                                                                                                                                                 
generating indices... genindex
writing additional pages... search
copying static files... done
copying extra files... done
dumping search index in English (code: en) ... done
dumping object inventory... done
build succeeded.

The HTML pages are in _build/html.

[master-q]

Where should I take simple example of krml file to be compiled?

[master-q]

I think I should take the other people's advice for this issue, because it may be not suitable for kernel layer...