https://github.com/project-everest/hacl-star
History
Tip revision: 7e7a8007d3ddc833aa7aedb6698b1b5fa6c8a831 authored by Santiago Zanella-Beguelin on 02 November 2018, 13:12:35 UTC
Function to allocate a stuck buffer an initialize it with a stateful function with read effect
Tip revision: 7e7a800
File Mode Size
c
experimental
fst
ml
tutorial
Lib.Buffer.fsti -rw-r--r-- 28.8 KB
Lib.ByteBuffer.fsti -rw-r--r-- 4.0 KB
Lib.ByteSequence.fsti -rw-r--r-- 2.7 KB
Lib.IntTypes.fsti -rw-r--r-- 12.3 KB
Lib.IntVector.fsti -rw-r--r-- 5.3 KB
Lib.LoopCombinators.fsti -rw-r--r-- 4.5 KB
Lib.Loops.fsti -rw-r--r-- 546 bytes
Lib.NatMod.fsti -rw-r--r-- 579 bytes
Lib.Network.fsti -rw-r--r-- 1.4 KB
Lib.Print.fsti -rw-r--r-- 548 bytes
Lib.Random.fsti -rw-r--r-- 265 bytes
Lib.RawIntTypes.fsti -rw-r--r-- 1.6 KB
Lib.Sequence.Lemmas.fsti -rw-r--r-- 3.1 KB
Lib.Sequence.fsti -rw-r--r-- 8.8 KB
Makefile -rw-r--r-- 965 bytes

back to top