Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
RefinedC
Commits
62831eb4
Commit
62831eb4
authored
Jan 18, 2022
by
Paul
Browse files
clean admits in other examples
parent
c6e6e73d
Pipeline
#60285
passed with stage
in 15 minutes and 40 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
linux/casestudies/mt7601u/proofs/mac/mac_lemmas.v
View file @
62831eb4
...
...
@@ -83,7 +83,7 @@ Global Program Instance rc_flags_BitfieldDesc : BitfieldDesc rc_flags := {|
sig_atom
(
range_of
10
1
)
$
sig_end
|}.
Next
Obligation
.
Admitt
ed
.
Next
Obligation
.
destruct
1
;
solve_sig_wf
.
Q
ed
.
(* Lemma rc_flags_repr_tpd r : *)
(* check_has_ty (rc_flags_repr r) (bv bitfield_sig). *)
...
...
@@ -222,7 +222,7 @@ Global Program Instance rate_BitfieldDesc : BitfieldDesc rate := {|
sig_atom
(
range_of
14
2
)
$
sig_end
|}.
Next
Obligation
.
Admitt
ed
.
Next
Obligation
.
destruct
1
;
solve_sig_wf
.
Q
ed
.
(* Lemma rate_repr_typed r : *)
(* check_has_ty (rate_repr r) (bv bitfield_sig). *)
...
...
@@ -409,7 +409,7 @@ Global Program Instance info_flags_BitfieldDesc : BitfieldDesc info_flags := {|
sig_atom
(
range_of
31
1
)
$
sig_end
|}.
Next
Obligation
.
Admitt
ed
.
Next
Obligation
.
destruct
1
;
solve_sig_wf
.
Q
ed
.
(* Lemma info_flags_repr_tpd r : *)
(* check_has_ty (info_flags_repr r) (bv bitfield_sig). *)
...
...
@@ -618,7 +618,7 @@ Global Program Instance enc_flags_BitfieldDesc : BitfieldDesc enc_flags := {|
sig_atom
(
range_of
7
1
)
$
sig_end
|}.
Next
Obligation
.
Admitt
ed
.
Next
Obligation
.
destruct
1
;
solve_sig_wf
.
Q
ed
.
(* Lemma enc_flags_repr_tpd r : *)
(* check_has_ty (enc_flags_repr r) (bv bitfield_sig). *)
...
...
@@ -702,7 +702,7 @@ Global Program Instance hw_value_BitfieldDesc : BitfieldDesc hw_value := {|
sig_atom
(
range_of
8
2
)
$
sig_end
|}.
Next
Obligation
.
Admitt
ed
.
Next
Obligation
.
destruct
1
;
solve_sig_wf
.
Q
ed
.
(* Lemma hw_value_repr_tpd r : *)
(* check_has_ty (hw_value_repr r) (bv bitfield_sig). *)
...
...
linux/casestudies/proofs/tcp_input/tcp_input_lemmas.v
View file @
62831eb4
...
...
@@ -39,7 +39,7 @@ Global Program Instance tcp_ecn_flags_BitFieldDesc : BitfieldDesc tcp_ecn_flags
sig_atom
(
range_of
3
1
)
$
sig_end
|}.
Next
Obligation
.
Admitt
ed
.
Next
Obligation
.
destruct
1
;
solve_sig_wf
.
Q
ed
.
Global
Instance
simpl_exist_tcp_ecn_flags
P
:
SimplExist
tcp_ecn_flags
P
(
∃
ok
queue_cwr
demand_cwr
seen
,
...
...
@@ -102,7 +102,7 @@ Global Program Instance inet_csk_ack_state_BitFieldDesc : BitfieldDesc inet_csk_
sig_atom
(
range_of
4
1
)
$
sig_end
|}.
Next
Obligation
.
Admitt
ed
.
Next
Obligation
.
destruct
1
;
solve_sig_wf
.
Q
ed
.
Global
Instance
simpl_exist_inet_csk_ack_state
P
:
SimplExist
inet_csk_ack_state
P
(
∃
sched
timer
pushed
pushed_2
now
,
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment