diff options
| author | James Pollard <james@pollard.dev> | 2020-06-11 14:47:52 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-11 14:47:52 +0100 |
| commit | d0257b0a47ad998e01715e9bc6ba612b834765f1 (patch) | |
| tree | a356047d4cc1a0f6fb008d63512184d4075ee4e4 /src/verilog | |
| parent | d3be4601c9bc68fddaf4dc08c648f03d95a39e1d (diff) | |
| download | vericert-d0257b0a47ad998e01715e9bc6ba612b834765f1.tar.gz vericert-d0257b0a47ad998e01715e9bc6ba612b834765f1.zip | |
Working on proof.
Diffstat (limited to 'src/verilog')
| -rw-r--r-- | src/verilog/HTL.v | 21 | ||||
| -rw-r--r-- | src/verilog/Value.v | 5 |
2 files changed, 20 insertions, 6 deletions
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 2e4ef1a..82aac41 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -46,6 +46,7 @@ Record module: Type := mod_entrypoint : node; mod_st : reg; mod_stk : reg; + mod_stk_len : nat; mod_finish : reg; mod_return : reg }. @@ -60,6 +61,14 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := | _, _ => empty_assocmap end. +Fixpoint zeroes' (acc : list value) (n : nat) : list value := + match n with + | O => acc + | S n => zeroes' ((NToValue 32 0)::acc) n + end. + +Definition zeroes : nat -> list value := zeroes' nil. + (** * Operational Semantics *) Definition genv := Globalenvs.Genv.t fundef unit. @@ -69,7 +78,8 @@ Inductive stackframe : Type := forall (res : reg) (m : module) (pc : node) - (assoc : assocmap), + (reg_assoc : assocmap) + (arr_assoc : AssocMap.t (list value)), stackframe. Inductive state : Type := @@ -125,13 +135,12 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (State res m m.(mod_entrypoint) (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint)) (init_regs args m.(mod_params))) - (AssocMap.empty (list value))) + (AssocMap.set m.(mod_stk) (zeroes m.(mod_stk_len)) (AssocMap.empty (list value)))) | step_return : - forall g m asr i r sf pc mst, + forall g m asr asa i r sf pc mst, mst = mod_st m -> - step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0 - (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) - (AssocMap.empty (list value))). + step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 + (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) asa). Hint Constructors step : htl. Inductive initial_state (p: program): state -> Prop := diff --git a/src/verilog/Value.v b/src/verilog/Value.v index d527b15..b1ee353 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -296,6 +296,11 @@ Inductive val_value_lessdef: val -> value -> Prop := val_value_lessdef (Vint i) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. +Inductive opt_val_value_lessdef: option val -> value -> Prop := +| opt_lessdef_some: + forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v' +| opt_lessdef_none: forall v, opt_val_value_lessdef None v. + Lemma valueToZ_ZToValue : forall n z, (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z -> |