jasmin

高保证和高速密码学的语言

  • 语言Rocq Prover
  • 默认分支main
  • 大小27.6 MB
  • 更新11 小时前
在 GitHub 打开
avatarjasmin-lang
391
89157
MIT License

项目介绍

jasmin-lang/jasmin 是一个托管在 GitHub 上的开源项目，主要使用 Rocq Prover 编写，采用 MIT License 许可证，目前获得 391 个 Star、89 次 Fork。

仓库全名
jasmin-lang/jasmin
开源许可证
MIT License
Star 数
391
Fork 数
89
未关闭 Issue
157

README 摘要

Jasmin About Jasmin denotes both a language and a compiler designed for writing high-assurance and high-speed cryptography. Jasmin implementations aim at being efficient, safe, correct, and secure. Reference documentation of the language and compiler are on readthedocs. Installation For a complete installation guide covering several use cases, please read our documentation. If you just want to install the Jasmin…

完整内容见 GitHub 原始 README 或本页 。

常见问题

jasmin 用什么语言开发？

主要使用 Rocq Prover 编写，采用 MIT License 许可证，目前有 391 个 Star。

jasmin 可以免费商用吗？

仓库采用 MIT License 许可证，可免费使用与修改，商业使用请遵守许可证条款（例如保留版权声明与许可声明）。

如何获取 jasmin 的源码？

可以直接克隆仓库：git clone https://github.com/jasmin-lang/jasmin.git，默认分支为 main；安装与运行步骤见仓库 README。

jasmin 最近还在维护吗？

仓库最近一次更新为 11 小时前，当前有 157 个未关闭 Issue；Star 数为 391，可作为社区活跃度的参考。

本页面展示项目元数据与原始 README，GitRead 中文社区 编辑团队负责选题收录。

相关仓库

mit-plv/fiat-crypto avatar
fiat-cryptomit-plv
2 周前
851
181
214

Fiat 的密码学原始码生成

Rocq Prover
180.2 MB
0
详情
jwiegley/category-theory avatar
category-theoryjwiegley
1 天前
819
85
611

An axiom-free formalization of category theory in Coq for personal study and practical work

category-theorycoqmonad+7
Rocq Prover
23.1 MB
0
详情
math-comp/math-comp avatar
math-compmath-comp
6月10日
684
132
178

数学组成部分

coqcoq-formalizationmathcomp+5
Rocq Prover
18.9 MB
0
详情
mit-plv/kami avatar
kamimit-plv
9月17日
173
31
3

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

bluespeccoqhardware-description-language+2
Rocq Prover
4.7 MB
0
详情
mit-plv/fiat avatar
fiatmit-plv
2 天前
157
34
1

主要自动化的结构正确程序综合

Rocq Prover
12.8 MB
0
详情
PrincetonUniversity/DeepSpecDB avatar
DeepSpecDBPrincetonUniversity
2025年11月21日
28
3
1

暂无描述

Rocq Prover
14.9 MB
0
详情
thery/hanoi avatar
hanoithery
1 周前
26
2
0

Coq的河内塔

Rocq Prover
1.6 MB
0
详情
thery/T2048 avatar
T2048thery
2 周前
22
2
0

a version of the 2048 game for Coq

2048coqgame
Rocq Prover
51 KB
0
详情

关于

GitHub 原始描述（英文）

Language for high-assurance and high-speed cryptography

描述取自 GitHub 官方 API，保持仓库作者书写的原文。

简要分析

热度分
578
价值分
254
活跃状态
活跃
compilercoqlanguage
GitHub

语言占比

C
Dune
Makefile
Nix
OCaml
Python
Raku
Rocq Prover
Shell
Standard ML
V
Verilog
eC

Release

贡献者

vbglvbglbgregoirbgregoirstrubstrubeponiereponierbeschmibeschmiAntoineSereAntoineSereakoutsosakoutsosartart78artart78sarranzsarranzmbbarbosambbarbosaMrDaikiMrDaikicassiersgcassiersg

README

Jasmin

pipeline status project chat project chat

About

Jasmin denotes both a language and a compiler designed for writing high-assurance and high-speed cryptography. Jasmin implementations aim at being efficient, safe, correct, and secure.

Reference documentation of the language and compiler are on readthedocs.

Installation

For a complete installation guide covering several use cases, please read our documentation.

If you just want to install the Jasmin tools, here is a TL;DR:

  • with APT (debian, ubuntu), a package is available in a dedicated repository, see the documentation

  • from AUR (arch linux), a package is available in the Arch User Repository, see the documentation

  • with nix

    nix-env -iA nixpkgs.jasmin-compiler

  • with opam

    opam install jasmin

Getting support

The Formosa-Crypto Zulip Chat is meant for anybody interested in high-assurance cryptography using EasyCrypt, Jasmin, and related tools.

License

Jasmin is free software. All files in this distribution are, unless specified otherwise, licensed under the MIT license. The documentation (under docs/) is licensed separately from the compiler, under the CC-BY 4.0.

评论

暂无评论