104 lines
2.7 KiB
Coq
104 lines
2.7 KiB
Coq
(*
|
|
https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.Strings.Byte.html
|
|
https://coq.inria.fr/doc/V8.19.0/refman/user-extensions/syntax-extensions.html#string-notations
|
|
https://github.com/bedrocksystems/BRiCk/blob/a4ac08a9feede5629ceb7f2f72ca1ead926cb7df/theories/prelude/bytestring_core.v#L154
|
|
*)
|
|
|
|
Require Import List.
|
|
Import ListNotations.
|
|
Require Import Strings.Byte.
|
|
|
|
Inductive blist: Type :=
|
|
| BNil
|
|
| BCons: bool -> blist -> blist.
|
|
|
|
Fixpoint to_list (bl: blist): list bool :=
|
|
match bl with
|
|
| BNil => nil
|
|
| BCons b bs => b :: to_list bs
|
|
end.
|
|
|
|
Fixpoint of_list (l: list bool): blist :=
|
|
match l with
|
|
| nil => BNil
|
|
| cons b bs => BCons b (of_list bs)
|
|
end.
|
|
|
|
Definition length (bl: blist): nat := List.length (to_list bl).
|
|
|
|
Fixpoint blist_parse (b: list Byte.byte): blist :=
|
|
match b with
|
|
| nil => BNil
|
|
| cons b bs =>
|
|
match b with
|
|
| x30 => BCons false (blist_parse bs)
|
|
| x31 => BCons true (blist_parse bs)
|
|
| x20 => blist_parse bs
|
|
| _ => blist_parse bs
|
|
end
|
|
end.
|
|
(* ctr is a counter to leave a space after each 4-tuple *)
|
|
Fixpoint blist_print_aux (bl: blist) (ctr: nat): list Byte.byte :=
|
|
match bl with
|
|
| BNil => []
|
|
| BCons b bs =>
|
|
let nxt := match b with
|
|
| false => x30
|
|
| true => x31
|
|
end in
|
|
nxt ::
|
|
match Nat.eqb ctr 3 with
|
|
| true => x20 :: (blist_print_aux bs 0)
|
|
| false => (blist_print_aux bs (S ctr))
|
|
end
|
|
end.
|
|
Fixpoint blist_print (bl: blist): list Byte.byte :=
|
|
let rem := 4 - (Nat.modulo (length bl) 4) in
|
|
let prefix := List.repeat false rem in
|
|
let lst := to_list bl in
|
|
let newbl := of_list (prefix ++ lst) in
|
|
blist_print_aux newbl 0.
|
|
Declare Scope bl_scope.
|
|
Delimit Scope bl_scope with bl.
|
|
String Notation blist blist_parse blist_print: bl_scope.
|
|
|
|
Compute "0"%bl.
|
|
Compute "00"%bl.
|
|
Compute "000"%bl.
|
|
Compute "0000"%bl.
|
|
Compute "00000"%bl.
|
|
Compute "11101101001001001"%bl.
|
|
Compute "11 101 1010 01001001"%bl.
|
|
(* "0001 1101 1010 0100 1001 "%bl : blist *)
|
|
|
|
(* Before adding 4-tuple padding and space *)
|
|
(* Compute "000"%bl. *)
|
|
(* (1* "000"%bl : blist *1) *)
|
|
(* Compute to_list "010203"%bl. *)
|
|
(* (1* [false; true; false; false] : list bool *1) *)
|
|
(* Compute to_list "011101"%bl. *)
|
|
(* (1* [false; true; true; true; false; true] : list bool *1) *)
|
|
|
|
(**********************************)
|
|
|
|
Declare Scope bv_scope.
|
|
Delimit Scope bv_scope with bv.
|
|
|
|
Definition byte_parse (b: Byte.byte): bool :=
|
|
match b with
|
|
| x31 => true
|
|
| _ => false
|
|
end.
|
|
Definition byte_print (b: bool): Byte.byte :=
|
|
match b with
|
|
| false => x30
|
|
| true => x31
|
|
end.
|
|
String Notation bool byte_parse byte_print: bv_scope.
|
|
|
|
Compute [false; true].
|
|
(* ["0"%bv; "1"%bv] : list bool *)
|
|
Compute ["0"; "1"]%bv.
|
|
(* ["0"%bv; "1"%bv] : list bool *)
|
|
|