Skip to main content

Browse the archive

Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC 
Merge pull request #207 from franziskuskiefer/franziskus-libintvec-mozilla
 
Only add libintvector.h include when necessary for mozilla dist
2 parent s 5b69e68 + eefad99
Raw File
Vale.X64.InsSha.fsti.hints 
[
  "r�\r\u0015c�y�|y���%ޔ",
  [
    [
      "Vale.X64.InsSha.va_lemma_SHA256_rnds2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1ac5541806f355944a04e7bdf6a74b55",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "typing_Vale.SHA.SHA_helpers.k"
      ],
      0,
      "beefcd63e0700b4c339934c0804ef127"
    ],
    [
      "Vale.X64.InsSha.va_wp_SHA256_rnds2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
        "typing_Vale.SHA.SHA_helpers.k"
      ],
      0,
      "481ca60d86413fc4cc6d5475d005bca7"
    ],
    [
      "Vale.X64.InsSha.va_quick_SHA256_rnds2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "2d3ce32d1b75c5257fcbad07f304a1c3"
    ],
    [
      "Vale.X64.InsSha.va_lemma_SHA256_msg1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256", "int_inversion",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "4ada06fa79d1e7bb127c444d64bb271f"
    ],
    [
      "Vale.X64.InsSha.va_wp_SHA256_msg1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256", "int_inversion",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "5d2fb106a01286672cb0b323f1313c6b"
    ],
    [
      "Vale.X64.InsSha.va_quick_SHA256_msg1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "c9f92e2fc78260a2ec9a6104bdb350dd"
    ],
    [
      "Vale.X64.InsSha.va_lemma_SHA256_msg2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256", "int_inversion",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "b96a6335b9feb23257d341e4a851737e"
    ],
    [
      "Vale.X64.InsSha.va_wp_SHA256_msg2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256", "int_inversion",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "bae3180dcbf3cee1df60377539af5c6f"
    ],
    [
      "Vale.X64.InsSha.va_quick_SHA256_msg2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "83ceae046ff135fc602e87ef37719b73"
    ]
  ]
]
back to top