Change the definitions of marshal and unmarshal

[euclidgame]

Currently, the Marshalable trait is like:

pub trait Marshalable: Sized {
    spec fn marshal(self) -> Value;
    spec fn unmarshal(value: Value) -> Result<Self, ParseDynamicObjectError>;
    proof fn marshal_preserves_integrity()
        ensures
            forall |o: Self| Self::unmarshal(#[trigger] o.marshal()).is_Ok() && o == Self::unmarshal(o.marshal()).get_Ok_0();
}

The marshal method returns a Value type value and the unmarshal method receives a value of Value type as parameter.

Previously, this worked well. Problem occurs when we remove the body of every marshal and unmarshal that this may cause the to_dynamic_preserves_integrity to fail.

Take PersistentVolumeClaimView as an example:

open spec fn to_dynamic_object(self) -> DynamicObjectView {
     DynamicObjectView {
          kind: self.kind(),
          metadata: self.metadata,
          data: Value::Object(Map::empty()
                                  .insert(Self::spec_field(), if self.spec.is_None() {Value::Null} else {
                                      self.spec.get_Some_0().marshal()
                                  })),
      }
}

open spec fn from_dynamic_object(obj: DynamicObjectView) -> PersistentVolumeClaimView {
     PersistentVolumeClaimView {
         metadata: obj.metadata,
         spec: if obj.data.get_Object_0()[Self::spec_field()].is_Null() {Option::None} else {
             Option::Some(PersistentVolumeClaimSpecView::unmarshal(obj.data.get_Object_0()[Self::spec_field()]))
         },
     }
}

Suppose o is a PersistentVolumeClaimView type (whose spec is not None). When it calls to_dynamic_object(), we should get a return value (say dyo) whose data equals o.spec.get_Some_0().marshal(). Since there is no method body of marshal(), it is possible that marshal() just returns a Value::Null. In this case, if we want to parse dyo to get back o, we will, however, get a PersistentVolumeClaimView value whose spec is Option::None.

In fact, the from_dynamic_object method is what goes wrong. We can't determine whether the spec comes from a marshal process just by checking if it is Null. So even though marshal preserves integrity, to_dynamic_object and from_dynamic_object are not symmetric processes.

Is it possible for marshal() to return a Null value? If not, we should make this explicit. Otherwise, we have to rewrite the two methods to_dynamic_object and from_dynamic_object.

[marshtompsxd]

What does your current to_dynamic_preserves_integrity look like?

[marshtompsxd]

btw you should also get the Ok content from the unmarshal

spec: if obj.data.get_Object_0()[Self::spec_field()].is_Null() {Option::None} else {
    Option::Some(PersistentVolumeClaimSpecView::unmarshal(obj.data.get_Object_0()[Self::spec_field()]).get_Ok_0())
},

[euclidgame]

I make from_dynamic_object() return Result. And the integrity is
forall |o: Self| Self::from_dynamic_object(o.to_dynamic_object()).is_Ok() && o == self::from_dynamic_object(o.to_dynamic_object()).get_Ok_0()

[euclidgame]

btw you should also get the Ok content from the unmarshal

Of course. The code block I posted was from the main branch. I thought the return value of unmarshal had nothing to do with this issue so I just used this version.

[marshtompsxd]

I think PersistentVolumeClaimSpecView::marshal_preserves_integrity should already have everything you need to prove to_dynamic_preserves_integrity?

[euclidgame]

I think no. Can you see this

In fact, the from_dynamic_object method is what goes wrong. We can't determine whether the spec comes from a marshal process just by checking if it is Null. So even though marshal preserves integrity, to_dynamic_object and from_dynamic_object are not symmetric processes.

[marshtompsxd]

Thanks for pointing out. Now I see the problem. We can add another (trusted) proof to say the result of marshal is not Null