[
  "Œ\rsĈÑitÛá*/ªì3@",
  [
    [
      "Hacl.Hash.SHA1.legacy_update_multi",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_md",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "29c6462ee6cbf2f8054a8e2015c506fe"
    ],
    [
      "Hacl.Hash.SHA1.legacy_update_last",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_md",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "b8084645eaa0cdc493dedb35156bbaf6"
    ],
    [
      "Hacl.Hash.SHA1.legacy_hash",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_md",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "1eb87b1abd08a831bcd5f3802323363b"
    ]
  ]
]