Skip to main content

Browse the archive

Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC 
Merge pull request #298 from project-everest/vdum_ocaml_nits
 
OCaml API: Don't run unit tests which require unsupported features
2 parent s 760addb + 28f416c
Raw File
Vale.AES.GHash_s.fst.hints 
[
  "\u0000l\u001e?@\b�O\u0003j�]���G",
  [
    [
      "Vale.AES.GHash_s.ghash_plain_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.hasEq_lemma",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Vale.Def.Types_s.quad32"
      ],
      0,
      "9ae8b356b860f09545d28fc3a4a22ace"
    ],
    [
      "Vale.AES.GHash_s.ghash_LE_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_cee79fb2a0b31329a2e2b29d477b66be_1",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "equation_Vale.AES.GHash_s.ghash_plain_LE",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Lib.Seqs_s.all_but_last",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3cde0f73125500a52bff30114a1a1137",
        "refinement_interpretation_Tm_refine_3e04674625ba1e90ddf6da6977508e33",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "typing_FStar.Seq.Base.length",
        "typing_Vale.Lib.Seqs_s.all_but_last", "well-founded-ordering-on-nat"
      ],
      0,
      "843692157407205ab4db6a642430b45d"
    ],
    [
      "Vale.AES.GHash_s.ghash_LE_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "81d3ea20e78001cc47ea7410daa4b838"
    ],
    [
      "Vale.AES.GHash_s.ghash_plain_LE",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.hasEq_lemma",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Vale.Def.Types_s.quad32"
      ],
      0,
      "26db177c70bf110f98e13aca06ee8ea4"
    ],
    [
      "Vale.AES.GHash_s.ghash_LE_def",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_cee79fb2a0b31329a2e2b29d477b66be_1",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "equation_Vale.AES.GHash_s.ghash_plain_LE",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Lib.Seqs_s.all_but_last",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3cde0f73125500a52bff30114a1a1137",
        "refinement_interpretation_Tm_refine_3e04674625ba1e90ddf6da6977508e33",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "typing_FStar.Seq.Base.length",
        "typing_Vale.Lib.Seqs_s.all_but_last", "well-founded-ordering-on-nat"
      ],
      0,
      "08daeaa097a451331959fb747214e4cc"
    ]
  ]
]
back to top