-
Notifications
You must be signed in to change notification settings - Fork 1
/
_CoqProject
50 lines (50 loc) · 1.32 KB
/
_CoqProject
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
-R . lib
#Common/general results
proofs/Common/ByteFacts.v
proofs/Common/CommonSSR.v
proofs/Common/ZSeq.v
#Pure mathcomp/functional model
#proofs/Poly/PolyField.v
#proofs/Poly/BoolField.v
proofs/Poly/ListPoly.v
proofs/Poly/ByteField.v
proofs/Matrix/Gaussian.v
proofs/Matrix/GaussRestrict.v
proofs/Matrix/LinIndep.v
proofs/Matrix/Vandermonde.v
proofs/RS/ReedSolomon.v
#Intermediate layer (VST + mathcomp)
proofs/Matrix/ListMatrix.v
proofs/Matrix/MatrixTransform.v
proofs/Matrix/VandermondeByte.v
proofs/RS/ReedSolomonList.v
#Functional model for packet/buffer management
proofs/FEC/AssocList.v
proofs/FEC/AbstractPacket.v
proofs/FEC/Endian.v
proofs/FEC/IP.v
proofs/FEC/CommonFEC.v
proofs/FEC/Block.v
proofs/FEC/Producer.v
proofs/FEC/ConsumerGeneric.v
proofs/FEC/ConsumerNoTimeouts.v
proofs/FEC/Reorder.v
proofs/FEC/ConsumerTimeouts.v
proofs/FEC/SeqCmp.v
proofs/FEC/ConsumerMachine.v
proofs/FEC/ProducerConsumerCorrectness.v
#C code for packet/buffer management
src/modified/mini_prod3/fecActuator/redFecActuator.v
src/modified/mini_prod3/fecActuator/blackFecActuator.v
#VST(core FEC)
src/modified/mini_prod3/fecActuator/fec.v
proofs/VST/CommonVST.v
proofs/VST/Specs.v
proofs/VST/FECTactics.v
proofs/VST/PopArrays.v
proofs/VST/Verif_field.v
proofs/VST/Verif_matrix.v
proofs/VST/Verif_encode.v
proofs/VST/Verif_decode.v
#Evaluation (core FEC)
proofs/Eval.v