-
Notifications
You must be signed in to change notification settings - Fork 6
/
Copy pathprint.html
1086 lines (1019 loc) · 63.2 KB
/
print.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!DOCTYPE HTML>
<html lang="en" class="light" dir="ltr">
<head>
<!-- Book generated using mdBook -->
<meta charset="UTF-8">
<title>hax</title>
<meta name="robots" content="noindex">
<!-- Custom HTML head -->
<meta name="description" content="">
<meta name="viewport" content="width=device-width, initial-scale=1">
<meta name="theme-color" content="#ffffff">
<link rel="icon" href="favicon.svg">
<link rel="shortcut icon" href="favicon.png">
<link rel="stylesheet" href="css/variables.css">
<link rel="stylesheet" href="css/general.css">
<link rel="stylesheet" href="css/chrome.css">
<link rel="stylesheet" href="css/print.css" media="print">
<!-- Fonts -->
<link rel="stylesheet" href="FontAwesome/css/font-awesome.css">
<link rel="stylesheet" href="fonts/fonts.css">
<!-- Highlight.js Stylesheets -->
<link rel="stylesheet" href="highlight.css">
<link rel="stylesheet" href="tomorrow-night.css">
<link rel="stylesheet" href="ayu-highlight.css">
<!-- Custom theme stylesheets -->
<link rel="stylesheet" href="static/custom.css">
<!-- MathJax -->
<script async src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
</head>
<body class="sidebar-visible no-js">
<div id="body-container">
<!-- Provide site root to javascript -->
<script>
var path_to_root = "";
var default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? "navy" : "light";
</script>
<!-- Work around some values being stored in localStorage wrapped in quotes -->
<script>
try {
var theme = localStorage.getItem('mdbook-theme');
var sidebar = localStorage.getItem('mdbook-sidebar');
if (theme.startsWith('"') && theme.endsWith('"')) {
localStorage.setItem('mdbook-theme', theme.slice(1, theme.length - 1));
}
if (sidebar.startsWith('"') && sidebar.endsWith('"')) {
localStorage.setItem('mdbook-sidebar', sidebar.slice(1, sidebar.length - 1));
}
} catch (e) { }
</script>
<!-- Set the theme before any content is loaded, prevents flash -->
<script>
var theme;
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
if (theme === null || theme === undefined) { theme = default_theme; }
var html = document.querySelector('html');
html.classList.remove('light')
html.classList.add(theme);
var body = document.querySelector('body');
body.classList.remove('no-js')
body.classList.add('js');
</script>
<input type="checkbox" id="sidebar-toggle-anchor" class="hidden">
<!-- Hide / unhide sidebar before it is displayed -->
<script>
var body = document.querySelector('body');
var sidebar = null;
var sidebar_toggle = document.getElementById("sidebar-toggle-anchor");
if (document.body.clientWidth >= 1080) {
try { sidebar = localStorage.getItem('mdbook-sidebar'); } catch(e) { }
sidebar = sidebar || 'visible';
} else {
sidebar = 'hidden';
}
sidebar_toggle.checked = sidebar === 'visible';
body.classList.remove('sidebar-visible');
body.classList.add("sidebar-" + sidebar);
</script>
<nav id="sidebar" class="sidebar" aria-label="Table of contents">
<div class="sidebar-scrollbox">
<ol class="chapter"><li class="chapter-item expanded "><a href="index.html"><strong aria-hidden="true">1.</strong> Introduction</a></li><li class="chapter-item expanded "><a href="quick_start/intro.html"><strong aria-hidden="true">2.</strong> Quick start</a></li><li class="chapter-item expanded "><a href="tutorial/index.html"><strong aria-hidden="true">3.</strong> Tutorial</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="tutorial/panic-freedom.html"><strong aria-hidden="true">3.1.</strong> Panic freedom</a></li><li class="chapter-item expanded "><a href="tutorial/properties.html"><strong aria-hidden="true">3.2.</strong> Properties on functions</a></li><li class="chapter-item expanded "><a href="tutorial/data-invariants.html"><strong aria-hidden="true">3.3.</strong> Data invariants</a></li></ol></li><li class="chapter-item expanded "><a href="examples/intro.html"><strong aria-hidden="true">4.</strong> Examples</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="examples/rust-by-examples/intro.html"><strong aria-hidden="true">4.1.</strong> Rust By Example</a></li><li class="chapter-item expanded "><a href="examples/fstar/intro.html"><strong aria-hidden="true">4.2.</strong> Using the F* backend</a></li><li class="chapter-item expanded "><a href="examples/coq/intro.html"><strong aria-hidden="true">4.3.</strong> Using the Coq backend</a></li><li class="chapter-item expanded "><a href="examples/coq/intro.html"><strong aria-hidden="true">4.4.</strong> Using the ProVerif backend</a></li></ol></li><li class="chapter-item expanded "><a href="faq/intro.html"><strong aria-hidden="true">5.</strong> Troubleshooting/FAQ</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="faq/include-flags.html"><strong aria-hidden="true">5.1.</strong> The include flag: which items should be extracted, and how?</a></li></ol></li><li class="chapter-item expanded "><a href="contributing/intro.html"><strong aria-hidden="true">6.</strong> Contributing</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="contributing/architecture.html"><strong aria-hidden="true">6.1.</strong> Architecture</a></li><li class="chapter-item expanded "><a href="contributing/libraries_macros.html"><strong aria-hidden="true">6.2.</strong> Libraries & Macros</a></li><li class="chapter-item expanded "><a href="contributing/ast_ebnf.html"><strong aria-hidden="true">6.3.</strong> AST/EBNF</a></li><li class="spacer"></li></ol></li><li class="chapter-item expanded "><a href="misc/archive.html">Archive</a></li></ol>
</div>
<div id="sidebar-resize-handle" class="sidebar-resize-handle">
<div class="sidebar-resize-indicator"></div>
</div>
</nav>
<!-- Track and set sidebar scroll position -->
<script>
var sidebarScrollbox = document.querySelector('#sidebar .sidebar-scrollbox');
sidebarScrollbox.addEventListener('click', function(e) {
if (e.target.tagName === 'A') {
sessionStorage.setItem('sidebar-scroll', sidebarScrollbox.scrollTop);
}
}, { passive: true });
var sidebarScrollTop = sessionStorage.getItem('sidebar-scroll');
sessionStorage.removeItem('sidebar-scroll');
if (sidebarScrollTop) {
// preserve sidebar scroll position when navigating via links within sidebar
sidebarScrollbox.scrollTop = sidebarScrollTop;
} else {
// scroll sidebar to current active section when navigating via "next/previous chapter" buttons
var activeSection = document.querySelector('#sidebar .active');
if (activeSection) {
activeSection.scrollIntoView({ block: 'center' });
}
}
</script>
<div id="page-wrapper" class="page-wrapper">
<div class="page">
<div id="menu-bar-hover-placeholder"></div>
<div id="menu-bar" class="menu-bar sticky">
<div class="left-buttons">
<label id="sidebar-toggle" class="icon-button" for="sidebar-toggle-anchor" title="Toggle Table of Contents" aria-label="Toggle Table of Contents" aria-controls="sidebar">
<i class="fa fa-bars"></i>
</label>
<button id="theme-toggle" class="icon-button" type="button" title="Change theme" aria-label="Change theme" aria-haspopup="true" aria-expanded="false" aria-controls="theme-list">
<i class="fa fa-paint-brush"></i>
</button>
<ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
<li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
<li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
<li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
<li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
<li role="none"><button role="menuitem" class="theme" id="ayu">Ayu</button></li>
</ul>
<button id="search-toggle" class="icon-button" type="button" title="Search. (Shortkey: s)" aria-label="Toggle Searchbar" aria-expanded="false" aria-keyshortcuts="S" aria-controls="searchbar">
<i class="fa fa-search"></i>
</button>
</div>
<h1 class="menu-title">hax</h1>
<div class="right-buttons">
<a href="print.html" title="Print this book" aria-label="Print this book">
<i id="print-button" class="fa fa-print"></i>
</a>
</div>
</div>
<div id="search-wrapper" class="hidden">
<form id="searchbar-outer" class="searchbar-outer">
<input type="search" id="searchbar" name="searchbar" placeholder="Search this book ..." aria-controls="searchresults-outer" aria-describedby="searchresults-header">
</form>
<div id="searchresults-outer" class="searchresults-outer hidden">
<div id="searchresults-header" class="searchresults-header"></div>
<ul id="searchresults">
</ul>
</div>
</div>
<!-- Apply ARIA attributes after the sidebar and the sidebar toggle button are added to the DOM -->
<script>
document.getElementById('sidebar-toggle').setAttribute('aria-expanded', sidebar === 'visible');
document.getElementById('sidebar').setAttribute('aria-hidden', sidebar !== 'visible');
Array.from(document.querySelectorAll('#sidebar a')).forEach(function(link) {
link.setAttribute('tabIndex', sidebar === 'visible' ? 0 : -1);
});
</script>
<div id="content" class="content">
<main>
<h1 id="introduction"><a class="header" href="#introduction">Introduction</a></h1>
<p>hax is a tool for high assurance translations that translates a large subset of
Rust into formal languages such as <a href="https://www.fstar-lang.org/">F*</a> or <a href="https://coq.inria.fr/">Coq</a>.
This extends the scope of the hacspec project, which was previously a DSL embedded in Rust,
to a usable tool for verifying Rust programs.</p>
<blockquote>
<p>So what is <strong>hacspec</strong> now?</p>
</blockquote>
<p>hacspec is the functional subset of Rust that can be used, together with a hacspec
standard library, to write succinct, executable, and verifiable specifications in
Rust.
These specifications can be translated into formal languages with hax.</p>
<div style="break-before: page; page-break-before: always;"></div><h1 id="quick-start-with-hax-and-f"><a class="header" href="#quick-start-with-hax-and-f">Quick start with hax and F*</a></h1>
<p>Do you want to try hax out on a Rust crate of yours? This chapter is
what you are looking for!</p>
<h2 id="setup-the-tools"><a class="header" href="#setup-the-tools">Setup the tools</a></h2>
<ul>
<li><input type="checkbox" class="user-checkable"/> <a href="https://github.com/hacspec/hax?tab=readme-ov-file#installation">Install the hax toolchain</a>.<br />
<span style="margin-right:30px;"></span>🪄 Running <code>cargo hax --version</code> should print some version info.</li>
<li><input type="checkbox" class="user-checkable"/> <a href="https://github.com/FStarLang/FStar/blob/master/INSTALL.md">Install F*</a> <em>(optional: only if want to run F*)</em></li>
</ul>
<h2 id="setup-the-crate-you-want-to-verify"><a class="header" href="#setup-the-crate-you-want-to-verify">Setup the crate you want to verify</a></h2>
<p><em>Note: the instructions below assume you are in the folder of the specific crate (<strong>not workspace!</strong>) you want to extract.</em></p>
<p><em>Note: this part is useful only if you want to run F*.</em></p>
<ul>
<li><input type="checkbox" class="user-checkable"/> Create the folder <code>proofs/fstar/extraction</code> folder, right next to the <code>Cargo.toml</code> of the crate you want to verify.<br />
<span style="margin-right:30px;"></span>🪄 <code>mkdir -p proofs/fstar/extraction</code></li>
<li><input type="checkbox" class="user-checkable"/> Copy <a href="https://gist.github.com/W95Psp/4c304132a1f85c5af4e4959dd6b356c3">this makefile</a> to <code>proofs/fstar/extraction/Makefile</code>.<br />
<span style="margin-right:30px;"></span>🪄 <code>curl -o proofs/fstar/extraction/Makefile https://gist.githubusercontent.com/W95Psp/4c304132a1f85c5af4e4959dd6b356c3/raw/Makefile</code></li>
<li><input type="checkbox" class="user-checkable"/> Add <code>hax-lib</code> as a dependency to your crate, enabled only when using hax.<br />
<span style="margin-right:30px;"></span>🪄 <code>cargo add --target 'cfg(hax)' --git https://github.com/hacspec/hax hax-lib</code><br />
<span style="margin-right:30px;"></span><span style="opacity: 0;">🪄</span> <em>(<code>hax-lib</code> is not mandatory, but this guide assumes it is present)</em></li>
</ul>
<h2 id="partial-extraction"><a class="header" href="#partial-extraction">Partial extraction</a></h2>
<p><em>Note: the instructions below assume you are in the folder of the
specific crate you want to extract.</em></p>
<p>Run the command <code>cargo hax into fstar</code> to extract every item of your
crate as F* modules in the subfolder <code>proofs/fstar/extraction</code>.</p>
<p><strong>What is critical? What is worth verifying?</strong><br />
Probably, your Rust crate contains mixed kinds of code: some parts are
critical (e.g. the library functions at the core of your crate) while
some others are not (e.g. the binary driver that wraps the
library). In this case, you likely want to extract only partially your
crate, so that you can focus on the important part.</p>
<p><strong>Partial extraction.</strong><br />
If you want to extract a function
<code>your_crate::some_module::my_function</code>, you need to tell <code>hax</code> to
extract nothing but <code>my_function</code>:</p>
<pre><code class="language-bash">cargo hax into -i '-** +your_crate::some_module::my_function' fstar
</code></pre>
<p>Note this command will extract <code>my_function</code> but also any item
(function, type, etc.) from your crate which is used directly or
indirectly by <code>my_function</code>. If you don't want the dependency, use
<code>+!</code> instead of <code>+</code> in the <code>-i</code> flag.</p>
<p><strong>Unsupported Rust code.</strong><br />
hax <a href="https://github.com/hacspec/hax?tab=readme-ov-file#supported-subset-of-the-rust-language">doesn't support every Rust
constructs</a>,
<code>unsafe</code> code, or complicated mutation scheme. That is another reason
for extracting only a part of your crate. When running hax, if an item
of your crate, say a function <code>my_crate::f</code>, is not handled by hax,
you can append <code>-my_crate::f</code> to the <code>-i</code> flag. You can learn more
about the <code>-i</code> flag <a href="quick_start/../faq/include-flags.html">in the FAQ</a>.</p>
<h2 id="start-f-verification"><a class="header" href="#start-f-verification">Start F* verification</a></h2>
<p>After running the hax toolchain on your Rust code, you will end up
with various F* modules in the <code>proofs/fstar/extraction</code> folder. The
<code>Makefile</code> in <code>proofs/fstar/extraction</code> will run F*.</p>
<ol>
<li><strong>Lax check:</strong> the first step is to run <code>OTHERFLAGS="--lax" make</code>,
which will run F* in "lax" mode. The lax mode just makes sure basic
typechecking works: it is not proving anything. This first step is
important because there might be missing libraries. If F* is not
able to find a definition, it is probably a <code>libcore</code> issue: you
probably need to edit the F* library, which lives in the
<code>proofs-libs</code> directory in the root of the hax repo.</li>
<li><strong>Typecheck:</strong> the second step is to run <code>make</code>. This will ask F*
to typecheck fully your crate. This is very likely that you need to
add preconditions and postconditions at this stage. Indeed, this
second step is about panic freedom: if F* can typecheck your crate,
it means your code <em>never</em> panics, which already is an important
property.</li>
</ol>
<p>To go further, please read the next chapter.</p>
<div style="break-before: page; page-break-before: always;"></div><h1 id="tutorial"><a class="header" href="#tutorial">Tutorial</a></h1>
<p>This tutorial is a guide for formally verifying properties about Rust
programs using the hax toolchain. hax is a tool that translates Rust
programs to various formal programming languages.</p>
<p>The formal programming languages we target are called <em>backends</em>. Some
of them, e.g. <a href="https://fstar-lang.org/">F*</a> or
<a href="https://coq.inria.fr/">Coq</a>, are general purpose formal programming
languages. Others are specialized tools:
<a href="https://bblanche.gitlabpages.inria.fr/proverif/">ProVerif</a> is
dedicated to proving properties about protocols.</p>
<p>This tutorial focuses on proving properties with the
<a href="https://fstar-lang.org/">F* programming language</a>.</p>
<div style="break-before: page; page-break-before: always;"></div><h1 id="panic-freedom"><a class="header" href="#panic-freedom">Panic freedom</a></h1>
<p>Let's start with a simple example: a function that squares a <code>u8</code>
integer. To extract this function to F* using hax, we simply need to
run the command <code>cargo hax into fstar</code> in the directory of the crate
in which the function <code>square</code> is defined.</p>
<p><em>Note: throughout this tutorial, you can edit the snippets of code and
extract to F* by clicking the play button ( <i class="fa fa-play"></i> ), or even typecheck it with the button ( <i class="fa fa-check"></i> ).</em></p>
<pre><pre class="playground"><code class="language-rust editable">fn square(x: u8) -> u8 {
x * x
}</code></pre></pre>
<p>Though, if we try to verify this function, F* is complaining about a
subtyping issue: F* tells us that it is not able to prove that the
result of the multiplication <code>x * x</code> fits the range of <code>u8</code>. The
multiplication <code>x * x</code> might indeed be overflowing!</p>
<p>For instance, running <code>square(16)</code> panics: <code>16 * 16</code> is <code>256</code>, which
is just over <code>255</code>, the largest integer that fits <code>u8</code>. Rust does not
ensure that functions are <em>total</em>: a function might panic at any
point, or might never terminate.</p>
<h2 id="rust-and-panicking-code"><a class="header" href="#rust-and-panicking-code">Rust and panicking code</a></h2>
<p>Quoting the chapter <a href="https://doc.rust-lang.org/book/ch09-03-to-panic-or-not-to-panic.html">To <code>panic!</code> or Not to
<code>panic!</code></a>
from the Rust book:</p>
<blockquote>
<p>The <code>panic!</code> macro signals that your program is in a state it can't
handle and lets you tell the process to stop instead of trying to
proceed with invalid or incorrect values.</p>
</blockquote>
<p>A Rust program should panics only in a situation where an assumption
or an invariant is broken: a panics models an <em>invalid</em> state. Formal
verification is about proving such invalid state cannot occur, at all.</p>
<p>From this observation emerges the urge of proving Rust programs to be
panic-free!</p>
<h2 id="fixing-our-squaring-function"><a class="header" href="#fixing-our-squaring-function">Fixing our squaring function</a></h2>
<p>Let's come back to our example. There is an informal assumption to the
multiplication operator in Rust: the inputs should be small enough so
that the addition doesn't overflow.</p>
<p>Note that Rust also provides <code>wrapping_mul</code>, a non-panicking variant
of the multiplication on <code>u8</code> that wraps when the result is bigger
than <code>255</code>. Replacing the common multiplication with <code>wrapping_mul</code> in
<code>square</code> would fix the panic, but then, <code>square(256)</code> returns zero.
Semantically, this is not what one would expect from <code>square</code>.</p>
<p>Our problem is that our function <code>square</code> is well-defined only when
its input is within <code>0</code> and <code>15</code>.</p>
<h3 id="solution-a-reflect-the-partialness-of-the-function-in-rust"><a class="header" href="#solution-a-reflect-the-partialness-of-the-function-in-rust">Solution A: reflect the partialness of the function in Rust</a></h3>
<p>A first solution is to make <code>square</code> return an <code>Option<u8></code> instead of a <code>u8</code>:</p>
<pre><pre class="playground"><code class="language-rust editable">fn square_option(x: u8) -> Option<u8> {
if x >= 16 {
None
} else {
Some(x * x)
}
}</code></pre></pre>
<p>Here, F* is able to prove panic-freedom: calling <code>square</code> with any
input is safe. Though, one may argue that <code>square</code>'s input being small
enough should really be an assumption. Having to deal with the
possible integer overflowing whenever squaring is a huge burden. Can
we do better?</p>
<h3 id="solution-b-add-a-precondition"><a class="header" href="#solution-b-add-a-precondition">Solution B: add a precondition</a></h3>
<p>The type system of Rust doesn't allow the programmer to formalize the
assumption that <code>square</code> expects a small <code>u8</code>. This becomes
possible using hax: one can annotate a function with a pre-condition
on its inputs.</p>
<p>The pre-conditions and post-conditions on a function form a
<em>contract</em>: "if you give me some inputs that satisfies a given formula
(<em>the precondition</em>), I will produce a return value that satisfy
another formula (<em>the postcondition</em>)". Outside this contracts,
anything might happen: the function might panic, might run forever,
erase your disk, or anything.</p>
<p>The helper crate
<a href="https://github.com/hacspec/hax/tree/main/hax-lib">hax-lib</a>
provdes the <code>requires</code>
<a href="https://doc.rust-lang.org/reference/procedural-macros.html">proc-macro</a>
which lets user writting pre-conditions directly in Rust.</p>
<pre><pre class="playground"><code class="language-rust editable">#[hax_lib::requires(x < 16)]
fn square_requires(x: u8) -> u8 {
x * x
}</code></pre></pre>
<p>With this precondition, F* is able to prove panic freedom. From now
on, it is the responsibility of the clients of <code>square</code> to respect the
contact. The next step is thus be to verify, through hax extraction,
that <code>square</code> is used correctly at every call site.</p>
<h2 id="common-panicking-situations"><a class="header" href="#common-panicking-situations">Common panicking situations</a></h2>
<p>Multiplication is not the only panicking function provided by the Rust
library: most of the other integer arithmetic operation have such
informal assumptions.</p>
<p>Another source of panics is indexing. Indexing in an array, a slice or
a vector is a partial operation: the index might be out of range.</p>
<p>In the example folder of hax, you can find the <a href="https://github.com/hacspec/hax/blob/main/examples/chacha20/src/lib.rs"><code>chacha20</code>
example</a>
that makes use of pre-conditions to prove panic freedom.</p>
<p>Another solution for safe indexing is to use the <a href="https://matklad.github.io/2018/06/04/newtype-index-pattern.html">newtype index
pattern</a>,
which is <a href="https://github.com/hacspec/hax/blob/d668de4d17e5ddee3a613068dc30b71353a9db4f/tests/attributes/src/lib.rs#L98-L126">also supported by
hax</a>. The <a href="tutorial/data-invariants.html#newtype-and-refinements">data invariants</a> chapter gives more details about this.</p>
<div style="break-before: page; page-break-before: always;"></div><h1 id="proving-properties"><a class="header" href="#proving-properties">Proving properties</a></h1>
<p>In the last chapter, we proved one property on the <code>square</code> function:
panic freedom. After adding a precondition, the signature of the
<code>square</code> function was <code>x:u8 -> Pure u8 (requires x <. 16uy) (ensures fun _ -> True)</code>.</p>
<p>This contract stipulates that, given a small input, the function will
<em>return a value</em>: it will not panic or diverge. We could enrich the
contract of <code>square</code> with a post-condition about the fact it is a
increasing function:</p>
<pre><pre class="playground"><code class="language-rust editable">#[hax_lib::requires(x < 16)]
#[hax_lib::ensures(|result| result >= x)]
fn square_ensures(x: u8) -> u8 {
x * x
}</code></pre></pre>
<p>Such a simple post-condition is automatically proven by F*. The
properties of our <code>square</code> function are not fascinating. Let's study a
more interesting example: <a href="https://en.wikipedia.org/wiki/Barrett_reduction">Barrett reduction</a>.</p>
<h2 id="a-concrete-example-of-contract-barrett-reduction"><a class="header" href="#a-concrete-example-of-contract-barrett-reduction">A concrete example of contract: Barrett reduction</a></h2>
<p>While the correctness of <code>square</code> is obvious, the Barrett reduction is
not.</p>
<p>Given <code>value</code> a field element (a <code>i32</code> whose absolute value is at most
<code>BARRET_R</code>), the function <code>barrett_reduce</code> defined below computes
<code>result</code> such that:</p>
<ul>
<li><code>result ≡ value (mod FIELD_MODULUS)</code>;</li>
<li>the absolute value of <code>result</code> is bound as follows:
<code>|result| < FIELD_MODULUS</code>.</li>
</ul>
<p>It is easy to write this contract directly as <code>hax::requires</code> and
<code>hax::ensures</code> annotations, as shown in the snippet below.</p>
<pre><pre class="playground"><code class="language-rust editable">type FieldElement = i32;
const FIELD_MODULUS: i32 = 3329;
const BARRETT_SHIFT: i64 = 26;
const BARRETT_R: i64 = 0x4000000; // 2^26
const BARRETT_MULTIPLIER: i64 = 20159; // ⌊(BARRETT_R / FIELD_MODULUS) + 1/2⌋
#[hax_lib::requires((i64::from(value) >= -BARRETT_R && i64::from(value) <= BARRETT_R))]
#[hax_lib::ensures(|result| result > -FIELD_MODULUS && result < FIELD_MODULUS
&& result % FIELD_MODULUS == value % FIELD_MODULUS)]
fn barrett_reduce(value: i32) -> i32 {
let t = i64::from(value) * BARRETT_MULTIPLIER;
let t = t + (BARRETT_R >> 1);
let quotient = t >> BARRETT_SHIFT;
let quotient = quotient as i32;
let sub = quotient * FIELD_MODULUS;
// Here a lemma to prove that `(quotient * 3329) % 3329 = 0`
// may have to be called in F*.
value - sub
}</code></pre></pre>
<!-- Note that we call to `cancel_mul_mod`, a lemma: in Rust, this have no
effect, but in F*, that establishes that `(quotient * 3329) % 3329` is
zero. -->
<p>Before returning, a lemma may have to be called in F* to prove the correctness
of the reduction.
The lemma is <code>Math.Lemmas.cancel_mul_mod (v quotient) 3329;</code>, which establishes
that <code>(quotient * 3329) % 3329</code> is zero.
With the help of that one lemma, F* is able to prove the
reduction computes the expected result.
(We may expose lemmas like this to call from Rust directly in future.)</p>
<p>This Barrett reduction examples is taken from
<a href="https://github.com/cryspen/libcrux/tree/main">libcrux</a>'s proof of
Kyber which is using hax and F*.</p>
<p>This example showcases an <strong>intrinsic proof</strong>: the function
<code>barrett_reduce</code> not only computes a value, but it also ship a proof
that the post-condition holds. The pre-condition and post-condition
gives the function a formal specification, which is useful both for
further formal verification and for documentation purposes.</p>
<h2 id="extrinsic-properties-with-lemmas"><a class="header" href="#extrinsic-properties-with-lemmas">Extrinsic properties with lemmas</a></h2>
<p>Consider the <code>encrypt</code> and <code>decrypt</code> functions below. Those functions
have no precondition, don't have particularly interesting properties
individually. However, the composition of the two yields an useful
property: encrypting a ciphertext and decrypting the result with a
same key produces the ciphertext again. <code>|c| decrypt(c, key)</code> is the
inverse of <code>|p| encrypt(p, key)</code>.</p>
<pre><pre class="playground"><code class="language-rust editable">fn encrypt(plaintext: u32, key: u32) -> u32 {
plaintext ^ key
}
fn decrypt(ciphertext: u32, key: u32) -> u32 {
ciphertext ^ key
}</code></pre></pre>
<p>In this situation, adding a pre- or a post-condition to either
<code>encrypt</code> or <code>decrypt</code> is not useful: we want to state our inverse
property about both of them. Better, we want this property to be
stated directly in Rust: just as with pre and post-conditions, the
Rust souces should clearly state what is to be proven.</p>
<p>To this end, Hax provides a macro <code>lemma</code>. Below, the Rust function
<code>encrypt_decrypt_identity</code> takes a key and a plaintext, and then
states the inverse property. The body is empty: the details of the
proof itself are not relevant, at this stage, we only care about the
statement. The proof will be completed manually in the proof
assistant.</p>
<pre><pre class="playground"><code class="language-rust editable"><span class="boring">fn encrypt(plaintext: u32, key: u32) -> u32 {
</span><span class="boring"> plaintext ^ key
</span><span class="boring">}
</span><span class="boring">
</span><span class="boring">fn decrypt(ciphertext: u32, key: u32) -> u32 {
</span><span class="boring"> ciphertext ^ key
</span><span class="boring">}
</span><span class="boring">
</span>#[hax_lib::lemma]
#[hax_lib::requires(true)]
fn encrypt_decrypt_identity(
key: u32,
plaintext: u32,
) -> Proof<{ decrypt(encrypt(plaintext, key), key) == plaintext }> {
}</code></pre></pre>
<div style="break-before: page; page-break-before: always;"></div><h1 id="data-invariants"><a class="header" href="#data-invariants">Data invariants</a></h1>
<p>In the two previous chapters we saw how to write specifications on
functions, be it with pre and post-condition or with lemmas. In this
chapter, we will see how to maintain invariants with precise types.</p>
<h2 id="making-illegal-states-unpresentable"><a class="header" href="#making-illegal-states-unpresentable">Making illegal states unpresentable</a></h2>
<p>With the Barrett example, we were working on a certain field, whose
elements were represented as <code>i32</code> integers. To simplify, let's
consider <code>F₃</code>, the finite field with 3 elements (say <code>0</code>, <code>1</code> and
<code>2</code>). Every element of <code>F3</code> can be represented as a <code>i32</code> integers,
but the converse doesn't hold: the vast majority of <code>i32</code> integers are
not in of <code>F₃</code>.</p>
<p>Representing <code>F₃</code> as <code>i32</code>s, every time we define a function consuming
<code>F₃</code> elements, we face the risk to consume <em>illegal</em> elements. We are
thus back to <a href="tutorial/panic-freedom.html">chapter 4.1</a>: we should panic on
illegal elements, and add hax pre-conditions on every single
function. That's not ideal: the property of being either <code>0</code>, <code>1</code> or
<code>2</code> should be encoded directly on the type representing <code>F₃</code> elements.</p>
<h3 id="enums-to-then-rescue"><a class="header" href="#enums-to-then-rescue"><code>enum</code>s to then rescue</a></h3>
<p>Rust alone already can solve our representation issues with
<a href="https://doc.rust-lang.org/book/ch06-00-enums.html">enums</a>! Below, we
define the <code>enum</code> type <code>F3</code> which has only three constructor: <code>F3</code>
represent exactly the elements of <code>F₃</code>, not more, not less.</p>
<pre><pre class="playground"><code class="language-rust editable">enum F3 {
E1,
E2,
E3,
}</code></pre></pre>
<p>With <code>F3</code>, there doesn't exist illegal values at all: we can now
define <a href="https://en.wikipedia.org/wiki/Partial_function"><em>total</em>
functions</a> on <code>F₃</code>
elements. We dropped altogether a source of panic!</p>
<p>Soon you want to work with a bigger finite field: say
<code>F₂₃₄₇</code>. Representing this many <code>q</code> different elements with an Rust
enum would be very painful... The <code>enum</code> approach falls apart.</p>
<h3 id="newtype-and-refinements"><a class="header" href="#newtype-and-refinements">Newtype and refinements</a></h3>
<p>Since we don't want an <code>enum</code> with 2347 elements, we have to revert to
a type that can hold this many elements. The smallest integer type
large enough provided by Rust is <code>u16</code>.</p>
<p>Let's define <code>F</code> a
<a href="https://matklad.github.io/2018/06/04/newtype-index-pattern.html">"newtype"</a>:
a <a href="https://doc.rust-lang.org/book/ch05-00-structs.html">struct</a> with
one <code>u16</code> field <code>v</code>. Notice the refinment annotation on <code>v</code>: the
extraction of this type <code>F</code> via hax will result in a type enforcing
<code>v</code> small enough.</p>
<pre><pre class="playground"><code class="language-rust editable">pub const Q: u16 = 2347;
#[hax_lib::attributes]
pub struct F {
#[hax_lib::refine(v < Q)]
pub v: u16,
}</code></pre></pre>
<p>In Rust, we can now define functions that operates on type <code>F</code>,
assuming they are in bounds with respect to <code>F₂₃₄₇</code>: every such
assumption will be checked and enforced by the proof assistant. As an
example, below is the implementation of the addition for type <code>F</code>.</p>
<pre><pre class="playground"><code class="language-rust editable"><span class="boring">pub const Q: u16 = 2347;
</span><span class="boring">
</span><span class="boring">#[hax_lib::attributes]
</span><span class="boring">pub struct F {
</span><span class="boring"> #[hax_lib::refine(v < Q)]
</span><span class="boring"> pub v: u16,
</span><span class="boring">}
</span>
use core::ops::Add;
impl Add for F {
type Output = Self;
fn add(self, rhs: Self) -> Self {
Self {
v: (self.v + rhs.v) % Q,
}
}
}</code></pre></pre>
<p>Here, F* is able to prove automatically that (1) the addition doesn't
overflow and (2) that the invariant of <code>F</code> is preserved. The
definition of type <code>F</code> in F* (named <code>t_F</code>) very explicitly requires
the invariant as a refinement on <code>v</code>.</p>
<div style="break-before: page; page-break-before: always;"></div><h1 id="examples"><a class="header" href="#examples">Examples</a></h1>
<p>This chapter contains various examples that demonstrates how hax can
be used to prove properties about programs. Each example is
self-contained. hax being a tool that can extract Rust to various
backends, this section provides examples for each backend.</p>
<p>The first subsection takes some examples from <a href="https://doc.rust-lang.org/rust-by-example/">Rust by
Example</a>, and shows how to
prove properties on them.</p>
<p>The other sections present backend-specific examples.</p>
<div style="break-before: page; page-break-before: always;"></div><h1 id="rust-by-example"><a class="header" href="#rust-by-example">Rust By Example</a></h1>
<div style="break-before: page; page-break-before: always;"></div><h1 id="using-the-f-backend"><a class="header" href="#using-the-f-backend">Using the F* backend</a></h1>
<div style="break-before: page; page-break-before: always;"></div><h1 id="using-the-proverif-backend"><a class="header" href="#using-the-proverif-backend">Using the ProVerif backend</a></h1>
<div style="break-before: page; page-break-before: always;"></div><h1 id="using-the-proverif-backend-1"><a class="header" href="#using-the-proverif-backend-1">Using the ProVerif backend</a></h1>
<div style="break-before: page; page-break-before: always;"></div><h1 id="troubleshootingfaq"><a class="header" href="#troubleshootingfaq">Troubleshooting/FAQ</a></h1>
<p>This chapter captures a list of common questions or issues and how to resolve them. If you happen to run into an issue that is not documented here, please consider submitting a pull request!</p>
<div style="break-before: page; page-break-before: always;"></div><h1 id="rust-item-extraction-using-cargo-hax"><a class="header" href="#rust-item-extraction-using-cargo-hax"><strong>Rust Item Extraction Using <code>cargo hax</code></strong></a></h1>
<h2 id="overview"><a class="header" href="#overview"><strong>Overview</strong></a></h2>
<p>When extracting Rust items with hax, it is often necessary to include only a specific subset of items from a crate. The <code>cargo hax into</code> subcommand provides the <code>-i</code> flag to control which items are included or excluded, and how their dependencies are handled. This allows precise tailoring of the extraction process.</p>
<h2 id="the--i-flag"><a class="header" href="#the--i-flag"><strong>The <code>-i</code> Flag</strong></a></h2>
<p>The <code>-i</code> flag accepts a list of patterns with modifiers to define inclusion or exclusion rules for Rust items. Patterns are processed sequentially from left to right, determining which items are extracted.</p>
<h3 id="basic-concepts"><a class="header" href="#basic-concepts"><strong>Basic Concepts</strong></a></h3>
<ul>
<li><strong>Patterns</strong>: Rust paths with support for <code>*</code> and <code>**</code> globs.
<ul>
<li><code>*</code> matches any single segment (e.g., <code>mycrate::*::myfn</code>).</li>
<li><code>**</code> matches any subpath, including empty segments (e.g., <code>**::myfn</code>).</li>
</ul>
</li>
<li><strong>Modifiers</strong>:
<ul>
<li><code>+</code>: Includes items and their dependencies (transitively).</li>
<li><code>+~</code>: Includes items and their <strong>direct dependencies only</strong>.</li>
<li><code>+!</code>: Includes only the item itself (no dependencies).</li>
<li><code>+:</code>: Includes only the item's type signature (no body or dependencies).</li>
<li><code>-</code>: Excludes items.</li>
</ul>
</li>
</ul>
<p>By default, <strong>all items are included</strong>, unless explicitly modified.</p>
<h3 id="practical-examples-of-the--i-flag-usage"><a class="header" href="#practical-examples-of-the--i-flag-usage"><strong>Practical Examples of the <code>-i</code> Flag Usage</strong></a></h3>
<p>Consider the following crate (<code>mycrate</code>) with the <code>lib.rs</code> module:</p>
<pre><pre class="playground"><code class="language-rust"><span class="boring">#![allow(unused)]
</span><span class="boring">fn main() {
</span>fn interesting_function() { aux() }
fn aux() { foo::f() }
fn something_else() { /* ... */ }
mod foo {
fn f() { /* ... */ }
fn g() { /* ... */ }
fn h() { /* ... */ }
fn interesting_function() { something() }
fn something() { /* ... */ }
mod bar {
fn interesting_function() { /* ... */ }
}
}
fn not_that_one() { not_that_one_dependency() }
fn not_that_one_dependency() { /* ... */ }
fn not_extracting_function(_: u8) -> u8 {
unsafe { /* ... */ }
0
}
<span class="boring">}</span></code></pre></pre>
<h4 id="1-selectively-including-items-with-dependencies"><a class="header" href="#1-selectively-including-items-with-dependencies"><strong>1. Selectively Including Items with Dependencies</strong></a></h4>
<pre><code class="language-bash">cargo hax into -i '-** +mycrate::**::interesting_function' <BACKEND>
</code></pre>
<ul>
<li><strong>Explanation</strong>:
<ul>
<li><code>-**</code>: Excludes all items by default.</li>
<li><code>+mycrate::**::interesting_function</code>: Includes all items matching <code>mycrate::**::interesting_function</code> and their dependencies.</li>
</ul>
</li>
<li><strong>Extracted Items</strong>:
<ol>
<li><code>mycrate::interesting_function</code> (direct match).</li>
<li><code>mycrate::foo::interesting_function</code> (direct match).</li>
<li><code>mycrate::foo::bar::interesting_function</code> (direct match).</li>
<li><code>mycrate::aux</code> (dependency of <code>mycrate::interesting_function</code>).</li>
<li><code>mycrate::foo::f</code> (dependency of <code>mycrate::aux</code>).</li>
<li><code>mycrate::foo::something</code> (dependency of <code>mycrate::foo::interesting_function</code>).</li>
</ol>
</li>
</ul>
<h4 id="2-excluding-specific-items"><a class="header" href="#2-excluding-specific-items"><strong>2. Excluding Specific Items</strong></a></h4>
<pre><code class="language-bash">cargo hax into -i '+** -*::not_that_one' <BACKEND>
</code></pre>
<ul>
<li><strong>Explanation</strong>:
<ul>
<li><code>+**</code>: Includes all items by default.</li>
<li><code>-*::not_that_one</code>: Excludes any item named <code>not_that_one</code>, but keeps all other items, including <code>not_that_one_dependency</code>.</li>
</ul>
</li>
<li><strong>Extracted Items</strong>: All except <code>mycrate::not_that_one</code>.</li>
</ul>
<h4 id="3-including-items-without-dependencies"><a class="header" href="#3-including-items-without-dependencies"><strong>3. Including Items Without Dependencies</strong></a></h4>
<pre><code class="language-bash">cargo hax into -i '-** +!mycrate::interesting_function' <BACKEND>
</code></pre>
<ul>
<li><strong>Explanation</strong>:
<ul>
<li><code>-**</code>: Excludes all items by default.</li>
<li><code>+!mycrate::interesting_function</code>: Includes only <code>mycrate::interesting_function</code>, without dependencies.</li>
</ul>
</li>
<li><strong>Extracted Items</strong>: Only <code>mycrate::interesting_function</code>.</li>
</ul>
<h4 id="4-including-items-with-direct-dependencies-only"><a class="header" href="#4-including-items-with-direct-dependencies-only"><strong>4. Including Items with Direct Dependencies Only</strong></a></h4>
<pre><code class="language-bash">cargo hax into -i '-** +~mycrate::interesting_function' <BACKEND>
</code></pre>
<ul>
<li><strong>Explanation</strong>:
<ul>
<li><code>-**</code>: Excludes all items by default.</li>
<li><code>+~mycrate::interesting_function</code>: Includes <code>mycrate::interesting_function</code> and its direct dependencies (but not their transitive dependencies).</li>
</ul>
</li>
<li><strong>Extracted Items</strong>:
<ol>
<li><code>mycrate::interesting_function</code>.</li>
<li><code>mycrate::aux</code> (direct dependency).</li>
</ol>
</li>
<li><strong>Excluded Items</strong>:
<ul>
<li><code>mycrate::foo::f</code> (transitive dependency of <code>mycrate::aux</code>).</li>
</ul>
</li>
</ul>
<h4 id="5-including-items-in-signature-only-mode"><a class="header" href="#5-including-items-in-signature-only-mode"><strong>5. Including Items in Signature-Only Mode</strong></a></h4>
<pre><code class="language-bash">cargo hax into -i '+:mycrate::not_extracting_function' <BACKEND>
</code></pre>
<ul>
<li><strong>Explanation</strong>:
<ul>
<li><code>+:mycrate::not_extracting_function</code>: Includes only the type signature of <code>mycrate::not_extracting_function</code> (e.g., as an assumed or axiomatized symbol).</li>
</ul>
</li>
<li><strong>Extracted Items</strong>:
<ul>
<li>The type signature of <code>mycrate::not_extracting_function</code>, without its body or dependencies.</li>
</ul>
</li>
</ul>
<h3 id="summary"><a class="header" href="#summary"><strong>Summary</strong></a></h3>
<p>The <code>-i</code> flag offers powerful control over extraction, allowing fine-grained inclusion and exclusion of items with various dependency handling strategies. Use it to:</p>
<ul>
<li>Extract specific items and their dependencies (<code>+</code> or <code>+~</code>).</li>
<li>Exclude certain items (<code>-</code>).</li>
<li>Include items without dependencies (<code>+!</code>).</li>
<li>Extract type signatures only (<code>+:</code>).</li>
</ul>
<p>For complex crates, this flexibility ensures only the necessary parts are extracted, optimizing analysis or transformation workflows.</p>
<div style="break-before: page; page-break-before: always;"></div><h1 id="contributing"><a class="header" href="#contributing">Contributing</a></h1>
<p>This chapter contains information about internals of hax.</p>
<p>Please read the <a href="https://github.com/hacspec/hax/blob/main/CONTRIBUTING.md"><code>CONTRIBUTING.md</code></a> before opening a pull request.</p>
<div style="break-before: page; page-break-before: always;"></div><h1 id="architecture"><a class="header" href="#architecture">Architecture</a></h1>
<p>Hax is a software pipeline designed to transform Rust code into various formal verification backends such as <strong>F*</strong>, <strong>Coq</strong>, <strong>ProVerif</strong>, and <strong>EasyCrypt</strong>. It comprises two main components:</p>
<ol>
<li><strong>The Frontend</strong> (written in Rust)</li>
<li><strong>The Engine</strong> (written in OCaml)</li>
</ol>
<p>The frontend hooks into the Rust compiler, producing a abstract syntax tree for a given crate. The engine then takes this AST in input, applies various transformation, to reach in the end the language of the backend: F*, Coq...</p>
<h2 id="the-frontend-rust"><a class="header" href="#the-frontend-rust">The Frontend (Rust)</a></h2>
<p>The frontend is responsible for extracting and exporting Rust code's abstract syntax trees (ASTs) in a format suitable for processing by the engine (or by other tools).</p>
<h3 id="hax-frontend-exporter-library"><a class="header" href="#hax-frontend-exporter-library"><a href="https://hacspec.org/hax/frontend/hax_frontend_exporter/index.html"><code>hax-frontend-exporter</code> Library</a></a></h3>
<p>This library mirrors the internal types of the Rust compiler (<code>rustc</code>) that constitute the <strong>HIR</strong> (High-Level Intermediate Representation), <strong>THIR</strong> (Typed High-Level Intermediate Representation), and <strong>MIR</strong> (Mid-Level Intermediate Representation) ASTs. It extends them with additional information such as attributes, trait implementations, and removes ID indirections.</p>
<p><strong><code>SInto</code> Trait:</strong> The library defines an entry point for translating a given <code>rustc</code> value to its mirrored hax version using the <a href="https://hacspec.org/hax/frontend/hax_frontend_exporter/trait.SInto.html"><code>SInto</code></a> trait (stateful <code>into</code>). For a value <code>x</code> of type <code>T</code> from <code>rustc</code>, if <code>T</code> is mirrored by hax, then <code>x.sinto(s)</code> produces an augmented and simplified "hax-ified" AST for <code>x</code>. Here, <code>s</code> represents the state holding information about the translation process.</p>
<h3 id="hax-driver-binary"><a class="header" href="#hax-driver-binary"><code>hax-driver</code> Binary</a></h3>
<p><code>hax-driver</code> is a custom Rust compiler driver that behaves like <code>rustc</code> but performs additional tasks:</p>
<ol>
<li><strong>Item Enumeration:</strong> Lists all items in a crate.</li>
<li><strong>AST Transformation:</strong> Applies <code>sinto</code> on each item to generate the hax-ified AST.</li>
<li><strong>Output Generation:</strong> Outputs the mirrored items into a <code>haxmeta</code> file within the <code>target</code> directory.</li>
</ol>
<h3 id="cargo-hax-binary"><a class="header" href="#cargo-hax-binary"><code>cargo-hax</code> Binary</a></h3>
<p><code>cargo-hax</code> provides a <code>hax</code> subcommand for Cargo, accessible via <code>cargo hax --help</code>. It serves as the command-line interface for hax, orchestrating both the frontend and the engine.</p>
<p><strong>Workflow:</strong></p>
<ol>
<li><strong>Custom Build Execution:</strong> Runs <code>cargo build</code>, instructing Cargo to use <code>hax-driver</code> instead of <code>rustc</code>.</li>
<li><strong>Multiple Compiler Invocations:</strong> <code>cargo build</code> invokes <code>hax-driver</code> multiple times with various options.</li>
<li><strong>Inter-Process Communication:</strong> <code>hax-driver</code> communicates with <code>cargo-hax</code> via <code>stderr</code> using JSON lines.</li>
<li><strong>Metadata Generation:</strong> Produces <code>haxmeta</code> files containing the transformed ASTs.</li>
<li><strong>Engine Invocation (Optional):</strong> If requested, runs the engine, passing options and <code>haxmeta</code> information via <code>stdin</code> serialized as JSON.</li>
<li><strong>Interactive Communication:</strong> Engages in interactive communication with the engine.</li>
<li><strong>User Reporting:</strong> Outputs results and diagnostics to the user.</li>
</ol>
<h2 id="the-engine-ocaml---documentation"><a class="header" href="#the-engine-ocaml---documentation">The Engine (OCaml - <a href="https://hacspec.org/hax/engine/hax-engine/index.html">documentation</a>)</a></h2>
<p>The engine processes the transformed ASTs and options provided via JSON input from <code>stdin</code>. It performs several key functions to convert the hax-ified Rust code into the target backend language.</p>
<h3 id="importing-and-simplifying-asts"><a class="header" href="#importing-and-simplifying-asts">Importing and Simplifying ASTs</a></h3>
<ul>
<li><strong>AST Importation:</strong> Imports the hax-ified Rust THIR AST. This is module <a href="https://hacspec.org/hax/engine/hax-engine/Hax_engine/Import_thir/index.html"><code>Import_thir</code></a>.</li>
<li><strong>Internal AST Conversion:</strong> Converts the imported AST into a simplified and opinionated internal AST designed for ease of transformation and analysis. This is mostly the functor <a href="https://hacspec.org/hax/engine/hax-engine/Hax_engine/Ast/Make/index.html"><code>Ast.Make</code></a>.</li>
</ul>
<h3 id="internal-ast-and-features"><a class="header" href="#internal-ast-and-features">Internal AST and Features</a></h3>
<p>The internal AST is defined using a <strong>functor</strong> that takes a list of type-level booleans, referred to as <strong>features</strong>, and produces the AST types accordingly.</p>
<p>Features are for instances, mutation, loops, unsafe code. The enumeration <a href="https://hacspec.org/hax/engine/hax-engine/Hax_engine/Features/Enumeration/index.html"><code>Features.Enumeration</code></a> lists all those features.</p>
<p><strong>Feature Witnesses:</strong> On relevant AST nodes, feature witnesses are included to enforce constraints at the type level. For example, in the <code>loop</code> expression constructor, a witness of type <code>F.loop</code> is used, where <code>F</code> represents the current feature set. If <code>F.loop</code> is an empty type, constructing a <code>loop</code> expression is prohibited, ensuring that loops are disallowed in contexts where they are not supported.</p>
<h3 id="transformation-phases"><a class="header" href="#transformation-phases">Transformation Phases</a></h3>
<p>The engine executes a sequence of <strong>phases</strong>, which are determined based on the target backend. Each phase:</p>
<ol>
<li><strong>Input:</strong> Takes a list of items from an AST with specific feature constraints.</li>
<li><strong>Output:</strong> Transforms these items into a new AST type, potentially enabling or disabling features through type-level changes.</li>
</ol>
<p>The phases can be found in the <a href="https://hacspec.org/hax/engine/hax-engine/Hax_engine/Phases/index.html"><code>Phases</code></a> module.</p>
<h3 id="backend-code-generation"><a class="header" href="#backend-code-generation">Backend Code Generation</a></h3>
<p>After completing the transformation phases:</p>
<ol>
<li><strong>Backend Printer Invocation:</strong> Calls the printer associated with the selected backend to generate the target code.</li>
<li><strong>File Map Creation:</strong> Produces a map from file names to their contents, representing the generated code.</li>
<li><strong>Output Serialization:</strong> Outputs the file map and additional information (e.g., errors) as JSON to <code>stderr</code>.</li>
</ol>
<h3 id="communication-protocol"><a class="header" href="#communication-protocol">Communication Protocol</a></h3>
<p>The engine communicates asynchronously with the frontend using a protocol defined in <a href="https://hacspec.org/hax/frontend/hax_types/engine_api/protocol/index.html"><code>hax_types::engine_api::protocol</code></a>. This communication includes:</p>
<ul>
<li><strong>Diagnostic Data:</strong> Sending error messages, warnings, and other diagnostics.</li>
<li><strong>Profiling Information:</strong> Providing performance metrics and profiling data.</li>
<li><strong>Pretty-Printing Requests:</strong> Requesting formatted versions of Rust source code or diagnostics for better readability.</li>
</ul>
<div style="break-before: page; page-break-before: always;"></div><h1 id="libraries"><a class="header" href="#libraries">Libraries</a></h1>
<h1 id="macros-and-attributes"><a class="header" href="#macros-and-attributes">Macros and attributes</a></h1>
<p>The hax engine understands only one attribute: <code>#[_hax::json(PAYLOAD)]</code>,
where <code>PAYLOAD</code> is a JSON serialization of the Rust enum
<code>hax_lib_macros_types::AttrPayload</code>.</p>
<p>Note <code>#[_hax::json(PAYLOAD)]</code> is a <a href="https://github.com/rust-lang/rust/issues/66079">tool
attribute</a>: an
attribute that is never expanded.</p>
<p>In the engine, the OCaml module <code>Attr_payloads</code> offers an API to query
attributes easily. The types in crate <code>hax_lib_macros_types</code> and
corresponding serializers/deserializers are automatically generated in
OCaml, thus there is no manual parsing involved.</p>
<h2 id="user-experience"><a class="header" href="#user-experience">User experience</a></h2>
<p>Asking the user to type <code>#[_hax::json(some_long_json)]</code> is not very
friendly. Thus, the crate <code>hax-lib-macros</code> defines a bunch of <a href="https://doc.rust-lang.org/beta/reference/procedural-macros.html">proc
macros</a>
that defines nice and simple-to-use macros. Those macro take care of
cooking some <code>hax_lib_macros_types::AttrPayload</code> payload(s), then
serialize those payloads to JSON and produce one or more
<code>#[_hax::json(serialized_payload)]</code> attributes.</p>
<div style="break-before: page; page-break-before: always;"></div><p>We currently take inputs from the following AST (visualization can be done
using <a href="https://rr.red-dove.com/ui">https://rr.red-dove.com/ui</a>). Literals are strings, numbers and
booleans.</p>
<pre><code class="language-ebnf">char ::= [a-zA-Z]
string ::= char*
digit ::= [0-9]
uint ::= digit+
int ::= ("-")? uint
float ::= int (".")? uint
bool ::= "true" | "false"
local_var ::= ident
global_var ::= rust-path-identifier
literal ::=
| '"' string '"'
| "'" char "'"
| int
| float (* [a] *)
| bool
</code></pre>
<p>We support a number of simple types characters, strings, booleans and
numbers. Number types for integers (8,16,32,64,128 bit or machine sized)
and floats (16,32, or 64 bit). Composite types are tuples, fixed length
lists (arrays), variable length lists (vectors/slices), ptr types, and
function types. Lastly we have named types defined by items, e.g. enums
and structs.</p>
<pre><code class="language-ebnf">ty ::=
| "bool"
| "char"
| "u8" | "u16" | "u32" | "u64"
| "u128" | "usize"
| "i8" | "i16" | "i32" | "i64"
| "i128" | "isize"
| "f16" | "f32" | "f64" (* [a] *)
| "str"
| (ty ",")*
| "[" ty ";" int "]"
| "[" ty "]"
| "*const" ty | "*mut" ty (* [b] *)
| "*" expr | "*mut" expr (* [b] *)
| ident
| (ty "->")* ty
| "dyn" (goal)+ (* [c] *)
</code></pre>
<p>The patterns allowed reflect these types. Wildcard patterns, literal
types, typed patterns, list patterns, record or tuple patterns.</p>
<pre><code class="language-ebnf">pat ::=
| "_"
| ident "{" (ident ":" pat ";")* "}"
| ident "(" (pat ",")* ")"
| (pat "|")* pat
| "[" (pat ",")* "]" (* [d] *)
| "&" pat
| literal
| ("&")? ("mut")? ident ("@" pat)? (* [e] *)
</code></pre>
<p>The simple expressions are literals, local or global variables, type
casts, assignments and lists. Control flow expressions, if statements,
match statements, loops, return, break and continue. The rest is blocks,
macro calls, lambda functions and borrowing.</p>
<pre><code class="language-ebnf">expr ::=
| "if" expr "{" expr "}" ("else" "{" expr "}")?
| "if" "let" pat (":" ty)? "=" expr "{" expr "}" ("else" "{" expr "}")?
| expr "(" (expr ",")* ")"
| literal
| "[" (expr ",")* "]" | "[" expr ";" int "]"
| ident "{" (ident ":"expr ";")* "}"
| ident "{" (ident ":"expr ";")* ".." expr "}"
| "match" expr guard "{"
(("|" pat)* "=>" (expr "," | "{" expr "}"))*
"}"
| "let" pat (":" ty)? "=" expr ";" expr
| "let" pat (":" ty)? "=" expr "else" "{" expr "}" ";" expr
| modifiers "{" expr "}"
| local_var
| global_var
| expr "as" ty
| "loop" "{" expr "}"
| "while" "(" expr ")" "{" expr "}"
| "for" "(" pat "in" expr ")" "{" expr "}"
| "for" "(" "let" ident "in" expr ".." expr ")" "{" expr "}"
| "break" expr
| "continue"
| pat "=" expr
| "return" expr
| expr "?"
| "&" ("mut")? expr (* [e] *)
| "&" expr "as" "&const _" (* [b] *)
| "&mut" expr "as" "&mut _"
| "|" pat "|" expr
</code></pre>
<p>The items supported are functions, type aliasing, enums, structs, trait
definitions and implementations, and imports.</p>
<pre><code class="language-ebnf">item ::=
| "const" ident "=" expr
| "static" ident "=" expr (* [b] *)
| modifiers "fn" ident ("<" (generics ",")* ">")? "(" (pat ":" ty ",")* ")" (":" ty)? "{" expr "}"
| "type" ident "=" ty
| "enum" ident ("<" (generics ",")* ">")? "{" (ident ("(" (ty)* ")")? ",")* "}"
| "struct" ident ("<" (generics ",")* ">")? "{" (ident ":" ty ",")* "}"
| "trait" ident ("<" (generics ",")* ">")? "{" (trait_item)* "}"
| "impl" ("<" (generics ",")* ">")? ident "for" ty "{" (impl_item)* "}"
| "mod" ident "{" (item)* "}"
| "use" path ";"
</code></pre>
<h2 id="full-ebnf"><a class="header" href="#full-ebnf">Full eBNF</a></h2>
<pre><code class="language-ebnf">char ::= [a-zA-Z]
string ::= char*
digit ::= [0-9]
uint ::= digit+
int ::= ("-")? uint
float ::= int (".")? uint
bool ::= "true" | "false"
local_var ::= ident
global_var ::= rust-path-identifier
literal ::=
| '"' string '"'
| "'" char "'"
| int
| float [a]
| bool
generic_value ::=
| "'" ident
| ty
| expr
goal ::=
| ident "<" (generic_value ",")* ">"
ty ::=
| "bool"
| "char"
| "u8" | "u16" | "u32" | "u64"
| "u128" | "usize"
| "i8" | "i16" | "i32" | "i64"
| "i128" | "isize"
| "f16" | "f32" | "f64" (* [a] *)
| "str"
| (ty ",")*
| "[" ty ";" int "]"
| "[" ty "]"
| "*const" ty | "*mut" ty (* [b] *)
| "*" expr | "*mut" expr (* [b] *)
| ident
| (ty "->")* ty
| "dyn" (goal)+ (* [c] *)
pat ::=
| "_"
| ident "{" (ident ":" pat ";")* "}"
| ident "(" (pat ",")* ")"
| (pat "|")* pat
| "[" (pat ",")* "]" (* [d] *)
| "&" pat
| literal
| ("&")? ("mut")? ident ("@" pat)? (* [e] *)
modifiers ::=
| ""
| "unsafe" modifiers
| "const" modifiers
| "async" modifiers (* [b] *)
guard ::=
| "if" "let" pat (":" ty)? "=" expr
expr ::=
| "if" expr "{" expr "}" ("else" "{" expr "}")?
| "if" "let" pat (":" ty)? "=" expr "{" expr "}" ("else" "{" expr "}")?
| expr "(" (expr ",")* ")"
| literal
| "[" (expr ",")* "]" | "[" expr ";" int "]"
| ident "{" (ident ":"expr ";")* "}"
| ident "{" (ident ":"expr ";")* ".." expr "}"
| "match" expr guard "{"
(("|" pat)* "=>" (expr "," | "{" expr "}"))*
"}"
| "let" pat (":" ty)? "=" expr ";" expr
| "let" pat (":" ty)? "=" expr "else" "{" expr "}" ";" expr
| modifiers "{" expr "}"
| local_var
| global_var
| expr "as" ty
| "loop" "{" expr "}"
| "while" "(" expr ")" "{" expr "}"
| "for" "(" pat "in" expr ")" "{" expr "}"
| "for" "(" "let" ident "in" expr ".." expr ")" "{" expr "}"
| "break" expr
| "continue"
| pat "=" expr
| "return" expr
| expr "?"
| "&" ("mut")? expr (* [e] *)
| "&" expr "as" "&const _" (* [b] *)
| "&mut" expr "as" "&mut _"
| "|" pat "|" expr
impl_item ::=