Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
EverCrypt.Hash.Incremental.fsti.hints
[
"1���сT\u001bW\u0003�#Z\u000bU",
[
[
"EverCrypt.Hash.Incremental.bytes_any_hash_fits",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equation_EverCrypt.Hash.Incremental.bytes_any_hash",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.word_length",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_898a63c05b6cf18e4d31dfeaa233fa0b"
],
0,
"708fafdaf91a5b375dd699d52bbca1dc"
],
[
"EverCrypt.Hash.Incremental.any_hash_t_fits",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equation_EverCrypt.Hash.Incremental.any_hash_t",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.word_length",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_c3946e882ea3726bb38cf802601a8a96"
],
0,
"50b6501a0041983bef77d4382d6585e7"
],
[
"EverCrypt.Hash.Incremental.loc_includes_union_l_footprint_s",
1,
0,
0,
[ "@query" ],
0,
"9bc16d61cd2916055fa611a42420ea25"
],
[
"EverCrypt.Hash.Incremental.invariant",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_EverCrypt.Hash.Incremental.state",
"equation_LowStar.Buffer.pointer",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e"
],
0,
"3df3d90763c713f5edd43055048cb6bd"
],
[
"EverCrypt.Hash.Incremental.update_pre",
1,
0,
0,
[ "@query" ],
0,
"42953ad1ef35240114b47c769d7ab74a"
],
[
"EverCrypt.Hash.Incremental.finish_st",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"lemma_EverCrypt.Hash.Incremental.hash_fits",
"refinement_interpretation_Tm_refine_b9688d2cc74c3f47e54760f7117117a9"
],
0,
"9309088674de0ebd6996602037299d2f"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...