Skip to content
This repository has been archived by the owner on Dec 13, 2022. It is now read-only.

support for 8-bit and 16-bit MMIO #843

Merged
merged 11 commits into from
Jul 1, 2021
Merged

support for 8-bit and 16-bit MMIO #843

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
e09fae6
wip adding support for 8bit MMIO
samuelgruetter Jun 25, 2021
08bbae9
wip, copy MinimalMMIO because incompatible with Kami/riscv-coq proof,
samuelgruetter Jun 29, 2021
77f025a
update bedrock2 & coqutil to get better ZnWords
samuelgruetter Jun 29, 2021
ad21488
using nat instead of access_size allows completing
samuelgruetter Jun 29, 2021
2c50c0c
update bedrock2 for better ZnWords
samuelgruetter Jun 30, 2021
2dac80d
prove that the Aes and Hmac state machine satisfy the new assumptions
samuelgruetter Jun 30, 2021
727d485
make sure AesToC prelude uses the same MMIO names as the bedrock2 source
samuelgruetter Jun 30, 2021
cd4ad9a
fix outdated comments
samuelgruetter Jun 30, 2021
a5e5788
Merge branch 'main' into 8bitMMIO
samuelgruetter Jun 30, 2021
16da61e
style fix
samuelgruetter Jul 1, 2021
fbe75f6
Merge branch '8bitMMIO' of github.com:samuelgruetter/silveroak into 8…
samuelgruetter Jul 1, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 10 additions & 9 deletions investigations/bedrock2/Aes/Aes.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Require Import bedrock2.Syntax.
Require Import bedrock2.NotationsCustomEntry.
Require Import bedrock2.ToCString.
Require Import coqutil.Word.Interface.
Require Import Bedrock2Experiments.LibBase.MMIOLabels.
Require Import Bedrock2Experiments.StateMachineSemantics.
Require Import Bedrock2Experiments.Aes.Constants.
Require Import Bedrock2Experiments.Aes.AesSemantics.
Expand Down Expand Up @@ -51,7 +52,7 @@ Section Impl.
([aes_cfg_operation; aes_cfg_mode; aes_cfg_key_len;
aes_cfg_manual_operation],
[], bedrock_func_body:(
output! WRITE (AES_CTRL0,
output! WRITE32 (AES_CTRL0,
((aes_cfg_operation << AES_CTRL_OPERATION) |
((aes_cfg_mode & AES_CTRL_MODE_MASK)
<< AES_CTRL_MODE_OFFSET) |
Expand Down Expand Up @@ -103,13 +104,13 @@ Section Impl.

i = 0 ;
while (i < num_regs_key_used) {
output! WRITE (AES_KEY00 + (i * 4), load4(key + (i * 4)));
output! WRITE32 (AES_KEY00 + (i * 4), load4(key + (i * 4)));
i = i + 1
};

i = num_regs_key_used ;
while (i < AES_NUM_REGS_KEY) {
output! WRITE (AES_KEY00 + (i * 4), 0);
output! WRITE32 (AES_KEY00 + (i * 4), 0);
i = i + 1
}
))).
Expand All @@ -129,7 +130,7 @@ Section Impl.
([iv], [], bedrock_func_body:(
i = 0 ;
while (i < AES_NUM_REGS_IV) {
output! WRITE (AES_IV00 + (i * 4), load4( iv + (i * 4) ));
output! WRITE32 (AES_IV00 + (i * 4), load4( iv + (i * 4) ));
i = i + 1
}
))).
Expand All @@ -150,7 +151,7 @@ Section Impl.
bedrock_func_body:(
i = 0 ;
while (i < AES_NUM_REGS_DATA) {
output! WRITE (AES_DATA_IN00 + (i * 4), load4( data + (i * 4) ));
output! WRITE32 (AES_DATA_IN00 + (i * 4), load4( data + (i * 4) ));
i = i + 1
}
))).
Expand All @@ -172,7 +173,7 @@ Section Impl.
bedrock_func_body:(
i = 0 ;
while (i < AES_NUM_REGS_DATA) {
io! val = READ ( AES_DATA_OUT00 + (i * 4) ) ;
io! val = READ32 ( AES_DATA_OUT00 + (i * 4) ) ;
store4( data + (i * 4), val ) ; (* data[i] = val *)
i = i + 1
}
Expand All @@ -189,7 +190,7 @@ Section Impl.
("b2_data_ready",
([], [out],
bedrock_func_body:(
io! status = READ (AES_STATUS0) ;
io! status = READ32 (AES_STATUS0) ;
out = status & (1 << AES_STATUS_INPUT_READY)
))).

Expand All @@ -204,7 +205,7 @@ Section Impl.
("b2_data_valid",
([], [out],
bedrock_func_body:(
io! status = READ (AES_STATUS0) ;
io! status = READ32 (AES_STATUS0) ;
out = status & (1 << AES_STATUS_OUTPUT_VALID)
))).

Expand All @@ -219,7 +220,7 @@ Section Impl.
("b2_idle",
([], [out],
bedrock_func_body:(
io! status = READ (AES_STATUS0) ;
io! status = READ32 (AES_STATUS0) ;
out = status & (1 << AES_STATUS_IDLE)
))).

Expand Down
73 changes: 37 additions & 36 deletions investigations/bedrock2/Aes/AesProperties.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ Require Import coqutil.Tactics.letexists.
Require Import coqutil.Z.Lia.
Require Import Cava.Util.List.
Require Import Cava.Util.Tactics.
Require Import Bedrock2Experiments.LibBase.MMIOLabels.
Require Import Bedrock2Experiments.StateMachineSemantics.
Require Import Bedrock2Experiments.StateMachineProperties.
Require Import Bedrock2Experiments.Tactics.
Expand Down Expand Up @@ -139,7 +140,11 @@ Section Proofs.

Local Ltac infer :=
repeat first [ progress infer_states_equal
| progress infer_state_data_equal ].
| progress infer_state_data_equal
| match goal with
| H: parameters.read_step _ _ _ _ _ |- _ => apply proj2 in H
| H: parameters.write_step _ _ _ _ _ |- _ => apply proj2 in H
end ].

(* TODO: lots of annoying bit arithmetic here, maybe try to clean it up *)
Lemma status_read_always_ok s :
Expand All @@ -161,14 +166,14 @@ Section Proofs.
| H : Forall _ [] |- _ => clear H
end.
cbv beta in *.
destruct s; cbn [read_step reg_category status_matches_state].
{ exists (word.of_Z 0). eexists; ssplit; [ | reflexivity ].
destruct s; unfold read_step; cbn [read_step reg_category status_matches_state].
{ exists (word.of_Z 0). eexists; ssplit; try reflexivity; [].
cbv [is_flag_set]. boolsimpl.
rewrite !word.eqb_eq; [ reflexivity | apply word.unsigned_inj .. ].
all:push_unsigned; rewrite Z.land_0_l; reflexivity. }
{ exists (word.or (word.slu (word.of_Z 1) (word.of_Z AES_STATUS_IDLE))
(word.slu (word.of_Z 1) (word.of_Z AES_STATUS_INPUT_READY))).
eexists; ssplit; [ | reflexivity ].
eexists; ssplit; try reflexivity; [].
cbv [is_flag_set]. boolsimpl.
repeat lazymatch goal with
| |- (_ && _)%bool = true => apply Bool.andb_true_iff; split
Expand Down Expand Up @@ -205,7 +210,7 @@ Section Proofs.
(intro Heq; apply word.of_Z_inj_small in Heq; lia).
cbn [negb]. eauto. }
{ exists (word.slu (word.of_Z 1) (word.of_Z AES_STATUS_OUTPUT_VALID)).
eexists; split; [ | reflexivity ].
eexists; ssplit; try reflexivity; [].
rewrite is_flag_set_shift by (cbv [boolean]; tauto || lia).
rewrite word.eqb_ne by
(intro Heq; apply word.of_Z_inj_small in Heq; lia).
Expand Down Expand Up @@ -233,12 +238,12 @@ Section Proofs.
(forall s' val,
read_step s STATUS val s' ->
(* implied by other preconditions but convenient to have separately *)
execution ((map.empty, READ, [addr], (map.empty, [val])) :: t) s' ->
post ((map.empty, READ, [addr], (map.empty, [val])) :: t)
execution ((map.empty, READ32, [addr], (map.empty, [val])) :: t) s' ->
post ((map.empty, READ32, [addr], (map.empty, [val])) :: t)
m (map.put l bind val)) ->
cmd call (cmd.interact [bind] READ [addre]) t m l post.
cmd call (cmd.interact [bind] READ32 [addre]) t m l post.
Proof.
intros; eapply interact_read; intros; infer;
intros; eapply (interact_read 4); intros; infer;
cbv [parameters.read_step state_machine_parameters] in *;
eauto.
pose proof status_read_always_ok s. logical_simplify.
Expand All @@ -258,12 +263,11 @@ Section Proofs.
(forall s',
write_step s CTRL val s' ->
(* implied by other preconditions but convenient to have separately *)
execution ((map.empty, WRITE, [addr;val], (map.empty, [])) :: t) s' ->
post ((map.empty, WRITE, [addr;val], (map.empty, [])) :: t)
m l) ->
cmd call (cmd.interact [] WRITE [addre;vale]) t m l post.
execution ((map.empty, WRITE32, [addr;val], (map.empty, [])) :: t) s' ->
post ((map.empty, WRITE32, [addr;val], (map.empty, [])) :: t) m l) ->
cmd call (cmd.interact [] WRITE32 [addre;vale]) t m l post.
Proof.
intros; eapply interact_write; intros; infer;
intros; eapply (interact_write 4); intros; infer;
cbv [parameters.write_step state_machine_parameters] in *;
eauto.
cbv [write_step]. cbn [reg_category].
Expand Down Expand Up @@ -292,12 +296,11 @@ Section Proofs.
(forall s',
write_step (IDLE rs) (key_from_index i) val s' ->
(* implied by other preconditions but convenient to have separately *)
execution ((map.empty, WRITE, [addr;val], (map.empty, [])) :: t) s' ->
post ((map.empty, WRITE, [addr;val], (map.empty, [])) :: t)
m l) ->
cmd call (cmd.interact [] WRITE [addre;vale]) t m l post.
execution ((map.empty, WRITE32, [addr;val], (map.empty, [])) :: t) s' ->
post ((map.empty, WRITE32, [addr;val], (map.empty, [])) :: t) m l) ->
cmd call (cmd.interact [] WRITE32 [addre;vale]) t m l post.
Proof.
intros; eapply interact_write; intros; infer;
intros; eapply (interact_write 4); intros; infer;
cbv [parameters.write_step state_machine_parameters] in *;
eauto.
{ repeat (destruct i; try lia); subst; cbn; ring. }
Expand Down Expand Up @@ -325,12 +328,11 @@ Section Proofs.
(forall s',
write_step (IDLE rs) (iv_from_index i) val s' ->
(* implied by other preconditions but convenient to have separately *)
execution ((map.empty, WRITE, [addr;val], (map.empty, [])) :: t) s' ->
post ((map.empty, WRITE, [addr;val], (map.empty, [])) :: t)
m l) ->
cmd call (cmd.interact [] WRITE [addre;vale]) t m l post.
execution ((map.empty, WRITE32, [addr;val], (map.empty, [])) :: t) s' ->
post ((map.empty, WRITE32, [addr;val], (map.empty, [])) :: t) m l) ->
cmd call (cmd.interact [] WRITE32 [addre;vale]) t m l post.
Proof.
intros; eapply interact_write; intros; infer;
intros; eapply (interact_write 4); intros; infer;
cbv [parameters.write_step state_machine_parameters] in *;
eauto.
{ repeat (destruct i; try lia); subst; cbn; ring. }
Expand Down Expand Up @@ -358,12 +360,11 @@ Section Proofs.
(forall s',
write_step (IDLE rs) (data_in_from_index i) val s' ->
(* implied by other preconditions but convenient to have separately *)
execution ((map.empty, WRITE, [addr;val], (map.empty, [])) :: t) s' ->
post ((map.empty, WRITE, [addr;val], (map.empty, [])) :: t)
m l) ->
cmd call (cmd.interact [] WRITE [addre;vale]) t m l post.
execution ((map.empty, WRITE32, [addr;val], (map.empty, [])) :: t) s' ->
post ((map.empty, WRITE32, [addr;val], (map.empty, [])) :: t) m l) ->
cmd call (cmd.interact [] WRITE32 [addre;vale]) t m l post.
Proof.
intros; eapply interact_write; intros; infer;
intros; eapply (interact_write 4); intros; infer;
cbv [parameters.write_step state_machine_parameters] in *;
eauto.
{ repeat (destruct i; try lia); subst; cbn; ring. }
Expand Down Expand Up @@ -399,12 +400,12 @@ Section Proofs.
(forall s' val,
read_step (DONE data) (data_out_from_index i) val s' ->
(* implied by other preconditions but convenient to have separately *)
execution ((map.empty, READ, [addr], (map.empty, [val])) :: t) s' ->
post ((map.empty, READ, [addr], (map.empty, [val])) :: t)
execution ((map.empty, READ32, [addr], (map.empty, [val])) :: t) s' ->
post ((map.empty, READ32, [addr], (map.empty, [val])) :: t)
m (map.put l bind val)) ->
cmd call (cmd.interact [bind] READ [addre]) t m l post.
cmd call (cmd.interact [bind] READ32 [addre]) t m l post.
Proof.
intros; eapply interact_read with (r:=data_out_from_index i);
intros; eapply (interact_read 4) with (r:=data_out_from_index i);
intros; infer;
cbv [parameters.read_step state_machine_parameters] in *;
eauto.
Expand Down Expand Up @@ -526,9 +527,9 @@ Section Proofs.
done_data_out2 done_data_out3];
eauto .. | ].

Local Notation aes_op_t := (enum_member aes_op) (only parsing).
Local Notation aes_mode_t := (enum_member aes_mode) (only parsing).
Local Notation aes_key_len_t := (enum_member aes_key_len) (only parsing).
Local Notation aes_op_t := (enum_member (aes_op (aes_constants_ok := consts_ok))) (only parsing).
Local Notation aes_mode_t := (enum_member (aes_mode (aes_constants_ok := consts_ok))) (only parsing).
Local Notation aes_key_len_t := (enum_member (aes_key_len (aes_constants_ok := consts_ok))) (only parsing).

Definition ctrl_operation (ctrl : parameters.word) : bool :=
is_flag_set ctrl AES_CTRL_OPERATION.
Expand Down
41 changes: 21 additions & 20 deletions investigations/bedrock2/Aes/AesSemantics.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith.
Require Import Coq.Lists.List.
Require Import Coq.Numbers.DecimalString.
Require Import bedrock2.Syntax bedrock2.Semantics.
Require Import bedrock2.ZnWords.
Require coqutil.Datatypes.String coqutil.Map.SortedList.
Require coqutil.Map.SortedListString coqutil.Map.SortedListWord.
Require Import coqutil.Map.Interface.
Expand Down Expand Up @@ -534,31 +535,31 @@ Section WithParameters.
{| StateMachineSemantics.parameters.state := state ;
StateMachineSemantics.parameters.register := Register ;
StateMachineSemantics.parameters.is_initial_state := eq UNINITIALIZED ;
StateMachineSemantics.parameters.read_step := read_step ;
StateMachineSemantics.parameters.write_step := write_step ;
StateMachineSemantics.parameters.read_step sz s a v s' :=
sz = 4%nat /\ read_step s a v s';
StateMachineSemantics.parameters.write_step sz s a v s' :=
sz = 4%nat /\ write_step s a v s' ;
StateMachineSemantics.parameters.reg_addr := reg_addr ;
StateMachineSemantics.parameters.is_reg_addr a :=
List.Exists (fun r => a = reg_addr r) all_regs;
StateMachineSemantics.parameters.isMMIOAddr a :=
List.Exists (fun r =>
word.unsigned (reg_addr r) <= word.unsigned a < word.unsigned (reg_addr r) + 4
) all_regs;
|}.

Global Instance state_machine_parameters_ok
: StateMachineSemantics.parameters.ok state_machine_parameters.
Proof.
constructor.
{ left; exact eq_refl. }
{ exact word_ok. }
{ exact mem_ok. }
{ exact reg_addr_unique. }
{ unfold parameters.is_reg_addr. cbn. intros.
eapply Exists_exists in H. destruct H as (r & rI & ?). subst a.
eapply reg_addr_aligned. }
{ unfold parameters.is_reg_addr. cbn. intros.
eapply Exists_exists in H. destruct H as (r & rI & ?). subst a.
eapply reg_addr_small. }
{ unfold parameters.is_reg_addr. cbn. intros.
eapply Exists_exists. eauto using all_regs_complete. }
{ unfold parameters.is_reg_addr. cbn. intros.
eapply Exists_exists. eauto using all_regs_complete. }
Defined.
constructor;
unfold parameters.isMMIOAddr; cbn;
intros;
try exact _;
repeat match goal with
| H: _ /\ _ |- _ => destruct H
end;
subst;
try eapply Exists_exists;
eauto using all_regs_complete, reg_addr_aligned, reg_addr_unique with zarith;
try ZnWords.
Qed.

End WithParameters.
5 changes: 3 additions & 2 deletions investigations/bedrock2/Aes/AesToC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ Require Import bedrock2.Syntax.
Require Import bedrock2.ToCString.
Require Import bedrock2.Variables.
Require Import coqutil.Z.HexNotation.
Require Import Bedrock2Experiments.LibBase.MMIOLabels.
Require Import Bedrock2Experiments.Aes.AesSemantics.
Require Import Bedrock2Experiments.Aes.Aes.
Require Import Bedrock2Experiments.Aes.Constants.
Expand Down Expand Up @@ -49,10 +50,10 @@ static inline void _br2_store(uintptr_t a, uintptr_t v, size_t sz) {
}

// bedrock2 MMIO aliases
void MMIOWRITE(uintptr_t addr, uintptr_t value) {
void " ++ MMIOLabels.WRITE32 ++ "(uintptr_t addr, uintptr_t value) {
REG32(addr) = value;
}
uintptr_t MMIOREAD(uintptr_t addr) {
uintptr_t " ++ MMIOLabels.READ32 ++ "(uintptr_t addr) {
return REG32(addr);
}

Expand Down
Loading