[
  "q��\\��6���,\u001c�\u0017�",
  [
    [
      "Vale.Wrapper.X64.Sha.uint64",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "34c1aaa1ad702878c3631d868345d13d"
    ],
    [
      "Vale.Wrapper.X64.Sha.sha256_update",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint32",
        "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_Vale.SHA.SHA_helpers.block_length",
        "equation_Vale.SHA.SHA_helpers.byte",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Lib.IntTypes.uint8",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_01dcf0288fdef2604902000932630d2f",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "c907803be87310b52e38665e10a707ad"
    ]
  ]
]