Skip to main content

Browse the archive

Revision c421c49f00116ed3f19ea07913a3fa0e75a24b1c authored by Jonathan Protzenko on 15 May 2020, 15:49:05 UTC, committed by GitHub on 15 May 2020, 15:49:05 UTC 
Merge branch 'master' into _aseem_ulib_patterns
2 parent s 5e5fe52 + 106583d
Raw File
Vale.Arch.HeapTypes_s.fst 
module Vale.Arch.HeapTypes_s
open FStar.Mul

let __reduce__ = ()

type base_typ:eqtype =
  | TUInt8
  | TUInt16
  | TUInt32
  | TUInt64
  | TUInt128

type taint:eqtype =
  | Public
  | Secret

type memTaint_t = (m:Map.t int taint{Set.equal (Map.domain m) (Set.complement Set.empty)})
back to top