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
Vale.X64.State.fsti.hints 
[
  "Z\u001e���\u000f�\u00120C�(��,\u007f",
  [
    [
      "Vale.X64.State.eval_maddr",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.X64.Machine_s.MConst",
        "disc_equation_Vale.X64.Machine_s.MIndex",
        "disc_equation_Vale.X64.Machine_s.MReg",
        "fuel_guarded_inversion_Vale.X64.Machine_s.maddr"
      ],
      0,
      "defb95c8d187cf9cf111fd50fc4bd33f"
    ],
    [
      "Vale.X64.State.to_nat64",
      1,
      1,
      0,
      [
        "@query", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "1e4704454be9b5e6bc186200ae6c0451"
    ],
    [
      "Vale.X64.State.eval_operand",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.X64.Machine_s.OConst",
        "disc_equation_Vale.X64.Machine_s.OMem",
        "disc_equation_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "fuel_guarded_inversion_Vale.X64.Machine_s.operand"
      ],
      0,
      "ba01efdb65bc48ab0bb72873c1bb4752"
    ],
    [
      "Vale.X64.State.eval_operand128",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.X64.Machine_s.OMem128",
        "disc_equation_Vale.X64.Machine_s.OReg128",
        "disc_equation_Vale.X64.Machine_s.OStack128",
        "fuel_guarded_inversion_Vale.X64.Machine_s.operand128"
      ],
      0,
      "d3aa2efd80e88c6230329e73626c8deb"
    ],
    [
      "Vale.X64.State.update_operand",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.X64.Machine_s.OConst",
        "disc_equation_Vale.X64.Machine_s.OMem",
        "disc_equation_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "fuel_guarded_inversion_Vale.X64.Machine_s.operand"
      ],
      0,
      "47661fc31d5b95b745dd3a25d503c702"
    ],
    [
      "Vale.X64.State.valid_src_operand",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.X64.Machine_s.OConst",
        "disc_equation_Vale.X64.Machine_s.OMem",
        "disc_equation_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "fuel_guarded_inversion_Vale.X64.Machine_s.operand"
      ],
      0,
      "8c57ec69e7c69f484b7c135014427fef"
    ],
    [
      "Vale.X64.State.valid_src_operand128",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.X64.Machine_s.OMem128",
        "disc_equation_Vale.X64.Machine_s.OReg128",
        "disc_equation_Vale.X64.Machine_s.OStack128",
        "fuel_guarded_inversion_Vale.X64.Machine_s.operand128"
      ],
      0,
      "c070ba0a68c839a75c6670a1efa5f0b8"
    ]
  ]
]
back to top