svGolf

Tasks / trusted base

The shared trusted base

The modules every task statement rests on.

Modules
17
Lines
15095

Every task statement rests on these modules: the ls-sv semantics of SystemVerilog and svGolf's statement helpers. A proved submission guarantees what its task's statement says under them. Each task page lists only the trusted text specific to that task. Any module of the ls-sv library may be imported by a proof; only the modules below are trusted, since proof helpers are kernel-checked like any submission. The list is computed from the import lines of the task statements.

modulerolefilelinessha256
LeanModels.Sv.Astls-sv semanticsLeanModels/Sv/Ast.lean220ddf990d46960
LeanModels.Sv.Basicls-sv semanticsLeanModels/Sv/Basic.lean83374d24ac1278a
LeanModels.Sv.Comb2ls-sv semanticsLeanModels/Sv/Comb2.lean355553d6eeecf42
LeanModels.Sv.Comb2Basels-sv semanticsLeanModels/Sv/Comb2Base.lean219673576972594f
LeanModels.Sv.Comb2Procls-sv semanticsLeanModels/Sv/Comb2Proc.lean303580b1c132bb3d
LeanModels.Sv.Comb2Soundls-sv semanticsLeanModels/Sv/Comb2Sound.lean2728bbaefbf8585
LeanModels.Sv.Comb2Termls-sv semanticsLeanModels/Sv/Comb2Term.lean672774c73de2b5c
LeanModels.Sv.Known2ls-sv semanticsLeanModels/Sv/Known2.lean101946f66561d915
LeanModels.Sv.Mono2ls-sv semanticsLeanModels/Sv/Mono2.lean971f5aee8e39ee6
LeanModels.Sv.Obsls-sv semanticsLeanModels/Sv/Obs.lean9053844f59766b0
LeanModels.Sv.Pure2ls-sv semanticsLeanModels/Sv/Pure2.lean72698439f9af2f7
LeanModels.Sv.Sem2ls-sv semanticsLeanModels/Sv/Sem2.lean10989b421e3718b1
LeanModels.Sv.Semanticsls-sv semanticsLeanModels/Sv/Semantics.lean50406652c4cca2c
LeanModels.Sv.Spec2ls-sv semanticsLeanModels/Sv/Spec2.lean522a2836f647332
SvGolf.TasksvGolf statement helperssvgolf/SvGolf/Task.lean282b3f184fea555
SvGolf.TaskReactsvGolf statement helperssvgolf/SvGolf/TaskReact.lean309a065631fb9c2
SvGolf.TaskSeqsvGolf statement helperssvgolf/SvGolf/TaskSeq.lean11762c1fdc159967