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
Hacl.HPKE.P256_CP256_SHA256.fsti.hints 
[
  "X����\u0015Qe�R5�\u0010\u0010G�",
  [
    [
      "Hacl.HPKE.P256_CP256_SHA256.setupBaseI",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
        "constructor_distinct_Spec.Agile.DH.DH_P256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok",
        "equality_tok_Spec.Agile.DH.DH_P256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.is_ciphersuite",
        "equation_Spec.GaloisField.gf",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "b0e0f6028d6b390bf8b6f94c3153a13f"
    ],
    [
      "Hacl.HPKE.P256_CP256_SHA256.setupBaseR",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
        "constructor_distinct_Spec.Agile.DH.DH_P256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok",
        "equality_tok_Spec.Agile.DH.DH_P256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.is_ciphersuite",
        "equation_Spec.GaloisField.gf",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "d83ce5292800bfbe50146bd09f603330"
    ],
    [
      "Hacl.HPKE.P256_CP256_SHA256.sealBase",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
        "constructor_distinct_Spec.Agile.DH.DH_P256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok",
        "equality_tok_Spec.Agile.DH.DH_P256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.is_ciphersuite",
        "equation_Spec.GaloisField.gf",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "8cebaf93d78d70803ec9f4ea05a03cd2"
    ],
    [
      "Hacl.HPKE.P256_CP256_SHA256.openBase",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
        "constructor_distinct_Spec.Agile.DH.DH_P256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok",
        "equality_tok_Spec.Agile.DH.DH_P256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.is_ciphersuite",
        "equation_Spec.GaloisField.gf",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "e4ba73dca260d82de2829c5b3c26d99c"
    ]
  ]
]
back to top