CHERI: fixing last Admit with new lemmas from coq-cheri-capabilies (#…

…580)

* adjustements to new coq-cheri-capabilities API.

* adjusted encode_decode lemma

* CHERI: fixing last Admit with new lemmas from `coq-cheri-capabilies`

coq/Morello/CapabilitiesGS.v

@@ -259,7 +259,14 @@ Module Type CAPABILITY_GS
  Parameter cap_encode_length:
  forall c l t, encode c = Some (l, t) -> List.length l = sizeof_cap.
 
- Parameter cap_exact_encode_decode:
- forall c c' t l, encode c = Some (l, t) -> decode l t = Some c' -> eqb c
-c' = true.
+ Parameter cap_encode_valid:
+ forall cap cb b,
+ cap_is_valid cap = true -> encode cap = Some (cb, b) -> b = true.
+
+ Parameter cap_encode_decode_bounds:
+ forall cap bytes t,
+ encode cap = Some (bytes, t) ->
+ exists cap', decode bytes t = Some cap'
+ /\ cap_get_bounds cap = cap_get_bounds cap'.
+
 End CAPABILITY_GS.

coq/Morello/MorelloCapsGS.v

@@ -238,15 +238,27 @@ Module Capability_GS <: CAPABILITY_GS (MorelloCaps.AddressValue) (MorelloCaps.Fl
  apply H.
  Qed.
 
- Lemma cap_exact_encode_decode:
- forall c c' t l, encode c = Some (l, t) -> decode l t = Some c' -> eqb c c' = true.
+ Lemma cap_encode_valid:
+ forall cap cb b,
+ cap_is_valid cap = true -> encode cap = Some (cb, b) -> b = true.
  Proof.
- intros.
- apply Capability.cap_exact_encode_decode with (t:=t0) (l:=l).
- auto.
- unfold decode in H0.
- destruct (Capability.decode l t0); inversion H0.
- reflexivity.
+ intros c cb b V E.
+ eapply Capability.cap_encode_valid; eauto.
+ Qed.
+
+ Lemma cap_encode_decode_bounds:
+ forall cap bytes t,
+ encode cap = Some (bytes, t) ->
+ exists cap', decode bytes t = Some cap'
+ /\ cap_get_bounds cap = cap_get_bounds cap'.
+ Proof.
+ intros cap0 bytes t E.
+ apply Capability.cap_encode_decode_bounds in E.
+ destruct E as [cap' [D E]].
+ unfold decode.
+ exists (add_gs cap').
+ rewrite D.
+ split;auto.
  Qed.
 
 End Capability_GS. 

coq/Proofs/Revocation.v

@@ -5577,25 +5577,27 @@ Module CheriMemoryImplWithProofs
  apply MorelloImpl.pointer_size_cap_size.
  Qed.
 
- Fact cap_encode_decode
+ Fact cap_encode_decode_bounds
  (cap : Capability_GS.t)
- (cb : list ascii)
- (b : bool) :
- Capability_GS.encode cap = Some (cb, b) ->
- decode_cap (map Some cb) true cap.
- Proof.
- intros ENC.
+ (cb : list ascii):
+ Capability_GS.cap_is_valid cap = true ->
+ Capability_GS.encode cap = Some (cb, true) ->
+ exists cap' : Capability_GS.t,
+ decode_cap (map Some cb) true cap' /\
+ Capability_GS.cap_get_bounds cap =
+ Capability_GS.cap_get_bounds cap'.
+ Proof.
+ intros V H.
+ apply Capability_GS.cap_encode_decode_bounds in H.
+ destruct H as [cap' [D E]].
+ exists cap'.
+ split;[|assumption].
  unfold decode_cap.
  exists cb.
- split.
- -
- clear.
- induction cb; cbn; constructor; tauto.
- -
- pose proof Capability_GS.cap_exact_encode_decode as H.
- specialize (H cap cap b cb ENC).
-
- Admitted.
+ split;[|assumption].
+ clear.
+ induction cb; cbn; constructor;auto.
+ Qed.
 
  (** Storing a capability bytes into memory and and addit it to capmeta preserves invariant *)
  Fact mem_state_with_cap_preserves:
@@ -5651,20 +5653,23 @@ Module CheriMemoryImplWithProofs
  destruct (MorelloCaps.AddressValue.morello_address_eq_dec start addr)
  as [EQ | NEQ].
  +
- subst start.
- exists cap.
+ apply AMap.P.F.add_mapsto_iff in M as [[_ M] | M]; [| tauto].
+ tuple_inversion.
+ pose proof (Capability_GS.cap_encode_valid cap cb b H0 E) as B.
+ subst b.
+ apply cap_encode_decode_bounds in E.
+ destruct E as [cap' [DX EX]].
+ exists cap'.
  split.
  --
- subst bs'.
  rewrite fetch_bytes_add_eq_o by lia.
- subst.
- clear - E.
- eapply cap_encode_decode.
  eassumption.
  --
- apply AMap.P.F.add_mapsto_iff in M as [[_ M] | M]; [| tauto].
- invc M.
+ unfold cap_bounds_within_alloc in *.
+ rewrite <- EX.
  now apply CAPA.
+ --
+ assumption.
  +
  eapply MIcap.
  *