diff --git a/.docker/build/build-standalone.sh b/.docker/build/build-standalone.sh index c8f2b3f68..5f1619824 100755 --- a/.docker/build/build-standalone.sh +++ b/.docker/build/build-standalone.sh @@ -13,6 +13,5 @@ build_home="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" rootPath=$(pwd) export_home KRML "$rootPath" result_file="result.txt" -exec_build $target - -grep Success < "$result_file" +out_file="log.txt" +{ { { { { { exec_build ; } 3>&1 1>&2 2>&3 ; } | sed -u 's!^![STDERR]!' ; } 3>&1 1>&2 2>&3 ; } | sed -u 's!^![STDOUT]!' ; } 2>&1 ; } | awk '{ print strftime("[%Y-%m-%d %H:%M:%S]"), $0 }' | tee $out_file diff --git a/.docker/standalone.Dockerfile b/.docker/standalone.Dockerfile index ed2b2affe..ac79249d3 100644 --- a/.docker/standalone.Dockerfile +++ b/.docker/standalone.Dockerfile @@ -1,13 +1,41 @@ -# This Dockerfile should be run from the root FStar directory +# This Dockerfile should be run from the root Karamel directory -ARG ocaml_version=4.12 -FROM ocaml/opam:ubuntu-ocaml-$ocaml_version +FROM ubuntu:22.04 -ADD --chown=opam:opam ./ karamel/ -WORKDIR karamel +# CI dependencies: opam, jq (to identify F* branch) +RUN apt-get update && \ + apt-get install -y --no-install-recommends \ + jq \ + ca-certificates \ + curl \ + wget \ + git \ + gawk \ + coreutils \ + sudo \ + opam -# CI dependencies: jq (to identify F* branch) -RUN sudo apt-get install -y --no-install-recommends jq + +# Create a new user and give them sudo rights +# NOTE: we give them the name "opam" to keep compatibility with +# derived hierarchical CI +RUN useradd -d /home/opam opam +RUN echo 'opam ALL=NOPASSWD: ALL' >> /etc/sudoers +RUN mkdir /home/opam +RUN chown opam:opam /home/opam +USER opam +ENV HOME /home/opam +WORKDIR $HOME +SHELL ["/bin/bash", "--login", "-c"] + +# Install OCaml +ARG OCAML_VERSION=4.12.0 +RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing +RUN opam env --set-switch | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile +ENV OPAMYES=1 + +ADD --chown=opam:opam ./ $HOME/karamel/ +WORKDIR $HOME/karamel # Dependencies (F* and opam packages) ENV FSTAR_HOME=$HOME/FStar @@ -29,3 +57,7 @@ RUN sudo pip3 install sphinx==1.7.2 jinja2==3.0.0 sphinx_rtd_theme ARG CI_THREADS=24 ARG CI_BRANCH=master RUN --mount=type=secret,id=DZOMO_GITHUB_TOKEN eval $(opam env) && DZOMO_GITHUB_TOKEN=$(sudo cat /run/secrets/DZOMO_GITHUB_TOKEN) .docker/build/build-standalone.sh $CI_THREADS $CI_BRANCH +# RUN eval $(opam env) && .docker/build/build-standalone.sh $CI_THREADS $CI_BRANCH + +WORKDIR $HOME +ENV KRML_HOME=$HOME/karamel diff --git a/.github/workflows/linux-x64-hierarchic.yaml b/.github/workflows/linux-x64-hierarchic.yaml index 021eafc89..cad303f27 100644 --- a/.github/workflows/linux-x64-hierarchic.yaml +++ b/.github/workflows/linux-x64-hierarchic.yaml @@ -23,14 +23,24 @@ jobs: if docker image inspect fstar:local-branch-$FSTAR_BRANCH ; then echo KRML_CI_FLAVOR=hierarchic >> $GITHUB_ENV ; else echo KRML_CI_FLAVOR=standalone >> $GITHUB_ENV ; fi - name: Build Karamel and its dependencies run: | - if { echo $GITHUB_REF_NAME | grep '/' ; } ; then - docker_build_tag_opt= - else - docker_build_tag_opt="-t karamel:local-branch-$GITHUB_REF_NAME" + ci_docker_image_tag=karamel:local-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT + docker buildx build --secret id=DZOMO_GITHUB_TOKEN -t $ci_docker_image_tag -f .docker/$KRML_CI_FLAVOR.Dockerfile --build-arg FSTAR_BRANCH=$FSTAR_BRANCH --build-arg CI_BRANCH=$GITHUB_REF_NAME . + if docker run $ci_docker_image_tag /bin/bash -c 'cat $KRML_HOME/result.txt' | grep Success ; then ci_docker_status=true ; else ci_docker_status=false ; fi + if $ci_docker_status ; then + if ! { echo $GITHUB_REF_NAME | grep '/' ; } ; then + docker tag $ci_docker_image_tag karamel:local-branch-$GITHUB_REF_NAME + fi + docker tag $ci_docker_image_tag karamel:local-commit-$GITHUB_SHA fi - docker buildx build --secret id=DZOMO_GITHUB_TOKEN $docker_build_tag_opt -t karamel:local-commit-$GITHUB_SHA -f .docker/$KRML_CI_FLAVOR.Dockerfile --build-arg FSTAR_BRANCH=$FSTAR_BRANCH --build-arg CI_BRANCH=$GITHUB_REF_NAME . + docker run $ci_docker_image_tag /bin/bash -c 'cat $KRML_HOME/log.txt' > log.txt + $ci_docker_status env: DZOMO_GITHUB_TOKEN: ${{ secrets.DZOMO_GITHUB_TOKEN }} + - name: Archive build log + uses: actions/upload-artifact@v3 + with: + name: log + path: log.txt - name: Compute elapsed time if: ${{ always() }} run: | diff --git a/karamel.opam b/karamel.opam index 9885fca61..ac87e3f5b 100644 --- a/karamel.opam +++ b/karamel.opam @@ -18,7 +18,7 @@ depends: [ "process" "fix" "visitors" - "wasm" {>= "1.1.1"} + "wasm" {>= "2.0.0"} "ppx_deriving" "ppx_deriving_yojson" "fstar" diff --git a/krmllib/hints/C.Endianness.fst.hints b/krmllib/hints/C.Endianness.fst.hints index d2e1acce5..ae1d1e68d 100644 --- a/krmllib/hints/C.Endianness.fst.hints +++ b/krmllib/hints/C.Endianness.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "a782db57b5a952f771da72dda32b8edc" + "a3e154db3012c09a95a2788d336bdec9" ], [ "C.Endianness.load16_le", @@ -17,7 +17,7 @@ 1, [ "@query" ], 0, - "2cc2dcf46a8d53bb32b116a94612493b" + "ceab66181437a6754b8535c633d399fd" ], [ "C.Endianness.store16_be", @@ -26,7 +26,7 @@ 1, [ "@query" ], 0, - "84addbd2f9840f43d9619bc1d6bffc06" + "383525b28da6b603638f4a91b97a2457" ], [ "C.Endianness.load16_be", @@ -35,7 +35,7 @@ 1, [ "@query" ], 0, - "71745e57e56de06fc402812aa3d59f81" + "13b6592234de9b76a94e2c2c2af2a4bd" ], [ "C.Endianness.store32_le", @@ -44,7 +44,7 @@ 1, [ "@query" ], 0, - "32468b8590d1b6e06390906c2dab63e2" + "b40fb439110606db773f6685776e1c32" ], [ "C.Endianness.load32_le", @@ -53,7 +53,7 @@ 1, [ "@query" ], 0, - "b770fbb3eb16bd547958d03841d04310" + "17024716b2d35577c06f1b2f7c92e10c" ], [ "C.Endianness.store32_be", @@ -62,7 +62,7 @@ 1, [ "@query" ], 0, - "9481bfbd2f8305c587c21ef3348fcfb9" + "5b92c8c6d4a87e2f689e9dc2bbf3093e" ], [ "C.Endianness.load32_be", @@ -71,7 +71,7 @@ 1, [ "@query" ], 0, - "1efc90224f6438ffed733179dd71a0ed" + "9c33f3cb3c7e7662bf94342efe9838c3" ], [ "C.Endianness.store64_le", @@ -80,7 +80,7 @@ 1, [ "@query" ], 0, - "842da27a9aa50b35cfc52190bdf56d8f" + "3b0ad5f3046a7c5f7bad2bc389543b02" ], [ "C.Endianness.load64_le", @@ -89,7 +89,7 @@ 1, [ "@query" ], 0, - "f6ec7dc48936fe76fb77c343d85f8e1b" + "16b3614ad77b565cb1ada8cd5f6d18eb" ], [ "C.Endianness.load64_be", @@ -98,7 +98,7 @@ 1, [ "@query" ], 0, - "4ca4195d265ed648187d44a697fc4e86" + "dac048bf93f2976d7155dec2a723f12f" ], [ "C.Endianness.store64_be", @@ -107,7 +107,7 @@ 1, [ "@query" ], 0, - "275b1013639857f060d1e4a829b529c5" + "cd21c8fc1c4c911447f222bbf7d961dc" ], [ "C.Endianness.load128_le", @@ -119,7 +119,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "1c8d420742ad3c2258bd48bcc8209316" + "f028578fd05ab0b770c150416c792112" ], [ "C.Endianness.store128_le", @@ -131,7 +131,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "cd7892d1dcfe9b2d5c633c4e0891c7b8" + "936ba7bea0843fea5eb155d8ecf5d9d3" ], [ "C.Endianness.load128_be", @@ -143,7 +143,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "008e8270b32e51ebad0eb4fd01e73d84" + "96546044af2abc1fd57ff39ef340b367" ], [ "C.Endianness.store128_be", @@ -155,7 +155,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "b22c0008c66231f308bb616971b70d30" + "912a59ab5b4aaac88590b3ec6f413556" ], [ "C.Endianness.index_32_be", @@ -219,7 +219,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "5c630f70ca284512689c0338445b4b8f" + "c5c6f61d6e01f97d3c52175c91d8025a" ], [ "C.Endianness.index_32_le", @@ -281,7 +281,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "8ff49a3b9547ccd393c47685df6f0fee" + "835b1d6b547e365d360d15ab1bf37cc1" ], [ "C.Endianness.index_64_be", @@ -344,7 +344,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "2d3d625581ab708679bd857ae8101adb" + "71eb2537bb2f692cc0f04a73e994d61b" ], [ "C.Endianness.index_64_le", @@ -404,7 +404,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "2db16df34e340019f4d8a1a9ef77062e" + "7e75b082c923492c3d30024045fed466" ], [ "C.Endianness.interval_4_disjoint", @@ -421,7 +421,7 @@ "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, - "2aeaf8f8492f9e45e48ed056fff88853" + "219e78002f0589d69143a89c91117cfb" ], [ "C.Endianness.upd_32_be", @@ -500,7 +500,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "5d6c84866f5a790db1c9587dd32cd0b6" + "931a4fe9745365571df078cda7f963b4" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.Failure.fst.hints b/krmllib/hints/C.Failure.fst.hints index 18f9eba6e..d7626cec5 100644 --- a/krmllib/hints/C.Failure.fst.hints +++ b/krmllib/hints/C.Failure.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "4883691299735faf4931de8987af14d4" + "cf79e35930e222e5b6da43e86f7ea2bb" ], [ "C.Failure.failwith", @@ -29,7 +29,7 @@ 1, [ "@query" ], 0, - "f6f23e608c4e636a5a478119a2ac1075" + "a1322b6a42d6da7146329de09f655219" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.Loops.fst.hints b/krmllib/hints/C.Loops.fst.hints index 33420c515..cec6ad202 100644 --- a/krmllib/hints/C.Loops.fst.hints +++ b/krmllib/hints/C.Loops.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.UInt32.v" ], 0, - "31ded2c429b8af58c93962a98839ebb9" + "40a8d9351062cd547952d66cf777f598" ], [ "C.Loops.for", @@ -40,7 +40,7 @@ "typing_FStar.UInt32.v" ], 0, - "03ac769296d852ed94332e5f67c05ffa" + "bac9bd495c115f9be773fdaf074aa843" ], [ "C.Loops.for", @@ -80,7 +80,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "58caaf700569346aa72029ac3952a5ea" + "434d6e5d068b1e2e8dc096b2e281c7de" ], [ "C.Loops.for64", @@ -101,7 +101,7 @@ "typing_FStar.UInt64.v" ], 0, - "402b0134b341680a3c025b848433bf90" + "5655970a3d3c1f30a733608bb2e8df1a" ], [ "C.Loops.for64", @@ -121,7 +121,7 @@ "typing_FStar.UInt64.v" ], 0, - "7606fd4952ef1fe7cba5bf036ed956b2" + "7c6d84a39f41c5b2fed46ed47f481655" ], [ "C.Loops.for64", @@ -161,7 +161,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt64.v" ], 0, - "61b5132a4984f081abcd95373314051c" + "396e3c30143fb5545ea5d0d1a51965da" ], [ "C.Loops.reverse_for", @@ -183,7 +183,7 @@ "typing_FStar.UInt32.v" ], 0, - "95ce5c41cb6b547ac4068627b8bff263" + "d52ab0f3a50739058888584a0dba635a" ], [ "C.Loops.reverse_for", @@ -205,7 +205,7 @@ "typing_FStar.UInt32.v" ], 0, - "90c833a3158b87f29af7c7ade2d57e01" + "b0b5cc311f7b95d11432c8c074a986e6" ], [ "C.Loops.reverse_for", @@ -246,7 +246,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "1a9162e3c98a5a605b6df3518320ebd2" + "5ef262fa9997437c8542333211c2858d" ], [ "C.Loops.interruptible_for", @@ -266,7 +266,7 @@ "typing_FStar.UInt32.v" ], 0, - "d906192242c0ee78adcee85336636d28" + "74d13187e8efc993eaffadfa1feaaa6c" ], [ "C.Loops.interruptible_for", @@ -286,7 +286,7 @@ "typing_FStar.UInt32.v" ], 0, - "16db364b639759c1f39928a5e2824bc2" + "db8b5b7252f51dc2a12cbcb35dc455b2" ], [ "C.Loops.interruptible_for", @@ -330,7 +330,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "ee642444fb0e934c22843f9006435c95" + "8abb46037dee083bd4052ac0b6cd638a" ], [ "C.Loops.do_while", @@ -355,7 +355,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "0c3d685788f9e05be74df6c3b5c6f957" + "95e717287e5ba6145293fbdde33252a9" ], [ "C.Loops.while", @@ -369,7 +369,7 @@ "refinement_interpretation_Tm_refine_b16bf82b210653a34e4d7322fab91ffb" ], 0, - "c45fba388844371f5e850272c986581f" + "689bf55f97ef0664d38a35b84ef2f1ea" ], [ "C.Loops.interruptible_reverse_for", @@ -391,7 +391,7 @@ "typing_FStar.UInt32.v" ], 0, - "4f324d1c462bed194200973be451f01c" + "b3bad794ce6b3c91e81fe41efdc1fd58" ], [ "C.Loops.interruptible_reverse_for", @@ -413,7 +413,7 @@ "typing_FStar.UInt32.v" ], 0, - "09bef6900aac8ca26933cc327941134b" + "72b05871d5c336ea3e8b40deb4f7ae98" ], [ "C.Loops.interruptible_reverse_for", @@ -458,7 +458,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "dba510b921aaf8c4aa2304a791ab7e27" + "888fa34b307409c8c6fd2c754db2f3ce" ], [ "C.Loops.map", @@ -467,7 +467,7 @@ 1, [ "@query" ], 0, - "2c0cb9556cd27e9c4a238e7576404b01" + "e47e58b6b336c18b679d654489387857" ], [ "C.Loops.map", @@ -476,7 +476,7 @@ 1, [ "@query" ], 0, - "e8fb59a9ecbe83efaa68605b6f9c6081" + "3533aeeedb00780892d825c4a0185084" ], [ "C.Loops.map", @@ -525,7 +525,7 @@ "typing_Spec.Loops.seq_map" ], 0, - "e1fe9c4daf133c6f183af9808c9060f9" + "33b4350687e5e0207fb61af582847790" ], [ "C.Loops.map2", @@ -540,7 +540,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "6a8ccaf89e259338f26e90b68da35620" + "75907114982abd8c430ded4c0eb7b987" ], [ "C.Loops.map2", @@ -549,7 +549,7 @@ 1, [ "@query" ], 0, - "996cc453e444a50885a8f7a2195d7f3c" + "68fcf02da25a75f32859035f0f4194a1" ], [ "C.Loops.map2", @@ -598,7 +598,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "9b31e2f715cd0159daa68e8dec8dc159" + "fb824c6b398ca7d2ea5419ea108ea18b" ], [ "C.Loops.in_place_map", @@ -607,7 +607,7 @@ 1, [ "@query" ], 0, - "bedbe22e11e0b6f900ebea2f0af68129" + "5b796006f2ed3a393baff276eb84adc0" ], [ "C.Loops.in_place_map", @@ -616,7 +616,7 @@ 1, [ "@query" ], 0, - "4e1686c7ef2b20b5d08b21c607ee35ac" + "4392c2f8be9edddaacef1be72431f8d7" ], [ "C.Loops.in_place_map", @@ -661,7 +661,7 @@ "typing_Spec.Loops.seq_map" ], 0, - "5b6309f12ef5bc932420f4e77da2519c" + "be55c1143b6afd4777fd153e8cfdbed1" ], [ "C.Loops.in_place_map2", @@ -676,7 +676,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "382f11aa96c7fdc1c79050ccec80e8ef" + "45bdb2e47e2160a887201d4fbf289694" ], [ "C.Loops.in_place_map2", @@ -685,7 +685,7 @@ 1, [ "@query" ], 0, - "1c4f87dd524b552e9e33489779742dec" + "187795f23f305cc4eb6ec0e28ede0f6d" ], [ "C.Loops.in_place_map2", @@ -732,7 +732,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "5237988801ac5b255d4007ad7641b404" + "edf9df2aadaee319bb6bb689da879438" ], [ "C.Loops.repeat", @@ -755,7 +755,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "be18d1f218b8b31bfbbc1ac6210016a7" + "a41eafbd0fc2dd2c644acab460d66475" ], [ "C.Loops.repeat", @@ -773,7 +773,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "5864dd2f00fa3b7042ce3ce186b5a3c7" + "dc9c601514b81e951ea81f722faf6f02" ], [ "C.Loops.repeat", @@ -806,7 +806,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "7290cc2a7a4929a99abd887e6c7f715d" + "cf5ef101a5d84ab591878b6befdd6a20" ], [ "C.Loops.repeat_range_body_impl", @@ -820,7 +820,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "df217d5e936d0ade56acb4ae4c057a91" + "039601536b5596e21a24da41d93b26af" ], [ "C.Loops.repeat_range_body_impl", @@ -839,7 +839,7 @@ "typing_FStar.UInt32.v" ], 0, - "f60cfa32dc731aa582b9125fad65a3c5" + "672c56dce99da3c043043bbea7b4fb96" ], [ "C.Loops.repeat_range", @@ -858,7 +858,7 @@ "typing_FStar.UInt32.v" ], 0, - "a60ddab9c2658af1c80365e91c0a50c7" + "bf29608775dc58615c21edef266e4690" ], [ "C.Loops.repeat_range", @@ -872,7 +872,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "aab011b86d2f00847f069e252686ac8e" + "d85f9d1e6490e5cf7bd0bd13dc1a3684" ], [ "C.Loops.repeat_range", @@ -897,7 +897,7 @@ "typing_FStar.UInt32.v" ], 0, - "f49f3d8e9823b413b20ef60b786d3380" + "ae508f1fa52a27d698500403d8f79816" ], [ "C.Loops.total_while_gen", @@ -912,7 +912,7 @@ "equality_tok_Prims.LexTop@tok", "typing_tok_Prims.LexTop@tok" ], 0, - "6950831c8f3e0a54a5c09056a67e6b32" + "2ef527300b008b10bcb08408ffcf9843" ], [ "C.Loops.total_while", @@ -932,7 +932,7 @@ "well-founded-ordering-on-nat" ], 0, - "0884e4483338a4567af7fe7514680362" + "3ae349ec2342fd4cf6019ad1fb31fa4e" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.String.fst.hints b/krmllib/hints/C.String.fst.hints index dd8fc8e74..2bb91c224 100644 --- a/krmllib/hints/C.String.fst.hints +++ b/krmllib/hints/C.String.fst.hints @@ -11,7 +11,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "8a37e0d09b445fa10f2a0e8779734178" + "819336892121622f102db68f98dc5909" ], [ "C.String.well_formed", @@ -23,7 +23,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "fccbfb9609d168f2eebb60a62013005d" + "facdc1c2eb5f912f02367b0f2ac36e78" ], [ "C.String.t", @@ -35,7 +35,7 @@ "lemma_FStar.Seq.Base.hasEq_lemma" ], 0, - "b4ce6cdb2e9ed876e12d6da030a376a0" + "5a490445b53fd0b4cd4a3a19fde43791" ], [ "C.String.length", @@ -50,7 +50,7 @@ "refinement_interpretation_Tm_refine_ed6e8a85e123e1e628ba0dad885f3031" ], 0, - "d6b1978241bf1051daae936e342f4873" + "87bc06329d0da31d059f61404e046488" ], [ "C.String.get", @@ -66,7 +66,7 @@ "refinement_interpretation_Tm_refine_dfcb8c150fd42ce38050af33905be19c" ], 0, - "4c8c3bd13af8e46ad57cb759fc10386b" + "f3a8eeac88bfe00db974f264b18ee2e1" ], [ "C.String.get", @@ -85,7 +85,7 @@ "typing_FStar.UInt32.v" ], 0, - "55d698cceed7b00155ed5a5d03721e39" + "a5b1c305f8ffa65f7cffb8eb17391785" ], [ "C.String.nonzero_is_lt", @@ -98,7 +98,7 @@ "fuel_guarded_inversion_C.String.t" ], 0, - "5835c585174262bed556376e6fe4ff0d" + "630311316a90cded37cb27dc711165c2" ], [ "C.String.nonzero_is_lt", @@ -119,7 +119,7 @@ "typing_FStar.UInt32.v" ], 0, - "d084237ee1279839e93170aa8946da16" + "b0a182aa1bfcaf276ec0f569e758a83b" ], [ "C.String.memcpy", @@ -133,7 +133,7 @@ "typing_FStar.UInt8.t" ], 0, - "a62721bc00716c9656c338412fff0fea" + "3a2a36f2c53b7ed7869778fd480c9f96" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.String.fsti.hints b/krmllib/hints/C.String.fsti.hints index 73c419e9e..3d17cb23b 100644 --- a/krmllib/hints/C.String.fsti.hints +++ b/krmllib/hints/C.String.fsti.hints @@ -11,7 +11,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "3d1138fbcb2dce627f1af6c0803238a7" + "ee68ac3029d650415f45a5bd4c21443a" ], [ "C.String.well_formed", @@ -23,7 +23,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "1c20810e688fa1cfe11633385cc26142" + "99ceba85009f2916c194d513d6c6a6ad" ], [ "C.String.get", @@ -39,7 +39,7 @@ "refinement_interpretation_Tm_refine_dfcb8c150fd42ce38050af33905be19c" ], 0, - "d85a011e6d5cf1eb46da4f93ba630a9c" + "4d0f156e99c8a97a61d2f465482cf17e" ], [ "C.String.nonzero_is_lt", @@ -52,7 +52,7 @@ "typing_C.String.length" ], 0, - "726a65a2962047fe6da0d147ce63b1a0" + "1aa237d251a1218a386742452691615a" ], [ "C.String.memcpy", @@ -66,7 +66,7 @@ "typing_FStar.UInt8.t" ], 0, - "8649fe195a82254eac781a9d099bcbb1" + "5f0fd84967905fb36815cd68bf112c76" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.fst.hints b/krmllib/hints/C.fst.hints index 854d4ce1b..384bc6364 100644 --- a/krmllib/hints/C.fst.hints +++ b/krmllib/hints/C.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query", "assumption_C.HasEq_char" ], 0, - "ff3bfca9434b59a5c3ab257299c225ea" + "8249693316a6741ea63b1d746d07963a" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/FStar.Krml.Endianness.fst.hints b/krmllib/hints/FStar.Krml.Endianness.fst.hints index 46e15a425..ab011f655 100644 --- a/krmllib/hints/FStar.Krml.Endianness.fst.hints +++ b/krmllib/hints/FStar.Krml.Endianness.fst.hints @@ -32,7 +32,7 @@ "well-founded-ordering-on-nat" ], 0, - "9487c890b3ca43e08646f975f2d3c4f7" + "4f596f9a4a5abd737c7bc33edf4138f2" ], [ "FStar.Krml.Endianness.be_to_n", @@ -65,7 +65,7 @@ "well-founded-ordering-on-nat" ], 0, - "fb915361de65909dca9d3b5136a9ccee" + "58bf78783662634ed3bfde47cb6a92e7" ], [ "FStar.Krml.Endianness.lemma_euclidean_division", @@ -77,7 +77,7 @@ "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, - "efdb7570933c0be5ccb91834d8ec46eb" + "cebed2c5a674d008133e0af21dd10e7c" ], [ "FStar.Krml.Endianness.lemma_factorise", @@ -89,7 +89,7 @@ "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, - "a8a7450b7f59579e711329542be9f788" + "69242c28476487c75acc7eef71bc4403" ], [ "FStar.Krml.Endianness.lemma_le_to_n_is_bounded", @@ -106,7 +106,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "b7a1d1f18e25a29601c0b40196345342" + "5d56e79c06a647b00b55fec087adfd63" ], [ "FStar.Krml.Endianness.lemma_le_to_n_is_bounded", @@ -124,7 +124,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "efbd37260edb0e51ebc96996b4f4dadd" + "84f54e5bb7840bbac2a5fc52831cbad9" ], [ "FStar.Krml.Endianness.lemma_le_to_n_is_bounded", @@ -166,7 +166,7 @@ "typing_Prims.pow2", "well-founded-ordering-on-nat" ], 0, - "31b2837654141356437bf5974cf7a36c" + "b6715cdf3e558f6c2cae5b9d2985cd6b" ], [ "FStar.Krml.Endianness.lemma_be_to_n_is_bounded", @@ -183,7 +183,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "b5f8b8b58cb1bdae0619302e06782e4e" + "b843159640729242b01030fc7ef2e6eb" ], [ "FStar.Krml.Endianness.lemma_be_to_n_is_bounded", @@ -201,7 +201,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "27c595f4df4efaaf6fc5eea994d1700e" + "f1a33dc05c03c619542f556e08cafcfc" ], [ "FStar.Krml.Endianness.lemma_be_to_n_is_bounded", @@ -240,7 +240,7 @@ "typing_Prims.pow2", "well-founded-ordering-on-nat" ], 0, - "3d5a9b5e6c562c1c72d3277d8e8ec656" + "ff1ee36ac9245a9c66c9f1fb8560b353" ], [ "FStar.Krml.Endianness.n_to_le", @@ -259,7 +259,7 @@ "typing_FStar.UInt32.v" ], 0, - "57ab5428af2e7c2635356f8d82cc94c1" + "af79886651a874584874af3097ec40fe" ], [ "FStar.Krml.Endianness.n_to_le", @@ -278,7 +278,7 @@ "typing_FStar.UInt32.v" ], 0, - "83539df16cba341880b48d677d0eaf6a" + "083ed9d2b9ebc6a7a9224354b99dcaf5" ], [ "FStar.Krml.Endianness.n_to_le", @@ -341,7 +341,7 @@ "typing_FStar.UInt8.t", "well-founded-ordering-on-nat" ], 0, - "9ef4a6ac65c028da9a893f83e57046c7" + "63d0bf77935c263d5d6201d01fc46c61" ], [ "FStar.Krml.Endianness.n_to_be", @@ -360,7 +360,7 @@ "typing_FStar.UInt32.v" ], 0, - "9b8d2c6664495eeed25227957741129b" + "80a26a42ff448a2ae1e094cae35a329e" ], [ "FStar.Krml.Endianness.n_to_be", @@ -379,7 +379,7 @@ "typing_FStar.UInt32.v" ], 0, - "401933c1e13f0cc333679da7bd5f800f" + "b247ba662ef941100fb863cae1a83846" ], [ "FStar.Krml.Endianness.n_to_be", @@ -442,7 +442,7 @@ "well-founded-ordering-on-nat" ], 0, - "a596fe9d1b8c3e557048e7faacc155a0" + "d64bbfb8debc83baeed219ad50a9f3f0" ], [ "FStar.Krml.Endianness.n_to_le_inj", @@ -461,7 +461,7 @@ "typing_FStar.UInt32.v" ], 0, - "5a7996fe30dc6dc48fb98949a974c57a" + "baf53c40110cdbd93b6582a4898b1173" ], [ "FStar.Krml.Endianness.n_to_le_inj", @@ -483,7 +483,7 @@ "typing_FStar.Krml.Endianness.n_to_le", "typing_FStar.UInt32.v" ], 0, - "8ff6bf08179c7faf2254a0893b7c0bb0" + "b7e78d1e2729e99b1685f3dc8e297427" ], [ "FStar.Krml.Endianness.n_to_be_inj", @@ -502,7 +502,7 @@ "typing_FStar.UInt32.v" ], 0, - "77b81d18ac54e38f581721621af3649f" + "7dd352e6c223f3140491cae49ffa0c33" ], [ "FStar.Krml.Endianness.n_to_be_inj", @@ -524,7 +524,7 @@ "typing_FStar.Krml.Endianness.n_to_be", "typing_FStar.UInt32.v" ], 0, - "23cbd89c9033e3a32d1ed9c2ac6ce53a" + "0eca33ab77732546319db52ff5d4582f" ], [ "FStar.Krml.Endianness.be_to_n_inj", @@ -580,7 +580,7 @@ "well-founded-ordering-on-nat" ], 0, - "7f826df4d6c314331433418d8e41749b" + "40bbcd75eff49d1d9255e259c14f8032" ], [ "FStar.Krml.Endianness.le_to_n_inj", @@ -637,7 +637,7 @@ "typing_FStar.UInt8.v", "well-founded-ordering-on-nat" ], 0, - "0aacdc215f46b0432d0549d10ac70b3f" + "55af0a877f91cd1f59a55388cd0dd349" ], [ "FStar.Krml.Endianness.n_to_be_be_to_n", @@ -656,7 +656,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "316353bf0e11ee0b776643fa6a73c163" + "c7d99237079c219c471070909b6f77ad" ], [ "FStar.Krml.Endianness.n_to_le_le_to_n", @@ -675,7 +675,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "9b3fcc60d83eea62aa028dc1f5844bde" + "ce2b6a11f388b8b3e6d2f2af7bd29631" ], [ "FStar.Krml.Endianness.uint32_of_le", @@ -695,7 +695,7 @@ "refinement_interpretation_Tm_refine_073e087ab5f9fabfeddf43c4ff72a1d0" ], 0, - "ce9041e0583ece56f09a728a8a28f76c" + "a9d190b6700bf30ec72f246c46c7b013" ], [ "FStar.Krml.Endianness.le_of_uint32", @@ -712,7 +712,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "2ebe350f6bd06932480a36eb674f92d3" + "b963931adb8f745033122494562681da" ], [ "FStar.Krml.Endianness.uint32_of_be", @@ -732,7 +732,7 @@ "refinement_interpretation_Tm_refine_073e087ab5f9fabfeddf43c4ff72a1d0" ], 0, - "2548c537a4833b66f6847155c9ea67f4" + "d68ee9eadaefad9796d1dc62775850a4" ], [ "FStar.Krml.Endianness.be_of_uint32", @@ -749,7 +749,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "0bfb546b511c42ad4b9159cbeee8a47e" + "bf05837bc0390a442031a7d8adfae05d" ], [ "FStar.Krml.Endianness.uint64_of_le", @@ -769,7 +769,7 @@ "refinement_interpretation_Tm_refine_1cb22d5b190a69600ef23f524d7a6d8a" ], 0, - "1322f9cca49b4d3f27c9bde496c57f1f" + "1f0f5775ea60b8423922eef1b9022728" ], [ "FStar.Krml.Endianness.le_of_uint64", @@ -786,7 +786,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "6aa2835045c5066427e50161203d7360" + "a09112125bb5e88498ad46bbadd3f583" ], [ "FStar.Krml.Endianness.uint64_of_be", @@ -806,7 +806,7 @@ "refinement_interpretation_Tm_refine_1cb22d5b190a69600ef23f524d7a6d8a" ], 0, - "47b0be5089b3ada35722a6d7a75a1f49" + "2c02bb33937ad381070be9a67277e151" ], [ "FStar.Krml.Endianness.be_of_uint64", @@ -823,7 +823,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "f72fbeb942e55df21c0b2d02baf327d4" + "ded8c0f07ce6872187a21ba28a12b15d" ], [ "FStar.Krml.Endianness.seq_uint32_of_le", @@ -837,7 +837,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "0786fda0a2fe2afc6002e8f49047c9bb" + "95a61f5ad4cbfd71885e2d06a14f242d" ], [ "FStar.Krml.Endianness.seq_uint32_of_le", @@ -877,7 +877,7 @@ "well-founded-ordering-on-nat" ], 0, - "2481f9bfd4c36d06b3125df995286882" + "ec8b39b58b0e31bc441673909b2be588" ], [ "FStar.Krml.Endianness.le_of_seq_uint32", @@ -913,7 +913,7 @@ "well-founded-ordering-on-nat" ], 0, - "fd84e16b08964ac51eb13bece1b4f14e" + "db83ae7eb73628d15bbbb6beafdb5793" ], [ "FStar.Krml.Endianness.seq_uint32_of_be", @@ -927,7 +927,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "35f9714edd62aed5db7e8201574a0fa1" + "08aeca41a1b9fe61d1123f048d2928c9" ], [ "FStar.Krml.Endianness.seq_uint32_of_be", @@ -967,7 +967,7 @@ "well-founded-ordering-on-nat" ], 0, - "bbb82f87df65a13df35065416ae13b2d" + "6afef9327ba8509710b1a2ad0b798250" ], [ "FStar.Krml.Endianness.be_of_seq_uint32", @@ -1003,7 +1003,7 @@ "well-founded-ordering-on-nat" ], 0, - "6a137ad8f7c680bac337da182c226095" + "29c8511b3a8ab7eb57826872722b5115" ], [ "FStar.Krml.Endianness.seq_uint64_of_le", @@ -1017,7 +1017,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "fb612a5866d92492c5931eb4d35a652a" + "d6ef873fbc4fb3e09cbabb707dfa1c4c" ], [ "FStar.Krml.Endianness.seq_uint64_of_le", @@ -1057,7 +1057,7 @@ "well-founded-ordering-on-nat" ], 0, - "5819df8f97b95ae3068d93099ebecb9e" + "4cb64bc3540a97cdd0cbe8435e9a9578" ], [ "FStar.Krml.Endianness.le_of_seq_uint64", @@ -1093,7 +1093,7 @@ "well-founded-ordering-on-nat" ], 0, - "ba32834824fa4c2a23714e10e7018130" + "dbedc39b2c6379149e9238308541e30e" ], [ "FStar.Krml.Endianness.seq_uint64_of_be", @@ -1107,7 +1107,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "3c2ef1036c9ee4f74fa0c656e5c0ac38" + "726ccbfa555f1a6af09fad5e1f9af895" ], [ "FStar.Krml.Endianness.seq_uint64_of_be", @@ -1147,7 +1147,7 @@ "well-founded-ordering-on-nat" ], 0, - "a5e9234268c2b12292d79c2d53c3d688" + "58171d994d19349467b947ae58eeb3c8" ], [ "FStar.Krml.Endianness.be_of_seq_uint64", @@ -1183,7 +1183,7 @@ "well-founded-ordering-on-nat" ], 0, - "fab3712f022a83569125d13b9ceb1d13" + "2bdd3e1d9a9b8f411d42dd359a7314e9" ], [ "FStar.Krml.Endianness.offset_uint32_be", @@ -1209,7 +1209,7 @@ "typing_FStar.UInt8.t" ], 0, - "ebb70833c3a5db252c2740c8698867a4" + "6fa9cd2a66acb51e3075400f190ad6d1" ], [ "FStar.Krml.Endianness.offset_uint32_be", @@ -1278,7 +1278,7 @@ "well-founded-ordering-on-nat" ], 0, - "d062b5c2f4a0090eab223662d305b7d2" + "1b0fc99e1a0a50ca531d44c0ff5b0de8" ], [ "FStar.Krml.Endianness.offset_uint32_le", @@ -1304,7 +1304,7 @@ "typing_FStar.UInt8.t" ], 0, - "b402c40c4bceba6242ef17c4db272263" + "68f6cb448e018eeb6e7c8012ab06498a" ], [ "FStar.Krml.Endianness.offset_uint32_le", @@ -1371,7 +1371,7 @@ "well-founded-ordering-on-nat" ], 0, - "4fec4f51b58688b9d648a2af8d6bd702" + "01bfbb259a432971f7ade579074b71fe" ], [ "FStar.Krml.Endianness.offset_uint64_be", @@ -1397,7 +1397,7 @@ "typing_FStar.UInt8.t" ], 0, - "f14b760b47d182d546a74cc6e29a4a6e" + "7bcc2a518053dd7a2d295bd566513314" ], [ "FStar.Krml.Endianness.offset_uint64_be", @@ -1466,7 +1466,7 @@ "well-founded-ordering-on-nat" ], 0, - "317cb6d14d20d4afb5a0eb3f19ca337c" + "3d2bc90cb618243149501b939e2e40b7" ], [ "FStar.Krml.Endianness.offset_uint64_le", @@ -1492,7 +1492,7 @@ "typing_FStar.UInt8.t" ], 0, - "07f264ac902e1e5880bdfcb46c2f742c" + "a9b885bb8bdbb22134242588e589d864" ], [ "FStar.Krml.Endianness.offset_uint64_le", @@ -1564,7 +1564,7 @@ "well-founded-ordering-on-nat" ], 0, - "3d1afbd2f5a77f4b9f31bb638d6c616d" + "693688d22a7b901f2e95f5afc1f038cc" ], [ "FStar.Krml.Endianness.tail_cons", @@ -1598,7 +1598,7 @@ "typing_FStar.Seq.Properties.tail" ], 0, - "ca6d5c52034d1a17bd59a9388e395ac0" + "328213b7c96b95ffc3432a7d9b5cb37a" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_append", @@ -1672,7 +1672,7 @@ "well-founded-ordering-on-nat" ], 0, - "ad685be330361e4008fd0d79c9d5d5ec" + "5aa49bb19189ef51bebad9b9530054a6" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_base", @@ -1728,7 +1728,7 @@ "typing_FStar.UInt8.t" ], 0, - "79a1fba4868f34cccf2c3274e5056c69" + "27e6b04e0881a17e1e1efde9dbe64ad0" ], [ "FStar.Krml.Endianness.le_of_seq_uint32_append", @@ -1791,7 +1791,7 @@ "typing_FStar.UInt8.t", "well-founded-ordering-on-nat" ], 0, - "ac6d29616e17f08c19eeb3f056208f7c" + "18d32bac571eb3c8027b02972fbc3dac" ], [ "FStar.Krml.Endianness.le_of_seq_uint32_base", @@ -1847,7 +1847,7 @@ "typing_FStar.UInt8.t" ], 0, - "be66ca40f8e9b15ba33d1b40a49d7afa" + "129a39961db0f649bca7f0e0f069210c" ], [ "FStar.Krml.Endianness.be_of_seq_uint64_append", @@ -1928,7 +1928,7 @@ "well-founded-ordering-on-nat" ], 0, - "54e4f7cf34a1f07e687179b5452ffc73" + "4e58c8267b9660de3f239749346c8982" ], [ "FStar.Krml.Endianness.be_of_seq_uint64_base", @@ -1986,7 +1986,7 @@ "typing_FStar.UInt8.t", "typing_Prims.pow2" ], 0, - "e4e849b8a91405b243e79e8ab546b35c" + "de4a07c73a87b4f9027441ad76b8ea4f" ], [ "FStar.Krml.Endianness.seq_uint32_of_be_be_of_seq_uint32", @@ -1998,7 +1998,7 @@ "refinement_interpretation_Tm_refine_a84773c2eb377e624aba800b71ec3ba0" ], 0, - "c7166137c071058ee6879aa8fea5191b" + "78ad1fec9dff332b28654dd5bc56bb57" ], [ "FStar.Krml.Endianness.seq_uint32_of_be_be_of_seq_uint32", @@ -2074,7 +2074,7 @@ "typing_FStar.UInt8.t", "well-founded-ordering-on-nat" ], 0, - "c1fb0002ef14f3c8044daf93082f5096" + "b2f6f9d632420655fb2e14828c38f8d2" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_seq_uint32_of_be", @@ -2086,7 +2086,7 @@ "refinement_interpretation_Tm_refine_4239cb7a019da00e7afc3bc55aa05dd7" ], 0, - "c8a5188ecfe8d29081d0403ff022cdd9" + "6d77d0868b789d4a7eade0e46bdcd4a2" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_seq_uint32_of_be", @@ -2164,7 +2164,7 @@ "typing_FStar.UInt8.v", "well-founded-ordering-on-nat" ], 0, - "5a8e932b101540c4cddd8e2695ee5769" + "81c2664786e0d5cbbc43dc403c1fb8a7" ], [ "FStar.Krml.Endianness.slice_seq_uint32_of_be", @@ -2214,7 +2214,7 @@ "typing_FStar.UInt32.t", "typing_FStar.UInt8.t" ], 0, - "0ed2f5ee0527f7cb66330b9da0f90252" + "c7c8e2b940510a568106f96fa8197e07" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_slice", @@ -2266,7 +2266,7 @@ "typing_FStar.UInt8.t" ], 0, - "d4517c1b24533f6bcb445fff67314019" + "f1715a0488c93965bf08e4814d622fbc" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/LowStar.Lib.AssocList.fst.hints b/krmllib/hints/LowStar.Lib.AssocList.fst.hints index 0b13acae4..7fe6c5057 100644 --- a/krmllib/hints/LowStar.Lib.AssocList.fst.hints +++ b/krmllib/hints/LowStar.Lib.AssocList.fst.hints @@ -8,7 +8,7 @@ 0, [ "@query", "equation_LowStar.Lib.AssocList.invariant" ], 0, - "2b83f653b770e276b654cea07bda6e53" + "221b5e043140dc09f56be90b961f9c05" ], [ "LowStar.Lib.AssocList.frame", @@ -73,7 +73,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "4df08b6b5132a3a669c3de9ff8c1e8a8" + "027801cbe29717894da84f2ccb81cbba" ], [ "LowStar.Lib.AssocList.footprint_in_r", @@ -86,7 +86,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "07e9a74c802234ad303669e51dc9a65f" + "0461e6099be945958d02ca68b1f166bd" ], [ "LowStar.Lib.AssocList.footprint_in_r", @@ -102,7 +102,7 @@ "fuel_guarded_inversion_LowStar.Lib.LinkedList2.t" ], 0, - "76aed2631922f18844be34b7a5aea391" + "bdcfdc8074bba66752ea5bbb09cbebfc" ], [ "LowStar.Lib.AssocList.create_in", @@ -136,7 +136,7 @@ "typing_Tm_abs_05dbb0bdbe4a61cef8fed1432b1b98e9" ], 0, - "7b171321838b69f733ea8aca1eee5009" + "5183a8366258672a385f9938b5a01fe9" ], [ "LowStar.Lib.AssocList.find_", @@ -145,7 +145,7 @@ 0, [ "@query" ], 0, - "f5d04f655d4db4cecb316462c4c9e4e8" + "1d3c03afc09efb19bf2457602fb3036b" ], [ "LowStar.Lib.AssocList.find_", @@ -230,7 +230,7 @@ "typing_Tm_abs_05dbb0bdbe4a61cef8fed1432b1b98e9" ], 0, - "0082e1e3dd246369ce963159493564de" + "1c671aa1c38df6642f38fb1aac2cec22" ], [ "LowStar.Lib.AssocList.find", @@ -248,7 +248,7 @@ "refinement_interpretation_Tm_refine_b582da5b18980dd549f83acfd27b47df" ], 0, - "0f7e2983a4bb8c679760a4cd82dd29f7" + "1f68bc110932c91070bcf4ff9d29e7ed" ], [ "LowStar.Lib.AssocList.add", @@ -344,7 +344,7 @@ "typing_Tm_abs_05dbb0bdbe4a61cef8fed1432b1b98e9" ], 0, - "9116345577fe2dcc2ba0f2efd10fb399" + "b30626d538e8703bfc4b0a85e1d6689d" ], [ "LowStar.Lib.AssocList.remove_all_", @@ -356,7 +356,7 @@ "refinement_interpretation_Tm_refine_666cbc765faa85ecb6368ba0ccf434cd" ], 0, - "2a7154c425fe1f31022db823e7799108" + "b2778da8376e68932274f8873f1e0ca8" ], [ "LowStar.Lib.AssocList.remove_all_", @@ -485,7 +485,7 @@ "typing_Tm_abs_05dbb0bdbe4a61cef8fed1432b1b98e9" ], 0, - "9cec48acd508a80211b5fe10cba199ee" + "3f3c48b67bd1ad5cc6a3e9572149bbd2" ], [ "LowStar.Lib.AssocList.remove_all", @@ -597,7 +597,7 @@ "typing_LowStar.Monotonic.Buffer.loc_regions" ], 0, - "35ceb85f067ecb4a7b52725fc135559d" + "b73c1f71320c6da7dac718ef221254ae" ], [ "LowStar.Lib.AssocList.clear", @@ -756,7 +756,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "b5488e6c7a9736a1d678f0d5bebfcd90" + "4f93676269a5a9b863bdd734a641db42" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/LowStar.Lib.LinkedList.fst.hints b/krmllib/hints/LowStar.Lib.LinkedList.fst.hints index 77a1a4288..c602c23c0 100644 --- a/krmllib/hints/LowStar.Lib.LinkedList.fst.hints +++ b/krmllib/hints/LowStar.Lib.LinkedList.fst.hints @@ -14,7 +14,7 @@ "projection_inverse_BoxInt_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "b15ff47acfd3c6265544c90d1f23bb40" + "67422fe23e3ea4d3f40825a6a361c874" ], [ "LowStar.Lib.LinkedList.cells", @@ -50,7 +50,7 @@ "typing_LowStar.Monotonic.Buffer.g_is_null" ], 0, - "03cdaed52a946a72c228209903596d6d" + "50ff86a57feff2ae8eac3f51506f0696" ], [ "LowStar.Lib.LinkedList.same_cells_same_pointer", @@ -86,7 +86,7 @@ "unit_typing" ], 0, - "66f9b5eb0f63d5da7f11a486961cf2b6" + "f81f24456a3d67b353874f25bed6b172" ], [ "LowStar.Lib.LinkedList.footprint", @@ -118,7 +118,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "ed5d73941c2a3f97e9c675b3f9ed0409" + "44f19b6eaecd909058163aaeaceafa3a" ], [ "LowStar.Lib.LinkedList.cells_pairwise_disjoint", @@ -152,7 +152,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "5446dea9f9d6e4ee8b89ab3b6c67de81" + "121bbeebac2ac42adff07a35d24b36b5" ], [ "LowStar.Lib.LinkedList.cells_live_freeable", @@ -186,7 +186,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "bed23b102e2fccd224f2e74981bab981" + "6c7fb0c0f597b4da484fe7741ea48075" ], [ "LowStar.Lib.LinkedList.invariant", @@ -195,7 +195,7 @@ 1, [ "@query", "equation_Prims.logical" ], 0, - "71ab784aa0a9ba26f4fe857002ce970f" + "1caa4ad52e040ede0b2122e466851ea3" ], [ "LowStar.Lib.LinkedList.invariant_loc_in_footprint", @@ -209,7 +209,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "d93121d7dab9aff36049a430c08a446a" + "e61e193e49719f40bb8dffc8d65468ff" ], [ "LowStar.Lib.LinkedList.invariant_loc_in_footprint", @@ -273,7 +273,7 @@ "typing_LowStar.Monotonic.Buffer.loc_not_unused_in" ], 0, - "d06cd696bc1848644709e1dd463bf4a8" + "044eadf108714b5da0187ea052dff5d4" ], [ "LowStar.Lib.LinkedList.frame", @@ -285,7 +285,7 @@ "refinement_interpretation_Tm_refine_9dfd5ec664d04b1adbe6909975d3119f" ], 0, - "f6f34c623f8c99346a6e68d6c4bde6a5" + "97c8a78f8d92550b26921d6ff94f9680" ], [ "LowStar.Lib.LinkedList.frame", @@ -376,7 +376,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "8b9d121f3e851e57c68585b8cde96f72" + "6da27430a01975804b27c2064a3e22d7" ], [ "LowStar.Lib.LinkedList.length_functional", @@ -418,7 +418,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "fe4f64b40c6fe20401ea9ce91a56b10e" + "5e3f8cfa43f10510051d8e1e3d47222b" ], [ "LowStar.Lib.LinkedList.gmap", @@ -433,7 +433,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "cd4e75b1c026ac5fa84d2c65dfce3add" + "db9dc55ac82c88c472398f35478bebdc" ], [ "LowStar.Lib.LinkedList.gfold_right", @@ -448,7 +448,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "279b8aee83aeb4f22c2b97a1f83ceec4" + "c1c9ece52facf52bc89a2cc32e2644fd" ], [ "LowStar.Lib.LinkedList.deref_cells_is_v", @@ -460,7 +460,7 @@ "refinement_interpretation_Tm_refine_2cdb1d22d11cea5954bcab0f89d645ec" ], 0, - "522bbcde40354e3a29a5a1d2ecc0b7aa" + "8085fc5caef1add6da354f0528c9c70b" ], [ "LowStar.Lib.LinkedList.deref_cells_is_v", @@ -524,7 +524,7 @@ "typing_LowStar.Lib.LinkedList.cells" ], 0, - "b1a2d01a62d220d5c28aa1d13360eff3" + "43a5f09f5080800f9c790d10e272d61e" ], [ "LowStar.Lib.LinkedList.footprint_via_cells_is_footprint", @@ -541,7 +541,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "1972ba459ceb31635a13405142cec141" + "03813b040b59a832c4c67dea518f64e7" ], [ "LowStar.Lib.LinkedList.footprint_via_cells_is_footprint", @@ -629,7 +629,7 @@ "typing_Tm_abs_3d46d953d7df849c026fcef6c4941216" ], 0, - "14f2defc7f7b4d782f64406047b7754d" + "256e59c36e795c9fa25f6b215c80a811" ], [ "LowStar.Lib.LinkedList.push", @@ -641,7 +641,7 @@ "refinement_interpretation_Tm_refine_2e3312cd41d7f5efbbbae3b2eeef697e" ], 0, - "c37d4f0e87dc91b4f03d84eec0afd775" + "af2b399d5ee46521e51d21eb28ac33d3" ], [ "LowStar.Lib.LinkedList.push", @@ -773,7 +773,7 @@ "typing_LowStar.Monotonic.Buffer.loc_unused_in" ], 0, - "ec9a851ac86c907acf0e4c942717db85" + "25c59d99c04b067390af6837059f1806" ], [ "LowStar.Lib.LinkedList.pop", @@ -804,7 +804,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "612dced94545c3644c518480e00eefb9" + "3137ea12c5ec897a8894db1b6e542642" ], [ "LowStar.Lib.LinkedList.pop", @@ -913,7 +913,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "48cfe2dec8357c04379836ea97f6b5a7" + "904b0b0863fdc88d62ebc0bd1679c58a" ], [ "LowStar.Lib.LinkedList.free_", @@ -925,7 +925,7 @@ "refinement_interpretation_Tm_refine_994dd8cb51034b7a0776f9bb28ca6f71" ], 0, - "98aeb8d2b1ea43ba5413de3d570d599f" + "7c0c0e311ab1f4c0cc2073db47122b99" ], [ "LowStar.Lib.LinkedList.free_", @@ -1015,7 +1015,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "841c4ee6d1320429b8644617d326d86a" + "8c91fbda38d0f607cd87f59385483afa" ], [ "LowStar.Lib.LinkedList.free", @@ -1027,7 +1027,7 @@ "refinement_interpretation_Tm_refine_baa6a0434e5b51218cc000deadc8f6bc" ], 0, - "ba4f4da8ef8ced4a0c774b6d37a353db" + "69b61508e2b722e14c765c7c3ffce64b" ], [ "LowStar.Lib.LinkedList.free", @@ -1114,7 +1114,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "1890f0686c489dc0d4bece5060c19467" + "e0ed09d4712f98651f8a2157806ec72d" ], [ "LowStar.Lib.LinkedList.length", @@ -1123,7 +1123,7 @@ 1, [ "@query" ], 0, - "278cd765a8e3c2a64947e24dbd94c23f" + "ff41d2046ce3d575569c2c0e46159a1a" ], [ "LowStar.Lib.LinkedList.length", @@ -1188,7 +1188,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "71602491f93d0c92bd314bc5c64812b2" + "83035071641b084dc7e3fa7ed8a4f20c" ], [ "LowStar.Lib.LinkedList.test", @@ -1325,7 +1325,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "52d4ef7721059c9edcf5a15416b8695a" + "d7c4482dcd2b6a3efdee5df18010a39b" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/LowStar.Lib.LinkedList2.fst.hints b/krmllib/hints/LowStar.Lib.LinkedList2.fst.hints index 391783ce3..b9a4c9702 100644 --- a/krmllib/hints/LowStar.Lib.LinkedList2.fst.hints +++ b/krmllib/hints/LowStar.Lib.LinkedList2.fst.hints @@ -17,7 +17,7 @@ "typing_LowStar.Lib.LinkedList2.__proj__Mkt__item__r" ], 0, - "a17da5c8a6505ff9861f953bbe50447d" + "dd2b19b132b3bc9c650b3bd86a927c75" ], [ "LowStar.Lib.LinkedList2.footprint", @@ -29,7 +29,7 @@ "l_and-interp" ], 0, - "944e238cc51e1416e6bd0893396dba1c" + "17a739ba8b9ecb4100b11c30fbcfdeaf" ], [ "LowStar.Lib.LinkedList2.cells", @@ -41,7 +41,7 @@ "l_and-interp" ], 0, - "a9595960c4bf78a1bd00e0d44a901952" + "e93a8fec7d5a1809c75ae0a2990d6b70" ], [ "LowStar.Lib.LinkedList2.footprint_in_r", @@ -111,7 +111,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "e9d96803b2cca4f7277ae65a6dbaffad" + "ea30f45fef7e71ffbafe1b998fb793ba" ], [ "LowStar.Lib.LinkedList2.frame_footprint", @@ -123,7 +123,7 @@ "refinement_interpretation_Tm_refine_09ad67b9d90ed7b17ddf31c45c68b636" ], 0, - "b4467a7132557d60a44899ec23e3e7ed" + "2d8c49273756105d1dfbb8a6e7044ecf" ], [ "LowStar.Lib.LinkedList2.frame_footprint", @@ -181,7 +181,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "18b961ebf68d9760245f327b53e639d0" + "454c5cb797a2eef89a9b3796e06ed730" ], [ "LowStar.Lib.LinkedList2.frame_region", @@ -193,7 +193,7 @@ "refinement_interpretation_Tm_refine_76a8d76aec5fe95490cf6c28517bab40" ], 0, - "81f28f5b8cf7ec1be7a49a6979f655d4" + "92a2c1fefaa46189959d7c8a59fd5a02" ], [ "LowStar.Lib.LinkedList2.frame_region", @@ -253,7 +253,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "74a2e6a43c34007be9c059ab59d72bbd" + "114c025e3fc7b9de7eaab18b5fec5120" ], [ "LowStar.Lib.LinkedList2.create_in", @@ -262,7 +262,7 @@ 0, [ "@query" ], 0, - "9ae5d7df0d5935914174b978b2c4b57c" + "3af83ff693e1fb005de2f7886969689a" ], [ "LowStar.Lib.LinkedList2.create_in", @@ -392,7 +392,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "a40c8b7a8b8057bb4aea7f8e6e1ca19a" + "aff6531e7b00402d6a30c1d5fb930cd8" ], [ "LowStar.Lib.LinkedList2.push", @@ -404,7 +404,7 @@ "refinement_interpretation_Tm_refine_89e26769e50512fd6a99e61c0fe00f0a" ], 0, - "7f148391906cb7815604380cf8dccbac" + "c7e66d1ecc349833eb90274e7c18be81" ], [ "LowStar.Lib.LinkedList2.push", @@ -521,7 +521,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "df076ccd2c7cb22a1e314d8fd0c59c26" + "ee46972b869dcc04914b4787e73bbd90" ], [ "LowStar.Lib.LinkedList2.pop", @@ -567,7 +567,7 @@ "typing_LowStar.Monotonic.Buffer.get" ], 0, - "f4ec994209421dbad312dd6782ae58b3" + "ecd5496d6880a68b5e83b79dad3d5725" ], [ "LowStar.Lib.LinkedList2.pop", @@ -689,7 +689,7 @@ "typing_Prims.uu___is_Cons" ], 0, - "3a422bce1963b66aaef54de3bb527b17" + "6ebb75ce9d92de9aab7a41395ae0c1f3" ], [ "LowStar.Lib.LinkedList2.maybe_pop", @@ -738,7 +738,7 @@ "typing_LowStar.Monotonic.Buffer.get" ], 0, - "f595e03610b5a64938bdf3eb8d409988" + "6f3b73812af905200cddc4aa19d16c53" ], [ "LowStar.Lib.LinkedList2.maybe_pop", @@ -883,7 +883,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "789096a930b290ac23c40c910e9364d4" + "167c7f3f819f9343aa775a073dbe6435" ], [ "LowStar.Lib.LinkedList2.clear", @@ -895,7 +895,7 @@ "refinement_interpretation_Tm_refine_89e26769e50512fd6a99e61c0fe00f0a" ], 0, - "248c89d5612eea54aff35bcb7e93ed49" + "1b2573cdb3a961dd5593bd3e558b4106" ], [ "LowStar.Lib.LinkedList2.clear", @@ -1005,7 +1005,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "a438e9fcb7dc496a0f91e4463e7f9a3c" + "5b168c4d470d3d77adc006651965c3f3" ], [ "LowStar.Lib.LinkedList2.free", @@ -1017,7 +1017,7 @@ "refinement_interpretation_Tm_refine_89e26769e50512fd6a99e61c0fe00f0a" ], 0, - "52fbd70a77718ec5874b9239a2c795c3" + "dbf492a4a8006f2d7f1ab5d4d59637ff" ], [ "LowStar.Lib.LinkedList2.free", @@ -1096,7 +1096,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "10959208fefc361e50fc78d0d5180d4d" + "4e2d8ea0c15296e777821c4a3c5878ab" ], [ "LowStar.Lib.LinkedList2.test", @@ -1232,7 +1232,7 @@ "typing_LowStar.Monotonic.Buffer.loc_unused_in" ], 0, - "256d8bf554049eda1fdf480b533dddca" + "d4646103d4e0a57b6577d6a65e87e439" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/Spec.Loops.fst.hints b/krmllib/hints/Spec.Loops.fst.hints index 5bed6f6fd..e254edba0 100644 --- a/krmllib/hints/Spec.Loops.fst.hints +++ b/krmllib/hints/Spec.Loops.fst.hints @@ -13,7 +13,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "b96617de2fd7ff3bf2b5a9572db8efd7" + "dfb8047f9a7e6b818a502f8947f3d47b" ], [ "Spec.Loops.seq_map", @@ -27,7 +27,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "7a12f7cc7fc0e9dc2a38091a2db80ec9" + "382adef578332fcf5b0e260f8722353b" ], [ "Spec.Loops.seq_map", @@ -73,7 +73,7 @@ "well-founded-ordering-on-nat" ], 0, - "8a0da2b4b85baec88511e11d739b68e2" + "391e25ba07bc1242b5422db63da4e2c1" ], [ "Spec.Loops.seq_map2", @@ -88,7 +88,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "b81c79cb5f2159118e79641fbaa8f73f" + "7f05b6d7f123c4a9f433d055ea419e13" ], [ "Spec.Loops.seq_map2", @@ -103,7 +103,7 @@ "refinement_interpretation_Tm_refine_aab03343de950d77c26ad9d98d2757b8" ], 0, - "5254398efd8d02c97e278b99f3601d76" + "a9629b7a62878576d73c95e33a4ae964" ], [ "Spec.Loops.seq_map2", @@ -152,7 +152,7 @@ "well-founded-ordering-on-nat" ], 0, - "6ae259bb12462beb56e31062b9b0ee69" + "cfbacb837b077e4436321806ebce068f" ], [ "Spec.Loops.repeat", @@ -169,7 +169,7 @@ "well-founded-ordering-on-nat" ], 0, - "c6d6d50ba17c73cc0ae5ef398fe18775" + "ed9d18b809d78ac61302733e0a880b29" ], [ "Spec.Loops.repeat_induction", @@ -182,7 +182,7 @@ "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001" ], 0, - "9fe0712d8d421ae43d4dbf4bef5e566f" + "a02c289c29b4fec84664a84d53a7a875" ], [ "Spec.Loops.repeat_induction", @@ -195,7 +195,7 @@ "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001" ], 0, - "01179a8d0f9c9a4e4ad09ef56adf8363" + "efff26a2cfd161aedf97d0424fc0ab69" ], [ "Spec.Loops.repeat_induction", @@ -224,7 +224,7 @@ "typing_Spec.Loops.repeat", "well-founded-ordering-on-nat" ], 0, - "73ee08e513c9138a10b16ebc56fa666a" + "c4a169637ab37bfce9f35dbe57eddb08" ], [ "Spec.Loops.repeat_base", @@ -247,7 +247,7 @@ "refinement_interpretation_Tm_refine_f52d524f7d227b5c40129c018d34fe1d" ], 0, - "32e87d16e4956be2c1a7985dd9048ab5" + "9f440aca4ff7ab23a7c51516628000bc" ], [ "Spec.Loops.repeat_range", @@ -273,7 +273,7 @@ "well-founded-ordering-on-nat" ], 0, - "fa1863204ec1bf90ff79eb18e420fa52" + "0e2710fe087ebdc54b3b52e1ebea6b94" ], [ "Spec.Loops.repeat_range_base", @@ -282,7 +282,7 @@ 1, [ "@query" ], 0, - "a6b41c6c5a140c353fb60946da76b886" + "8c44110b3a9c4c37a8744260fd473a63" ], [ "Spec.Loops.repeat_range_base", @@ -299,7 +299,7 @@ "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913" ], 0, - "9021c4f9d2e704dcabc83ade9d1e8b6a" + "3ef212600a687c98827cc2ece2a511a0" ], [ "Spec.Loops.repeat_range_induction", @@ -314,7 +314,7 @@ "refinement_interpretation_Tm_refine_8233d76b57e95451540fc312b717fa79" ], 0, - "0e8c2758aa7e4f878fe512db0b24dad5" + "ead7c3bc6d4b153e00f2aa0d20fccec1" ], [ "Spec.Loops.repeat_range_induction", @@ -329,7 +329,7 @@ "refinement_interpretation_Tm_refine_8233d76b57e95451540fc312b717fa79" ], 0, - "04362e9d278bd477b41e5d61d9bf140b" + "eb842adc6559b1a0ad22e2dcb1f02f5b" ], [ "Spec.Loops.repeat_range_induction", @@ -363,7 +363,7 @@ "typing_Spec.Loops.repeat_range", "well-founded-ordering-on-nat" ], 0, - "f139fc5ef4724a143d7517f8c30fca29" + "3e5e915c4874952f6074fc85bee7d292" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/TestLib.fsti.hints b/krmllib/hints/TestLib.fsti.hints index 99d8de58c..75c0f2b2e 100644 --- a/krmllib/hints/TestLib.fsti.hints +++ b/krmllib/hints/TestLib.fsti.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "9bbbfcfb8adc8cf75ff598e59404eddc" + "c29c023682d5e97ec74e87144b30404e" ], [ "TestLib.unsafe_malloc", @@ -17,7 +17,7 @@ 1, [ "@query" ], 0, - "d7a532c7c3f4b317399d833210ad3214" + "92fc635dcc5c9b478d1e33dd53c8e6dc" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/WasmSupport.fst.hints b/krmllib/hints/WasmSupport.fst.hints index 4cedfed20..fe48666d1 100644 --- a/krmllib/hints/WasmSupport.fst.hints +++ b/krmllib/hints/WasmSupport.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "020cb44a8dd2365456452a40fefd27df" + "c965ac2b57fca60a012b8d497a95a21a" ], [ "WasmSupport.betole64", @@ -29,7 +29,7 @@ 1, [ "@query" ], 0, - "f7246ebd0e97310c8aece52422692970" + "c1ee7e257784a8098ebba6c4cc47bcb0" ], [ "WasmSupport.memzero", @@ -63,7 +63,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "83986fc336e8be4e1e1aefa01f58f175" + "4ef5cbf49f3dd42d4b558022ee3048a5" ] ] ] \ No newline at end of file diff --git a/src/AstToCFlat.ml b/src/AstToCFlat.ml index 9dd519ce8..f29fcfa15 100644 --- a/src/AstToCFlat.ml +++ b/src/AstToCFlat.ml @@ -373,7 +373,7 @@ let extend (env: env) (binder: binder) (locals: locals): locals * var * env = size_of env binder.typ :: locals, v, { env with - binders = List.length locals :: env.binders; + binders = v :: env.binders; } (** Find a variable in the environment. *) @@ -899,32 +899,57 @@ and mk_expr (env: env) (locals: locals) (e: expr): locals * CF.expr = (* See digression for [dup32] in CFlatToWasm *) let scratch_locals = - [ I64; I64; I32; I32 ] + [ I64; I64; I32; I32; I32 ] let msg_i64 = format_of_string "Abort: %s was meant to be hand-written and \ provided at link-time, but contains an I64 and therefore cannot be called from \ WASM." -let mk_decl env (d: decl): env * CF.decl option = +let mk_wrapper orig_name n_args locals = + let name = orig_name ^ "_packed" in + (* KPrint.bprintf "%s: %d locals, %d args\n" name (List.length locals) n_args; *) + let ret = [ I32; I32 ] in + let locals = List.rev locals in + let args, locals = KList.split n_args locals in + let body = + CF.CastI64ToPacked ( + CF.CallFunc (orig_name, KList.make (List.length args) (fun i -> CF.Var i)) + ) + in + CF.(Function { name; args; ret; locals; body; public = true }) + +let mk_decl env (d: decl): env * CF.decl list = match d with | DFunction (_, flags, n, ret, name, args, body) -> assert (n = 0); - let public = not (List.exists ((=) Common.Private) flags) in + let public = not (List.mem Common.Private flags) in let locals, env = List.fold_left (fun (locals, env) b -> let locals, _, env = extend env b locals in locals, env ) ([], env) args in let locals = List.rev_append scratch_locals locals in + let name = GlobalNames.to_c_name env.names name in + + (* Interlude: generate a wrapper, possibly *) + let wrapper () = mk_wrapper name (List.length args) locals in + let locals, body = mk_expr env locals body in let ret = [ size_of env ret ] in let locals = List.rev locals in let args, locals = KList.split (List.length args) locals in - let name = GlobalNames.to_c_name env.names name in - env, Some CF.(Function { name; args; ret; locals; body; public }) + let wrapper = + if public && ret = [ I64 ] && not (List.mem Common.Internal flags) then + [ wrapper () ] + else + [] + in + env, [ + CF.(Function { name; args; ret; locals; body; public }) + ] @ wrapper | DType _ -> (* Not translating type declarations. *) - env, None + env, [] | DGlobal (flags, name, n, typ, body) -> assert (n = 0); @@ -936,11 +961,13 @@ let mk_decl env (d: decl): env * CF.decl option = in if size = I64 then begin Warn.(maybe_fatal_error ("", NotWasmCompatible (name, "I64 constant"))); - env, None + env, [] end else let env, body, post_init = mk_global env name body in let name = GlobalNames.to_c_name env.names name in - env, Some (CF.Global (name, size, body, post_init, public)) + env, [ + CF.Global (name, size, body, post_init, public) + ] | DExternal (_, _, lid, t, _) -> let name = GlobalNames.to_c_name env.names lid in @@ -953,14 +980,19 @@ let mk_decl env (d: decl): env * CF.decl option = Warn.(maybe_fatal_error ("", NotWasmCompatible (lid, "functions \ implemented natively in JS (because they're assumed) cannot take or \ return I64"))); - env, Some CF.(Function { name; args; ret; locals = scratch_locals; - body = CF.Abort (CF.StringLiteral (Printf.sprintf msg_i64 name)); - public = true - }) + env, [ + CF.(Function { name; args; ret; locals = scratch_locals; + body = CF.Abort (CF.StringLiteral (Printf.sprintf msg_i64 name)); + public = true + })] end else - env, Some (CF.ExternalFunction (name, args, ret)) + env, [ + CF.ExternalFunction (name, args, ret) + ] | _ -> - env, Some (CF.ExternalGlobal (name, size_of env t)) + env, [ + CF.ExternalGlobal (name, size_of env t) + ] (* Definitions to be skipped because they have a built-in compilation scheme. *) let skip (lid: lident) = @@ -975,9 +1007,7 @@ let mk_module env decls = else begin flush stdout; flush stderr; let env, d = mk_decl env d in - match d with - | None -> env, decls - | Some d -> env, d :: decls + env, List.rev_append d decls end with e -> flush stdout; diff --git a/src/CFlat.ml b/src/CFlat.ml index 5f8b515e2..e79e27eb8 100644 --- a/src/CFlat.ml +++ b/src/CFlat.ml @@ -135,6 +135,7 @@ and expr = | CallFunc of ident * expr list | Cast of expr * width * width (** from; to *) + | CastI64ToPacked of expr and var = int (** NOT De Bruijn *) diff --git a/src/CFlatToWasm.ml b/src/CFlatToWasm.ml index d752d7a4c..a96ac2d9b 100644 --- a/src/CFlatToWasm.ml +++ b/src/CFlatToWasm.ml @@ -31,6 +31,8 @@ let mk_type = function | I64 -> W.Types.I64Type +let mk_value_type t = W.Types.NumType (mk_type t) + (******************************************************************************) (* Initial imports for all modules *) (******************************************************************************) @@ -43,7 +45,7 @@ module Base = struct module_name = name_of_string "Karamel"; item_name = name_of_string "data_start"; idesc = dummy_phrase (GlobalImport W.Types.( - GlobalType (mk_type I32, Immutable)))}) + GlobalType (mk_value_type I32, Immutable)))}) let memory = let mtype = W.Types.MemoryType W.Types.({ min = 16l; max = None }) in @@ -261,9 +263,13 @@ let mk_drop = * top of the stack) and swap (to swap the two topmost operands). There are some * macros, such as grow_highwater (or 16/8-bit arithmetic), that we want to * expand at the last minute (since they use some very low-level Wasm concepts). - * Therefore, as a convention, every function frame has four "scratch" locals; - * the first two of size I64; the last two of size I32. The Wasm register - * allocator will take care of optimizing all of that. *) + * Therefore, as a convention, every function frame has five "scratch" locals; + * the first two of size I64; the last three of size I32. The Wasm register + * allocator will take care of optimizing all of that. + * + * The first four scratch locals (up to env.n_args + 3) are always available and their value is not + * guaranteed to be preserved. The fifth one stores the stack pointer upon entry in a function, and + * therefore should never be used except in mk_func. *) let dup32 env = [ dummy_phrase (W.Ast.LocalTee (mk_var (env.n_args + 2))); dummy_phrase (W.Ast.LocalGet (mk_var (env.n_args + 2))) ] @@ -313,12 +319,12 @@ let swap3264 env = * that purpose. *) let read_highwater = i32_zero @ - [ dummy_phrase W.Ast.(Load { ty = mk_type I32; align = 0; offset = 0l; sz = None }) ] + [ dummy_phrase W.Ast.(Load { ty = mk_type I32; align = 0; offset = 0l; pack = None }) ] let write_highwater env = i32_zero @ swap32 env @ - [ dummy_phrase W.Ast.(Store { ty = mk_type I32; align = 0; offset = 0l; sz = None }) ] + [ dummy_phrase W.Ast.(Store { ty = mk_type I32; align = 0; offset = 0l; pack = None }) ] let grow_highwater env = read_highwater @ @@ -553,14 +559,14 @@ module Debug = struct mk_const (mk_int32 (Int32.of_int ofs)) @ mk_const (mk_int32 (Int32.of_int c)) @ [ dummy_phrase W.Ast.(Store { - ty = mk_type I32; align = 0; offset = 0l; sz = Some W.Types.Pack8 })] + ty = mk_type I32; align = 0; offset = 0l; pack = Some W.Types.Pack8 })] in let rec byte_and_store ofs c t f tl = char ofs c @ f (mk_const (mk_int32 (Int32.of_int (ofs + 1)))) @ [ dummy_phrase W.Ast.(Store { - ty = mk_type t; align = 0; offset = 0l; sz = None })] @ + ty = mk_type t; align = 0; offset = 0l; pack = None })] @ aux (if t = I32 then ofs + 5 else ofs + 9) tl and aux ofs l = @@ -672,21 +678,21 @@ and mk_expr env (e: expr): W.Ast.instr list = | CallFunc (("load16_le_i" | "load16_le"), [ e ]) -> mk_expr env e @ - [ dummy_phrase W.Ast.(Load { ty = mk_type I32; align = 0; offset = 0l; sz = Some W.Types.(Pack16, ZX) })] + [ dummy_phrase W.Ast.(Load { ty = mk_type I32; align = 0; offset = 0l; pack = Some W.Types.(Pack16, ZX) })] | CallFunc (("load16_be_i" | "load16_be"), [ e ]) -> mk_expr env (CallFunc ("WasmSupport_betole16", [ CallFunc ("load16_le", [ e ])])) | CallFunc (("load32_le_i" | "load32_le"), [ e ]) -> mk_expr env e @ - [ dummy_phrase W.Ast.(Load { ty = mk_type I32; align = 0; offset = 0l; sz = None })] + [ dummy_phrase W.Ast.(Load { ty = mk_type I32; align = 0; offset = 0l; pack = None })] | CallFunc (("load32_be_i" | "load32_be"), [ e ]) -> mk_expr env (CallFunc ("WasmSupport_betole32", [ CallFunc ("load32_le", [ e ])])) | CallFunc (("load64_le_i" | "load64_le"), [ e ]) -> mk_expr env e @ - [ dummy_phrase W.Ast.(Load { ty = mk_type I64; align = 0; offset = 0l; sz = None })] + [ dummy_phrase W.Ast.(Load { ty = mk_type I64; align = 0; offset = 0l; pack = None })] | CallFunc (("load64_be_i" | "load64_be"), [ e ]) -> mk_expr env (CallFunc ("WasmSupport_betole64", [ CallFunc ("load64_le", [ e ])])) @@ -705,17 +711,17 @@ and mk_expr env (e: expr): W.Ast.instr list = [ dummy_phrase (W.Ast.Const (mk_int32 8l)) ] @ i32_add @ [ dummy_phrase (W.Ast.LocalGet (mk_var local_src)) ] @ - [ dummy_phrase W.Ast.(Load { ty = mk_type I64; align = 0; offset = 0l; sz = None })] @ + [ dummy_phrase W.Ast.(Load { ty = mk_type I64; align = 0; offset = 0l; pack = None })] @ [ dummy_phrase (W.Ast.Call (mk_var (find_func env "WasmSupport_betole64"))) ] @ - [ dummy_phrase W.Ast.(Store { ty = mk_type I64; align = 0; offset = 0l; sz = None })] @ + [ dummy_phrase W.Ast.(Store { ty = mk_type I64; align = 0; offset = 0l; pack = None })] @ (* Same thing with +8b offset. This is high. *) [ dummy_phrase (W.Ast.LocalGet (mk_var local_dst)) ] @ [ dummy_phrase (W.Ast.LocalGet (mk_var local_src)) ] @ [ dummy_phrase (W.Ast.Const (mk_int32 8l)) ] @ i32_add @ - [ dummy_phrase W.Ast.(Load { ty = mk_type I64; align = 0; offset = 0l; sz = None })] @ + [ dummy_phrase W.Ast.(Load { ty = mk_type I64; align = 0; offset = 0l; pack = None })] @ [ dummy_phrase (W.Ast.Call (mk_var (find_func env "WasmSupport_betole64"))) ] @ - [ dummy_phrase W.Ast.(Store { ty = mk_type I64; align = 0; offset = 0l; sz = None })] @ + [ dummy_phrase W.Ast.(Store { ty = mk_type I64; align = 0; offset = 0l; pack = None })] @ (* This is just a glorified memcpy. *) mk_unit @@ -731,8 +737,8 @@ and mk_expr env (e: expr): W.Ast.instr list = (* Push dst and src on the stack; load src; store. This is low. *) [ dummy_phrase (W.Ast.LocalGet (mk_var local_dst)) ] @ [ dummy_phrase (W.Ast.LocalGet (mk_var local_src)) ] @ - [ dummy_phrase W.Ast.(Load { ty = mk_type I64; align = 0; offset = 0l; sz = None })] @ - [ dummy_phrase W.Ast.(Store { ty = mk_type I64; align = 0; offset = 0l; sz = None })] @ + [ dummy_phrase W.Ast.(Load { ty = mk_type I64; align = 0; offset = 0l; pack = None })] @ + [ dummy_phrase W.Ast.(Store { ty = mk_type I64; align = 0; offset = 0l; pack = None })] @ (* Same thing with +8b offset. This is high. *) [ dummy_phrase (W.Ast.LocalGet (mk_var local_dst)) ] @ [ dummy_phrase (W.Ast.Const (mk_int32 8l)) ] @ @@ -740,15 +746,15 @@ and mk_expr env (e: expr): W.Ast.instr list = [ dummy_phrase (W.Ast.LocalGet (mk_var local_src)) ] @ [ dummy_phrase (W.Ast.Const (mk_int32 8l)) ] @ i32_add @ - [ dummy_phrase W.Ast.(Load { ty = mk_type I64; align = 0; offset = 0l; sz = None })] @ - [ dummy_phrase W.Ast.(Store { ty = mk_type I64; align = 0; offset = 0l; sz = None })] @ + [ dummy_phrase W.Ast.(Load { ty = mk_type I64; align = 0; offset = 0l; pack = None })] @ + [ dummy_phrase W.Ast.(Store { ty = mk_type I64; align = 0; offset = 0l; pack = None })] @ (* This is just a glorified memcpy. *) mk_unit | CallFunc (("store16_le_i" | "store16_le"), [ e1; e2 ]) -> mk_expr env e1 @ mk_expr env e2 @ - [ dummy_phrase W.Ast.(Store { ty = mk_type I32; align = 0; offset = 0l; sz = Some W.Types.Pack16 })] @ + [ dummy_phrase W.Ast.(Store { ty = mk_type I32; align = 0; offset = 0l; pack = Some W.Types.Pack16 })] @ mk_unit | CallFunc (("store16_be_i" | "store16_be"), [ e1; e2 ]) -> @@ -757,7 +763,7 @@ and mk_expr env (e: expr): W.Ast.instr list = | CallFunc (("store32_le_i" | "store32_le"), [ e1; e2 ]) -> mk_expr env e1 @ mk_expr env e2 @ - [ dummy_phrase W.Ast.(Store { ty = mk_type I32; align = 0; offset = 0l; sz = None })] @ + [ dummy_phrase W.Ast.(Store { ty = mk_type I32; align = 0; offset = 0l; pack = None })] @ mk_unit | CallFunc (("store32_be_i" | "store32_be"), [ e1; e2 ]) -> @@ -766,7 +772,7 @@ and mk_expr env (e: expr): W.Ast.instr list = | CallFunc (("store64_le_i" | "store64_le"), [ e1; e2 ]) -> mk_expr env e1 @ mk_expr env e2 @ - [ dummy_phrase W.Ast.(Store { ty = mk_type I64; align = 0; offset = 0l; sz = None })] @ + [ dummy_phrase W.Ast.(Store { ty = mk_type I64; align = 0; offset = 0l; pack = None })] @ mk_unit | CallFunc (("store64_be_i" | "store64_be"), [ e1; e2 ]) -> @@ -802,7 +808,7 @@ and mk_expr env (e: expr): W.Ast.instr list = offset = Int32.of_int ofs; (* we store 32-bit integers in 32-bit slots, and smaller than that in * 32-bit slots as well, so no conversion M32 for us *) - sz = match size with + pack = match size with | A16 -> Some W.Types.(Pack16, ZX) | A8 -> Some W.Types.(Pack8, ZX) | _ -> None })] @@ -818,8 +824,22 @@ and mk_expr env (e: expr): W.Ast.instr list = mk_expr env e1 @ mk_cast w_from w_to + | CastI64ToPacked e -> + let scratch_i64 = mk_var (env.n_args + 0) in + mk_expr env e @ + (* Store result in first scratch local *) + [ dummy_phrase (W.Ast.LocalSet scratch_i64) ] @ + (* Load result, truncate low bits *) + [ dummy_phrase (W.Ast.LocalGet scratch_i64) ] @ + [ dummy_phrase W.Ast.(Convert (W.Values.I32 IntOp.WrapI64)) ] @ + (* Load result, shift 32 places, truncate to get high bits *) + [ dummy_phrase (W.Ast.LocalGet scratch_i64) ] @ + mk_const (mk_int64 32L) @ + [ dummy_phrase (W.Ast.Binary (mk_value I64 (Wasm.Ast.IntOp.ShrU))) ] @ + [ dummy_phrase W.Ast.(Convert (W.Values.I32 IntOp.WrapI64)) ] + | IfThenElse (e, b1, b2, s) -> - let s = mk_type s in + let s = mk_value_type s in mk_expr env e @ [ dummy_phrase (W.Ast.If (W.Ast.ValBlockType (Some s), mk_expr env b1, mk_expr env b2)) ] @@ -835,7 +855,7 @@ and mk_expr env (e: expr): W.Ast.instr list = ty = mk_type (if size = A64 then I64 else I32); align = 0; offset = Int32.of_int ofs; - sz = match size with + pack = match size with | A16 -> Some W.Types.Pack16 | A8 -> Some W.Types.Pack8 | _ -> None })] @ @@ -922,7 +942,7 @@ and mk_expr env (e: expr): W.Ast.instr list = | ((_, c), body) :: branches -> let c = int_of_string c in table.(c) <- mk_var (n - i); - [ dummy_phrase (W.Ast.Block (W.Ast.ValBlockType (Some s), + [ dummy_phrase (W.Ast.Block (W.Ast.ValBlockType (Some (W.Types.NumType s)), mk (i + 1) branches @ mk_expr env body @ [ dummy_phrase (W.Ast.Br (mk_var i))]))] @@ -936,8 +956,8 @@ and mk_expr env (e: expr): W.Ast.instr list = * case, for non-contiguous jump tables, and the out-of-bounds case, * which happens if the switch does not cover the last constructors. * *) - [ dummy_phrase (W.Ast.Block (W.Ast.ValBlockType (Some s), - [ dummy_phrase (W.Ast.Block (W.Ast.ValBlockType (Some s), + [ dummy_phrase (W.Ast.Block (W.Ast.ValBlockType (Some (W.Types.NumType s)), + [ dummy_phrase (W.Ast.Block (W.Ast.ValBlockType (Some (W.Types.NumType s)), dummy @ mk_expr env e @ [ dummy_phrase (W.Ast.BrTable (Array.to_list table, mk_var 0))]))] @ @@ -952,8 +972,8 @@ and mk_expr env (e: expr): W.Ast.instr list = let mk_func_type' args ret = dummy_phrase (W.Types.( FuncType ( - List.map mk_type args, - List.map mk_type ret))) + List.map mk_value_type args, + List.map mk_value_type ret))) let mk_func_type { args; ret; _ } = mk_func_type' args ret @@ -981,16 +1001,14 @@ let mk_func env { args; locals; body; name; ret; _ } = in (if name <> "WasmSupport_align_64" then Debug.mk env debug_enter else []) @ read_highwater @ + [ dummy_phrase (W.Ast.LocalSet (mk_var (env.n_args + 4))) ] @ mk_expr env body @ - (match ret with - | [ I32 ] -> swap32 env - | [ I64 ] -> swap6432 env - | _ -> []) @ + [ dummy_phrase (W.Ast.LocalGet (mk_var (env.n_args + 4))) ] @ write_highwater env @ if name <> "WasmSupport_align_64" then Debug.mk env debug_exit else [] in - let locals = List.map mk_type locals in + let locals = List.map mk_value_type locals in let ftype = mk_var i in dummy_phrase W.Ast.({ locals; ftype; body }) @@ -1025,8 +1043,8 @@ let mk_global env name size body post_init = post_init, body, false in init, dummy_phrase W.Ast.({ - gtype = W.Types.GlobalType (mk_type size, mut_of_bool mut); - value = dummy_phrase body + gtype = W.Types.GlobalType (mk_value_type size, mut_of_bool mut); + ginit = dummy_phrase body }), mut @@ -1047,7 +1065,7 @@ let add_global_imports module_name decls = })), mk_func_type f)) | Global (g_name, size, _, _, public) when public -> - let t = mk_type size in + let t = mk_value_type size in Hashtbl.add imports g_name (`Global (dummy_phrase W.Ast.({ module_name = name_of_string module_name; item_name = name_of_string g_name; @@ -1076,7 +1094,7 @@ let add_assumed_imports module_name decls = module_name = name_of_string module_name; item_name = name_of_string gname; idesc = dummy_phrase ( - GlobalImport W.Types.(GlobalType (mk_type t, W.Types.Immutable))) + GlobalImport W.Types.(GlobalType (mk_value_type t, W.Types.Immutable))) }))) | _ -> () @@ -1152,7 +1170,7 @@ let collect_external_imports env decls = inherit [_] iter method visit_CallFunc _ name _ = if not (StringSet.mem name known_funcs) && not (Hashtbl.mem env.funcs name) && not (is_primitive name) then - register_func name + register_func name method visit_GetGlobal _ name = if not (StringSet.mem name known_globals) && not (Hashtbl.mem env.globals name) then register_global name @@ -1260,14 +1278,14 @@ let mk_module (name, decls): (string * W.Ast.module_) = let last_func_index = n_imported_funcs + List.length funcs in funcs @ [ dummy_phrase W.Ast.({ locals = []; ftype = mk_var last_func_index; body = inits })], types @ [ mk_func_type' [] [] ], - Some (mk_var last_func_index) + Some (dummy_phrase W.Ast.({ sfunc = mk_var last_func_index })) in (* Side-effect: the table is now filled with all the string constants that * need to be laid out in the data segment. Compute said data segment. * Reminder: the data segment is just a convenient way to initialize memory at * module load-time. *) - let data = + let datas = let size = !(env.data_size) in let buf = Bytes.create size in if Options.debug "wasm" then @@ -1280,10 +1298,12 @@ let mk_module (name, decls): (string * W.Ast.module_) = Bytes.set buf (rel_addr + l) '\000'; ) env.strings; [ dummy_phrase W.Ast.({ - index = mk_var 0; - offset = dummy_phrase [ dummy_phrase ( - W.Ast.GlobalGet (mk_var (find_global env "data_start"))) ]; - init = Bytes.to_string buf })] + dmode = dummy_phrase (Active { + index = mk_var 0; + offset = dummy_phrase [ dummy_phrase ( + W.Ast.GlobalGet (mk_var (find_global env "data_start"))) ]; + }); + dinit = Bytes.to_string buf })] in (* We also to export how big is our data segment so that the next module knows @@ -1291,8 +1311,8 @@ let mk_module (name, decls): (string * W.Ast.module_) = * memory. *) let data_size_index = n_imported_globals + List.length globals in let globals = globals @ [ dummy_phrase W.Ast.({ - gtype = W.Types.GlobalType (mk_type I32, W.Types.Immutable); - value = dummy_phrase (mk_const (mk_int32 (Int32.of_int !(env.data_size)))) + gtype = W.Types.GlobalType (mk_value_type I32, W.Types.Immutable); + ginit = dummy_phrase (mk_const (mk_int32 (Int32.of_int !(env.data_size)))) })] in (* Export all of the current module's functions & globals. *) @@ -1327,7 +1347,7 @@ let mk_module (name, decls): (string * W.Ast.module_) = globals; exports; imports; - data; + datas; start }) in name, module_ diff --git a/test/.hints/Abbrev.fst.hints b/test/.hints/Abbrev.fst.hints index 33e1109aa..8e598cb5c 100644 --- a/test/.hints/Abbrev.fst.hints +++ b/test/.hints/Abbrev.fst.hints @@ -34,7 +34,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "31d3847c7345d74aa4c21792883c6cbe" + "5b56f07de22ee489b57a4656342d08a9" ] ] ] \ No newline at end of file diff --git a/test/.hints/AbstractStruct.fst.hints b/test/.hints/AbstractStruct.fst.hints index 47d8cc0b0..e5357e0c4 100755 --- a/test/.hints/AbstractStruct.fst.hints +++ b/test/.hints/AbstractStruct.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "7ae9f2049275344efc8c03c0080eab15" + "6e25b3876fb94331eda680a2ad0d5f01" ], [ "AbstractStruct.main", @@ -25,7 +25,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "e08b48b63ccdc0294c53ab0abb25d01a" + "0e81792562814ca0862db98a261f41ac" ] ] ] \ No newline at end of file diff --git a/test/.hints/Attributes.fst.hints b/test/.hints/Attributes.fst.hints index 86c349838..664e23ea6 100644 --- a/test/.hints/Attributes.fst.hints +++ b/test/.hints/Attributes.fst.hints @@ -45,7 +45,7 @@ "typing_FStar.Set.union" ], 0, - "54b014198854efdad78982a6c091fc72" + "2cb382d259f465b229f33355518a951b" ] ] ] \ No newline at end of file diff --git a/test/.hints/BadMatch.fst.hints b/test/.hints/BadMatch.fst.hints index dc9693d98..be5f558bc 100644 --- a/test/.hints/BadMatch.fst.hints +++ b/test/.hints/BadMatch.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "8881d7892c5cfe875cca3b3f087575fd" + "d5afd4ea8cdd37680afdab1acf7b3032" ], [ "BadMatch.baz", @@ -21,7 +21,7 @@ 1, [ "@query", "assumption_BadMatch.bar__uu___haseq" ], 0, - "4922381f1ffff2d6ec813c161d6ec76b" + "40d4333b5866f80df331fcab3bd1cba6" ] ] ] \ No newline at end of file diff --git a/test/.hints/BlitNull.fst.hints b/test/.hints/BlitNull.fst.hints index 2b62dc738..2c59de8a3 100644 --- a/test/.hints/BlitNull.fst.hints +++ b/test/.hints/BlitNull.fst.hints @@ -58,7 +58,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "30617e32215162828c35aad53bcf1217" + "c870e2135c2eb17714428e67156778de" ] ] ] \ No newline at end of file diff --git a/test/.hints/Buffer.Utils.fst.hints b/test/.hints/Buffer.Utils.fst.hints index 5519b8c18..3fceb25aa 100644 --- a/test/.hints/Buffer.Utils.fst.hints +++ b/test/.hints/Buffer.Utils.fst.hints @@ -22,7 +22,7 @@ "typing_FStar.UInt32.v" ], 0, - "641aeb4cd3c348e40a712b3e4abe1fe6" + "4ba7a00c542099d2e5b5272ebf357e6b" ], [ "Buffer.Utils.uint32_of_bytes", @@ -34,7 +34,7 @@ "refinement_interpretation_Tm_refine_307c3f8471f15f30d8324ebc79cdcdfb" ], 0, - "0a80d1b5ae499e430515e8bca4ea67ab" + "fc7ae73c8b7354351e746eb961542f8f" ], [ "Buffer.Utils.uint32_of_bytes", @@ -89,7 +89,7 @@ "typing_FStar.UInt8.v" ], 0, - "595852982ed4cc8add31ff9d1e7b5ed5" + "d61c4ef64304af3ff4e8121e9e545933" ], [ "Buffer.Utils.bytes_of_uint32s", @@ -178,7 +178,7 @@ "unit_inversion", "unit_typing" ], 0, - "81b82b74834003be5ff84658c8006c44" + "fa7d56937bc4a2174d67e6053740736b" ], [ "Buffer.Utils.bytes_of_uint32", @@ -199,7 +199,7 @@ "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec" ], 0, - "c3f70d75dbf07e06b7d5964f24a38bc8" + "19216dff47d705d8b2448aa2af219be6" ], [ "Buffer.Utils.bytes_of_uint32", @@ -270,7 +270,7 @@ "typing_FStar.UInt32.v", "typing_FStar.UInt8.t" ], 0, - "7d7c3bf6e0658da5404799b6f5d1eeb0" + "4cf6bc7443c2f461b8f6a23d1aad6ca0" ], [ "Buffer.Utils.memset", @@ -285,7 +285,7 @@ "typing_FStar.UInt32.v" ], 0, - "8d8d504a819c7d1fcd578235b6254b42" + "cf75abffaf270ce833e7860cfd3c90b2" ], [ "Buffer.Utils.memset", @@ -378,7 +378,7 @@ "unit_typing" ], 0, - "b82c8db098aaa310d9afc746e376da7c" + "8a97bb86511d1a787996bbb3218605b2" ] ] ] \ No newline at end of file diff --git a/test/.hints/C.Nullity.fsti.hints b/test/.hints/C.Nullity.fsti.hints index 57d5ffa92..a9172ad57 100644 --- a/test/.hints/C.Nullity.fsti.hints +++ b/test/.hints/C.Nullity.fsti.hints @@ -14,7 +14,7 @@ "refinement_interpretation_Tm_refine_0d4da60cb6187749d65a25df63d2ab15" ], 0, - "180cfb145ace907c88ce5708acecac30" + "2fde3fe35b07919cf2515d54b7124db4" ], [ "C.Nullity.pointer_distinct_sel_disjoint", @@ -80,7 +80,7 @@ "typing_FStar.UInt32.v" ], 0, - "43bd74eeb0ae47d33d6beda6bf90bcc5" + "d2e698f652bf3b2cf4b989cdeb9e7229" ] ] ] \ No newline at end of file diff --git a/test/.hints/C89.fst.hints b/test/.hints/C89.fst.hints index daa56448d..05195f948 100644 --- a/test/.hints/C89.fst.hints +++ b/test/.hints/C89.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "17fd175cf24e9f2ab0b093272d772d30" + "83592af2c8dc36fb9b156e4ed7f03d42" ], [ "C89.g", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "9e6b13857474daf80d0f8a9dd5f7437d" + "a20b455bfd9c6beea3e2cb83f521de53" ], [ "C89.h", @@ -62,7 +62,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "8f407a55249fc5c773aa122ab5d01d59" + "35fd63915e6a6b16773205f6d109afc6" ], [ "C89.i", @@ -83,7 +83,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "e266dfb575c866b33ed8c28fbe8cd7a2" + "cac8a66c41430a0cbdcbd365e4f351e4" ], [ "C89.touch", @@ -104,7 +104,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "eb27ba88f7982025769846e1e408ad29" + "26900d38bf539fb73f2a13f6fe714769" ], [ "C89.t", @@ -117,7 +117,7 @@ "typing_FStar.Int32.t", "typing_FStar.Int64.t" ], 0, - "17edcebc17edcc41ec85be3ae360954e" + "5fdc175d8548ea51c83e908ecc2a8e91" ], [ "C89.__proj__A__item___0", @@ -130,7 +130,7 @@ "refinement_interpretation_Tm_refine_dfc04c5c79d942a90086cac1eb7b1ae6" ], 0, - "0498a3395466c9d565615477f4cdaa1c" + "f7a15e1de5a27c2808f9afadcfbf6e33" ], [ "C89.__proj__B__item___0", @@ -143,7 +143,7 @@ "refinement_interpretation_Tm_refine_1a06de69b44dc8c0429a5d7e27c9f480" ], 0, - "16980bdd3e385c2dee51117399d46d0b" + "b4cd2b53009f001277e87e60bf7d1872" ], [ "C89.point", @@ -156,7 +156,7 @@ "typing_FStar.Int32.t" ], 0, - "b9188f9b847f80ad0a32addabde8f36b" + "789a91e9111c8913027c4b05adbd5c70" ], [ "C89.__proj__Point2d__item___0", @@ -169,7 +169,7 @@ "refinement_interpretation_Tm_refine_17ea200a8473bdb82b8d303711705436" ], 0, - "59bcc8e3b794580880f04a27d6d1bbf9" + "05f6ada2ec38ddc66c8bedbbb5baa321" ], [ "C89.__proj__Point2d__item___1", @@ -182,7 +182,7 @@ "refinement_interpretation_Tm_refine_17ea200a8473bdb82b8d303711705436" ], 0, - "c1b1f39c460dfc19be5541bbada7e09a" + "97ed22e4b072491bd0a5003dbc36798c" ], [ "C89.__proj__Point3d__item___0", @@ -195,7 +195,7 @@ "refinement_interpretation_Tm_refine_8a3bd36ce8fbd7cbd87cdc6980d27ae6" ], 0, - "c8531cc3dc9f4227c4494e07c4c1c843" + "c044ef5b6552d0f4767d84ab37c9f5aa" ], [ "C89.__proj__Point3d__item___1", @@ -208,7 +208,7 @@ "refinement_interpretation_Tm_refine_8a3bd36ce8fbd7cbd87cdc6980d27ae6" ], 0, - "e736a8696fec2ec20bda563a1ed15431" + "3ff528db105bbc6b36d26fb7f80d9ae5" ], [ "C89.__proj__Point3d__item___2", @@ -221,7 +221,7 @@ "refinement_interpretation_Tm_refine_8a3bd36ce8fbd7cbd87cdc6980d27ae6" ], 0, - "861ce2dae04889a5b80ac77c89b6e92a" + "51b75af5c4aa35801d92109c22ced9fc" ], [ "C89.main", @@ -321,7 +321,7 @@ "typing_FStar.UInt32.t", "typing_Prims.pow2" ], 0, - "121ee5b03d05ee126522a8b7eb7c6e27" + "5d6c66b383bb4a1c083b413268f18c48" ] ] ] \ No newline at end of file diff --git a/test/.hints/CheckedInt.fst.hints b/test/.hints/CheckedInt.fst.hints index df1c3833e..f151b9d34 100644 --- a/test/.hints/CheckedInt.fst.hints +++ b/test/.hints/CheckedInt.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "c08b0ad21509685c7782918044fa95e7" + "50f2b509d4651b5cf675fa5dfd7e3072" ], [ "CheckedInt.two", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "2aac390897f48005e5ea63a5fce2000a" + "fce43f8ac42fbb101a4a7a366da83453" ], [ "CheckedInt.main", @@ -54,7 +54,7 @@ "primitive_Prims.op_Subtraction" ], 0, - "9baef6caa0c6b951a43a82d675e44b4d" + "90d99c2de0dd9284cfa266748acb19cf" ] ] ] \ No newline at end of file diff --git a/test/.hints/ColoredRegion.fst.hints b/test/.hints/ColoredRegion.fst.hints index d0ff57ab4..2d9e451f2 100644 --- a/test/.hints/ColoredRegion.fst.hints +++ b/test/.hints/ColoredRegion.fst.hints @@ -44,7 +44,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "a456ba3e5753dafc5e5b30f368efbd51" + "8dfccfe75f568f753df00da71b587ed0" ] ] ] \ No newline at end of file diff --git a/test/.hints/Comment.fst.hints b/test/.hints/Comment.fst.hints index 2be89bae2..8314534ff 100644 --- a/test/.hints/Comment.fst.hints +++ b/test/.hints/Comment.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "6b4f90e6769d32aa13d66aeff611e1cc" + "c9766e6a140a6b386fe24e9af2773025" ] ] ] \ No newline at end of file diff --git a/test/.hints/ConstBuffer.fst.hints b/test/.hints/ConstBuffer.fst.hints index 21ac51a37..06f890024 100644 --- a/test/.hints/ConstBuffer.fst.hints +++ b/test/.hints/ConstBuffer.fst.hints @@ -31,7 +31,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "1c1f414490295be139c7c5a8c5b7ee8d" + "45363158c0cfb957881f3a8f40678cfc" ], [ "ConstBuffer.main", @@ -92,7 +92,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "34d340ac492e6fdba111d553ac20752d" + "9f15b0b39440bcab0615125fef8c2ad9" ] ] ] \ No newline at end of file diff --git a/test/.hints/Crypto.Symmetric.Chacha20.fst.hints b/test/.hints/Crypto.Symmetric.Chacha20.fst.hints index 31008708b..fc3a630e1 100644 --- a/test/.hints/Crypto.Symmetric.Chacha20.fst.hints +++ b/test/.hints/Crypto.Symmetric.Chacha20.fst.hints @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec" ], 0, - "fbcda6670121d98f290664a7d20cfe08" + "d1f899c0cf47ec3599073e8b0c9bf5a0" ], [ "Crypto.Symmetric.Chacha20.counter_mode", @@ -128,7 +128,7 @@ "unit_typing" ], 0, - "acee39b6c62652801f37597857f85635" + "3d2feeee8acf20166bc9a2c62e23138a" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ctypes1.fst.hints b/test/.hints/Ctypes1.fst.hints index f373a963e..142d146e3 100644 --- a/test/.hints/Ctypes1.fst.hints +++ b/test/.hints/Ctypes1.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "ad7c1f822a93592f25e3f47b0785e9a7" + "c59db447fbbd8947df7dac87bf90b155" ], [ "Ctypes1.point_no_bind", @@ -25,7 +25,7 @@ "typing_FStar.UInt32.t" ], 0, - "466a64fab47e6b00a951199ca5cbe3da" + "20ce80fd9884f84ca2ef9ea9aad14bd3" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ctypes2.fst.hints b/test/.hints/Ctypes2.fst.hints index daa4b0f57..02b703a0c 100644 --- a/test/.hints/Ctypes2.fst.hints +++ b/test/.hints/Ctypes2.fst.hints @@ -24,7 +24,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "9d58039baedd8dafd224416307f3d7a2" + "ed30a5e0e6ee0e856752e0fea07290d1" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ctypes3.fst.hints b/test/.hints/Ctypes3.fst.hints index 667332f90..c4267916f 100644 --- a/test/.hints/Ctypes3.fst.hints +++ b/test/.hints/Ctypes3.fst.hints @@ -13,7 +13,7 @@ "typing_FStar.UInt32.t" ], 0, - "201f6adac298f78ed84d17d54a7a4a42" + "e9e11250e4446cee7f5be3cf2ab802a8" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ctypes4.fst.hints b/test/.hints/Ctypes4.fst.hints index 029ea1303..f56f7605c 100644 --- a/test/.hints/Ctypes4.fst.hints +++ b/test/.hints/Ctypes4.fst.hints @@ -24,7 +24,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "0ab7628649548ddee202a004b091d333" + "e6549b594280abfbc9ccfe62f4deaa3d" ], [ "Ctypes4.move_circle", @@ -37,7 +37,7 @@ "typing_Ctypes3.__proj__Mkcircle__item__r" ], 0, - "5ccf1c7e895aee4e9e6c735aff3fe825" + "c2502b29e706da6b4e3294114c4aa96d" ], [ "Ctypes4.my_not", @@ -62,7 +62,7 @@ "true_interp" ], 0, - "db83dc3fe3f3588e58a87fa41cbefb18" + "0fca6d5c9a9f46161dc9ab5562e8bcca" ], [ "Ctypes4.tr", @@ -77,7 +77,7 @@ "typing_FStar.UInt32.t" ], 0, - "8cac74677dd2dbfa2b53ec573dc55a5a" + "6b2bd65b8ee1a697367ddf7e41470776" ], [ "Ctypes4.replicate", @@ -90,7 +90,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "07e863382241db026a36288105e85009" + "f81137c504e3879501261bc0eede21e8" ], [ "Ctypes4.int_opt", @@ -103,7 +103,7 @@ "typing_FStar.UInt32.t" ], 0, - "bbd317c43558d5a38f52f9bab3aa89f9" + "956406587e43d2347aa2e02f71e05dd6" ], [ "Ctypes4.__proj__IntSome__item___0", @@ -116,7 +116,7 @@ "refinement_interpretation_Tm_refine_747e8dbcdadc1011beb312d289ca27b1" ], 0, - "67e952b911616a36f53b8da7fa606690" + "a462adc1be8277a87b89b6d5114ee439" ], [ "Ctypes4.maybe_double", @@ -138,7 +138,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "1f41cd25e3b5a661d01af140b4394d6c" + "72f597f9d69e0156671b6235c32bd443" ], [ "Ctypes4.maybe_double", @@ -174,7 +174,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "31680fabd5a56998605f2e0512991880" + "8270c9eb3eef3007950ab7b94b0d86e3" ], [ "Ctypes4.__proj__L__item___0", @@ -187,7 +187,7 @@ "refinement_interpretation_Tm_refine_369514edfb0ad292ed962e8252b9565a" ], 0, - "86955b9a9d28aeca851bf7f594710bfa" + "d72b2c04bd4a96c6a18e8aabe3450f37" ], [ "Ctypes4.__proj__R__item___0", @@ -200,7 +200,7 @@ "refinement_interpretation_Tm_refine_692b693643b05e0d1ba47aa0fabd554b" ], 0, - "700768114a83aaead23168b5fe50b1e4" + "7992113eae0dd11900ecb2e23f6ff941" ], [ "Ctypes4.make_L", @@ -213,7 +213,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "fc2d99c8acae0eb55b1af7e77af3d0c2" + "f7d9a80a1d14ecf0ed14e84696099ee8" ], [ "Ctypes4.make_R", @@ -226,7 +226,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "6fc0e8f3a365e210c38db07ce45862df" + "b0585082890a8eba289c5e6fd519956c" ], [ "Ctypes4.flip_t", @@ -249,7 +249,7 @@ "true_interp" ], 0, - "1ffab6cd935364acec099febb58b5f4a" + "4dea31eb58f66dddcaa955e910b4216b" ], [ "Ctypes4.unsupported_t", @@ -262,7 +262,7 @@ "typing_FStar.UInt128.t", "typing_FStar.UInt32.t" ], 0, - "2da5ea65a524c37ea66a2f62ffa6056a" + "a5450ca1138baa443c3b075035a0c813" ], [ "Ctypes4.unsupported_abstract_t", @@ -275,7 +275,7 @@ "typing_FStar.UInt128.t", "typing_FStar.UInt32.t" ], 0, - "66649594ccbb48ec68b184dd6d265de2" + "3c12fb098db488b7915aad20efd12045" ], [ "Ctypes4.create_u", @@ -308,7 +308,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "bb682748d4491725b1349687408095a9" + "51bb46940ccdc32f099ef2d33f01b71a" ], [ "Ctypes4.read_u_a2", @@ -324,7 +324,7 @@ "typing_Ctypes4.__proj__Mkunsupported_abstract_t__item__a2" ], 0, - "f00960f60877e96733fdc67607b625a9" + "bc7d6d9aef8f0ca5ed9c410e41dc6514" ] ] ] \ No newline at end of file diff --git a/test/.hints/CustomEq.fst.hints b/test/.hints/CustomEq.fst.hints index 4a52c261e..6585ad472 100644 --- a/test/.hints/CustomEq.fst.hints +++ b/test/.hints/CustomEq.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "d01d03811873df9e883ca657d25ba7d6" + "d39e029f981abb647ed6ff18642e4b8d" ], [ "CustomEq.t", @@ -21,7 +21,7 @@ 1, [ "@query", "assumption_CustomEq.point__uu___haseq" ], 0, - "b9fd204b544504fd00b81b4a7151c272" + "190f8272a90a39023181d88e1e72c041" ], [ "CustomEq.__proj__A__item__p1", @@ -34,7 +34,7 @@ "refinement_interpretation_Tm_refine_b42bbc5acfd996b49e25c6ab17e83c41" ], 0, - "3a5aa177b51e370640d37dcc6800eeb6" + "17c4548fe1a3b7e5f9c913d9596c4d42" ], [ "CustomEq.__proj__A__item__p2", @@ -47,7 +47,7 @@ "refinement_interpretation_Tm_refine_b42bbc5acfd996b49e25c6ab17e83c41" ], 0, - "d922f216a1da6758f7def5406a819ae8" + "dfe708ce412d110cf15856b69bd915be" ], [ "CustomEq.__proj__B__item___0", @@ -60,7 +60,7 @@ "refinement_interpretation_Tm_refine_499f060f30a6559751f4282e23af22de" ], 0, - "5a8b5f8f5b5c01137a3930ecf4ced7ac" + "307ae41e5825212a7897699a7096cb14" ], [ "CustomEq.p1", @@ -81,7 +81,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "aa8e8e9ca81ed5377b1077946ae40f0c" + "0d8f2288c1b03c75106f068f0969a59b" ], [ "CustomEq.f", @@ -102,7 +102,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "a5164970a62e723945942ff5172f7b39" + "6753b2fd28028ea84ac7b6cc7137a843" ], [ "CustomEq.p2", @@ -128,7 +128,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "005e99c213bb187f455babfc7eb48f4e" + "2ef612d2f0f029c81874ed022b967f93" ], [ "CustomEq.t1", @@ -143,7 +143,7 @@ "typing_FStar.Int64.t" ], 0, - "124ba2dec3660db0e7c97eec9d9bf359" + "5db3421b6c040fa850d5a7e88d46ef95" ], [ "CustomEq.t2", @@ -164,7 +164,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "d915d5da9ae29143637911e8e6dd2b2b" + "697dc1e9f93b218ecfcc6bd3d39e7c87" ], [ "CustomEq.id", @@ -185,7 +185,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "033372e3fe50d50a9d13d2dbaed82915" + "2199702c3f8f09ab0b848b108df0bc6f" ], [ "CustomEq.main", @@ -205,7 +205,7 @@ "typing_FStar.Int64.t" ], 0, - "d5f653630fd7260f7b139fe04cf83b9b" + "a3f5a34bd462a41cc873c8ea891a3058" ] ] ] \ No newline at end of file diff --git a/test/.hints/DataTypes.fst.hints b/test/.hints/DataTypes.fst.hints index 84d28b7b4..2d6d5a61f 100644 --- a/test/.hints/DataTypes.fst.hints +++ b/test/.hints/DataTypes.fst.hints @@ -12,7 +12,7 @@ "refinement_interpretation_Tm_refine_599cdc3d9160d7b695e8959f132bb409" ], 0, - "14989a470c2d99f3e3bdc29c4b657d9f" + "7fc3b3d9d5b58024c3ca252a73f4bb79" ], [ "DataTypes.__proj__A__item__b", @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_599cdc3d9160d7b695e8959f132bb409" ], 0, - "5afdc29608741e20065b167a33d9f2b3" + "bc13be9dbe8e0427c0be6732db25e00f" ], [ "DataTypes.__proj__B__item__c", @@ -38,7 +38,7 @@ "refinement_interpretation_Tm_refine_e0fbb0ccb14c7057144f6a5a325e8ddd" ], 0, - "e67050fbba9b65072faa180f34315210" + "ba987a08ed3f33ab9e2466c3b7d8e4ac" ], [ "DataTypes.__proj__B__item__d", @@ -51,7 +51,7 @@ "refinement_interpretation_Tm_refine_e0fbb0ccb14c7057144f6a5a325e8ddd" ], 0, - "b09cd50a639c91e206b9371861546bf5" + "c149f4189324d2c8d44274866e16f466" ], [ "DataTypes.__proj__B__item__e", @@ -64,7 +64,7 @@ "refinement_interpretation_Tm_refine_e0fbb0ccb14c7057144f6a5a325e8ddd" ], 0, - "b5b403237b7d3419f30bc3e4d6ad08d2" + "28f2233bc514311cf3a9df17b6d46ea4" ], [ "DataTypes.__proj__C__item__f", @@ -77,7 +77,7 @@ "refinement_interpretation_Tm_refine_b63a9a8aecee956770bb1476545b326e" ], 0, - "1b497e9aa7469244c2d5c072b11f6522" + "71a33cc0d307f04abefd9d4bff0792dc" ], [ "DataTypes.__proj__C__item__g", @@ -90,7 +90,7 @@ "refinement_interpretation_Tm_refine_b63a9a8aecee956770bb1476545b326e" ], 0, - "f2b322738ec402313342c99d9016ab0c" + "b195bf6b9aacaf9b37931a3234528fa0" ], [ "DataTypes.__proj__D__item__h", @@ -103,7 +103,7 @@ "refinement_interpretation_Tm_refine_4c835444c923ef29c3c5e4f8248f0c1c" ], 0, - "6e8bced1eb617dd2fcf796a8d3f2c4a9" + "a9f5581adf2f22459de374fb96672ff7" ], [ "DataTypes.__proj__D__item__i", @@ -116,7 +116,7 @@ "refinement_interpretation_Tm_refine_4c835444c923ef29c3c5e4f8248f0c1c" ], 0, - "4bb0e6011302a7f89831a0508aa9a129" + "9a8c940be28194d5c0fc725ee8f06d1d" ], [ "DataTypes.test", @@ -138,7 +138,7 @@ "typing_tok_DataTypes.E@tok" ], 0, - "085aa90cf61d947676e61760ecbf0a04" + "a65696f5f95cb2eacb411d90b2c9194d" ], [ "DataTypes.something", @@ -159,7 +159,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "6190d1ee96bb7bd2d4f529a8c7b1e1eb" + "9bcfa68bb303070bdc908d00e4b3f079" ], [ "DataTypes.whatever", @@ -180,7 +180,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "31bb3ebd2c89d2b755f10084817ec8fb" + "7d539066403d4c891a80ab947cd589af" ], [ "DataTypes.point", @@ -193,7 +193,7 @@ "typing_FStar.UInt32.t" ], 0, - "a95b24b3dfdeac3984e60773bbccb299" + "96045fc9270cc8a4847648108ebca87c" ], [ "DataTypes.f", @@ -212,7 +212,7 @@ "true_interp" ], 0, - "08b7622babf852f656205461dfcb8a16" + "4489a537e3fdd208504880a41e4d2fd6" ], [ "DataTypes.f'", @@ -231,7 +231,7 @@ "true_interp" ], 0, - "1a0bc4543cd0a65c7c30ba530a2f82a5" + "37a715826b90c6782f54355808fbc011" ], [ "DataTypes.main", @@ -272,7 +272,7 @@ "typing_tok_C.EXIT_FAILURE@tok", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "9b50b1613400638735c27196764881ad" + "86a0bd00c70427ee3e2c694fb6fc1b7d" ] ] ] \ No newline at end of file diff --git a/test/.hints/DataTypesEq.fst.hints b/test/.hints/DataTypesEq.fst.hints index 9d297fbd5..c5b5be410 100644 --- a/test/.hints/DataTypesEq.fst.hints +++ b/test/.hints/DataTypesEq.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "7b901992a7b7d812f15459c7596b7980" + "8f49c79d9efe967f535f1eb476925f76" ], [ "DataTypesEq.__proj__A__item___0", @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_7fe4ec39530be71d09622e6ea631b362" ], 0, - "650b2e1c776b032b809e7bd9d5a88c22" + "7c88f2e1c669fd30746087a37e88fecb" ], [ "DataTypesEq.__proj__B__item___0", @@ -38,7 +38,7 @@ "refinement_interpretation_Tm_refine_4d5e6c06bbfb6471b81e2745aebd0ea5" ], 0, - "495a785d4784a821269faf03585de801" + "621e20c1a91cc45b9447aaae35f1621c" ], [ "DataTypesEq.f", @@ -59,7 +59,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "f79908c3d2e81b1fef649c65e670353c" + "a3a8de5ea8057456626944033edc4469" ], [ "DataTypesEq.main", @@ -68,7 +68,7 @@ 1, [ "@query", "assumption_DataTypesEq.t__uu___haseq" ], 0, - "3e749784df7daf81d7ab94be438e747c" + "8389615b0931052a2dffc24f717ad27c" ] ] ] \ No newline at end of file diff --git a/test/.hints/DataTypesSimple.fst.hints b/test/.hints/DataTypesSimple.fst.hints index 18288e227..e94d72a6d 100644 --- a/test/.hints/DataTypesSimple.fst.hints +++ b/test/.hints/DataTypesSimple.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "7379a514a4d0e7aebbfdd1fc8665d194" + "470e8abde7f0fc2ab6e0483f7e4be629" ], [ "DataTypesSimple.f", @@ -35,7 +35,7 @@ "typing_tok_DataTypesSimple.Cons1@tok" ], 0, - "0394f5af3e7ac3ae90af73d1eb93d848" + "f4dbf12c68d475c37e921c3eaa949ebd" ], [ "DataTypesSimple.main", @@ -56,7 +56,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "f03041083635938cf7c40dfbe65eddfd" + "069284a75fb68efaace2a399e96feded" ] ] ] \ No newline at end of file diff --git a/test/.hints/Endianness.fst.hints b/test/.hints/Endianness.fst.hints index 10595da5e..f586957f3 100644 --- a/test/.hints/Endianness.fst.hints +++ b/test/.hints/Endianness.fst.hints @@ -63,7 +63,7 @@ "typing_FStar.Set.complement", "typing_FStar.Set.singleton" ], 0, - "f0f67243d59a3ee0846874d17e1614d2" + "f974edbba0d86c515b48ce5e3ae55c0e" ] ] ] \ No newline at end of file diff --git a/test/.hints/EqB.fst.hints b/test/.hints/EqB.fst.hints index 8bf389485..3ed9aa0f3 100644 --- a/test/.hints/EqB.fst.hints +++ b/test/.hints/EqB.fst.hints @@ -74,7 +74,7 @@ "typing_FStar.UInt32.t" ], 0, - "4bef7049dcafd5bc746f10318ecbc59a" + "5170f0bdd83765316ac5b505d498ff89" ] ] ] \ No newline at end of file diff --git a/test/.hints/EtaStruct.fst.hints b/test/.hints/EtaStruct.fst.hints index 3805e5ef7..dd0e9e012 100644 --- a/test/.hints/EtaStruct.fst.hints +++ b/test/.hints/EtaStruct.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "6b33ba59d584aa6c8e79e9bb3b1018cf" + "c0a6b6e353db5354c13a0829942838dc" ], [ "EtaStruct.f", @@ -27,7 +27,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "9e0baf974feeb74d5c341ec4d46b89aa" + "7450a2bc2b6f931a89d26e21d7a9a7cc" ], [ "EtaStruct.main", @@ -36,7 +36,7 @@ 1, [ "@query" ], 0, - "cdba4c4533a3745edf26e772e2120795" + "10e8c8b96927c5fc60c65b8795331154" ] ] ] \ No newline at end of file diff --git a/test/.hints/ExitCode.fst.hints b/test/.hints/ExitCode.fst.hints index 64f70c4cf..6437ada18 100644 --- a/test/.hints/ExitCode.fst.hints +++ b/test/.hints/ExitCode.fst.hints @@ -21,7 +21,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "b92a674726080c1307725f8382be3c61" + "b4d1eef7a5c6fd7fd2bd9da7cc54afdf" ] ] ] \ No newline at end of file diff --git a/test/.hints/Failwith.fst.hints b/test/.hints/Failwith.fst.hints index 85182a3bf..dea70d035 100644 --- a/test/.hints/Failwith.fst.hints +++ b/test/.hints/Failwith.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "fbfc55ad140e02842b0a05fa40674ff6" + "65bc9cae03e54e6827f90e693bafa0b2" ], [ "Failwith.main", @@ -33,7 +33,7 @@ "function_token_typing_C.exit_success" ], 0, - "39a42e5baa6cf23e43bdcfdb74588346" + "5ef1f12ca3c94d175db358312aa5a874" ] ] ] \ No newline at end of file diff --git a/test/.hints/Fill.fst.hints b/test/.hints/Fill.fst.hints index f45b9c01d..c9440a47d 100644 --- a/test/.hints/Fill.fst.hints +++ b/test/.hints/Fill.fst.hints @@ -17,7 +17,7 @@ "true_interp" ], 0, - "f36425ac3a8e64c9864bc3a2c184b483" + "87a9222df9c80fb82a0b33ad94b609f3" ], [ "Fill.fill_out_uint8", @@ -34,7 +34,7 @@ "true_interp" ], 0, - "b65c71d2d1a853b1fa021fdbe25a3d0a" + "8b4e37e3a82df4d2754b9592acf2665f" ], [ "Fill.test", @@ -106,7 +106,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "17c24a9f7b9b8eb9d85dd79d5b0f8c87" + "ca6b293e960d92929c33e3b8500d58b7" ], [ "Fill.main", @@ -155,7 +155,7 @@ "typing_FStar.Set.singleton", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "f8363d40890993262d896b1c3014bede" + "34704d2b5b9caf68226fb0daee9ec085" ] ] ] \ No newline at end of file diff --git a/test/.hints/Flat.fst.hints b/test/.hints/Flat.fst.hints index 09e6ae9ac..76fe70982 100644 --- a/test/.hints/Flat.fst.hints +++ b/test/.hints/Flat.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "9969b591d31f1ea421cff546675cf7d4" + "bcd8d7f7f4ad8bfc4ac5d6d6df7a00ff" ], [ "Flat.main", @@ -91,7 +91,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "cda30e9d29096c5e06dd2091bde587c0" + "4ad6cfb095f233ba4e2d87a9d76dd480" ] ] ] \ No newline at end of file diff --git a/test/.hints/FunPtr.fst.hints b/test/.hints/FunPtr.fst.hints index 3459727de..d07f8d913 100644 --- a/test/.hints/FunPtr.fst.hints +++ b/test/.hints/FunPtr.fst.hints @@ -14,7 +14,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "cc9efae92c8ab8376ced49870c89db39" + "d7de99bcf1423f74d95e738af779aafa" ], [ "FunPtr.main", @@ -30,7 +30,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "116929c3fd0f2a976bd0e7819be8882c" + "680b58003184845b513baf8ebb898541" ] ] ] \ No newline at end of file diff --git a/test/.hints/FunctionalEncoding.fst.hints b/test/.hints/FunctionalEncoding.fst.hints index 2c54b20e3..33775f772 100644 --- a/test/.hints/FunctionalEncoding.fst.hints +++ b/test/.hints/FunctionalEncoding.fst.hints @@ -15,7 +15,7 @@ "typing_FunctionalEncoding.__proj__Mkanimal__item__species" ], 0, - "faf06f18f6cd6db4b4294ed85efbe45e" + "bf748082b88c767e0a285601bdd89bc1" ] ] ] \ No newline at end of file diff --git a/test/.hints/GcTypes.fst.hints b/test/.hints/GcTypes.fst.hints index c070f9dec..7a8aa82d6 100644 --- a/test/.hints/GcTypes.fst.hints +++ b/test/.hints/GcTypes.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "d4ea4ddad39506c7c7f5b56301d8d7aa" + "5b7e1403230fbcca21c431827130ee11" ], [ "GcTypes.main", @@ -33,7 +33,7 @@ "refinement_interpretation_Tm_refine_abf749ae3c800f91a6f1dcf2ecb5621e" ], 0, - "ef1d0f30627caf708320a50e933c217c" + "133e67684fa9096d854ee70a2145021a" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ghost1.fst.hints b/test/.hints/Ghost1.fst.hints index b54ac4e7a..6dbd4b24f 100644 --- a/test/.hints/Ghost1.fst.hints +++ b/test/.hints/Ghost1.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "46f6023782c497342cbe95cfaa34e331" + "b1cce2810860760b17969376d4e26bcc" ], [ "Ghost1.test", @@ -29,7 +29,7 @@ 1, [ "@query", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans" ], 0, - "e406062d893d90b8e67ca806e8899591" + "50c139e2783f856103a5bc878bf07bb5" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder.fst.hints b/test/.hints/HigherOrder.fst.hints index 1fec5d87b..77a853031 100644 --- a/test/.hints/HigherOrder.fst.hints +++ b/test/.hints/HigherOrder.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "88314f31b65e1d584906368186f58726" + "642d0ab605475d8b7cbcb384736af8c1" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder2.fst.hints b/test/.hints/HigherOrder2.fst.hints index f09d34f2c..6462fc7db 100644 --- a/test/.hints/HigherOrder2.fst.hints +++ b/test/.hints/HigherOrder2.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "a36cc03ee2daf765827c9e0f11dd0d63" + "895cafb970a601ab7c5d1fcc9ce1059d" ], [ "HigherOrder2.exampleFunc", @@ -31,7 +31,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "7180f3e97cbc411d01e091dbe3f2ff4b" + "513a950713e5b4d243c0721d90e5c0f0" ], [ "HigherOrder2.main", @@ -60,7 +60,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "a9a516e9c8d574620826a05265db62b6" + "74f37d4d9f00d98f8847e54c3a28aed1" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder3.fst.hints b/test/.hints/HigherOrder3.fst.hints index d9ae0addb..f68ec2cf2 100644 --- a/test/.hints/HigherOrder3.fst.hints +++ b/test/.hints/HigherOrder3.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "6cb45f701057ef59c6b60b7d1405c9d1" + "fb2b5358e570036f0f630ffab77052bf" ], [ "HigherOrder3.exampleFunc", @@ -25,7 +25,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "e618805851aede5810914b76455b0b5c" + "89c09f2e46923df31512b9d29025a16d" ], [ "HigherOrder3.main", @@ -50,7 +50,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "6180d87872f988c0458fd1a678a659ea" + "f3666141a15ffecbb98082160475e5d2" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder4.fst.hints b/test/.hints/HigherOrder4.fst.hints index e83166a75..7d3688ddd 100644 --- a/test/.hints/HigherOrder4.fst.hints +++ b/test/.hints/HigherOrder4.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "c7f8d28764d1c2c6eec19e4e5526314b" + "23408e3dfa672b50b52c5decee6653cc" ], [ "HigherOrder4.createContainer", @@ -66,7 +66,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "d54e019a397ac45d532eb3f0a362b91e" + "459295d460599695baa8d249595158b6" ], [ "HigherOrder4.main", @@ -118,7 +118,7 @@ "typing_Prims.pow2" ], 0, - "6629a3f986f23c22d1d4367b8051ae8b" + "b125d137ff0c411b4d7007c2b60d8dc9" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder5.fst.hints b/test/.hints/HigherOrder5.fst.hints index 09a8f3345..43708e4bc 100644 --- a/test/.hints/HigherOrder5.fst.hints +++ b/test/.hints/HigherOrder5.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "366cc59e0bd3670ab7b8554a87ffea5f" + "bcb707c76ab31a9a60ff7ba146963106" ], [ "HigherOrder5.t_D", @@ -25,7 +25,7 @@ "typing_FStar.Int32.t", "typing_FStar.Monotonic.HyperHeap.rid" ], 0, - "2b1fa6d35f6b4e8752ff29528557e2c4" + "94aa1f471f5cf308c55d5bd95fe38a9a" ], [ "HigherOrder5.foo", @@ -38,7 +38,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "8d4b42a30d63531d3ec4ecd8db624b64" + "d44c387c457b1de89189534e54237624" ], [ "HigherOrder5.main", @@ -87,7 +87,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.pow2" ], 0, - "2a97d811cf49324c56e6b5268dd5110b" + "95bfcc230d2eb4a0b99a86b6c6e214bc" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder6.fst.hints b/test/.hints/HigherOrder6.fst.hints index 6382062fa..3cba5ccdd 100644 --- a/test/.hints/HigherOrder6.fst.hints +++ b/test/.hints/HigherOrder6.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "acd76970759df93d24c5d3b1b399e6d3" + "9e55a266f858e8f3322f2ad2fae69393" ], [ "HigherOrder6.t_D", @@ -25,7 +25,7 @@ "typing_FStar.Int32.t", "typing_FStar.Monotonic.HyperHeap.rid" ], 0, - "ee3e3ac239076f0e3342e7e3d0601f4b" + "ede509ccf007cfe0016446021f3658de" ], [ "HigherOrder6.foo", @@ -38,7 +38,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "e53f229148a9d6c9355b8c0e42bc3695" + "e67263140b9ef3ec35e8e88e19992dc3" ], [ "HigherOrder6.main", @@ -87,7 +87,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.pow2" ], 0, - "349ac03045f40828d14dab68ec984a2f" + "a55970d2c6ad0e493dca6c311a5e0b3d" ] ] ] \ No newline at end of file diff --git a/test/.hints/Hoisting.fst.hints b/test/.hints/Hoisting.fst.hints index 299cff95f..33e6a6cd3 100644 --- a/test/.hints/Hoisting.fst.hints +++ b/test/.hints/Hoisting.fst.hints @@ -42,7 +42,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.pow2" ], 0, - "aa51870218264d9a578afba4f9b21d7b" + "e307045ffb26bfa726ae3e5eb8806262" ], [ "Hoisting.main", @@ -127,7 +127,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "b4e4a77404e0fbe246bfb27faeb6ac07" + "f3899fee546e9a3e33cd1e23eb899051" ] ] ] \ No newline at end of file diff --git a/test/.hints/IfDef.fst.hints b/test/.hints/IfDef.fst.hints index 2d3345d84..01e85530b 100644 --- a/test/.hints/IfDef.fst.hints +++ b/test/.hints/IfDef.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "59450dec56a85a8d9bf80ad1f3746e77" + "1d6584b8d8d8d5d6c0e03a661d327a60" ], [ "IfDef.foo'", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "4085955d947fb415ca8ac9a5690cb1e1" + "5172bf4e3fed260eb234bcf96046b1de" ], [ "IfDef.test", @@ -63,7 +63,7 @@ "unit_typing" ], 0, - "e45a0e2ff0b2bba60e2334f92913ff5d" + "1565a412befc11438196efecc95a6858" ], [ "IfDef.bar", @@ -84,7 +84,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "1b9a17730571fb185b33bb6e2806c4da" + "8153f82d909a4ecf97b11b4783284266" ], [ "IfDef.test3", @@ -93,7 +93,7 @@ 1, [ "@query", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans" ], 0, - "b743c0a03ececd652e82595eeed44b32" + "d245a0400806fb6ed264c3f6122c72d8" ] ] ] \ No newline at end of file diff --git a/test/.hints/IfThenElse.fst.hints b/test/.hints/IfThenElse.fst.hints index 69defb38e..33fdb9101 100644 --- a/test/.hints/IfThenElse.fst.hints +++ b/test/.hints/IfThenElse.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "bc9b617a90224210b732f44ea80db736" + "37b198666e8507440420d1e31450bcae" ], [ "IfThenElse.main", @@ -34,7 +34,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "86cbc67110baca29426c2d242845c3a7" + "2e6ece93758319dafa92204930f412bd" ] ] ] \ No newline at end of file diff --git a/test/.hints/InitializerLists.fst.hints b/test/.hints/InitializerLists.fst.hints index ddaf489ad..9b581aa0d 100644 --- a/test/.hints/InitializerLists.fst.hints +++ b/test/.hints/InitializerLists.fst.hints @@ -27,7 +27,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "15b6222fdd30895d5370f787822fc30b" + "0455109095f5bbe3e097383269784db0" ], [ "InitializerLists.x2", @@ -55,7 +55,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "6f2eeb94c04ad1864c6987f4ee5f35f8" + "aa81124b83a12fefd821dfe6000893fd" ], [ "InitializerLists.x3", @@ -83,7 +83,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "5f51d086c63d9e0d2da0daedc11b593b" + "56664997aa2e4f783181524d8cc9923b" ], [ "InitializerLists.f", @@ -96,7 +96,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "79d2b249a6e154c9a431591bd2d1b7c2" + "8516bc161bb053426d5dbcf2531bd90d" ], [ "InitializerLists.main", @@ -147,7 +147,7 @@ "typing_InitializerLists.x" ], 0, - "5933f76a042e85041aff0c90c372e052" + "a36f130686e51913ff6ecfa9ceecf8e7" ] ] ] \ No newline at end of file diff --git a/test/.hints/Inline.fst.hints b/test/.hints/Inline.fst.hints index a3794d200..e7680164b 100644 --- a/test/.hints/Inline.fst.hints +++ b/test/.hints/Inline.fst.hints @@ -37,7 +37,7 @@ "typing_FStar.Int32.t", "typing_FStar.Int32.v" ], 0, - "9581207f1273aac061965a5814652019" + "6e5cd2728939f16305770f7da8c89aca" ], [ "Inline.main", @@ -118,7 +118,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "b1740e06efb14870159286054cc3afcc" + "d1f27b5e8b3c457c33878479f27fb81f" ] ] ] \ No newline at end of file diff --git a/test/.hints/InlineNoExtract.fst.hints b/test/.hints/InlineNoExtract.fst.hints index 9a68f4efe..fbaeac81e 100644 --- a/test/.hints/InlineNoExtract.fst.hints +++ b/test/.hints/InlineNoExtract.fst.hints @@ -14,7 +14,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "eb7ff9c576cf5ed3d222580889bebbb6" + "dee8ec21861182d1164ec7960d6ee6bc" ], [ "InlineNoExtract.b", @@ -29,7 +29,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "ee1588bec6f092b2ea1be81dd04729c2" + "db53229d54a64750b4c65107737c59c2" ] ] ] \ No newline at end of file diff --git a/test/.hints/InlineTest.fst.hints b/test/.hints/InlineTest.fst.hints index 5b7d208ad..0f593f9c5 100644 --- a/test/.hints/InlineTest.fst.hints +++ b/test/.hints/InlineTest.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "917b44b70d85b17c00fa2ec43fab06cd" + "92cb0fdc1df57b45542cf7ebdfacff0e" ], [ "InlineTest.__proj__Error__item___0", @@ -21,7 +21,7 @@ "refinement_interpretation_Tm_refine_dc1c4313057dcc858ffa9fd88c3f020d" ], 0, - "00c4ab239d876e31ead711daa68f0f95" + "1f6539f68039ed8d776ff034e7b6a2df" ], [ "InlineTest.__proj__Correct__item___0", @@ -34,7 +34,7 @@ "refinement_interpretation_Tm_refine_dc046c5c58c78691ac946f81662277ac" ], 0, - "29808d0bff53d3689c87502f82b0e680" + "13d6708a6cc831c08b564ef111a2a6a6" ], [ "InlineTest.main", @@ -52,7 +52,7 @@ "projection_inverse_InlineTest.Correct__b" ], 0, - "98396f0d88509c96ecf37d5d8104a6c4" + "27f76fb7158aceb040915ce05ed903de" ] ] ] \ No newline at end of file diff --git a/test/.hints/Intro.fst.hints b/test/.hints/Intro.fst.hints index 46b9085ef..02920e3a8 100644 --- a/test/.hints/Intro.fst.hints +++ b/test/.hints/Intro.fst.hints @@ -82,7 +82,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "a9468295e16539bf9f24f4e2e90a7443" + "7d879ac78c3b34812fbee6738527ed26" ] ] ] \ No newline at end of file diff --git a/test/.hints/Layered.fst.hints b/test/.hints/Layered.fst.hints index 1e5f51bcf..e08d50719 100644 --- a/test/.hints/Layered.fst.hints +++ b/test/.hints/Layered.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "914fd2ad78188ef40686266e83d7ab5f" + "9f72716a17874f632d4cd00d25b1089d" ], [ "Layered.return", @@ -29,7 +29,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "fe706a6c8d55cbfe64d1d6d3e89c17c9" + "7a96a0f5a43035d7c18f505d677bd5e1" ], [ "Layered.bind_wp", @@ -53,7 +53,7 @@ "typing_tok_Layered.Context@tok" ], 0, - "d0f3640e1089117bb6cffddd25aa68d3" + "7e7c45b921a59326a80f1f2e1e0b0640" ], [ "Layered.bind", @@ -89,7 +89,7 @@ "typing_tok_Layered.Context@tok" ], 0, - "5f47937d40eb817f7d82ad1358ec5ab7" + "caf018b2f09c28a9005499643a2573df" ], [ "Layered.subcomp", @@ -110,7 +110,7 @@ "typing_tok_Layered.Context@tok" ], 0, - "c348a51ac7ccbcaf0d35f54d2cadc39c" + "8dd12ae5796e4393de98112e31690c17" ], [ "Layered.if_then_else_wp", @@ -125,7 +125,7 @@ "refinement_interpretation_Tm_refine_b5b7150a72165c5a72019df5afbe737b" ], 0, - "5e0ce6a2b0008fb4f7545f8eefca446b" + "de91e6deca118d7a92245597d54d51ef" ], [ "Layered.BUG", @@ -137,7 +137,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "08f9a31b8a203e978c7766e90ed24e52" + "48875792642bedb39a9ea32832e6acb6" ], [ "Layered.BUG", @@ -149,7 +149,7 @@ "refinement_interpretation_Tm_refine_de09779676242898794a0b057d5f5bb4" ], 0, - "398ab1855c136c98d0f5aad66a735451" + "54fba8e35135dc9e31c6482b195674de" ], [ "Layered.get_ctx", @@ -175,7 +175,7 @@ "typing_tok_Layered.Context@tok" ], 0, - "32a5d82d9c2f51a7ee7999024ccdec9d" + "bc2758d6f4acda316200998db89e2f98" ], [ "Layered.lift_pure_wp", @@ -196,7 +196,7 @@ "typing_Tm_abs_d0f415a5361a9d7988d8e425dc193472" ], 0, - "dd756f539a4a6803de415859d20dc431" + "75732f728e3226b18ad8b2531e90c005" ], [ "Layered.lift_pure", @@ -227,7 +227,7 @@ "typing_Tm_abs_efa2eac81cd2c08d7047b2fc27fb6578" ], 0, - "3c652054f44e5014a956556fbd28034d" + "b972adea37835748ae6a1443bc59ba2c" ], [ "Layered.test", @@ -254,7 +254,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "e199b0560f2e7c459f1abcd0a6fcd37f" + "c5233d9351d1d2fdd91b7ddb329f0b45" ], [ "Layered.main", @@ -283,7 +283,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "50676ae694aa5593265ae73aa617e7a3" + "05ea8da3141890cc3d9cbe105d0fc647" ] ] ] \ No newline at end of file diff --git a/test/.hints/Library.fst.hints b/test/.hints/Library.fst.hints index a56ffa876..7d9df7e34 100644 --- a/test/.hints/Library.fst.hints +++ b/test/.hints/Library.fst.hints @@ -82,7 +82,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "9c5d18c901fa49d93c7e73482ce5aa7f" + "ada01f63cdd9519648e5faac9aa31030" ] ] ] \ No newline at end of file diff --git a/test/.hints/LinkedList1.fst.hints b/test/.hints/LinkedList1.fst.hints index 6bc172237..185065a26 100644 --- a/test/.hints/LinkedList1.fst.hints +++ b/test/.hints/LinkedList1.fst.hints @@ -11,7 +11,7 @@ "refinement_interpretation_Tm_refine_a3ca1ff7326b0e9a8828d37afc6032a0" ], 0, - "73354acd04c8fa9e683611f1b01760a5" + "b5d305b2ecd3f7688c29bdb3318c48d8" ], [ "LinkedList1.__proj__Cons__item__data", @@ -23,7 +23,7 @@ "refinement_interpretation_Tm_refine_a3ca1ff7326b0e9a8828d37afc6032a0" ], 0, - "fac2d519c804ff52d4152e24b6b329fe" + "0bb02a53fe436ffe4600a0f60acc288c" ], [ "LinkedList1.well_formed", @@ -45,7 +45,7 @@ "well-founded-ordering-on-nat" ], 0, - "94739d4940a9cccddbaf0682717e9bd3" + "8e9b802555c485f52102d9204bf2e9e8" ], [ "LinkedList1.cons_nonzero_length", @@ -65,7 +65,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "bc731090e7c87219ad2657ffc4db71ec" + "d99197752b7b0ea886c11f3c1eed0bb0" ], [ "LinkedList1.length_functional", @@ -79,7 +79,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "c67c20f85a4a7fb91ff34d507135ec54" + "0b66ba70c6fe19c665d5215d1549f65d" ], [ "LinkedList1.length_functional", @@ -131,7 +131,7 @@ "well-founded-ordering-on-nat" ], 0, - "b74e30b6f7ead5f19bbeb0a903b31d9d" + "90157666e5bf1237effb87ee4b11b72d" ], [ "LinkedList1.live_nil", @@ -164,7 +164,7 @@ "typing_FStar.Monotonic.HyperStack.sel" ], 0, - "c2867b389c2dd675fb2b73d98a5bb727" + "33610d636ababf684e7137a2eea0eefc" ], [ "LinkedList1.live_cons", @@ -208,7 +208,7 @@ "typing_LinkedList1.__proj__Cons__item__next" ], 0, - "ff0be01e2a835ed27d576378a7b9b5b2" + "3ff6052946aa5df7a1bf48451be20fab" ], [ "LinkedList1.disjoint", @@ -222,7 +222,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "f5b4953b359aa6ab862285de4b263754" + "497b0ac12bc80c099658f6253852043d" ], [ "LinkedList1.disjoint_from_list", @@ -239,7 +239,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "00e3d0b3d02f165fd8d78c2414b1a63f" + "53d9074fe0510572808d4b50e9371ece" ], [ "LinkedList1.footprint", @@ -253,7 +253,7 @@ "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, - "bae8e116cc974cd451219d7ed713cc59" + "f80ca26f66a753cb991944fcee51dd13" ], [ "LinkedList1.footprint", @@ -268,7 +268,7 @@ "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, - "9477243fa061c26630ccd613f46dbd70" + "f34b967a661ec29175b1e3234dbf63a4" ], [ "LinkedList1.footprint", @@ -332,7 +332,7 @@ "well-founded-ordering-on-nat" ], 0, - "f126cb5162b782a567a72ab029a69508" + "f50ba0a2bb34a85ed6187cde93576098" ], [ "LinkedList1.modifies_disjoint_footprint", @@ -361,7 +361,7 @@ "typing_FStar.Monotonic.HyperStack.as_addr" ], 0, - "907498430ddf3b5b4afb693bd0e90b76" + "ea345cef8d446bbcf6bc2d30144e46ae" ], [ "LinkedList1.modifies_disjoint_footprint", @@ -483,7 +483,7 @@ "well-founded-ordering-on-nat" ], 0, - "4e7fb91192aca6ad86d83d82299727a2" + "a581875aa30fea38a76187260e2b9f9e" ], [ "LinkedList1.well_formed_distinct_lengths_disjoint", @@ -497,7 +497,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "7576884f976bf7fef6e5c2e9a36f3e29" + "f787f37ad656429fa7925ac48b81cba6" ], [ "LinkedList1.well_formed_distinct_lengths_disjoint", @@ -572,7 +572,7 @@ "typing_LinkedList1.disjoint", "well-founded-ordering-on-nat" ], 0, - "0b78e1d14aae9b94de8f002971bdd492" + "3f7d8ba4ea2d5572e763946373883875" ], [ "LinkedList1.well_formed_gt_lengths_disjoint_from_list", @@ -584,7 +584,7 @@ "refinement_interpretation_Tm_refine_5d2eff6d62a1f8cf87698b717524ff0a" ], 0, - "6837335e862a40038a4dbb9aa5aef20c" + "ba10ca24640ada6b1fa8c92b449437f9" ], [ "LinkedList1.well_formed_gt_lengths_disjoint_from_list", @@ -662,7 +662,7 @@ "well-founded-ordering-on-nat" ], 0, - "d636d946bec068978cd04c3a6bf5d3bd" + "bbc387185303afeb21b01f765786e9cb" ], [ "LinkedList1.well_formed_head_tail_disjoint", @@ -728,7 +728,7 @@ "typing_LinkedList1.footprint", "unit_typing" ], 0, - "a0eef73f93d2d8f63b674922e93fe38e" + "aaaaf1a57e4e649e16cfa37cc8676598" ], [ "LinkedList1.unused_in_well_formed_disjoint_from_list", @@ -740,7 +740,7 @@ "refinement_interpretation_Tm_refine_54fa2561676551e9325b5dabb22af904" ], 0, - "b9f69e20915df6655db5ac4ef3e29696" + "6403c5fbdc27df63ed75b5a69768975b" ], [ "LinkedList1.unused_in_well_formed_disjoint_from_list", @@ -826,7 +826,7 @@ "typing_LinkedList1.footprint", "well-founded-ordering-on-nat" ], 0, - "d998d137d978f68a9855eef16f0e848d" + "12bca59ae226061e7005afa721dea9e8" ], [ "LinkedList1.pop", @@ -838,7 +838,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "0baeb500781467194299c59b2191a076" + "2c9ba2881a4ed37642f4e893f7e1369e" ], [ "LinkedList1.pop", @@ -972,7 +972,7 @@ "typing_LowStar.Monotonic.Buffer.loc_addresses" ], 0, - "5a79153a6a5aa76246d644ed026491ce" + "45795d3da67cb60b5622f2a2696e9487" ], [ "LinkedList1.push", @@ -987,7 +987,7 @@ "typing_FStar.Ghost.reveal" ], 0, - "dc8ad682032ba71aa904b571381dc18c" + "d7609f04f395d8f388a21695695ac160" ], [ "LinkedList1.push", @@ -1142,7 +1142,7 @@ "typing_LowStar.Monotonic.Buffer.region_liveness_insensitive_locs" ], 0, - "23b3116cede7e00fa70ac651cd6e081d" + "97fd0add224eaa9cb9cec7b205db972f" ], [ "LinkedList1.length", @@ -1151,7 +1151,7 @@ 1, [ "@query" ], 0, - "1a9fb2993a6d43340687a1cbee96bbc1" + "d3a35a012a046ea4e0ba09c82cf9d1a7" ], [ "LinkedList1.length", @@ -1221,7 +1221,7 @@ "typing_FStar.UInt32.v" ], 0, - "8da5293980e8ccf4b4982a59a56e861e" + "3a4f045bccb785619c99721db719c660" ], [ "LinkedList1.main", @@ -1301,7 +1301,7 @@ "typing_FStar.StrongExcludedMiddle.strong_excluded_middle" ], 0, - "5c561311efff2834c8cd721ba6c60698" + "a5397abac9ab49e96b062f1827c020cf" ] ] ] \ No newline at end of file diff --git a/test/.hints/LinkedList2.fst.hints b/test/.hints/LinkedList2.fst.hints index c3cf62c93..73edde16c 100644 --- a/test/.hints/LinkedList2.fst.hints +++ b/test/.hints/LinkedList2.fst.hints @@ -17,7 +17,7 @@ "well-founded-ordering-on-nat" ], 0, - "b01077364f448dc8f418d918e203d766" + "cf1079c77c4b365f920f27c0d2a65084" ], [ "LinkedList2.cons_nonzero_length", @@ -43,7 +43,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "4083db35d2db1ffe4309938ac44f7e02" + "d249232df33c293dd30835a51849bf5e" ], [ "LinkedList2.length_functional", @@ -57,7 +57,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "4d5b67b8eddf0b0ff2a03b8a85bee224" + "ca2661b53c6779b216162ce54616c474" ], [ "LinkedList2.length_functional", @@ -92,7 +92,7 @@ "well-founded-ordering-on-nat" ], 0, - "7bddbf537dc6a9760d080a4a1520f91d" + "deae374d64b51d3fa8e09065a11fc641" ], [ "LinkedList2.live_nil", @@ -118,7 +118,7 @@ "typing_C.Nullity.is_null", "typing_FStar.Buffer.length" ], 0, - "53fab0744b5f96c8c4a9a6a9c83e4ce2" + "451c777fdb64c1e2080527f8edec1bfb" ], [ "LinkedList2.live_cons", @@ -161,7 +161,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "8d9fc497490f5f729900bf83f954e6b4" + "d14917564713da378e4c42f2efb2b41a" ], [ "LinkedList2.footprint", @@ -191,7 +191,7 @@ "well-founded-ordering-on-nat" ], 0, - "e2ca2a4c808bb1ce80d4cc0c481ccbfe" + "c752ccb3651c0afba2389aaab32fbd48" ], [ "LinkedList2.modifies_disjoint_footprint", @@ -203,7 +203,7 @@ "refinement_interpretation_Tm_refine_1a7a399b01bde27a9da612a33e4f7eff" ], 0, - "1f841df0c9f1471d530ac0a46f5c1c0b" + "36da4efecd59f7c4eeb6b98fb7ae2b71" ], [ "LinkedList2.modifies_disjoint_footprint", @@ -276,7 +276,7 @@ "typing_LinkedList2.footprint", "well-founded-ordering-on-nat" ], 0, - "5e1a8318fe90c6dca4fca66ffb69ae3b" + "b287747a6510c2a6e975e24de79ea6e9" ], [ "LinkedList2.well_formed_distinct_lengths_disjoint", @@ -290,7 +290,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "123fb73607e6c7e5400d1aef09f553bb" + "1c1d0ef3603c21f6f0fbb1a649f3cacc" ], [ "LinkedList2.well_formed_distinct_lengths_disjoint", @@ -345,7 +345,7 @@ "well-founded-ordering-on-nat" ], 0, - "cc92343db39c575dc18787f3901fb4c2" + "4015430e00260855ea09632360312a18" ], [ "LinkedList2.well_formed_gt_lengths_disjoint_from_list", @@ -357,7 +357,7 @@ "refinement_interpretation_Tm_refine_c81c79fe6d6f45972f0574fd4ca431db" ], 0, - "992d863fe2ef21186e7d002741644cae" + "a7d366caae6288111f30f29f26f9a415" ], [ "LinkedList2.well_formed_gt_lengths_disjoint_from_list", @@ -416,7 +416,7 @@ "typing_LinkedList2.footprint", "well-founded-ordering-on-nat" ], 0, - "b08460259939cffc6d12b50d60dcacdd" + "cdb3e247266651986dbec19df8f18cff" ], [ "LinkedList2.well_formed_head_tail_disjoint", @@ -462,7 +462,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "75a27db081445a7d64aa8731d1a75ef4" + "889a35e88ebfa5474ffc2ca6033f4bdc" ], [ "LinkedList2.unused_in_well_formed_disjoint_from_list", @@ -474,7 +474,7 @@ "refinement_interpretation_Tm_refine_71060f1b21c11070c805e09158382b50" ], 0, - "379f2bfdb36ec7e06923b6dd1dbe35db" + "4863ebe4532201fee983f1f7e2f2eeb4" ], [ "LinkedList2.unused_in_well_formed_disjoint_from_list", @@ -532,7 +532,7 @@ "typing_LinkedList2.footprint", "well-founded-ordering-on-nat" ], 0, - "9ecac29d1306444cda2893ba5dc0c3a7" + "8c35904c0f39439953453e5a7277a40f" ], [ "LinkedList2.pop", @@ -548,7 +548,7 @@ "refinement_interpretation_Tm_refine_610746826f8faaaa969bcb2a27509311" ], 0, - "3826f0761803b8d935c37fd917dafa20" + "f29c97167f52e0314dfb0f8dcbde20d1" ], [ "LinkedList2.pop", @@ -608,7 +608,7 @@ "typing_LinkedList2.footprint", "typing_LinkedList2.t" ], 0, - "fc2399c99fc2a4336e14243a3c08fa69" + "50cf66cf25cd8f722429daed488245c2" ], [ "LinkedList2.push", @@ -625,7 +625,7 @@ "typing_FStar.Ghost.reveal" ], 0, - "1c37cbb366ccd6f9432b758c4fd812bf" + "17d60f03e99ce027d6578cf1acc97527" ], [ "LinkedList2.push", @@ -758,7 +758,7 @@ "typing_LinkedList2.t" ], 0, - "23f92d204ee6baef566cc0653593451f" + "27fd11c5919546cae89e84c138b4a9ff" ], [ "LinkedList2.length", @@ -767,7 +767,7 @@ 1, [ "@query" ], 0, - "8494f32b345f9d87b318062462d43e7a" + "0158064e01873c62f6203bf024a2da5b" ], [ "LinkedList2.length", @@ -830,7 +830,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "d8a72e81bc3ad2d535291e8a4b832e9c" + "1df14eb508a80fa0b5ea3a6a6c674c68" ], [ "LinkedList2.main", @@ -910,7 +910,7 @@ "typing_FStar.UInt32.v", "typing_LinkedList2.t" ], 0, - "b64bb00fca13f03a4ac55c4e1aaa4ca2" + "e7198cfbadf02bd80a5da418a007ea27" ] ] ] \ No newline at end of file diff --git a/test/.hints/LinkedList3.fst.hints b/test/.hints/LinkedList3.fst.hints index c9a0f9a8f..d85d80ade 100644 --- a/test/.hints/LinkedList3.fst.hints +++ b/test/.hints/LinkedList3.fst.hints @@ -17,7 +17,7 @@ "well-founded-ordering-on-nat" ], 0, - "66607097be93f1eebd90d2a881e0230e" + "8f725bca8daf9809d072c79f44cb88ce" ], [ "LinkedList3.cons_nonzero_length", @@ -49,7 +49,7 @@ "typing_LowStar.Monotonic.Buffer.g_is_null" ], 0, - "7ad952093d693c2d885cb9389214ce93" + "a5871d303a99d8c749a60a787515a28e" ], [ "LinkedList3.length_functional", @@ -63,7 +63,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "fd3fed51638665088d5ce7946b51826e" + "8c0154900326fc69b2fd43173d252e79" ], [ "LinkedList3.length_functional", @@ -98,7 +98,7 @@ "well-founded-ordering-on-nat" ], 0, - "ecbb185c959cbdf15c823d4188b4e9a1" + "d2995da1821d1a2127b64d9ba706d08f" ], [ "LinkedList3.live_nil", @@ -130,7 +130,7 @@ "typing_LowStar.Monotonic.Buffer.length" ], 0, - "990ccbaedd2358eb345284210323f660" + "6ed9e06671865fc1e9fec9c922ff6f45" ], [ "LinkedList3.live_cons", @@ -175,7 +175,7 @@ "typing_LowStar.Monotonic.Buffer.get" ], 0, - "69302d9dc5f19c19f26e499f3fffecd4" + "a6f0418d90d93620a0737ce0ee4ed268" ], [ "LinkedList3.footprint", @@ -205,7 +205,7 @@ "well-founded-ordering-on-nat" ], 0, - "c452576ee068ed7d3f6e721af7345c9a" + "d331b4462c8efd1f95908f3facbfb16d" ], [ "LinkedList3.modifies_disjoint_footprint", @@ -217,7 +217,7 @@ "refinement_interpretation_Tm_refine_0b57dddc68898b9619355f21ce0c9e40" ], 0, - "16a8cab1e0c85eb001c83825d36f3234" + "496db2302dac8f6a4b7ecb4816a31b22" ], [ "LinkedList3.modifies_disjoint_footprint", @@ -268,7 +268,7 @@ "well-founded-ordering-on-nat" ], 0, - "d55d20b00f69e8f3fe677c7571663855" + "a2d70e26a5bb84858d790bdc60ee1b6f" ], [ "LinkedList3.well_formed_distinct_lengths_disjoint", @@ -282,7 +282,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "9439c3835ae9ca1847aee05c8decd6ae" + "d54bfe6c10ceebcc6eac5075d232ee72" ], [ "LinkedList3.well_formed_distinct_lengths_disjoint", @@ -340,7 +340,7 @@ "well-founded-ordering-on-nat" ], 0, - "dd7a98b004cfa566975f0fabb3425635" + "e95dcfa90edaf990d61ced5267c7cf8b" ], [ "LinkedList3.well_formed_gt_lengths_disjoint_from_list", @@ -352,7 +352,7 @@ "refinement_interpretation_Tm_refine_26e4ab6728a562f67991d35daefeca22" ], 0, - "b4304b1edf22a0a0095d7fcaadabfbf4" + "ce98cf09d44de6fe4f99066687958072" ], [ "LinkedList3.well_formed_gt_lengths_disjoint_from_list", @@ -409,7 +409,7 @@ "well-founded-ordering-on-nat" ], 0, - "5ade51cf336c8a207b11fcc9944f5403" + "e2397e81454315ef4640dae26bc56b28" ], [ "LinkedList3.well_formed_head_tail_disjoint", @@ -449,7 +449,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "303ee7ee39fb4c74d99a31ad601168f7" + "981e4923575ed67251275d6d321310f8" ], [ "LinkedList3.unused_in_well_formed_disjoint_from_list", @@ -461,7 +461,7 @@ "refinement_interpretation_Tm_refine_7861eb32c6fa156a1b5a5b9496f25f14" ], 0, - "1c5c7961d668825c4b04a144beb4f08b" + "284a2bb1b8996d864945eac5fbe07ab9" ], [ "LinkedList3.unused_in_well_formed_disjoint_from_list", @@ -536,7 +536,7 @@ "well-founded-ordering-on-nat" ], 0, - "232b20b77c13f4913dcc91ea42839ad3" + "45bf306aea9be7050ff2e67f1bd900e4" ], [ "LinkedList3.pop", @@ -551,7 +551,7 @@ "refinement_interpretation_Tm_refine_849dd87a0704847cf995021569fd0af6" ], 0, - "eb27a98a4155c99650adeb79b77029bf" + "1e4a6d1d0bd386cf281e4667339cc091" ], [ "LinkedList3.pop", @@ -606,7 +606,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "cf6b6e05e2044f4ba9d3599a85825826" + "a7a4c8c7d94769d75fd16858e466da43" ], [ "LinkedList3.push", @@ -623,7 +623,7 @@ "typing_FStar.Ghost.reveal" ], 0, - "6a82dac07f91f15ca5df6949286384ae" + "649ff50937f7e8b4fcdd9ce6f209da29" ], [ "LinkedList3.push", @@ -724,7 +724,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "d9521e11cc670fae3c399ef67b036938" + "aa14b011b2e46dec3bdfc1f1c4727a35" ], [ "LinkedList3.length", @@ -733,7 +733,7 @@ 1, [ "@query" ], 0, - "6b637f719aeda6ac6976e169c3e9147c" + "8b7832f7f44ab9de2f341f9e8c522ce3" ], [ "LinkedList3.length", @@ -789,7 +789,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "be0036358012c7aefdf2c2203d5374c2" + "d165fd07b408b6abc425db7b1205f332" ], [ "LinkedList3.main", @@ -861,7 +861,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "b8b7c73195fbb2e88eb04f8ea1cd92fd" + "4ce6011c5bc0f6b5695ba6cce7694e12" ] ] ] \ No newline at end of file diff --git a/test/.hints/LinkedList4.fst.hints b/test/.hints/LinkedList4.fst.hints index 1ea300f50..26805fd03 100644 --- a/test/.hints/LinkedList4.fst.hints +++ b/test/.hints/LinkedList4.fst.hints @@ -13,7 +13,7 @@ "projection_inverse_BoxInt_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "940825637c6569a00bd291c8b389236f" + "2df8614eae5a8fc9867ba61305a569e2" ], [ "LinkedList4.length_functional", @@ -53,7 +53,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "dfe07c0c7a9a87f0064e4892ad4f4a49" + "b0f5001bf74f9dca3ea9733dc5807324" ], [ "LinkedList4.footprint", @@ -80,7 +80,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "2a15be6d3cb523735b7477cb449d7f90" + "0df441d6462665daaa1544248017f75a" ], [ "LinkedList4.modifies_disjoint_footprint", @@ -92,7 +92,7 @@ "refinement_interpretation_Tm_refine_d727ca06ab1d2e19ab86ac8a0ebec43a" ], 0, - "ee8fbc8dc464a067633f68ecebcc071a" + "cf9b538fee40e42bde6c77d6078a57e5" ], [ "LinkedList4.modifies_disjoint_footprint", @@ -146,7 +146,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "c3bbba7129e416d27cab92f72ae82dcb" + "f665621d9a69efeafb656284e80b511b" ], [ "LinkedList4.well_formed_distinct_lengths_disjoint", @@ -160,7 +160,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "60a622654ce03a51f0c1e0ca80b073cf" + "781a7b1647bc9e66079a5fdeaf5a4b28" ], [ "LinkedList4.well_formed_distinct_lengths_disjoint", @@ -214,7 +214,7 @@ "well-founded-ordering-on-nat" ], 0, - "493a6b9e54f7ff6519878b6e43ae59e9" + "c9d74e2036d51208110103f53a4f546e" ], [ "LinkedList4.well_formed_gt_lengths_disjoint_from_list", @@ -226,7 +226,7 @@ "refinement_interpretation_Tm_refine_7a66ed8ab1149aa32c4f07ae5b36b85c" ], 0, - "1ede2420067dd5fe3f27a15e97212067" + "c015065a974235b40152e5313b7c6ea3" ], [ "LinkedList4.well_formed_gt_lengths_disjoint_from_list", @@ -294,7 +294,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "0e3ef098db62277a4d4f770cc9ea2315" + "5eb75b496419b69b14d8bf57ec3e5cde" ], [ "LinkedList4.well_formed_head_tail_disjoint", @@ -327,7 +327,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "f9f6289eb372741dfa95bf7d67b8304b" + "37543ba34d20d5afb1b4b9330d21e2b4" ], [ "LinkedList4.unused_in_well_formed_disjoint_from_list", @@ -339,7 +339,7 @@ "refinement_interpretation_Tm_refine_d06d91ecfb2529ebdc073668be613711" ], 0, - "5cc2e4a7a6d5a820e2ca4589dc5c208b" + "d6941a67549a471342208ec695df6470" ], [ "LinkedList4.unused_in_well_formed_disjoint_from_list", @@ -418,7 +418,7 @@ "typing_Prims.uu___is_Nil" ], 0, - "152ff60ed4ccb25ab44031052a4e5d3b" + "43374af4d3adcdc0b461a17264b0e03a" ], [ "LinkedList4.pop", @@ -433,7 +433,7 @@ "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e" ], 0, - "8df7ecc86345219396b6b47f6f1876fe" + "0abd93fcaaf0409cd49e67820c8e54b1" ], [ "LinkedList4.pop", @@ -488,7 +488,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "3f930311adcecd59ce701b76dc6f82b6" + "13b2dbbcdeab1d74f2e1560d0eaf7783" ], [ "LinkedList4.push", @@ -502,7 +502,7 @@ "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e" ], 0, - "1130039ef8b0aa23e5a77bf6efc25a06" + "9ab270f818246d713cea18e12264eb09" ], [ "LinkedList4.push", @@ -612,7 +612,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "0c7c62d7dd11be12883b12d4e3feabf2" + "6032ffaca364f2c99edd77ce6e74d43f" ], [ "LinkedList4.length", @@ -621,7 +621,7 @@ 1, [ "@query" ], 0, - "5cdd03070b1e0cb5cb69b8b5e012bb90" + "9efed31be185ad2be858c07b9a4d57db" ], [ "LinkedList4.length", @@ -682,7 +682,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "92e60b546e112bf1d7c15f1620509a7d" + "40d7de54f48e1f18169e358edab8ba63" ], [ "LinkedList4.main", @@ -761,7 +761,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "bdc36bf37553c199e262b95c0b9c5270" + "cab436ad5ef6cd16055c74a6767a1fa9" ] ] ] \ No newline at end of file diff --git a/test/.hints/Loops.fst.hints b/test/.hints/Loops.fst.hints index 09b0ef72a..27c14b551 100644 --- a/test/.hints/Loops.fst.hints +++ b/test/.hints/Loops.fst.hints @@ -86,7 +86,7 @@ "typing_LowStar.Monotonic.Buffer.length" ], 0, - "882d3eb4968aed284e5706ec82024021" + "e339ae51acc5fa7c8478fdb2c6fa7bef" ], [ "Loops.sum_to_n_buf", @@ -190,7 +190,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "b731aab4ed9d43e4f98ba6e3e9d8a4c4" + "fa8a142688c1571c35f0657d3cbdd3ca" ], [ "Loops.count_to_n", @@ -276,7 +276,7 @@ "typing_LowStar.Monotonic.Buffer.length" ], 0, - "72d273c1205b679a0b02cd0cecb01717" + "c394fef298f49ad9a24c8925ce86e998" ], [ "Loops.wait_for_false", @@ -306,7 +306,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "1d90e5f9dfbbd8c265a03c28ceb199f3" + "c15f3f552efe4935a19b5e656dd81dc5" ], [ "Loops.test_pre", @@ -318,7 +318,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "2d4194f442f9e0d89192d0909e96de2a" + "589fd6506e70fd5c0c00f596d872b611" ], [ "Loops.test_post", @@ -330,7 +330,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "4eff5a1fa3a9478a7b66642f863c032d" + "16074afe64aeb03ff68c28f57ed3d503" ], [ "Loops.square_while", @@ -460,7 +460,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "9b53e5a73cc25124e6b0c61897cff417" + "ae4611e84dc8064f67d9cdc6900251b3" ], [ "Loops.test_map", @@ -562,7 +562,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "c37c6ef6cff22b023452e694b992085c" + "8f036ffec9262ad5e1ea013d39cb3fa7" ], [ "Loops.main", @@ -661,7 +661,7 @@ "typing_LowStar.Monotonic.Buffer.len", "typing_Prims.pow2" ], 0, - "7fb15fc0726643bd72b39f8f93b400f3" + "cfeb690c3aeddbf3abd5c73866671e7c" ] ] ] \ No newline at end of file diff --git a/test/.hints/ML16.fst.hints b/test/.hints/ML16.fst.hints index 9dcefb417..f33f4dff7 100644 --- a/test/.hints/ML16.fst.hints +++ b/test/.hints/ML16.fst.hints @@ -88,7 +88,7 @@ "typing_FStar.UInt.fits", "typing_FStar.UInt32.v" ], 0, - "b3d49a5619d67c5ff0656ae3442bafe6" + "db6cf3d4386af07984d51d8af31ccc3d" ], [ "ML16.test2", @@ -152,7 +152,7 @@ "typing_FStar.UInt32.v" ], 0, - "0a0404cfa8d313b75629d7ce59de3c53" + "70c84a1ac0989a8018c766014e95836a" ], [ "ML16.main", @@ -229,7 +229,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "eb438ccb45842f31f668032731a77144" + "c3780655fa538383561f9d26a9661148" ] ] ] \ No newline at end of file diff --git a/test/.hints/Macro.fst.hints b/test/.hints/Macro.fst.hints index 7f7a3b4ef..8a72d7abe 100644 --- a/test/.hints/Macro.fst.hints +++ b/test/.hints/Macro.fst.hints @@ -24,7 +24,7 @@ "typing_Prims.pow2" ], 0, - "e7397cf286b350e0dbc10223418add96" + "a03b2a07697910f35d55e840538b5af0" ] ] ] \ No newline at end of file diff --git a/test/.hints/MallocFree.fst.hints b/test/.hints/MallocFree.fst.hints index 8adaf1828..bbb90b731 100644 --- a/test/.hints/MallocFree.fst.hints +++ b/test/.hints/MallocFree.fst.hints @@ -82,7 +82,7 @@ "typing_FStar.UInt32.t", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "b4a94514cb957ce0a9b9b743e5f6b36f" + "c34766821fb882e0caa28e18b2d8854c" ] ] ] \ No newline at end of file diff --git a/test/.hints/MemCpy.fst.hints b/test/.hints/MemCpy.fst.hints index 9b42acb28..272bda775 100644 --- a/test/.hints/MemCpy.fst.hints +++ b/test/.hints/MemCpy.fst.hints @@ -37,7 +37,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.cons" ], 0, - "02de6978f0c3c184ed974cb44f9e49ae" + "f596a1de11704c747f95d8f0b9d12fcd" ], [ "MemCpy.memcpy", @@ -46,7 +46,7 @@ 0, [ "@query" ], 0, - "51e777f66cc3ea7cde7005b7d2064f37" + "5eec95effb2ca37572c455de18cb4484" ], [ "MemCpy.memcpy", @@ -100,7 +100,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "98af73cd51248ca47ee7550c410d8702" + "8a83f266262c9f0eaf6b77b4ff7cd3dc" ], [ "MemCpy.main", @@ -197,7 +197,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "0014df5f6f6b2e52d14d8a43a96e8556" + "284a77b46b59adbc069440606ede395c" ] ] ] \ No newline at end of file diff --git a/test/.hints/MemCpyModel.fst.hints b/test/.hints/MemCpyModel.fst.hints index 05597486b..71ea6c349 100644 --- a/test/.hints/MemCpyModel.fst.hints +++ b/test/.hints/MemCpyModel.fst.hints @@ -39,7 +39,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice" ], 0, - "dc430622fd09b4e362e3fa82892e0a8f" + "967461cb99a4e7e1bda6723a2185afa1" ], [ "MemCpyModel.memcpy", @@ -125,7 +125,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "3e34c2a965692cf72ab578728e31193f" + "25aa4b6f0394581901ceff561a20c653" ] ] ] \ No newline at end of file diff --git a/test/.hints/Mini.fst.hints b/test/.hints/Mini.fst.hints index 4da03755e..a40f531f9 100644 --- a/test/.hints/Mini.fst.hints +++ b/test/.hints/Mini.fst.hints @@ -13,7 +13,7 @@ "refinement_interpretation_Tm_refine_8fd6f269a3ccd743e70c909024d76576" ], 0, - "2c5b232ecbee39c5084541d626d48bd3" + "f47356adfab8ea895f3352f5c39ab3d5" ], [ "Mini.g", @@ -39,7 +39,7 @@ "typing_FStar.UInt32.v" ], 0, - "1bf6e09551b9c6c92bffa1a4c4ed659c" + "d43469af1d0520f64f52022e6a8d28c7" ] ] ] \ No newline at end of file diff --git a/test/.hints/MutRec.fst.hints b/test/.hints/MutRec.fst.hints index fe41e3644..9335db245 100644 --- a/test/.hints/MutRec.fst.hints +++ b/test/.hints/MutRec.fst.hints @@ -13,7 +13,7 @@ "refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051" ], 0, - "215245c2fc6b7fabfbe5cd5433b3aa7b" + "a332afc5ea1fef38fd659bab346c753f" ], [ "MutRec.f", @@ -67,7 +67,7 @@ "typing_FStar.Set.singleton" ], 0, - "f066c888d7ee8289066011e46d6364ce" + "6d34b2dcba1b2dda9124fcd47ec35a8d" ] ] ] \ No newline at end of file diff --git a/test/.hints/NameCollisionHelper.fst.hints b/test/.hints/NameCollisionHelper.fst.hints index aed02005e..f37f251ec 100644 --- a/test/.hints/NameCollisionHelper.fst.hints +++ b/test/.hints/NameCollisionHelper.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "1823e7a6fa196c37b68d5e85fbff9b0e" + "287fcab1c6c20cf066af42624e90849e" ] ] ] \ No newline at end of file diff --git a/test/.hints/NoExtract.fst.hints b/test/.hints/NoExtract.fst.hints index f321173b2..9eb67345a 100644 --- a/test/.hints/NoExtract.fst.hints +++ b/test/.hints/NoExtract.fst.hints @@ -14,7 +14,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "fa031a0423c38d051237c032c5f2b262" + "08a5a9fb848c15c414ef1a41eaf5c44b" ], [ "NoExtract.b", @@ -29,7 +29,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "8b618c480057392a9c4cb41678312e03" + "16115c464574cde344b9355439e53058" ] ] ] \ No newline at end of file diff --git a/test/.hints/NoShadow.fst.hints b/test/.hints/NoShadow.fst.hints index e38b7ada7..fb0981fd3 100644 --- a/test/.hints/NoShadow.fst.hints +++ b/test/.hints/NoShadow.fst.hints @@ -22,7 +22,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "bcf3d74bc2875bd7b9d6ecb47784246f" + "56e8b0385088ed8a7285cdf3c586ca57" ], [ "NoShadow.g", @@ -45,7 +45,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "68704b88b10aeb6be07a5d8725299bbb" + "aa85073d18a2c0e36da434df2474b0ee" ], [ "NoShadow.b", @@ -66,7 +66,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "e1567f6f10ee468a16bdedd7e3791b70" + "6d23b403c3e9debbeb6091e41753e5d7" ], [ "NoShadow.h", @@ -121,7 +121,7 @@ "typing_FStar.Set.singleton" ], 0, - "7dcdb523d1a5134a1da9749dea170cb0" + "d90d07303c08de2777fa20e97715311e" ], [ "NoShadow.main", @@ -146,7 +146,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "b3efe5dbe8af9322b1c0699510566269" + "a9bfffe4b2ddfc6d59414fce6d5dc2f6" ] ] ] \ No newline at end of file diff --git a/test/.hints/Null.fst.hints b/test/.hints/Null.fst.hints index ae92f48e5..44bdac80d 100644 --- a/test/.hints/Null.fst.hints +++ b/test/.hints/Null.fst.hints @@ -26,7 +26,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "bce08780307e03e9c96d72a7261d9e31" + "8aeb1d425998f7fdaa6866beb7e837a8" ], [ "Null.main", @@ -45,7 +45,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "1aa23893e0ccbd90d13ea9ea58c409be" + "9e33d23adad250741e4a59acf22f8fe4" ] ] ] \ No newline at end of file diff --git a/test/.hints/OptimizedOption.fst.hints b/test/.hints/OptimizedOption.fst.hints index 1a8d1509a..181c98e23 100644 --- a/test/.hints/OptimizedOption.fst.hints +++ b/test/.hints/OptimizedOption.fst.hints @@ -15,7 +15,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "f4ce313e51a4f52df533c8dbe5be84bd" + "947cae649a44c80204b64ed625a670bb" ] ] ] \ No newline at end of file diff --git a/test/.hints/ParamAbbrev.fst.hints b/test/.hints/ParamAbbrev.fst.hints index 58bedd6a0..10fbc2344 100644 --- a/test/.hints/ParamAbbrev.fst.hints +++ b/test/.hints/ParamAbbrev.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "7b75d9abd5ffa2c051a7058b01ed7cf6" + "71c3163efb19d973af4924dfffdea531" ], [ "ParamAbbrev.g", @@ -42,7 +42,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "b6c11c747b12cc70d4b38c096f3fa2a6" + "bc1974215c6b79ff1e10d29fad2e6a30" ], [ "ParamAbbrev.touch", @@ -63,7 +63,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "7e6a01e53e75bd3235d6609a50e916f9" + "b3a7c377606713b96f3ce8fc9b4bde6c" ], [ "ParamAbbrev.main", @@ -89,7 +89,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "4f7ebc99bdb99ef4dbbad6ad5ade80d6" + "c3718e06c6782e34df9baf7e242ddff2" ] ] ] \ No newline at end of file diff --git a/test/.hints/Parameterized.fst.hints b/test/.hints/Parameterized.fst.hints index a87088f14..037aca8f3 100644 --- a/test/.hints/Parameterized.fst.hints +++ b/test/.hints/Parameterized.fst.hints @@ -13,7 +13,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "1e5f9cf52e044764d175bf41dfc47bb3" + "812571cfc9e0b9b4479b7831af3231d3" ], [ "Parameterized.get", @@ -27,7 +27,7 @@ "refinement_interpretation_Tm_refine_7661503e258cd8eb6e95252fc3102979" ], 0, - "99382dde0a9570eac4ad66b0ffeed30b" + "828b5b4c703f9975c4bf849cad99acd6" ], [ "Parameterized.main", @@ -75,7 +75,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "135f644e2ee1a5f5170f0a8a37165cf0" + "e0f37ae5a3b8459824ca1a6f4e7da035" ] ] ] \ No newline at end of file diff --git a/test/.hints/PatternAny.fst.hints b/test/.hints/PatternAny.fst.hints index 373fd77e7..b3da07881 100644 --- a/test/.hints/PatternAny.fst.hints +++ b/test/.hints/PatternAny.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query", "assumption_PatternAny.role__uu___haseq" ], 0, - "ec18959ca7d323a8178420cdda0bc4b5" + "7e8d8e1691c75c757e8249e6c128527e" ] ] ] \ No newline at end of file diff --git a/test/.hints/PolyComp.fst.hints b/test/.hints/PolyComp.fst.hints index 2b9fa3760..1a2d3b762 100644 --- a/test/.hints/PolyComp.fst.hints +++ b/test/.hints/PolyComp.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "bedab1a78acf1613ac70b88d4dd0f322" + "c79efc6f5700833d43a876c6b6e8c71c" ], [ "PolyComp.__proj__B__item___0", @@ -20,7 +20,7 @@ "refinement_interpretation_Tm_refine_ace5180d8b9c0680cccc5c56d8744ca7" ], 0, - "edec1bd862f7bd8d635364697a50f526" + "38958a215415248e04d2362b4a3b3cf4" ], [ "PolyComp.one_t", @@ -33,7 +33,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "8f19cf4b5e88f2fcb05ec728dc03f6b5" + "62fe1c1a8b80f7fd0c83a71a6706c0ed" ], [ "PolyComp.another_t", @@ -46,7 +46,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "67bdaefcd870de59f5bfd558374818f4" + "4c7eefbec0f33f88a21cc4ad16b194ef" ], [ "PolyComp.yet_another_t", @@ -59,7 +59,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "8b519ba3b50fa686a06d1ce9a201ecd2" + "3b4b1f294c04464573e787c51c0b3551" ], [ "PolyComp.main", @@ -86,7 +86,7 @@ "typing_FStar.Int32.t", "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "7cded1e75dcfa5b6e266ad43d102a27c" + "e837002963f8e3e4ba5d846d170a07f8" ] ] ] \ No newline at end of file diff --git a/test/.hints/Polymorphic.fst.hints b/test/.hints/Polymorphic.fst.hints index dae0b0b94..a456b706c 100644 --- a/test/.hints/Polymorphic.fst.hints +++ b/test/.hints/Polymorphic.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "d663fc097c625011ce74fde7e01f31de" + "8e6771ef1fe87df1763fc21945c0ecb1" ], [ "Polymorphic.main", @@ -46,7 +46,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "2ae0dd50b372c3d2584f0ea879d2838d" + "dfcad12e400e0ea525495eb3e5593903" ] ] ] \ No newline at end of file diff --git a/test/.hints/Printf.fst.hints b/test/.hints/Printf.fst.hints index 9f6dbd0e3..aa2f0cf56 100644 --- a/test/.hints/Printf.fst.hints +++ b/test/.hints/Printf.fst.hints @@ -85,7 +85,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "0b2a76ec828a4e24f0da0296e17e8c9a" + "191ee467c6c32b73d0f0353dce076421" ] ] ] \ No newline at end of file diff --git a/test/.hints/Private.fst.hints b/test/.hints/Private.fst.hints index f69a3d318..0634e7766 100644 --- a/test/.hints/Private.fst.hints +++ b/test/.hints/Private.fst.hints @@ -47,7 +47,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "785313897fdbf1fd7f7d62d6180c9162" + "a2dfe6abab68018d1a6e0a6cdf7d03e1" ] ] ] \ No newline at end of file diff --git a/test/.hints/PrivateInclude1.fst.hints b/test/.hints/PrivateInclude1.fst.hints index aadc37441..48441351d 100644 --- a/test/.hints/PrivateInclude1.fst.hints +++ b/test/.hints/PrivateInclude1.fst.hints @@ -26,7 +26,7 @@ "typing_Prims.pow2", "typing_PrivateInclude1.foobar" ], 0, - "2ffcc5fdb860f0e0d0f8c746cf564680" + "180261b8afbe79d504a6cabdea1eed84" ] ] ] \ No newline at end of file diff --git a/test/.hints/PrivateInclude2.fst.hints b/test/.hints/PrivateInclude2.fst.hints index 43826de54..1d9a9335c 100644 --- a/test/.hints/PrivateInclude2.fst.hints +++ b/test/.hints/PrivateInclude2.fst.hints @@ -21,7 +21,7 @@ "typing_FStar.Int32.v", "typing_PrivateInclude1.f", "unit_typing" ], 0, - "9a11a76308f824e34167ed5f02e3b1ba" + "2c028a84fe542461ed6b6ec69ba4f672" ] ] ] \ No newline at end of file diff --git a/test/.hints/PushPop.fst.hints b/test/.hints/PushPop.fst.hints index 42539da60..5cd932bfa 100644 --- a/test/.hints/PushPop.fst.hints +++ b/test/.hints/PushPop.fst.hints @@ -44,7 +44,7 @@ "typing_FStar.Set.union" ], 0, - "28a427cd45d289299c98ea253e3bab2b" + "276373c23aae6a90e8fbb5a69150dc3b" ], [ "PushPop.main", @@ -76,7 +76,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "8dbcb4f4c2ed9d4c54ef151205d9bb4a" + "762a1e1d709997a0703f3e4ec9f262ca" ] ] ] \ No newline at end of file diff --git a/test/.hints/RecordTypingLimitation.fst.hints b/test/.hints/RecordTypingLimitation.fst.hints index 5d1f0550f..fdd9d125c 100644 --- a/test/.hints/RecordTypingLimitation.fst.hints +++ b/test/.hints/RecordTypingLimitation.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "ad9c5e761217b92cba4e2c85c136589d" + "f7746de895a48119706cd4017eac9575" ] ] ] \ No newline at end of file diff --git a/test/.hints/Recursive.fst.hints b/test/.hints/Recursive.fst.hints index 57ee158b5..a8b56c16a 100644 --- a/test/.hints/Recursive.fst.hints +++ b/test/.hints/Recursive.fst.hints @@ -12,7 +12,7 @@ "refinement_interpretation_Tm_refine_fe78738bbffac158d58c53f89b03a1b7" ], 0, - "3a4be5050fc30974cc25744f7a24023d" + "e5fcb8e23da8bd729d3a8d0486a83708" ], [ "Recursive.__proj__Cons__item__next", @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_fe78738bbffac158d58c53f89b03a1b7" ], 0, - "488524acf079b906b5a9900d03576392" + "074ce697a6a67e1841b006df9250bdcd" ] ] ] \ No newline at end of file diff --git a/test/.hints/RecursivePoly.fst.hints b/test/.hints/RecursivePoly.fst.hints index d7f357e27..56e08774f 100644 --- a/test/.hints/RecursivePoly.fst.hints +++ b/test/.hints/RecursivePoly.fst.hints @@ -12,7 +12,7 @@ "refinement_interpretation_Tm_refine_ec0be7ef8d42c8c1f9f883ea579d9abf" ], 0, - "f2c833573bed49c31c3f268634639887" + "88c14cb009190516a76357b3940e44b8" ], [ "RecursivePoly.__proj__Cons__item__next", @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_ec0be7ef8d42c8c1f9f883ea579d9abf" ], 0, - "128a324450312da3c13dc1c90e9d6468" + "06f02987ae0bc407d3e0aba83268df39" ], [ "RecursivePoly.f", @@ -46,7 +46,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "bfd72db7210caa04d20c664bcb9e3f78" + "5cf65f268797f61e4b965a2df1cb40b1" ], [ "RecursivePoly.g", @@ -67,7 +67,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "c1d238ea979cacfbbe5672a868280a54" + "6b9b7010b4f6570d133cbe2ca9e54ecd" ] ] ] \ No newline at end of file diff --git a/test/.hints/Renaming.fst.hints b/test/.hints/Renaming.fst.hints index 231c4db54..bcc4776c3 100644 --- a/test/.hints/Renaming.fst.hints +++ b/test/.hints/Renaming.fst.hints @@ -15,7 +15,7 @@ "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2" ], 0, - "dfb191fd250974572286612bb7db3992" + "4abd2be5207594c9e7a981a692c26785" ], [ "Renaming.main", @@ -32,7 +32,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "5024d35e98da56be26869956d4f9c9fe" + "49e414895d988416da1b7ec2b2cffddf" ] ] ] \ No newline at end of file diff --git a/test/.hints/RingBuffer.fst.hints b/test/.hints/RingBuffer.fst.hints index b49e7664d..8aba01cab 100644 --- a/test/.hints/RingBuffer.fst.hints +++ b/test/.hints/RingBuffer.fst.hints @@ -12,7 +12,7 @@ "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e" ], 0, - "e7a435bf8d925912ab38dd104e2d1e29" + "962c4b6f966c5cd094896c06fcf48b3d" ], [ "RingBuffer.well_formed_f", @@ -24,7 +24,7 @@ "haseqRingBuffer_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d" ], 0, - "61c707319ff625676adc25c65f33b9c4" + "4cb99aa5b37f08322e42c7d2dd074ffd" ], [ "RingBuffer.next", @@ -51,7 +51,7 @@ "typing_FStar.UInt32.v" ], 0, - "7efa0d7086aa8e7dd1eb562022be01d5" + "d0e6dfda597efd205a3ed5b1c1cae6f0" ], [ "RingBuffer.prev", @@ -77,7 +77,7 @@ "typing_FStar.UInt32.v" ], 0, - "4cc67f587f13fdf290affbb7af39355d" + "82c3ee665f09dcef0c22e1603362be22" ], [ "RingBuffer.remaining_space", @@ -113,7 +113,7 @@ "typing_RingBuffer.__proj__Mkt__item__total_length" ], 0, - "11e0d8b960adbe85e6e0476fbb291bc2" + "9d689aaf326538aa06beee1218752cb4" ], [ "RingBuffer.as_list_f", @@ -161,7 +161,7 @@ "well-founded-ordering-on-nat" ], 0, - "87a4dca498c852e198e0117f7d86732a" + "7ddc4d4fe70cc2e52ade9b63f744aa4b" ], [ "RingBuffer.as_list_f", @@ -203,7 +203,7 @@ "well-founded-ordering-on-nat" ], 0, - "d894f557b430446536e8ed571b073060" + "e802578ed18bb5d7be78ab5927df242e" ], [ "RingBuffer.seq_update_unused_preserves_list", @@ -227,7 +227,7 @@ "typing_FStar.UInt32.v" ], 0, - "d0b7f824d2f66411169378869f436004" + "512db360a5d163a4898fc0bbffb41e35" ], [ "RingBuffer.seq_update_unused_preserves_list", @@ -283,7 +283,7 @@ "well-founded-ordering-on-nat" ], 0, - "6c1d7561574b65d346af007a405c97e2" + "d87ea422f26420e4d033acb6ac4fbcc7" ], [ "RingBuffer.as_list", @@ -300,7 +300,7 @@ "haseqRingBuffer_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d" ], 0, - "a2973f2769dbdca0a139ab697c464525" + "8dbf246eea2be2eacd5a951b176272a5" ], [ "RingBuffer.pop", @@ -395,7 +395,7 @@ "typing_RingBuffer.as_list", "typing_RingBuffer.remaining_space" ], 0, - "7fcbe92eac244bfe4221e15c7ac24ac0" + "de635a0879b49cc2ad6eac48e861bc9e" ], [ "RingBuffer.push", @@ -501,7 +501,7 @@ "typing_RingBuffer.prev", "typing_RingBuffer.remaining_space" ], 0, - "cbdb377f392ecf937bc129eec0dc090e" + "21d622120346e240eaa348ceab155702" ], [ "RingBuffer.one_past_last", @@ -531,7 +531,7 @@ "typing_FStar.UInt32.v" ], 0, - "7be43f53cce8aeb7abd01723c22ab59b" + "5aae88bf4ba74be7c9135fdbacdb48fc" ], [ "RingBuffer.as_list_append_one", @@ -561,7 +561,7 @@ "typing_RingBuffer.one_past_last" ], 0, - "93586babfe13ca259d6c34c1d95886a9" + "1e66f7330365ab73f698aeb09cdfb9f0" ], [ "RingBuffer.as_list_append_one", @@ -628,7 +628,7 @@ "well-founded-ordering-on-nat" ], 0, - "90eb51e9d329ddc48df2e1aa88baa7fa" + "20d6fc8ee41f445e9123caa83411def9" ], [ "RingBuffer.push_back", @@ -717,7 +717,7 @@ "typing_RingBuffer.as_list_f", "typing_RingBuffer.remaining_space" ], 0, - "19f439445944eb715783f190e69d430f" + "4a93e2664ddcbc58b3acae8c9df8cf13" ], [ "RingBuffer.as_list_minus_one", @@ -752,7 +752,7 @@ "typing_RingBuffer.prev" ], 0, - "a748da4b319cca9447509aa5fdcae862" + "bf0e651509aa1534f1adcfecd9758a69" ], [ "RingBuffer.as_list_minus_one", @@ -822,7 +822,7 @@ "typing_RingBuffer.prev", "well-founded-ordering-on-nat" ], 0, - "8758d4c0938df9c3d6c63eb03e3869a7" + "c8808267fa03b2fe30a336c826144783" ], [ "RingBuffer.pop_back", @@ -910,7 +910,7 @@ "typing_RingBuffer.as_list_f", "typing_RingBuffer.remaining_space" ], 0, - "298e694cc83c728a24f172dc0656a3c3" + "76157b46d08f8173c80d168ff8eeb265" ], [ "RingBuffer.create", @@ -1007,7 +1007,7 @@ "typing_RingBuffer.remaining_space" ], 0, - "5f308a83df50dccebda83a477a8ee330" + "bba7de640700834c21abff796afaec85" ], [ "RingBuffer.main", @@ -1121,7 +1121,7 @@ "typing_RingBuffer.space_left" ], 0, - "1af105724cb1ff91ef9a612331c84b87" + "11af43ab7a861cefa603a7d0663ca07d" ] ] ] \ No newline at end of file diff --git a/test/.hints/Scope.fst.hints b/test/.hints/Scope.fst.hints index 045759237..a263661c5 100644 --- a/test/.hints/Scope.fst.hints +++ b/test/.hints/Scope.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "9466c0eb4cce1e1363b105129686a74c" + "d5ff08688fa1af90a5cc02312f9900c6" ], [ "Scope.main", @@ -117,7 +117,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "7b569629c54e07fe3a9015a8be5ecbb2" + "07b69cfe1dcfd9080811fc16f90e8baa" ] ] ] \ No newline at end of file diff --git a/test/.hints/Server.fst.hints b/test/.hints/Server.fst.hints index ab73b6166..5c312b985 100644 --- a/test/.hints/Server.fst.hints +++ b/test/.hints/Server.fst.hints @@ -16,7 +16,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "df54b3ccc469383571a008571a0b7b25" + "ac4ee6f597c256275bd4fb4edef44259" ], [ "Server.bufstrcmp", @@ -37,7 +37,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "d771db09da59d4469320137864495fc3" + "50abc70e0c551554e2b4e49c119f2762" ], [ "Server.bufstrcmp", @@ -193,7 +193,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "6d5712125bc95f092aa21586cad4d532" + "8e56d09a94e44a4f4da8ce5531bbb7ca" ], [ "Server.bufstrcpy", @@ -219,7 +219,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "8b3d271cc729137c8fb06e50081567f8" + "db348e4d48ae991f4c009e55aec8bfb4" ], [ "Server.bufcpy", @@ -243,7 +243,7 @@ "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder" ], 0, - "2a2b8b81b22af23ff8012e1d2057205f" + "ed309bd2d06528c0b454df264b12977c" ], [ "Server.respond", @@ -297,7 +297,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "55c12a6bb02f6131228f410d1074f8b3" + "dff7a70cbf555a6499431eb54227143a" ], [ "Server.respond_index", @@ -409,7 +409,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "0d93d7860570c3f47a2ff9853b5fedd0" + "6143eb77c71b53265f4f5578cea481d2" ], [ "Server.respond_stats", @@ -540,7 +540,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "110047263bd5230bd261f5346f288ee7" + "0d674dc55b3432ea42dfaf046ec29aad" ], [ "Server.respond_404", @@ -673,7 +673,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "2b30d80969e982a0f9674bd691a0d2c2" + "bcd91ffc41e934443c94f1f4270ffcdb" ], [ "Server.server", @@ -812,7 +812,7 @@ "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_Prims.pow2" ], 0, - "a013633674bfc6bdb3a73c581dd47825" + "280bb8898f87ebf43d4c34fc1160f0b1" ] ] ] \ No newline at end of file diff --git a/test/.hints/SimpleWasm.fst.hints b/test/.hints/SimpleWasm.fst.hints index e3a01e887..ecc009d4c 100644 --- a/test/.hints/SimpleWasm.fst.hints +++ b/test/.hints/SimpleWasm.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "f0a52cac185b2922c97e6b71fc892a9e" + "a2c28aa65d989f90b1fa5259a8cb60a2" ], [ "SimpleWasm.main", @@ -37,7 +37,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "2391e5a216d724411fa03a088214168e" + "f596984b17ac81415a13505e099959d5" ] ] ] \ No newline at end of file diff --git a/test/.hints/StaticHeaderLib.fst.hints b/test/.hints/StaticHeaderLib.fst.hints index a61c6e487..2cb00f172 100644 --- a/test/.hints/StaticHeaderLib.fst.hints +++ b/test/.hints/StaticHeaderLib.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "e84cfa80fd54d1ee73f39fc897a2b56e" + "3d13c9d566351c4d6c6a130a71cac1e1" ], [ "StaticHeaderLib.private_helper", @@ -33,7 +33,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "1fa366b54274c63a97ea86c4ed846586" + "25f98fb49d86d51a9eba73304f781977" ], [ "StaticHeaderLib.helper", @@ -42,7 +42,7 @@ 1, [ "@query", "typing_StaticHeaderLib.__proj__Mkt__item__x" ], 0, - "120f9f1f8ff0fd000619124cbdf8f971" + "b239ea3535aec9bb1f97f07ef2b15ca2" ] ] ] \ No newline at end of file diff --git a/test/.hints/StaticHeaderLib.fsti.hints b/test/.hints/StaticHeaderLib.fsti.hints index b64d9f8cc..da1e8e889 100644 --- a/test/.hints/StaticHeaderLib.fsti.hints +++ b/test/.hints/StaticHeaderLib.fsti.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "e84cfa80fd54d1ee73f39fc897a2b56e" + "3d13c9d566351c4d6c6a130a71cac1e1" ], [ "StaticHeaderLib.private_helper", @@ -33,7 +33,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "1fa366b54274c63a97ea86c4ed846586" + "25f98fb49d86d51a9eba73304f781977" ] ] ] \ No newline at end of file diff --git a/test/.hints/SteelNotNull.fst.hints b/test/.hints/SteelNotNull.fst.hints index 9f5591ed7..c65fc6093 100644 --- a/test/.hints/SteelNotNull.fst.hints +++ b/test/.hints/SteelNotNull.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "eb6ce26c8b3f26e0a7d4b38b1a1a51ab" + "f717c81c6fea98e9e0a89639d9fb7b85" ] ] ] \ No newline at end of file diff --git a/test/.hints/SteelNull.fst.hints b/test/.hints/SteelNull.fst.hints index 921e7312e..d3ed6cad5 100644 --- a/test/.hints/SteelNull.fst.hints +++ b/test/.hints/SteelNull.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "eb6ce26c8b3f26e0a7d4b38b1a1a51ab" + "f717c81c6fea98e9e0a89639d9fb7b85" ] ] ] \ No newline at end of file diff --git a/test/.hints/StringLit.fst.hints b/test/.hints/StringLit.fst.hints index c1d59157e..72f8e427b 100644 --- a/test/.hints/StringLit.fst.hints +++ b/test/.hints/StringLit.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "05bb770837558d05f6288abec8d2567e" + "25e5555e38043f4c757d2214ca8337f9" ], [ "StringLit.cat", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "fa62b1e1671d23753fd4f0f7ccd65195" + "fa6b4f9afd41e88b4d7ff7724a436c25" ], [ "StringLit.test_c_string", @@ -50,7 +50,7 @@ 1, [ "@query" ], 0, - "d3c2173b35b5870311b2f2af6b851e0e" + "90a84f8ba5411fe0f535fac4be609386" ], [ "StringLit.main", @@ -69,7 +69,7 @@ "typing_FStar.Int.Cast.uint8_to_int32" ], 0, - "6a7694f859081bce74ecc724f1d28892" + "7089cdb8042e004d85abd061a0d7f6c0" ] ] ] \ No newline at end of file diff --git a/test/.hints/Strlen.fst.hints b/test/.hints/Strlen.fst.hints index 5a185ec83..334f0181f 100644 --- a/test/.hints/Strlen.fst.hints +++ b/test/.hints/Strlen.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "2a12fa86001820e1a380e30e09e2df3e" + "515b12965f5eb19412d2e85bc8f5f17c" ], [ "Strlen.main", @@ -24,7 +24,7 @@ "typing_tok_C.EXIT_FAILURE@tok", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "fd5269e42c8e962031c1cea9d3e8101e" + "91b63f506d986e7974b75bad97798712" ] ] ] \ No newline at end of file diff --git a/test/.hints/Structs.fst.hints b/test/.hints/Structs.fst.hints index 4b59895aa..0bc3eea69 100644 --- a/test/.hints/Structs.fst.hints +++ b/test/.hints/Structs.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "4ab2b8b234f1dae6d5dab9f181ab289c" + "7ba6ef4c20f48b6cd25c5e169e90047b" ], [ "Structs.f", @@ -33,7 +33,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "057c0243993a27cbc93bddb9fdc6b21f" + "80531f0a0bddf331c9ecdbc051267630" ], [ "Structs.main", @@ -45,7 +45,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "fbad3163ff904a66759efa3f930b047e" + "c46aee78ac53ad423fc933df28d644aa" ] ] ] \ No newline at end of file diff --git a/test/.hints/Structs2.fst.hints b/test/.hints/Structs2.fst.hints index 93a1a5f71..e73c75c84 100644 --- a/test/.hints/Structs2.fst.hints +++ b/test/.hints/Structs2.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt8.t" ], 0, - "c50dcac397b1bfc6aa25b9e70afe843b" + "bb92d960ccd0e48fb75907016caeec10" ], [ "Structs2.point", @@ -25,7 +25,7 @@ "typing_FStar.UInt32.t" ], 0, - "cc6137af273dcb6394300e3354972e31" + "03257e7e7480a314fe7c6dc7cabe9b0b" ], [ "Structs2.t", @@ -37,7 +37,7 @@ "assumption_Structs2.point__uu___haseq" ], 0, - "47503258f43ab8b25dc865628d6d0348" + "54beb5575711de8498ed13650e4fa9af" ], [ "Structs2.test1", @@ -58,7 +58,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "af55fb7e3589d952694e32294d69d8d8" + "2b5b590d3a525553b52aef61701ab471" ], [ "Structs2.main", @@ -84,7 +84,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "1d28e749ba486deaf34cd0189cdd59cb" + "bd0eeea3981fc24a7d600629a8456f2d" ] ] ] \ No newline at end of file diff --git a/test/.hints/Substitute.fst.hints b/test/.hints/Substitute.fst.hints index 0131834af..99cf892d6 100644 --- a/test/.hints/Substitute.fst.hints +++ b/test/.hints/Substitute.fst.hints @@ -21,7 +21,7 @@ "typing_FStar.Int32.t" ], 0, - "e3e63553061417389533670c3eba9721" + "16b03e6d9134f69805832188a44ffcf4" ], [ "Substitute.main", @@ -50,7 +50,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "b33ea83e415add9449b108ca883800c3" + "eedf9205835289c4f2b706c17e048812" ] ] ] \ No newline at end of file diff --git a/test/.hints/TailCalls.fst.hints b/test/.hints/TailCalls.fst.hints index d46a46c4d..6080e383e 100644 --- a/test/.hints/TailCalls.fst.hints +++ b/test/.hints/TailCalls.fst.hints @@ -43,7 +43,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.pow2" ], 0, - "227c4e4a384293f6322cf4e5a5a0b9ea" + "b9d73f5bb407f6f28e5c0b65f4e76460" ] ] ] \ No newline at end of file diff --git a/test/.hints/TailCalls2.fst.hints b/test/.hints/TailCalls2.fst.hints index 402515872..25c2b9d4b 100644 --- a/test/.hints/TailCalls2.fst.hints +++ b/test/.hints/TailCalls2.fst.hints @@ -23,7 +23,7 @@ "typing_FStar.Int32.v", "well-founded-ordering-on-nat" ], 0, - "85788cbebfd7917c48c35c6faf1d0a60" + "d35806d2dd08c521691fd25c2fd32612" ] ] ] \ No newline at end of file diff --git a/test/.hints/TestAlloca.fst.hints b/test/.hints/TestAlloca.fst.hints index cf454b077..47271d325 100644 --- a/test/.hints/TestAlloca.fst.hints +++ b/test/.hints/TestAlloca.fst.hints @@ -14,7 +14,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "4d4885f0a2f44e19200574938ca39178" + "9d0d57387ff72f5ad573ed3c7b5b5f56" ], [ "TestAlloca.main", @@ -79,7 +79,7 @@ "typing_FStar.Set.singleton", "typing_FStar.UInt32.v" ], 0, - "6345f738c0beb720b4fb7ef06dd46d43" + "e10349561515444f2aba3a36c0795b6f" ] ] ] \ No newline at end of file diff --git a/test/.hints/TopLevelArray.fst.hints b/test/.hints/TopLevelArray.fst.hints index aa41efe23..39cc56e55 100644 --- a/test/.hints/TopLevelArray.fst.hints +++ b/test/.hints/TopLevelArray.fst.hints @@ -27,7 +27,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "34e43662a287993036e21cb3d86a5b67" + "a5b27fb89ba3ec07b6d724a9c111f50c" ], [ "TopLevelArray.y", @@ -55,7 +55,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "1de1e657697fe255ef6197cbda3178fb" + "897c38f63ac7348bf1c2675e013ca1f1" ], [ "TopLevelArray.x", @@ -83,7 +83,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "292b45ca965825e56daa4feaf96897a6" + "a24f905b319d97b41bc49af2a2f9058a" ], [ "TopLevelArray.g", @@ -97,7 +97,7 @@ "refinement_interpretation_TopLevelArray_Tm_refine_cb33895ece621ae8bc092dc7297a0116" ], 0, - "7921cad83304f7f08ce3cae69e6e3fcc" + "b0c39294901ae4d465c64d82c0f11d39" ], [ "TopLevelArray.main", @@ -119,7 +119,7 @@ "typing_TopLevelArray.__proj__Mkt__item__y", "typing_TopLevelArray.x" ], 0, - "71d5bb1a63e14c205641c9515be8d0d1" + "023eacf2abd532b2eb1683bf92d9bbe3" ] ] ] \ No newline at end of file diff --git a/test/.hints/TotalLoops.fst.hints b/test/.hints/TotalLoops.fst.hints index 19678e284..28f38cf65 100644 --- a/test/.hints/TotalLoops.fst.hints +++ b/test/.hints/TotalLoops.fst.hints @@ -16,7 +16,7 @@ "well-founded-ordering-on-nat" ], 0, - "37bf54c59892520719c6449fc7822cb9" + "48dc3014247e20ba872e29683c627ff3" ], [ "TotalLoops.t", @@ -30,7 +30,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "4aa4ee0cdb9030f3b0130129a5bf3926" + "8846ee8e8619fe2a767dd91af3bb9387" ], [ "TotalLoops.tfib", @@ -70,7 +70,7 @@ "typing_TotalLoops.__proj__Mkt__item__i", "typing_TotalLoops.fib" ], 0, - "bb0aab59d91749968bdb7fe6c883bfb5" + "f6e0797910c4f50ce8aa921b205873db" ] ] ] \ No newline at end of file diff --git a/test/.hints/Tuples.fst.hints b/test/.hints/Tuples.fst.hints index 0645cf7a5..0abee9b67 100644 --- a/test/.hints/Tuples.fst.hints +++ b/test/.hints/Tuples.fst.hints @@ -47,7 +47,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "2e54776eab6f486c4d5b82bfa538a178" + "b77d0a4c480c96ef18d4182af6b65d6b" ] ] ] \ No newline at end of file diff --git a/test/.hints/UBuffer.fst.hints b/test/.hints/UBuffer.fst.hints index fd174dd09..c92557b00 100644 --- a/test/.hints/UBuffer.fst.hints +++ b/test/.hints/UBuffer.fst.hints @@ -98,7 +98,7 @@ "typing_LowStar.UninitializedBuffer.initialization_preorder" ], 0, - "b3affd472c1957fb0b00da3b10653ee3" + "954178abe6a8cd4bde930640f6b76dd4" ], [ "UBuffer.test_ub_stack", @@ -188,7 +188,7 @@ "typing_LowStar.UninitializedBuffer.initialization_preorder" ], 0, - "ae53389e042d03ef55f1997a90def4fa" + "a48a9cde59aced8e48e76d4229b96b42" ], [ "UBuffer.main", @@ -213,7 +213,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "2355ed6f55d6514881a8754a53777162" + "17ca4e794501db8e2cf9592a9650b243" ] ] ] \ No newline at end of file diff --git a/test/.hints/Unsound.fst.hints b/test/.hints/Unsound.fst.hints index 05a28d1b7..887783492 100644 --- a/test/.hints/Unsound.fst.hints +++ b/test/.hints/Unsound.fst.hints @@ -13,7 +13,7 @@ "refinement_interpretation_Tm_refine_652f0f3ffdde8cb9fe553db21d874aee" ], 0, - "3d4b99df6d26294ed903e2efb8661621" + "fa63c48c336800c4fb031600c873eba2" ], [ "Unsound.g", @@ -26,7 +26,7 @@ "refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051" ], 0, - "30207d60f838c8f4c10e9898d241cfdf" + "ffc55c6cdadcd03159dfa10f14c028cc" ], [ "Unsound.main", @@ -98,7 +98,7 @@ "typing_FStar.UInt32.t", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "864293ff9ca4006ac5a6615068de30c7" + "17423ed69f57005f3a3c03bbc61eafae" ] ] ] \ No newline at end of file diff --git a/test/.hints/UnusedParameter.fst.hints b/test/.hints/UnusedParameter.fst.hints index d3849485b..74000a8c7 100644 --- a/test/.hints/UnusedParameter.fst.hints +++ b/test/.hints/UnusedParameter.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int64.t" ], 0, - "5c07c276973e0e0d17ee98562943c92c" + "fb9a34ae0863b42867ae6c6d9abdbf42" ], [ "UnusedParameter.touch", @@ -33,7 +33,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "266c00b9b6fc8e2781cecf244ec0fe54" + "93dd62967899c1caabbec80afbdb1de2" ] ] ] \ No newline at end of file diff --git a/test/.hints/Unused_A.fst.hints b/test/.hints/Unused_A.fst.hints index 13b2f17d5..97118a6d6 100644 --- a/test/.hints/Unused_A.fst.hints +++ b/test/.hints/Unused_A.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "98c6f60737e5bd91a9625812ccf95193" + "57ae91333b52cf22aef16bb9a1d802b7" ] ] ] \ No newline at end of file diff --git a/test/.hints/Unused_B.fst.hints b/test/.hints/Unused_B.fst.hints index 3e8627ff3..f7d50351b 100644 --- a/test/.hints/Unused_B.fst.hints +++ b/test/.hints/Unused_B.fst.hints @@ -34,7 +34,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "649c94c6b46793a6bff3646deea07483" + "ab8344d85f39ef9abc94d205ef0b52c1" ] ] ] \ No newline at end of file diff --git a/test/.hints/Uu.fst.hints b/test/.hints/Uu.fst.hints index 54206cb89..8468ce61d 100644 --- a/test/.hints/Uu.fst.hints +++ b/test/.hints/Uu.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "55a7331a61791caa9ea0fcfafedb6d14" + "1389ea9e26781ffcc72d15e4f6897280" ] ] ] \ No newline at end of file diff --git a/test/.hints/VariableMerge.fst.hints b/test/.hints/VariableMerge.fst.hints index fde912733..0609f2c10 100644 --- a/test/.hints/VariableMerge.fst.hints +++ b/test/.hints/VariableMerge.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "813d1bf010b65385e98b0ba4fb161f47" + "36ab4f9c6b82eeda4209bb4c7c096565" ], [ "VariableMerge.test", @@ -34,7 +34,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "f16c4bd0b55276befe220bbbd679474e" + "f359d5473cd06011a4a8d88cb85a5441" ], [ "VariableMerge.test1", @@ -56,7 +56,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "71a55b0723ba6f0b626a665d92d6abac" + "b4f885f90424d8e7e71bb235147376d4" ], [ "VariableMerge.test2", @@ -78,7 +78,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "f3c9c21b72c55c17dfb5f1624ea514a5" + "1b99d4308d01199ea0826d9b22f632a9" ], [ "VariableMerge.main", @@ -101,7 +101,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "b63d595ce8b85c316f08fe15ef99c3bb" + "1a1d365f0f99257a3e2869333c6c5bea" ] ] ] \ No newline at end of file diff --git a/test/.hints/Verbatim.fst.hints b/test/.hints/Verbatim.fst.hints index 46de890c9..cd4bffc9e 100644 --- a/test/.hints/Verbatim.fst.hints +++ b/test/.hints/Verbatim.fst.hints @@ -15,7 +15,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "04cc03451f1c5e5cc069bfc0705d0989" + "b03811af8148adf0a101e22af367e94b" ] ] ] \ No newline at end of file diff --git a/test/.hints/Vla.fst.hints b/test/.hints/Vla.fst.hints index e351d8366..ec0a57d9a 100644 --- a/test/.hints/Vla.fst.hints +++ b/test/.hints/Vla.fst.hints @@ -48,7 +48,7 @@ "typing_FStar.UInt32.t", "typing_FStar.UInt32.v" ], 0, - "06baa36f539773e8848a1c343786e73b" + "749eaf47be5e66e89e26d245a0a433ed" ], [ "Vla.main", @@ -65,7 +65,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "db0ee3412e3621749d23c405765e4432" + "714e45e39921de37f3457af7d5d7da5d" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm1.fst.hints b/test/.hints/Wasm1.fst.hints index 46b27e6f7..55a897644 100644 --- a/test/.hints/Wasm1.fst.hints +++ b/test/.hints/Wasm1.fst.hints @@ -38,7 +38,7 @@ "typing_FStar.UInt.fits", "typing_FStar.UInt32.v" ], 0, - "7c2d8ba4c51130ecebc065ce6e2b2b87" + "cc6ec0b2fa273f03a42e9d496e565e70" ], [ "Wasm1.maybe_true", @@ -59,7 +59,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "4cfa8ed59a0e0dffe67b957bc0e27e78" + "72e3fcafca5d6c8113824e4a44e2cb47" ], [ "Wasm1.fact'", @@ -72,7 +72,7 @@ "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans" ], 0, - "36cbd033422164579428c242d096c2b1" + "7a7383de523a2042b3e49ee88150ed1c" ], [ "Wasm1.minus", @@ -95,7 +95,7 @@ "typing_FStar.UInt32.v" ], 0, - "9a16224e2a90d41b4aded70368750465" + "01c5abe903a4b92e68051abc19dab717" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm10.fst.hints b/test/.hints/Wasm10.fst.hints index 810921abb..7d739488a 100644 --- a/test/.hints/Wasm10.fst.hints +++ b/test/.hints/Wasm10.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "ec17ed48a8214fc42544d58076673a0c" + "d63d4f2413b9b49bdd550568a2d8f199" ], [ "Wasm10.b", @@ -40,7 +40,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "7cf4911e3379d2a55b12f75034ffc7fd" + "f9a13c3d944c87c6f63d8fe7f6e0a725" ], [ "Wasm10.main", @@ -58,7 +58,7 @@ "typing_Wasm10.b" ], 0, - "9b71b1a18975f7d35430b8d0026b7dba" + "f2aa8f936661f9903c4221915e90e99c" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm2.fst.hints b/test/.hints/Wasm2.fst.hints index a9529b303..fbe5dd1af 100644 --- a/test/.hints/Wasm2.fst.hints +++ b/test/.hints/Wasm2.fst.hints @@ -79,7 +79,7 @@ "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_Prims.pow2" ], 0, - "5e070062c84a4c8c969f3b899be8bb9e" + "68c56c74d8da1bc3f13ae0b573966b05" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm3.fst.hints b/test/.hints/Wasm3.fst.hints index a4993f1e5..e93a71803 100644 --- a/test/.hints/Wasm3.fst.hints +++ b/test/.hints/Wasm3.fst.hints @@ -64,7 +64,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "c5f87b32fea7e1b3870f8f52f7d0b5fa" + "9f50b3298b37e7afee19c66954fe6cf1" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm4.fst.hints b/test/.hints/Wasm4.fst.hints index 6093ab603..7c699825f 100644 --- a/test/.hints/Wasm4.fst.hints +++ b/test/.hints/Wasm4.fst.hints @@ -14,7 +14,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "dd53ec9f2c81b0e43b68dead2bc3ed0e" + "1e1a400907c3c8d43cb921b8273673b1" ], [ "Wasm4.test", @@ -27,7 +27,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "347681b144ad658c30c341185026719e" + "7927cb7691874a56d6f80fe2bdb87ac9" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm5.fst.hints b/test/.hints/Wasm5.fst.hints index 94ffa6aa4..c7412845e 100644 --- a/test/.hints/Wasm5.fst.hints +++ b/test/.hints/Wasm5.fst.hints @@ -27,7 +27,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "60a3a66632085c1efc71e12b8cb93602" + "fe8dc241ec7bd57780ef5659a05cd638" ], [ "Wasm5.y", @@ -55,7 +55,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "0be8545b0a5ef4c891e5b342c60b20f6" + "815d431acefcf01784431c7cb7e8c2e0" ], [ "Wasm5.main", @@ -72,7 +72,7 @@ "typing_Wasm5.x" ], 0, - "44f184f542714223e14ae5e147f7f5a9" + "85b0291653c4b57759793ff001e97cf4" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm6.fst.hints b/test/.hints/Wasm6.fst.hints index be2d34571..508597c25 100644 --- a/test/.hints/Wasm6.fst.hints +++ b/test/.hints/Wasm6.fst.hints @@ -14,7 +14,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "2ff466d8c2565a64ba159ee69d067ce3" + "cb139bccfde7b793885adeff7f6d602b" ], [ "Wasm6.snd", @@ -29,7 +29,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "be3bc2eede87be8540134194eaf18c9d" + "aa456b471b4e65ce4ff51cef0cff0752" ], [ "Wasm6.main", @@ -97,7 +97,7 @@ "typing_LowStar.Monotonic.Buffer.g_is_null" ], 0, - "b8ee9b369cda5f6d3d5f0ba909801a43" + "bc50620d03c173867618a54b276472e7" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm7.fst.hints b/test/.hints/Wasm7.fst.hints index 07c3d079a..011c60e5b 100644 --- a/test/.hints/Wasm7.fst.hints +++ b/test/.hints/Wasm7.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "b9e34f7f5a5a76bef56b1006beba06ee" + "3cadf2faef37197c2801207af8a77f7a" ], [ "Wasm7.__proj__A__item___0", @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_ec10ccf333cf39e2d779a27ff25f9f69" ], 0, - "b5a54d95211250b31af54934c6e3893b" + "7bda24d802652e82c377939ba7815a31" ], [ "Wasm7.__proj__A__item___1", @@ -38,7 +38,7 @@ "refinement_interpretation_Tm_refine_ec10ccf333cf39e2d779a27ff25f9f69" ], 0, - "00598f82c00864070d4e07136c676de7" + "1fd6054d5b561e1623a7746ecc6f6c01" ], [ "Wasm7.__proj__B__item___0", @@ -51,7 +51,7 @@ "refinement_interpretation_Tm_refine_1ce3b1dcced40bb1a9aec7baaac607ca" ], 0, - "dbb4338cb55f1769a5aac314dfad8fb4" + "ab15052108f05580aeb094c695cbeb16" ], [ "Wasm7.__proj__B__item___1", @@ -64,7 +64,7 @@ "refinement_interpretation_Tm_refine_1ce3b1dcced40bb1a9aec7baaac607ca" ], 0, - "f094ce7fb1c0e197bc0e54447b58dcaf" + "23bd40c68db67ab0f02e18e7ccac5b34" ], [ "Wasm7.__proj__B__item___2", @@ -77,7 +77,7 @@ "refinement_interpretation_Tm_refine_1ce3b1dcced40bb1a9aec7baaac607ca" ], 0, - "7bee33c139749957db61fc3c4b19ecfc" + "50a17f6476557f321a4b7f59792f81a6" ], [ "Wasm7.v2", @@ -90,7 +90,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "20b705e883dbdcb1fe73916fd53a41d3" + "2c07e6a563837b67984ae512c3f0e816" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm8.fst.hints b/test/.hints/Wasm8.fst.hints index de7bfe66b..81e24a50f 100644 --- a/test/.hints/Wasm8.fst.hints +++ b/test/.hints/Wasm8.fst.hints @@ -27,7 +27,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "240c82924b7b039b00d182177ffa1cf0" + "323fceac6d7bd9d67bf5c5aea5779555" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm9.fst.hints b/test/.hints/Wasm9.fst.hints index 188868a5d..aa6021ea5 100644 --- a/test/.hints/Wasm9.fst.hints +++ b/test/.hints/Wasm9.fst.hints @@ -81,7 +81,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "cc79a52e47ebe76a3d64c0755b9b873a" + "c33929d6c99da79b359680018377cd0a" ] ] ] \ No newline at end of file diff --git a/test/.hints/WasmTrap.fst.hints b/test/.hints/WasmTrap.fst.hints index e30eee2d9..27e03ec38 100644 --- a/test/.hints/WasmTrap.fst.hints +++ b/test/.hints/WasmTrap.fst.hints @@ -55,7 +55,7 @@ "typing_FStar.UInt32.t", "typing_FStar.UInt32.v" ], 0, - "4b65d767e01e213571b199c4e3235b24" + "dd71dea7e9314a743bbbe6fecd76e789" ] ] ] \ No newline at end of file diff --git a/test/.hints/WildCard.fst.hints b/test/.hints/WildCard.fst.hints index eb659b8fa..d4a1bca60 100644 --- a/test/.hints/WildCard.fst.hints +++ b/test/.hints/WildCard.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "26a5a92e7677a1c9cacfcd20986b61cf" + "b08d7c9df013a23448bf8e6620277847" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wireguard.fst.hints b/test/.hints/Wireguard.fst.hints index 28dfb7d65..7afe7ef27 100644 --- a/test/.hints/Wireguard.fst.hints +++ b/test/.hints/Wireguard.fst.hints @@ -15,7 +15,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "df6d55ad017eac1a22c0c8db5a5b6294" + "934ba396c32374404e9b45dff4891b44" ], [ "Wireguard.peers_footprint", @@ -31,7 +31,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "6c32432868c6669395db1941773e1bf4" + "4fa9dbb427e72818b3d7ea9892036de8" ], [ "Wireguard.peers_disjoint", @@ -47,7 +47,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "d91cee99f2bd291483b6d9b54a37b5b1" + "00adfd239a3bcbff4e3fae8afc2a2541" ], [ "Wireguard.peers_invariants", @@ -64,7 +64,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "603daffcc3d54aedff98d4d34eb5fcaf" + "2fc1ea5a3f9bda5e9b5346dba29a1466" ], [ "Wireguard.peer_by_id", @@ -82,7 +82,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "d14536e93752381be23ddf97daa30798" + "f21e891e6d511c2b24849de123d15dc6" ], [ "Wireguard.peer_of_id_in_peers", @@ -102,7 +102,7 @@ "typing_LowStar.Lib.LinkedList.t" ], 0, - "4eab2662e60afd5fbd2e4f5db74369d6" + "11b372eef374328d385fc5939174c0a1" ], [ "Wireguard.peers_back", @@ -122,7 +122,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "4752c7d3fa2efc64b6b9c7ca0a16545f" + "920a05913cff051700032dc0abebab4e" ], [ "Wireguard.invariant", @@ -140,7 +140,7 @@ "typing_Wireguard.__proj__Mkdevice__item__r" ], 0, - "d778a58457ba9679c506cd8553e6bcc7" + "1c4fe5d3586d9c1a279e3394c4df5c39" ], [ "Wireguard.peer_footprint_in", @@ -206,7 +206,7 @@ "typing_Wireguard.peer_footprint", "typing_Wireguard.peers_footprint" ], 0, - "2de377d92b302746015d63732a0a0f3a" + "62198547ea9d643287ea92dbcd92c158" ], [ "Wireguard.device_peers_footprint_in", @@ -215,7 +215,7 @@ 0, [ "@query", "equation_Wireguard.invariant" ], 0, - "db94fac5779f1b5273b1ac197a2ead68" + "2d7caa1aed0d88e51938627f4540a1f2" ], [ "Wireguard.frame_peers_back", @@ -291,7 +291,7 @@ "typing_Wireguard.__proj__Mkpeer__item__hs" ], 0, - "f42a1e2603de20bb9e9e1cedcb85e03c" + "67c5dde1306504f3eb8b4097415c0714" ], [ "Wireguard.frame_peers_invariants", @@ -377,7 +377,7 @@ "typing_Wireguard.peer_footprint" ], 0, - "c7993a3bbd6d927ddf383fe797e3145d" + "1f6b570124ac481e0704537d6387c7ff" ], [ "Wireguard.cell_by_id_is_peer_by_id", @@ -389,7 +389,7 @@ "refinement_interpretation_Tm_refine_e3e1e282af9636913d877dace707a50a" ], 0, - "2565769fad425842d61d512eade8afd0" + "b8bc7ec27eab094fae4e889143756172" ], [ "Wireguard.cell_by_id_is_peer_by_id", @@ -496,7 +496,7 @@ "typing_Wireguard.cell_by_id", "typing_Wireguard.peer_by_id" ], 0, - "a73436d4fc5c655879886f7c6c8aaff8" + "715f707c6ed705e1b30a3d1a7bab5b90" ], [ "Wireguard.peer_by_id_invariant", @@ -532,7 +532,7 @@ "projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons" ], 0, - "5b5adc692f24de5b7a3971722a57693d" + "3c24abb45c6c86fd12120e62c7f8ada7" ], [ "Wireguard.frame_invariant", @@ -633,7 +633,7 @@ "typing_Wireguard.peers_footprint" ], 0, - "667dee0c3c5c0e64b8f34c5c02bf68ef" + "30969ef777fe8c292f2f8cd41b1e8ea6" ], [ "Wireguard.create_in", @@ -770,7 +770,7 @@ "typing_LowStar.Monotonic.Buffer.loc_regions" ], 0, - "743dc003f93c80e9a8771f1c55732bf2" + "d89a099d24f432b6b2240a3bc2c084d9" ], [ "Wireguard.free_peer_list", @@ -875,7 +875,7 @@ "typing_Wireguard.peer_footprint" ], 0, - "c0ba0c5a7324b1f181a298112421c133" + "c41279ffef5cc0c506ec3f6ed981a9b0" ], [ "Wireguard.free_", @@ -941,7 +941,7 @@ "typing_Wireguard.__proj__Mkdevice__item__r_peers_payload" ], 0, - "9a8bdff20ca334f3f011b9ae8ebdcabb" + "8ddb09393fb20375e6d105081b53c2e8" ], [ "Wireguard.insert_peer", @@ -950,7 +950,7 @@ 0, [ "@query" ], 0, - "feaec717cef143f6b3e3ed04a4aba297" + "d8d6eb38de9796405d3cc8a1c2e4afa6" ], [ "Wireguard.insert_peer", @@ -1146,7 +1146,7 @@ "typing_Wireguard.peers_footprint" ], 0, - "caa67a1d1e9505e289aa3a5222b87946" + "6409ec3f7b9c41cd7f951993d9724f58" ], [ "Wireguard.find_peer_by_id_", @@ -1245,7 +1245,7 @@ "typing_Wireguard.cell_by_id" ], 0, - "2f55784bb6f8f64372b14c4dce890ba2" + "ff5d897dad248eab75a914c8085f63d8" ], [ "Wireguard.find_peer_by_id", @@ -1271,7 +1271,7 @@ "typing_Wireguard.__proj__Mkdevice__item__peers" ], 0, - "561500ccdaa807d28414c8f4a4901143" + "c3cf3b287125e147ec42bda41dc304ec" ], [ "Wireguard.link_peer_by_id", @@ -1381,7 +1381,7 @@ "typing_Wireguard.peer_by_id", "typing_Wireguard.peers_footprint" ], 0, - "b5148d24a0f83d6154da334c5fa36d8d" + "6bab775fa8871332037ca1fa7de465c6" ], [ "Wireguard.main", @@ -1586,7 +1586,7 @@ "typing_Wireguard.peer_by_id", "typing_Wireguard.peers_footprint" ], 0, - "dc71f42c1cef84759ee0b4617db33c1f" + "91105783c259972657a4fa5f35c90f2c" ] ] ] \ No newline at end of file