Skip to main content

Browse the archive

Revision aa1ca8698adfe929a9eff86ac143eaf90fc3e8ee authored by Jay Bosamiya on 03 June 2019, 21:51:38 UTC, committed by Jay Bosamiya on 03 June 2019, 21:51:38 UTC 
Get to work on proving write-behavior for instructions
1 parent 6055e85
Raw File
Vale.X64.Xmms.fst.hints 
[
  "\u0019\u001c��B�(����m\u0005��o",
  [
    [
      "Vale.X64.Xmms.of_fun",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.X64.Machine_s.xmm",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
      ],
      0,
      "4428c01a593ec62b02c65e643f2d7e4e"
    ],
    [
      "Vale.X64.Xmms.lemma_upd_eq",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Lib.Map16.map2",
        "equation_Vale.Lib.Map16.map4", "equation_Vale.Lib.Map16.map8",
        "equation_Vale.Lib.Map16.sel2", "equation_Vale.Lib.Map16.sel4",
        "equation_Vale.Lib.Map16.sel8", "equation_Vale.Lib.Map16.upd2",
        "equation_Vale.Lib.Map16.upd4", "equation_Vale.Lib.Map16.upd8",
        "equation_Vale.X64.Machine_s.xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four", "int_inversion",
        "int_typing", "primitive_Prims.op_LessThan",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
      ],
      0,
      "c4fd84fd6f28d2f230704cf4b8b1bb7a"
    ],
    [
      "Vale.X64.Xmms.lemma_upd_ne",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Lib.Map16.map2",
        "equation_Vale.Lib.Map16.map4", "equation_Vale.Lib.Map16.map8",
        "equation_Vale.Lib.Map16.sel2", "equation_Vale.Lib.Map16.sel4",
        "equation_Vale.Lib.Map16.sel8", "equation_Vale.Lib.Map16.upd2",
        "equation_Vale.Lib.Map16.upd4", "equation_Vale.Lib.Map16.upd8",
        "equation_Vale.X64.Machine_s.xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four", "int_inversion",
        "int_typing", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
      ],
      0,
      "3c30346dca4ae8fc1993720f1c44c9bb"
    ],
    [
      "Vale.X64.Xmms.lemma_equal_intro",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
        "equation_Vale.X64.Machine_s.xmm", "equation_Vale.X64.Xmms.equal",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
      ],
      0,
      "b8c48da9b72a3bc33edc65c2da0581d6"
    ],
    [
      "Vale.X64.Xmms.lemma_equal_elim",
      1,
      1,
      0,
      [ "@query", "eq2-interp", "equation_Vale.X64.Xmms.equal" ],
      0,
      "43836b170935560c84f54ecb29f5fd2f"
    ],
    [
      "Vale.X64.Xmms.lemma_eta",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.X64.Machine_s.xmm",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_Vale.X64.Xmms.lemma_equal_elim",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Xmms.eta"
      ],
      0,
      "35e86ebe3a9b8b1d8ce64b9d8ecb501b"
    ]
  ]
]
back to top