Skip to main content

Browse the archive

Revision b5e85960e109efb08b9c65a4ab85c9b4ef926419 authored by Jay Bosamiya on 04 June 2019, 18:24:09 UTC, committed by Jay Bosamiya on 04 June 2019, 18:24:09 UTC 
File at least verifies now; some lemmas broke though which we need to fix
1 parent 2a5defc
Raw File
WasmSupport.fst.hints 
[
  "�\u0016\\\"�8S�\u0011�\u0013\u000f���",
  [
    [
      "WasmSupport.check_buffer_size",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.HyperStack.ST.equal_domains",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
        "lemma_FStar.Set.lemma_equal_refl",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap"
      ],
      0,
      "56de1ed978b9b96635d526487e5386ab"
    ],
    [
      "WasmSupport.betole64",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "bfdb779d5538e82fe96ee8787913a66b"
    ]
  ]
]
back to top