diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-06-30 23:40:43 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-06-30 23:40:43 +0100 |
| commit | ded5a15a0ebcda4d11af32b3c4a46048b11e3c91 (patch) | |
| tree | fe166f8576d2948faf39c59bc4c346ea71d8b5e9 | |
| parent | 9006d9b31838846cde6275a4ce1aa87b21b2fa17 (diff) | |
| download | vericert-ded5a15a0ebcda4d11af32b3c4a46048b11e3c91.tar.gz vericert-ded5a15a0ebcda4d11af32b3c4a46048b11e3c91.zip | |
Remove useless comments
| -rw-r--r-- | src/hls/IfConversionproof.v | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v index 0b01e83..39ec046 100644 --- a/src/hls/IfConversionproof.v +++ b/src/hls/IfConversionproof.v @@ -53,9 +53,6 @@ Variant match_stackframe : stackframe -> stackframe -> Prop := (TF: transf_function f = tf), match_stackframe (Stackframe res f sp pc rs p) (Stackframe res tf sp pc rs p). -(* c ! pc = fc ! pc *) -(* \/ (c ! pc = a ++ fc ! pc' ++ b /\ fc ! pc = a ++ if p goto pc' ++ b) *) - Definition bool_order (b: bool): nat := if b then 1 else 0. Inductive if_conv_block_spec (c: code): SeqBB.t -> SeqBB.t -> Prop := @@ -300,12 +297,6 @@ Section CORRECTNESS. f.(fn_code) ! pc = Some block2 -> SeqBB.step tge sp in_s' block2 out_s. - (* (EXT: sem_extrap tf pc0 sp (Iexec (mki rs p m)) (Iexec (mki rs0 p0 m0)) b) - (STAR: star step ge (State stk f sp pc0 rs0 p0 m0) E0 (State stk f sp pc rs p m)) - (IS_B: exists b, f.(fn_code)!pc0 = Some b) - (SPEC: forall b_o, f.(fn_code) ! pc = Some b_o -> if_conv_block_spec f.(fn_code) b_o b), - *) - Variant match_states : option SeqBB.t -> state -> state -> Prop := | match_state_some : forall stk stk' f tf sp pc rs p m b pc0 rs0 p0 m0 |