Coq からの低レベル C コード生成
Low level C code generation by Coq

Tanaka Akira @tanaka_akr
National Institute of Advanced Industrial Science and Technology (AIST)TPP 2017
2017-12-06
Supplement material: https://github.com/akr/coq-html-escapeGoal• Verification in Coq• Low-level Fast C code
• Embed to other applications/languages

2

Materials• Coq•C• HTML escape• Intel SSE (SIMD instructions)• Ruby (application)
Do you know all of them?
3Coq Proof-assistant• Proof assistant– User writes a proof– Coq checks the proof• Coq has ML-like language, Gallina– Powerful type system– Gallina programs can be proved in Coq• Program Extraction to OCaml, Haskell and Scheme• C code generation by our plugin
https://github.com/akr/codegen4

We don't Use Coq Extraction• Extraction uses Obj.magic for dependent types
Obj.magic requires uniform representation
But non-uniform representation is important
for low-level programming such as
128 bit SSE register (__m128i type)• Stack consuming tail-recursion
customized inductive type & ocamlopt & toomuch arguments more than number ofregisters [coq-bugs 4312]• Modified extraction is difficult to distribute5

Development Flow
1. In Coqi. Define a specification and implementation
ii.Verify themiii.Convert the implementation into C

2.In Ci. Define supplemental code
ii.Define glue code for Ruby

3.In Ruby
i. Use the verified implementation
6

Translation Structure
Proof of the program
Hand-written
sourceprogram(Gallina)

Option monad &monadic actions(Gallina)

Hand-written"correctness"
proof (Gallina)
monadification plugin

Hand-written"absence of failures"
proof (Gallina)

Proof checkby Coq

Monadification

Monadifiedprogram(Gallina)

Proof checkby Coqcodegen plugin
Monomorphization
Equality provable
by "reflexivity"
tacticC code generation

Generatedprogram(C)

WorkingC program7

Benefits of This Scheme• Correctness by verification
C (without verification) is dangerous• Fast as hand-written C code8Simple Example: pow
Specification of power function in Gallina:(* pow a k = a ** k *)Fixpoint pow a k :=match k with| 0 => 1| k'.+1 => a * pow a k'
end.
Good: Obviously correct
Bad: Naive algorithm
Bad: (non-tail) recursion
9Complex but Fast pow
Definition uphalf' n := n – n./2.
(* fastpow_iter a k x = (a ** k) * x *)Fixpoint fastpow_iter a k x :=if k is k'.+1 thenif odd k thenfastpow_iter a k' (a * x)else
fastpow_iter (a * a) (uphalf' k') x
elsex.
Definition fastpow a k := fastpow_iter a k 1.
10

Complex and Fast pow (2)Bad: Not obviously correct
Good: Fast algorithm
Good: Tail recursion

11

Correctness for fastpow• We can prove equality of fastpow and pow in CoqLemma fastpow_pow a k : fastpow a k = pow a k.
Proof. (*snip*) Qed.
• This is the evidence that fastpow is correct• The proof is snipped because Coq proof isunreadable(interactive environment is required to read proof)

12

Code Generation from fastpow
nat n3_fastpow_iter(nat v2_a, nat v1_k, nat v0_x) {n3_fastpow_iter:;switch (sw_nat(v1_k)) {case_O_nat: { return v0_x; }case_S_nat: {nat v4_k_ = field0_S_nat(v1_k);bool v5_b = n1_odd(v1_k);
switch (sw_bool(v5_b)) {case_true_bool: {nat v6_n = n2_muln(v2_a, v0_x);v1_k = v4_k_; v0_x = v6_n; goto n3_fastpow_iter; }case_false_bool: {nat v7_n = n2_muln(v2_a, v2_a);nat v8_n = n1_uphalf_(v4_k_);v2_a = v7_n; v1_k = v8_n; goto n3_fastpow_iter; }}}}}
nat n2_fastpow(nat v10_a, nat v9_k) {nat v11_n = n0_O();
nat v12_n = n1_S(v11_n);
return n3_fastpow_iter(v10_a, v9_k, v12_n); }13Flowchart of fastpow_iter
fastpow_iter a k x

Yk=0NN

odd kY

k=k/2
a=a*a

k=k–1
x=a*x
return x

14

Primitives for fastpow• Types– bool: Boolean– nat: Peano's natural number• Functions– odd: nat → bool
– muln: nat → nat → nat

They are fully customizable in C level
15

bool
• Coq definition
Inductive bool : Set :=| true : bool
| false : bool.
• C Implementation (provided by user)/* bool type of C99 */#include <stdbool.h>/* constructors */#define n0_true() true
#define n0_false() false/* macros for "match" */#define sw_bool(b) (b)#define case_true_bool default#define case_false_bool case false

16nat (Peano's natural number)• Coq definition
Inductive nat : Set :=| O : nat(* zero *)| S : nat → nat. (* successor function *)• C Implementation
typedef uint64_t nat;#define n0_O() ((nat)0)#define n1_S(n) ((n)+1)#define sw_nat(n) (n)#define case_O_nat case 0#define case_S_nat default#define field0_S_nat(n) ((n)-1)/* primitive functions */#define n2_addn(a,b) ((a)+(b))#define n2_subn(a,b) ((a)-(b))#define n2_muln(a,b) ((a)*(b))#define n2_divn(a,b) ((a)/(b))#define n2_modn(a,b) ((a)%(b))#define n1_odd(n) ((n)&1)
17

Overflow on nat to uint64_t• uint64_t is not enough to represent nat• We implemented monadification plugin tothis conversion is safe (for a specifiedcondition)
https://github.com/akr/monadification18

Proof for no-overflow usingMonadification• Use option monad to represent failures• Translate primitives (S and muln) to return
None for overflow• Monadify fastpow (and dependents).
• Prove log2 (a ^ k) < 64 →fastpowM a k = Some (fastpow a k)
• See sample/pow.v of monadification plugin
for details
19Verified Program Development• Describe a program in Gallina• Describe a proposition (Gallina type)• Describe a proof (Gallina program)• Coq checks the proof (type check)• Generate C code from the Gallina
program• Define supplemental C code20Specification and Correctness• spec(x) = obviously-correct-function• imp(x) = complex-function• proposition of correctness:∀x. imp(x) = spec(x)(Other form of specification is possible...)21

Code Generation to C
• C code generation by our plugin
https://github.com/akr/codegen• Monomorphization to remove ML-stylepolymorphism• Simple mapping from Gallina subset to C
• Tail recursion is translated to goto
• Fully customizable implementation of data
types
22

What is Verified?
Verified:• The algorithm of fastpow• No program failures (such as integer overflow)
Not Verified• Translation mechanism to C
• Monadification mechanism• Implementation of primitives:bool, nat, muln, odd
23HTML EscapeHTML escape substitutes five characters in a string:& → &amp;< → &lt;> → &gt;" → &quot;' → &#39;
We ignore non-ASCII characters for simplicity.
24HTML Escape Specification
Definition html_escape_alist :=map (fun p => (p.1, seq_of_str p.2)) [::("&"%char, "amp"); ("<"%char, "lt"); (">"%char, "gt");(""""%char, "quot"); ("'"%char, "#39") ].
Definition html_escape_byte c :=if assoc c html_escape_alist is Some p then"&" ++ p.2 ++ ";"else[:: c].
Definition html_escape s := flatten (map html_escape_byte s).

This seems correct but doesn't work optimalin C: list (seq) and higher order function
25Expected Flowchart of
Naive HTML Escape in CY
input is empty
Ntake one byte and escape itappend escaped string to buffer

return buffer26

Primitive Types for HTML EscapeRequired types for "scan a memory region andstore the escaped result into a buffer"CoqCbool→ boolnat→ uint64_t
ascii→ unsigned charbyteptr → char*buffer → Ruby's VALUE (String)27

ascii type (unsigned char)• Coq definition(* ascii is 8 booleans *)Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).

• C Implementation
typedef unsigned char ascii;

28

byteptr type (char*)• Required operations to scan a memory region:
advance a pointer, dereference a pointer• Coq definition"char*" is represented using a list of ascii and an index
in it
Inductive byteptr := bptr : nat → seq ascii → byteptr.
bptradd (bptr i s) n = bptr (i + n) s
bptrget (bptr i s) = nth "000"%char s i• C Implementation
typedef const char *byteptr;#define n2_bptradd(p, n) (p + n)
#define n1_bptrget(p) (*(unsigned char *)p)29

buffer type (Ruby's VALUE)• Required operation for result buffer:append data at end of buffer• Coq definition
Inductive buffer := bufctr of seq ascii.
Definition bufaddmem buf ptr n := ...
• C Implementation– buffer: VALUE (String)– bufaddmem: rb_str_buf_cat• bufaddmem is pure but rb_str_buf_cat is destructive.
This problem is solved by copying the string whennecessary30

Tail Recursive HTML EscapeTranslatable to C

Fixpoint trec_html_escape buf ptr n :=match n with
| 0 => buf| n'.+1 =>let: (escptr, escn) :=html_escape_byte_table (bptrget ptr) in
trec_html_escape(bufaddmem buf escptr escn)(bptradd ptr 1)
n'end.

31

Correctness of Tail Recursive
HTML Escape• Definition trec_html_escape_stub s :=s_of_buf (trec_html_escape(bufctr [::]) (bptr 0 s) (size s)).
• Lemma trec_html_escape_correct s :trec_html_escape_stub s = html_escape s.
Proof. (*snip*) Qed.

32

Translated trec_html_escape in C
buffer n3_trec_html_escape(buffer v2_buf, byteptr v1_ptr, nat v0_n) {n3_trec_html_escape:;
switch (sw_nat(v0_n)) {branch bycase_O_nat: { return v2_buf; }switch statement
case_S_nat: {nat v4_n_ = field0_S_nat(v0_n);
ascii v5_a = n1_bptrget(v1_ptr);
prod_byteptr_nat v6_p = n1_html_escape_byte_table(v5_a);
byteptr v7_escptr = field0_pair_prod_byteptr_nat(v6_p);
nat v8_escn = field1_pair_prod_byteptr_nat(v6_p);
buffer v9_b = n3_bufaddmem(v2_buf, v7_escptr, v8_escn);
nat v10_n = n0_O();
nat v11_n = n1_S(v10_n);
byteptr v12_b = n2_bptradd(v1_ptr, v11_n);v2_buf = v9_b;
v1_ptr = v12_b;v0_n = v4_n_;
Jump bygoto n3_trec_html_escape; } } }goto statement33

Flowchart of trec_html_escape
trec_html_escape buf ptr nYn=0
N
escptr, escn =html_escape_byte_table(*ptr)

bufaddmem(buf, escptr, escn)
ptr++
n = n-1
return buf
34

Primitive Type for SSE• m128 → __m128i• __m128i is defined by intrinsics forIntel SSE35

m128 type• m128 consists 16 bytes. (SSE register is 128 bits)• Coq definition
Inductive m128 := c128 :ascii → ascii → ascii → ascii → ascii → ascii → ascii → ascii →ascii → ascii → ascii → ascii → ascii → ascii → ascii → ascii →m128.
Definition m128_of_seq s := c128
(nth "000"%char s 0) ...(snip)... (nth "000"%char s 15).
Definition m128_of_bptr ptr :=m128_of_seq (drop (i_of_bptr ptr) (s_of_bptr ptr)).
• C Implementation
typedef __m128i m128;#define n1_m128_of_bptr(p) _mm_loadu_si128((__m128i const*)(p))• __mm_loadu_si128 generates movdqu(move unaligned double quadword)
36SSE4.2 pcmpestri instruction• pcmpestri:
Packed Compare Explicit Length Strings, Return Index• Coq definition
Definition cmpestri_ubyte_eqany_ppol_lsig(a : m128) (la : nat) (b : m128) (lb : nat) :=let sa := take la (seq_of_m128 a) in
let sb := take lb (seq_of_m128 b) in
let p := mem sa in
if has p sb then find p sb else 16.
• C Implementation#define n4_cmpestri_ubyte_eqany_ppol_lsig(a, la, b, lb) \_mm_cmpestri(a, la, b, lb, \_SIDD_UBYTE_OPS|_SIDD_CMP_EQUAL_ANY| \_SIDD_POSITIVE_POLARITY|_SIDD_LEAST_SIGNIFICANT)• _mm_cmpestri is SSE intrinsic function which generates pcmpestri.
37

HTML Escape using SSE
Fixpoint sse_html_escape buf ptr m n :=match n with
| 0 => bufaddmem buf ptr m| n'.+1 =>let p1 := bptradd ptr m inif n <= 15 then
trec_html_escape (bufaddmem buf ptr m) p1 nelse
let i := cmpestri_ubyte_eqany_ppol_lsig
chars_to_escape num_chars_to_escape(m128_of_bptr p1) 16 in
if 16 <= i thensse_html_escape buf ptr (m + 16) (n' - 15)
else
let buf2 := bufaddmem buf ptr (m + i) in
let p2 := bptradd ptr (m + i) in
let c := bptrget p2 inlet p3 := bptradd p2 1 in
let: (escptr, escn) := html_escape_byte_table c inlet buf3 := bufaddmem buf2 escptr escn in
sse_html_escape buf3 p3 0 (n' - i)
end.

38

Flowchart of sse_html_escape
sse_html_escape buf p m nn=0Y

return (bufaddmem buf ptr m)

p1 = p + m
n<=15Ybuf = bufaddmem buf ptr mreturn trec_html_escape buf p1 ni = cmpestri chars_esc numch_esc (m128_of_bptr p1) 16
m = m+16n = n-16

Y 16<=ibuf = bufaddmem(buf, ptr, m+i)p2 = p1 + i
escptr, escn = html_escape_byte_table(*p2)
buf = bufaddmem(buf, escptr, escn)
p = p2 + 1
n = n-1-i
39

Correctness of HTML Escapeusing SSE• Definition sse_html_escape_stub s :=s_of_buf (sse_html_escape(bufctr [::]) (bptr 0 s) 0 (size s)).
• Lemma sse_html_escape_correct s :sse_html_escape_stub s = html_escape s.
Proof. (*snip*) Qed.
• This verification doesn't need real CPU
which support SSE4.2
40

Glue Code for Ruby Extension
VALUE
sse_html_escape(VALUE self, VALUE str){
buffer buf;
StringValue(str);
RB_GC_GUARD(str);
buf = buffer_new(RSTRING_LEN(str));n4_sse_html_escape(buf, RSTRING_PTR(str), 0, RSTRING_LEN(str));return buf.str;}
voidInit_verified_html_escape(){
rb_define_global_function("sse_html_escape", sse_html_escape, 1);}

41

Test
% ruby -I. -rverified_html_escape \-e 'p sse_html_escape("x < y")'"x &lt; y"42

Benchmark
SSE escape is slowest for
Tail recursive (non-SSE) escape is slow
too many escaping characters(rb_str_buf_cat is called for each byte)

CGI.escapeHTML isfast enough

SSE escape is fastest for
few escaping characters43Some Thoughts• pcmpestrm instruction may be faster thanpcmpestri.
I tried but it is difficult
Tips: BENCHMARK before PROOF• Linear type would be useful to remove
dynamic check of linear use of buffer

44Summary• Correct and fast C function can begenerated from Coq• The function is usable from realapplication (Ruby)

45