From 75ae0dd0a0cb4afdc5bbb10f7c9b6713290a42d2 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Fri, 18 Jun 2021 18:01:28 -0400 Subject: [PATCH 1/5] in StateMachineSemantics, replace all_regs and all_regs_complete by is_reg_addr and read/write_step_is_reg_addr, respectively, so that we can use word as the register type even though not all words are registers. Also generalize initial_state to is_initial_state. --- investigations/bedrock2/Aes/AesSemantics.v | 18 ++++-- investigations/bedrock2/StateMachineMMIO.v | 60 ++++++++----------- .../bedrock2/StateMachineSemantics.v | 13 ++-- 3 files changed, 46 insertions(+), 45 deletions(-) diff --git a/investigations/bedrock2/Aes/AesSemantics.v b/investigations/bedrock2/Aes/AesSemantics.v index c06842ccb..ea4aecb4a 100644 --- a/investigations/bedrock2/Aes/AesSemantics.v +++ b/investigations/bedrock2/Aes/AesSemantics.v @@ -533,11 +533,12 @@ Section WithParameters. : StateMachineSemantics.parameters 32 word mem := {| StateMachineSemantics.parameters.state := state ; StateMachineSemantics.parameters.register := Register ; - StateMachineSemantics.parameters.initial_state := UNINITIALIZED ; + StateMachineSemantics.parameters.is_initial_state := eq UNINITIALIZED ; StateMachineSemantics.parameters.read_step := read_step ; StateMachineSemantics.parameters.write_step := write_step ; StateMachineSemantics.parameters.reg_addr := reg_addr ; - StateMachineSemantics.parameters.all_regs := all_regs; + StateMachineSemantics.parameters.is_reg_addr a := + List.Exists (fun r => a = reg_addr r) all_regs; |}. Global Instance state_machine_parameters_ok @@ -548,9 +549,16 @@ Section WithParameters. { exact word_ok. } { exact mem_ok. } { exact reg_addr_unique. } - { exact all_regs_complete. } - { exact reg_addr_aligned. } - { exact reg_addr_small. } + { 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. End WithParameters. diff --git a/investigations/bedrock2/StateMachineMMIO.v b/investigations/bedrock2/StateMachineMMIO.v index 1e082a959..f1f6b5998 100644 --- a/investigations/bedrock2/StateMachineMMIO.v +++ b/investigations/bedrock2/StateMachineMMIO.v @@ -124,13 +124,8 @@ Section MMIO1. |}. Instance StateMachineMMIOSpec : MMIOSpec := - {| isMMIOAddr := - fun w => - Exists - (fun r => word.unsigned (parameters.reg_addr r) - <= word.unsigned w - <= word.unsigned (parameters.reg_addr r) + 4) - parameters.all_regs; + {| isMMIOAddr w := exists a, parameters.is_reg_addr a /\ + word.unsigned a <= word.unsigned w < word.unsigned a + 4; isMMIOAligned := fun n addr => n = 4%nat /\ (word.unsigned addr) mod 4 = 0; MMIOReadOK := fun n log addr val => @@ -218,14 +213,7 @@ Section MMIO1. ~ isMMIOAddr y -> x <> y. Proof. - unfold isMMIOAddr, StateMachineMMIOSpec in *. - intros *. rewrite <-Forall_Exists_neg. - rewrite Forall_forall, Exists_exists. - intros; logical_simplify. - intro; subst. - match goal with - | H : _ |- _ => eapply H; solve [eauto] - end. + intros x y Hx Hy C. subst. apply Hy. apply Hx. Qed. Instance FlatToRiscv_hyps: FlatToRiscvCommon.assumptions. @@ -246,15 +234,6 @@ Section MMIO1. change (@width Words32) with 32 in *; change (@Utility.word Words32) with (@word p) in *. - Lemma reg_addr_is_mmio r : isMMIOAddr (parameters.reg_addr r). - Proof. - pose proof word.unsigned_range (parameters.reg_addr r). - cbv [isMMIOAddr StateMachineMMIOSpec]. - apply Exists_exists. exists r. - split; [ apply parameters.all_regs_complete | ]. - simpl_paramrecords. auto with zarith. - Qed. - Lemma compile_ext_call_correct: forall resvars extcall argvars, FlatToRiscvCommon.compiles_FlatToRiscv_correctly (@FlatToRiscvDef.compile_ext_call compilation_params) @@ -366,11 +345,16 @@ Section MMIO1. end. cbv [Utility.add Utility.ZToReg MachineWidth_XLEN]; rewrite add_0_r. - unshelve erewrite (_ : _ = None); [eapply storeWord_in_MMIO_is_None; eauto using reg_addr_is_mmio |]. + unshelve erewrite (_ : _ = None). { + eapply storeWord_in_MMIO_is_None. 1: eassumption. + cbn. eexists. split; [eauto using parameters.write_step_is_reg_addr|blia]. + } cbv [MinimalMMIO.nonmem_store StateMachineMMIOSpec]. - split; [eauto using reg_addr_is_mmio|]. - split; [red; auto using parameters.reg_addrs_aligned|]. + split. { + cbn. eexists. split; [eauto using parameters.write_step_is_reg_addr|blia]. + } + split; [red; eauto using parameters.write_step_is_reg_addr, parameters.reg_addrs_aligned|]. repeat fwd. @@ -410,7 +394,10 @@ Section MMIO1. clear. unfold subset, PropSet.elem_of. intros. firstorder idtac. } eapply subset_trans. 1: eassumption. - clear -(*D4 M0*) D state_machine_parameters_ok. + assert (parameters.is_reg_addr (parameters.reg_addr x)) as IR. { + eauto using parameters.write_step_is_reg_addr. + } + clear -(*D4 M0*) IR D state_machine_parameters_ok. unfold invalidateWrittenXAddrs. change removeXAddr with (@List.removeb word word.eqb _). rewrite ?ListSet.of_list_removeb. @@ -420,13 +407,13 @@ Section MMIO1. specialize (D y). destruct D; [contradiction|]. rewrite ?and_assoc. split; [exact HIn|clear HIn]. - pose proof (parameters.reg_addrs_small x). + pose proof (parameters.reg_addrs_small (parameters.reg_addr x) IR). change (Memory.bytes_per_word 32) with 4 in *. pose proof (word.unsigned_range (parameters.reg_addr x)). ssplit; eapply disjoint_MMIO_goal; eauto. all:cbv [isMMIOAddr StateMachineMMIOSpec]. - all:eapply Exists_exists; exists x. - all:split; [ apply parameters.all_regs_complete | ]. + all:exists (parameters.reg_addr x). + all:split; [ exact IR | ]. all:simpl_paramrecords. all:push_unsigned. all:auto with zarith. } @@ -516,11 +503,16 @@ Section MMIO1. split; try discriminate. cbv [Utility.add Utility.ZToReg MachineWidth_XLEN]; rewrite add_0_r. - unshelve erewrite (_ : _ = None); [eapply loadWord_in_MMIO_is_None|]; eauto using reg_addr_is_mmio. + unshelve erewrite (_ : _ = None). { + eapply loadWord_in_MMIO_is_None. 1: eassumption. + cbn. eexists. split; [eauto using parameters.read_step_is_reg_addr|blia]. + } cbv [MinimalMMIO.nonmem_load StateMachineMMIOSpec]. - split; [apply reg_addr_is_mmio|]. - split; [red; auto using parameters.reg_addrs_aligned|]. + split. { + cbn. eexists. split; [eauto using parameters.read_step_is_reg_addr|blia]. + } + split; [red; eauto using parameters.read_step_is_reg_addr, parameters.reg_addrs_aligned|]. split. { cbv [MMIOReadOK]. let val := lazymatch goal with diff --git a/investigations/bedrock2/StateMachineSemantics.v b/investigations/bedrock2/StateMachineSemantics.v index d4e8642c6..cb61a3466 100644 --- a/investigations/bedrock2/StateMachineSemantics.v +++ b/investigations/bedrock2/StateMachineSemantics.v @@ -16,11 +16,11 @@ Module parameters. {mem : Interface.map.map word Byte.byte} := { state : Type; register : Type; - initial_state : state; + is_initial_state : state -> Prop; read_step : state -> register -> word -> state -> Prop; write_step : state -> register -> word -> state -> Prop; reg_addr : register -> word; - all_regs : list register; + is_reg_addr : word -> Prop; }. Global Arguments parameters : clear implicits. @@ -29,11 +29,12 @@ Module parameters. word_ok : word.ok word; (* for impl of mem below *) mem_ok : Interface.map.ok mem; (* for impl of mem below *) reg_addr_unique : forall r1 r2, reg_addr r1 = reg_addr r2 -> r1 = r2; - all_regs_complete : forall r, List.In r all_regs; reg_addrs_aligned : - forall r, word.unsigned (reg_addr r) mod (bytes_per_word width) = 0; + forall a, is_reg_addr a -> word.unsigned a mod (bytes_per_word width) = 0; reg_addrs_small : - forall r, word.unsigned (reg_addr r) + bytes_per_word width <= 2 ^ width; + forall a, is_reg_addr a -> word.unsigned a + bytes_per_word width <= 2 ^ width; + read_step_is_reg_addr : forall s a v s', read_step s a v s' -> is_reg_addr (reg_addr a); + write_step_is_reg_addr : forall s a v s', write_step s a v s' -> is_reg_addr (reg_addr a); }. End parameters. Notation parameters := parameters.parameters. @@ -70,7 +71,7 @@ Section WithParameters. trace *) Fixpoint execution (t : bedrock2_trace) (s : state) : Prop := match t with - | [] => s = initial_state + | [] => is_initial_state s | (_,action,args,(_,rets)) :: t => exists prev_state, execution t prev_state From 7e48316247215947bf20e6eff0f4e3a95810d5e1 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Fri, 18 Jun 2021 18:49:52 -0400 Subject: [PATCH 2/5] get started with hmac state machine --- investigations/bedrock2/Hmac/Hmac.v | 2 + investigations/bedrock2/Hmac/HmacSemantics.v | 97 ++++++++++++++++++++ 2 files changed, 99 insertions(+) create mode 100644 investigations/bedrock2/Hmac/HmacSemantics.v diff --git a/investigations/bedrock2/Hmac/Hmac.v b/investigations/bedrock2/Hmac/Hmac.v index 3ad9e04b8..b61bdc814 100644 --- a/investigations/bedrock2/Hmac/Hmac.v +++ b/investigations/bedrock2/Hmac/Hmac.v @@ -58,6 +58,8 @@ Definition b2_hmac_sha256_init: func := ("b2_hmac_sha256_init", ([], [], bedrock_func_body:( (* Clear the config, stopping the SHA engine. *) + (* Note: the above comment might be misleading: if the SHA engine is running, + writes to the CFG register are discarded, says the doc *) abs_mmio_write32(TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_CFG_REG_OFFSET, 0); (* Disable and clear interrupts. INTR_STATE register is rw1c. *) diff --git a/investigations/bedrock2/Hmac/HmacSemantics.v b/investigations/bedrock2/Hmac/HmacSemantics.v new file mode 100644 index 000000000..e92006f93 --- /dev/null +++ b/investigations/bedrock2/Hmac/HmacSemantics.v @@ -0,0 +1,97 @@ +Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +Require Import Coq.Lists.List. Import ListNotations. +Require Import Coq.micromega.Lia. +Require Import coqutil.Byte. +Require Import coqutil.Map.Interface. +Require Import coqutil.Word.Interface. +Require Import Bedrock2Experiments.StateMachineSemantics. +Require Import Bedrock2Experiments.Hmac.Constants. + +(* Note: AesSemantics.v seems to completely ignore its control register, + which results in a wrong specification in the sense that the specification + might say that a transition is possible even though it isn't. + In HmacSemantics.v, we don't attempt to model all features of the Hmac module either, + but we do try to reveal a correct subset of the full functionality of the + Hmac module. We only say that a transition is possible if the module has + been configured to use the mode that we're modeling, and disallow transitions + from an idle state that's not configured to use the mode that we're modeling. *) + +Axiom sha256: list byte -> list byte. + +Section WithParams. + Context {word: word 32} {mem: map.map word byte} + {word_ok: word.ok word} {mem_ok: map.ok mem}. + + Record idle_data := { + interrupts_enabled: bool; (* are interrupts enabled? *) + pending_interrupts: word; + hmac_en: bool; + sha_en: bool; + swap_endian: bool; + swap_digest: bool; + }. + + Definition the_only_supported_config: idle_data := {| + interrupts_enabled := false; + pending_interrupts := word.of_Z 0; + swap_digest := false; + swap_endian := true; + sha_en := true; + hmac_en := false; + |}. + + Inductive state := + | IDLE(config: idle_data) + | CONSUMING(sha_buffer: list byte) + | PROCESSING(sha_buffer: list byte) + | DONE(digest_buffer: list byte). + + Inductive read_step: state -> word -> word -> state -> Prop := . + + Inductive write_step: state -> word -> word -> state -> Prop := + | write_step_cfg: forall v s, + write_step (IDLE s) (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_CFG_REG_OFFSET)) v + (IDLE {| interrupts_enabled := interrupts_enabled s; + pending_interrupts := pending_interrupts s; + hmac_en := Z.testbit 0 (word.unsigned v); + sha_en := Z.testbit 1 (word.unsigned v); + swap_endian := Z.testbit 2 (word.unsigned v); + swap_digest := Z.testbit 3 (word.unsigned v); |}). + + Definition HMAC_MMIO_START: Z := + TOP_EARLGREY_HMAC_BASE_ADDR. + Definition HMAC_MMIO_PAST_END: Z := + TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_MSG_FIFO_REG_OFFSET + HMAC_MSG_FIFO_SIZE_BYTES. + + Global Instance state_machine_parameters: StateMachineSemantics.parameters 32 word mem := {| + StateMachineSemantics.parameters.state := state ; + StateMachineSemantics.parameters.register := word; + StateMachineSemantics.parameters.is_initial_state s := + match s with + | IDLE _ => True + | _ => False + end; + StateMachineSemantics.parameters.read_step := read_step; + StateMachineSemantics.parameters.write_step := write_step; + StateMachineSemantics.parameters.reg_addr := id; + StateMachineSemantics.parameters.is_reg_addr a := + HMAC_MMIO_START <= word.unsigned a < HMAC_MMIO_PAST_END /\ word.unsigned a mod 4 = 0; + |}. + + Axiom TODO: False. + + Global Instance state_machine_parameters_ok + : StateMachineSemantics.parameters.ok state_machine_parameters. + Proof. + constructor. + { left; exact eq_refl. } + { exact word_ok. } + { exact mem_ok. } + { cbn. unfold id. auto. } + { cbn. intuition auto. } + { cbn. lia. } + { cbn. unfold id. intros. inversion H; try lia; case TODO. } + { cbn. unfold id. intros. inversion H; try lia; case TODO. } + Qed. + +End WithParams. From b4ffc640b032343da3bde088fa700070b29819db Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Mon, 21 Jun 2021 12:50:46 -0400 Subject: [PATCH 3/5] wip hmac state machine, problem in hmac_sha256_final: after the done bit is detected, it is cleared by writing again 1 to it because it's rw1c, need to model this --- investigations/bedrock2/Hmac/HmacSemantics.v | 85 +++++++++++++++++--- 1 file changed, 75 insertions(+), 10 deletions(-) diff --git a/investigations/bedrock2/Hmac/HmacSemantics.v b/investigations/bedrock2/Hmac/HmacSemantics.v index e92006f93..2d91f8cb3 100644 --- a/investigations/bedrock2/Hmac/HmacSemantics.v +++ b/investigations/bedrock2/Hmac/HmacSemantics.v @@ -4,6 +4,7 @@ Require Import Coq.micromega.Lia. Require Import coqutil.Byte. Require Import coqutil.Map.Interface. Require Import coqutil.Word.Interface. +Require Import coqutil.Word.LittleEndianList. Require Import Bedrock2Experiments.StateMachineSemantics. Require Import Bedrock2Experiments.Hmac.Constants. @@ -18,12 +19,19 @@ Require Import Bedrock2Experiments.Hmac.Constants. Axiom sha256: list byte -> list byte. +Class timing := { + (* Max number of consecutive polls for "done" that can return "not done", + needed to prove termination of bedrock2 code. *) + max_negative_done_polls: Z; +}. + Section WithParams. Context {word: word 32} {mem: map.map word byte} - {word_ok: word.ok word} {mem_ok: map.ok mem}. + {word_ok: word.ok word} {mem_ok: map.ok mem} + {tim: timing}. - Record idle_data := { - interrupts_enabled: bool; (* are interrupts enabled? *) + Record config_data := { + interrupts_enabled: word; (* bit #i says if interrupt #i is enabled, i=0,1,2 *) pending_interrupts: word; hmac_en: bool; sha_en: bool; @@ -31,8 +39,8 @@ Section WithParams. swap_digest: bool; }. - Definition the_only_supported_config: idle_data := {| - interrupts_enabled := false; + Definition the_only_supported_config: config_data := {| + interrupts_enabled := word.of_Z 0; pending_interrupts := word.of_Z 0; swap_digest := false; swap_endian := true; @@ -41,22 +49,79 @@ Section WithParams. |}. Inductive state := - | IDLE(config: idle_data) + | IDLE(config: config_data) | CONSUMING(sha_buffer: list byte) - | PROCESSING(sha_buffer: list byte) + | PROCESSING(sha_buffer: list byte)(max_cycles_until_done: Z) | DONE(digest_buffer: list byte). - Inductive read_step: state -> word -> word -> state -> Prop := . + Inductive read_step: state -> word -> word -> state -> Prop := + | read_done_bit_not_done: forall b v n, + 0 < n -> + Z.testbit (word.unsigned v) HMAC_INTR_STATE_HMAC_DONE_BIT = false -> + read_step (PROCESSING b n) + (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_INTR_STATE_REG_OFFSET)) v + (PROCESSING b (n-1)) + | read_done_bit_done: forall b v n, + Z.testbit (word.unsigned v) HMAC_INTR_STATE_HMAC_DONE_BIT = true -> + read_step (PROCESSING b n) + (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_INTR_STATE_REG_OFFSET)) v + (DONE (sha256 b)). Inductive write_step: state -> word -> word -> state -> Prop := - | write_step_cfg: forall v s, + | write_cfg: forall v s, + 0 <= word.unsigned v < 2 ^ 4 -> write_step (IDLE s) (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_CFG_REG_OFFSET)) v (IDLE {| interrupts_enabled := interrupts_enabled s; pending_interrupts := pending_interrupts s; hmac_en := Z.testbit 0 (word.unsigned v); sha_en := Z.testbit 1 (word.unsigned v); swap_endian := Z.testbit 2 (word.unsigned v); - swap_digest := Z.testbit 3 (word.unsigned v); |}). + swap_digest := Z.testbit 3 (word.unsigned v); |}) + | write_intr_enable: forall v s, + 0 <= word.unsigned v < 2 ^ 3 -> + write_step (IDLE s) (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_INTR_ENABLE_REG_OFFSET)) v + (IDLE {| interrupts_enabled := v; + pending_interrupts := pending_interrupts s; + hmac_en := hmac_en s; + sha_en := sha_en s; + swap_endian := swap_endian s; + swap_digest := swap_digest s; |}) + | write_intr_state: forall v s, + 0 <= word.unsigned v < 2 ^ 3 -> + write_step (IDLE s) (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_INTR_STATE_REG_OFFSET)) v + (IDLE {| interrupts_enabled := interrupts_enabled s; + pending_interrupts := v; (* TODO FIX these bits are rw1c! *) + hmac_en := hmac_en s; + sha_en := sha_en s; + swap_endian := swap_endian s; + swap_digest := swap_digest s; |}) + | write_hash_start: + write_step (IDLE the_only_supported_config) + (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_CMD_REG_OFFSET)) + (word.of_Z (Z.shiftl 1 HMAC_CMD_HASH_START_BIT)) + (CONSUMING []) + | write_byte: forall b v, + write_step (CONSUMING b) + (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_MSG_FIFO_REG_OFFSET)) v + (CONSUMING (b ++ [byte.of_Z (word.unsigned v)])) + | write_word: forall b v, + write_step (CONSUMING b) + (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_MSG_FIFO_REG_OFFSET)) v + (CONSUMING (b ++ le_split 4 (word.unsigned v))) + | write_hash_process: forall b, + write_step (CONSUMING b) + (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_CMD_REG_OFFSET)) + (word.of_Z (Z.shiftl 1 HMAC_CMD_HASH_PROCESS_BIT)) + (PROCESSING b max_negative_done_polls). + + (* TODO: Can we make these register conventions more explicit in our spec? + ro read-only + wo write-only + rw read/write + rw1c read/write, writing 1 clears the bit, writing 0 has no effect + rw0c read/write, writing 0 clears the bit, writing 1 has no effect + rw1s read/write, writing 1 sets the bit, writing 0 has no effect *) + Definition HMAC_MMIO_START: Z := TOP_EARLGREY_HMAC_BASE_ADDR. From ff5067016f47f6efc4a123259b6aad79f4439526 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Mon, 21 Jun 2021 16:39:29 -0400 Subject: [PATCH 4/5] finish first sketch of hmac state machine --- investigations/bedrock2/Hmac/HmacSemantics.v | 189 +++++++++++++------ 1 file changed, 128 insertions(+), 61 deletions(-) diff --git a/investigations/bedrock2/Hmac/HmacSemantics.v b/investigations/bedrock2/Hmac/HmacSemantics.v index 2d91f8cb3..647205354 100644 --- a/investigations/bedrock2/Hmac/HmacSemantics.v +++ b/investigations/bedrock2/Hmac/HmacSemantics.v @@ -17,42 +17,80 @@ Require Import Bedrock2Experiments.Hmac.Constants. been configured to use the mode that we're modeling, and disallow transitions from an idle state that's not configured to use the mode that we're modeling. *) -Axiom sha256: list byte -> list byte. - Class timing := { (* Max number of consecutive polls for "done" that can return "not done", needed to prove termination of bedrock2 code. *) max_negative_done_polls: Z; }. +(* TODO integrate upstream *) +Require Import bedrock2.ZnWords. +Require Import coqutil.Tactics.Tactics. +Require Import Coq.Program.Tactics. +Require Import coqutil.Z.Lia. +(* use old version of canonicalize_word_width_and_instance because newer version + calls simpl_param_projections, which doesn't support parameter records with + more than 3 parameters in the *type* *) +Ltac canonicalize_word_width_and_instance ::= + repeat so fun hyporgoal => match hyporgoal with + | context [@word.unsigned ?wi ?inst] => + let wi' := eval cbn in wi in let inst' := eval cbn in inst in + progress ( change wi with wi' in *; change inst with inst' in * ) + | context [@word.signed ?wi ?inst] => + let wi' := eval cbn in wi in let inst' := eval cbn in inst in + progress ( change wi with wi' in *; change inst with inst' in * ) + | context[2 ^ ?wi] => + let wi' := eval cbn in wi in (* <-- will blow up as soon as we have 2^bigExpression... *) + progress ( change wi with wi' in * ) + end. +(* Fix cleanup_for_ZModArith to not clear word_ok (wasn't a problem until now because + there was always an instance of bedrock2.Semantics.parameters_ok depending on word_ok, + preventing word_ok from being cleared). *) +Ltac cleanup_for_ZModArith ::= + subst*; (* <-- substituting `@eq word _ _` might create opportunities for wordOps_to_ZModArith_step *) + repeat match goal with + | a := _ |- _ => subst a + | H: ?T |- _ => lazymatch T with + | @word.ok _ _ => fail + | _ => tryif is_lia T then fail else clear H + end + end. + + Section WithParams. Context {word: word 32} {mem: map.map word byte} {word_ok: word.ok word} {mem_ok: map.ok mem} {tim: timing}. - Record config_data := { - interrupts_enabled: word; (* bit #i says if interrupt #i is enabled, i=0,1,2 *) - pending_interrupts: word; + (* Note: sha256 only accepts messages of size up to `2^64-1` bits, so if we don't model + this restriction, we will have to be careful to not make contradictory assumptions + (eg if we add the MSG_LENGTH_LOWER and MSG_LENGTH_UPPER registers, we'll have to make + sure we don't assume that any list length can fit into these 2^64 bits, because + that would allow us to prove False). *) + Axiom sha256: list byte -> list word. (* returns a list of 8 32-bit words (=256 bits) *) + + Record idle_data := { + (* only the lowest 3 bits count, and we only model the case where all interrupts are + disabled, but we do have to check that the software disabled them *) + intr_enable: word; + + (* The hmac_done rw1c bit of hmac.INTR_STATE. + Writing true to it if true clears it (sets it to false) *) + hmac_done: bool; + + (* The bits of hmac.CFG *) hmac_en: bool; sha_en: bool; - swap_endian: bool; - swap_digest: bool; + swap_endian: bool; (* *false* means input is big-endian *) + swap_digest: bool; (* *true* means output is big-endian *) }. - Definition the_only_supported_config: config_data := {| - interrupts_enabled := word.of_Z 0; - pending_interrupts := word.of_Z 0; - swap_digest := false; - swap_endian := true; - sha_en := true; - hmac_en := false; - |}. - Inductive state := - | IDLE(config: config_data) + | IDLE(digest_buffer: list word)(s: idle_data) + (* since the configuration bits of idle_data can't be modified while CONSUMING or + PROCESSING, we don't need to include this data in these states *) | CONSUMING(sha_buffer: list byte) - | PROCESSING(sha_buffer: list byte)(max_cycles_until_done: Z) - | DONE(digest_buffer: list byte). + | PROCESSING(sha_buffer: list byte)(max_cycles_until_done: Z). Inductive read_step: state -> word -> word -> state -> Prop := | read_done_bit_not_done: forall b v n, @@ -65,38 +103,65 @@ Section WithParams. Z.testbit (word.unsigned v) HMAC_INTR_STATE_HMAC_DONE_BIT = true -> read_step (PROCESSING b n) (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_INTR_STATE_REG_OFFSET)) v - (DONE (sha256 b)). + (IDLE (sha256 b) + {| (* flag in INTR_STATE is set (even though interrupts are disabled) *) + hmac_done := true; + (* the remaining flags are the same as when we started processing: *) + intr_enable := word.of_Z 0; + hmac_en := false; + sha_en := true; + swap_endian := true; + swap_digest := false; + |}) + (* TODO the digest could also be read byte by byte *) + | read_digest: forall s d i v, + swap_endian s = true -> + swap_digest s = false -> + 0 <= i < 8 -> + List.nth_error d (Z.to_nat i) = Some v -> + read_step (IDLE d s) + (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_DIGEST_7_REG_OFFSET - (i * 4))) v + (IDLE d s). Inductive write_step: state -> word -> word -> state -> Prop := - | write_cfg: forall v s, - 0 <= word.unsigned v < 2 ^ 4 -> - write_step (IDLE s) (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_CFG_REG_OFFSET)) v - (IDLE {| interrupts_enabled := interrupts_enabled s; - pending_interrupts := pending_interrupts s; - hmac_en := Z.testbit 0 (word.unsigned v); - sha_en := Z.testbit 1 (word.unsigned v); - swap_endian := Z.testbit 2 (word.unsigned v); - swap_digest := Z.testbit 3 (word.unsigned v); |}) - | write_intr_enable: forall v s, - 0 <= word.unsigned v < 2 ^ 3 -> - write_step (IDLE s) (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_INTR_ENABLE_REG_OFFSET)) v - (IDLE {| interrupts_enabled := v; - pending_interrupts := pending_interrupts s; - hmac_en := hmac_en s; - sha_en := sha_en s; - swap_endian := swap_endian s; - swap_digest := swap_digest s; |}) - | write_intr_state: forall v s, - 0 <= word.unsigned v < 2 ^ 3 -> - write_step (IDLE s) (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_INTR_STATE_REG_OFFSET)) v - (IDLE {| interrupts_enabled := interrupts_enabled s; - pending_interrupts := v; (* TODO FIX these bits are rw1c! *) - hmac_en := hmac_en s; - sha_en := sha_en s; - swap_endian := swap_endian s; - swap_digest := swap_digest s; |}) - | write_hash_start: - write_step (IDLE the_only_supported_config) + | write_cfg: forall v d s, + write_step (IDLE d s) (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_CFG_REG_OFFSET)) v + (IDLE d {| intr_enable := intr_enable s; + hmac_done := hmac_done s; + hmac_en := Z.testbit 0 (word.unsigned v); + sha_en := Z.testbit 1 (word.unsigned v); + swap_endian := Z.testbit 2 (word.unsigned v); + swap_digest := Z.testbit 3 (word.unsigned v); |}) + | write_intr_enable: forall v d s, + write_step (IDLE d s) (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_INTR_ENABLE_REG_OFFSET)) v + (IDLE d {| intr_enable := word.and v (word.of_Z 7); + hmac_done := hmac_done s; + hmac_en := hmac_en s; + sha_en := sha_en s; + swap_endian := swap_endian s; + swap_digest := swap_digest s; |}) + | write_intr_state: forall v d s, + write_step (IDLE d s) (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_INTR_STATE_REG_OFFSET)) v + (IDLE d {| (* hmac_done is rw1c (clear on write-1) *) + hmac_done := if Z.testbit (word.unsigned v) HMAC_INTR_STATE_HMAC_DONE_BIT + then false else hmac_done s; + intr_enable := intr_enable s; + hmac_en := hmac_en s; + sha_en := sha_en s; + swap_endian := swap_endian s; + swap_digest := swap_digest s; |}) + | write_hash_start: forall d, + write_step (IDLE d (* Here one can see that we only model a subset of the features of + the HMAC module: in our model, starting the computation is only + possible from the specific configuration below. + But using an HMAC module with more features than what we expose + to the software is safe, so modeling only a subset is not a problem. *) + {| hmac_done := false; + intr_enable := word.of_Z 0; + hmac_en := false; + sha_en := true; + swap_endian := true; + swap_digest := false; |}) (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_CMD_REG_OFFSET)) (word.of_Z (Z.shiftl 1 HMAC_CMD_HASH_START_BIT)) (CONSUMING []) @@ -115,13 +180,17 @@ Section WithParams. (PROCESSING b max_negative_done_polls). (* TODO: Can we make these register conventions more explicit in our spec? - ro read-only - wo write-only - rw read/write - rw1c read/write, writing 1 clears the bit, writing 0 has no effect - rw0c read/write, writing 0 clears the bit, writing 1 has no effect - rw1s read/write, writing 1 sets the bit, writing 0 has no effect *) - + https://docs.opentitan.org/doc/rm/register_tool/ + none No access + ro Read Only + rc Read Only, reading clears + rw Read/Write + r0w1c Read zero, Write with 1 clears + rw1s Read, Write with 1 sets + rw1c Read, Write with 1 clears + rw0c Read, Write with 0 clears + wo Write Only + *) Definition HMAC_MMIO_START: Z := TOP_EARLGREY_HMAC_BASE_ADDR. @@ -133,7 +202,7 @@ Section WithParams. StateMachineSemantics.parameters.register := word; StateMachineSemantics.parameters.is_initial_state s := match s with - | IDLE _ => True + | IDLE digest_buffer _ => List.length digest_buffer = 8%nat | _ => False end; StateMachineSemantics.parameters.read_step := read_step; @@ -143,8 +212,6 @@ Section WithParams. HMAC_MMIO_START <= word.unsigned a < HMAC_MMIO_PAST_END /\ word.unsigned a mod 4 = 0; |}. - Axiom TODO: False. - Global Instance state_machine_parameters_ok : StateMachineSemantics.parameters.ok state_machine_parameters. Proof. @@ -155,8 +222,8 @@ Section WithParams. { cbn. unfold id. auto. } { cbn. intuition auto. } { cbn. lia. } - { cbn. unfold id. intros. inversion H; try lia; case TODO. } - { cbn. unfold id. intros. inversion H; try lia; case TODO. } + { cbn. unfold id. intros. inversion H; ZnWords. } + { cbn. unfold id. intros. inversion H; ZnWords. } Qed. End WithParams. From 6cc5801f98a526d9582536cd7030e5d6de8c6aa0 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Tue, 22 Jun 2021 16:59:52 -0400 Subject: [PATCH 5/5] make sure comment only mentions what's in its own file, so that comments are less prone to getting out of date --- investigations/bedrock2/Hmac/HmacSemantics.v | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/investigations/bedrock2/Hmac/HmacSemantics.v b/investigations/bedrock2/Hmac/HmacSemantics.v index 647205354..7615f6977 100644 --- a/investigations/bedrock2/Hmac/HmacSemantics.v +++ b/investigations/bedrock2/Hmac/HmacSemantics.v @@ -8,10 +8,7 @@ Require Import coqutil.Word.LittleEndianList. Require Import Bedrock2Experiments.StateMachineSemantics. Require Import Bedrock2Experiments.Hmac.Constants. -(* Note: AesSemantics.v seems to completely ignore its control register, - which results in a wrong specification in the sense that the specification - might say that a transition is possible even though it isn't. - In HmacSemantics.v, we don't attempt to model all features of the Hmac module either, +(* In HmacSemantics.v, we don't attempt to model all features of the Hmac module, but we do try to reveal a correct subset of the full functionality of the Hmac module. We only say that a transition is possible if the module has been configured to use the mode that we're modeling, and disallow transitions