val object_storage_to_td_equivalent_to_map (storage: object_storage_t)
    : Lemma
      (ensures
        (let td = object_storage_to_td storage in
          match storage with
          | ObjectStorageStruct fields -> td == ObjectTDStruct (map object_storage_to_td fields)
          | _ -> True)) [SMTPat (object_storage_to_td storage)]
val object_storage_to_td_equivalent_to_map (storage: object_storage_t)
    : Lemma
      (ensures
        (let td = object_storage_to_td storage in
          match storage with
          | ObjectStorageStruct fields -> td == ObjectTDStruct (map object_storage_to_td fields)
          | _ -> True)) [SMTPat (object_storage_to_td storage)]
let object_storage_to_td_equivalent_to_map (storage: object_storage_t)
  : Lemma (ensures (let td = object_storage_to_td storage in
                    match storage with
                    | ObjectStorageStruct fields -> td == ObjectTDStruct (map object_storage_to_td fields)
                    | _ -> True))
          [SMTPat (object_storage_to_td storage)] =
  let td = object_storage_to_td storage in
  match storage with
  | ObjectStorageStruct fields ->
      assert (equal (ObjectTDStruct?.field_tds td) (map object_storage_to_td fields))
  | _ -> ()
module Armada.Memory

open Armada.Base
open Armada.Computation
open Armada.Pointer
open Armada.Thread
open Armada.Type
open FStar.Sequence.Base
open Spec.Ubool
open Util.Seq

noeq type object_storage_t =
  | ObjectStorageWeaklyConsistentPrimitive:
      (primitive_td: primitive_td_t) ->
      (values: seq primitive_box_t) ->
      (local_versions: Spec.Map.t tid_t nat) ->
      object_storage_t
  | ObjectStoragePrimitive: (value: primitive_box_t) -> object_storage_t
  | ObjectStorageStruct: (fields: seq object_storage_t) -> object_storage_t
  | ObjectStorageArray: (element_td: object_td_t) -> (elements: seq object_storage_t) -> object_storage_t
  | ObjectStorageAbstract: (ty: Type) -> (value: ty) -> object_storage_t

let rec object_storage_to_td (storage: object_storage_t) : GTot object_td_t (decreases rank storage) =
  match storage with
  | ObjectStorageWeaklyConsistentPrimitive primitive_td _ _ -> ObjectTDPrimitive primitive_td
  | ObjectStoragePrimitive value -> ObjectTDPrimitive (primitive_box_to_td value)
  | ObjectStorageStruct fields -> ObjectTDStruct (map_refine object_storage_to_td fields)
  | ObjectStorageArray element_td elements -> ObjectTDArray element_td (length elements)
  | ObjectStorageAbstract ty _ -> ObjectTDAbstract ty
/
Util.Seq.fsti.checked Spec.Ubool.fst.checked Spec.Map.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked Armada.Type.fst.checked Armada.Thread.fst.checked Armada.Pointer.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked
Armada.Memory.fst
storage: Armada.Memory.object_storage_t
  -> FStar.Pervasives.Lemma
      (ensures
        (let td = Armada.Memory.object_storage_to_td storage in
          (match storage with
            | Armada.Memory.ObjectStorageStruct fields ->
              td ==
              Armada.Type.ObjectTDStruct (Util.Seq.map Armada.Memory.object_storage_to_td fields)
            | _ -> Prims.l_True)
          <:
          Type0)) [SMTPat (Armada.Memory.object_storage_to_td storage)]
Armada.Memory.object_storage_t FStar.Sequence.Base.seq Prims._assert FStar.Sequence.Base.equal Armada.Type.object_td_t Armada.Type.__proj__ObjectTDStruct__item__field_tds Util.Seq.map Armada.Memory.object_storage_to_td Prims.unit Prims.l_True Prims.squash Prims.eq2 Armada.Type.ObjectTDStruct Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
let object_storage_to_td_equivalent_to_map (storage: object_storage_t)
    : Lemma
      (ensures
        (let td = object_storage_to_td storage in
          match storage with
          | ObjectStorageStruct fields -> td == ObjectTDStruct (map object_storage_to_td fields)
          | _ -> True)) [SMTPat (object_storage_to_td storage)] =
  
let td = object_storage_to_td storage in
match storage with
| ObjectStorageStruct fields ->
  assert (equal (ObjectTDStruct?.field_tds td) (map object_storage_to_td fields))
| _ -> ()