val object_storage_to_value_preserves_validity (actor: tid_t) (storage: valid_object_storage_t)
    : Lemma (ensures object_value_valid (object_storage_to_value actor storage))
      (decreases rank storage)
val object_storage_to_value_preserves_validity (actor: tid_t) (storage: valid_object_storage_t)
    : Lemma (ensures object_value_valid (object_storage_to_value actor storage))
      (decreases rank storage)
let object_storage_to_value_preserves_validity
  (actor: tid_t)
  (storage: valid_object_storage_t)
  : Lemma (ensures object_value_valid (object_storage_to_value actor storage))
          (decreases rank storage) =
  object_storage_to_value_preserves_td actor storage
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

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))
  | _ -> ()

let rec object_storage_valid (storage: object_storage_t) : GTot bool (decreases rank storage) =
  match storage with
  | ObjectStorageWeaklyConsistentPrimitive primitive_td values local_versions ->
         u2b (forall tid.{:pattern local_versions tid} local_versions tid < length values)
      && u2b (forall value.{:pattern contains values value} contains values value ==> primitive_box_matches_primitive_td value primitive_td)
  | ObjectStoragePrimitive value -> true
  | ObjectStorageStruct fields ->
      u2b (forall field.{:pattern contains fields field} contains fields field ==> object_storage_valid field)
  | ObjectStorageArray element_td elements ->
      u2b (forall element.{:pattern contains elements element} contains elements element ==>
             object_storage_valid element /\ object_storage_to_td element == element_td)
  | ObjectStorageAbstract _ _ -> true

let valid_object_storage_t = (storage: object_storage_t{object_storage_valid storage})

let rec object_storage_to_value (actor: tid_t) (storage: object_storage_t)
  : GTot object_value_t (decreases rank storage) =
  match storage with
  | ObjectStorageWeaklyConsistentPrimitive _ values local_versions ->
      let version = local_versions actor in
      if version < length values then
        ObjectValuePrimitive (index values version)
      else
        ObjectValueAbstract bool false
  | ObjectStoragePrimitive value -> ObjectValuePrimitive value
  | ObjectStorageStruct fields -> ObjectValueStruct (map_refine (object_storage_to_value actor) fields)
  | ObjectStorageArray element_td elements -> ObjectValueArray element_td (map_refine (object_storage_to_value actor) elements)
  | ObjectStorageAbstract ty value -> ObjectValueAbstract ty value

let rec object_storage_to_value_preserves_td
  (actor: tid_t)
  (storage: valid_object_storage_t)
  : Lemma (ensures (let value = object_storage_to_value actor storage in
                      object_value_to_td value == object_storage_to_td storage
                    /\ object_value_valid value))
          (decreases rank storage) =
  match storage with
  | ObjectStorageWeaklyConsistentPrimitive primitive_td values local_versions ->
      let version = local_versions actor in
      assert (contains values (index values version))
  | ObjectStoragePrimitive _ -> ()
  | ObjectStorageStruct fields ->
      let value = object_storage_to_value actor storage in
      let td = object_storage_to_td storage in
      let field_tds = (ObjectTDStruct?.field_tds td) in
      (match value with
       | ObjectValueStruct value_fields ->
           introduce forall (i: nat). i < length fields ==>
                         object_value_to_td (index value_fields i) == index field_tds i
                       /\ object_value_valid (index value_fields i)
           with introduce _ ==> _
           with given_antecedent. (
             assert (contains fields (index fields i));
             object_storage_to_value_preserves_td actor (index fields i)
           );
           (match object_value_to_td (object_storage_to_value actor storage) with
            | ObjectTDStruct field_tds' -> assert (equal field_tds' field_tds)))
  | ObjectStorageArray element_td elements ->
      let value = object_storage_to_value actor storage in
      (match value with
       | ObjectValueArray _ value_elements ->
          introduce forall (i: nat). i < length elements ==>
                        object_value_to_td (index value_elements i) == element_td
                      /\ object_value_valid (index value_elements i)
          with introduce _ ==> _
          with given_antecedent. (
            assert (contains elements (index elements i));
            assert (index elements i << elements);
            object_storage_to_value_preserves_td actor (index elements i)
          )
      )
  | ObjectStorageAbstract ty value -> ()
/
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
actor: Armada.Base.tid_t -> storage: Armada.Memory.valid_object_storage_t
  -> FStar.Pervasives.Lemma
      (ensures Armada.Type.object_value_valid (Armada.Memory.object_storage_to_value actor storage))
      (decreases FStar.Sequence.Base.rank storage)
Armada.Base.tid_t Armada.Memory.valid_object_storage_t Armada.Memory.object_storage_to_value_preserves_td Prims.unit FStar.Sequence.Base.rank Prims.l_True Prims.squash Prims.b2t Armada.Type.object_value_valid Armada.Memory.object_storage_to_value Prims.Nil FStar.Pervasives.pattern
let object_storage_to_value_preserves_validity (actor: tid_t) (storage: valid_object_storage_t)
    : Lemma (ensures object_value_valid (object_storage_to_value actor storage))
      (decreases rank storage) =
  
object_storage_to_value_preserves_td actor storage