Skip to content

Commit 2dd300b

Browse files
nguyenvukhangnguyenvukhang
committed
First commit
0 parents  commit 2dd300b

8 files changed

Lines changed: 221 additions & 0 deletions

File tree

‎.github/workflows/ci.yml‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
name: CI
2+
3+
on:
4+
push:
5+
branches:
6+
- main
7+
- dev
8+
tags:
9+
- "v[0-9]+.[0-9]+.[0-9]+"
10+
11+
permissions:
12+
contents: write
13+
14+
jobs:
15+
lean:
16+
runs-on: ubuntu-24.04
17+
steps:
18+
- run: cargo install --git https://github.com/nguyenvukhang/slope.git
19+
- uses: actions/checkout@v4
20+
- uses: leanprover/lean-action@v1
21+
with:
22+
build: false
23+
lint: false
24+
test: false
25+
- run: make all

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
/.lake

‎Makefile‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
LAKE_BUILD := lake build --log-level=warning
2+
3+
current: focus
4+
5+
focus: check
6+
slope build SFBits
7+
8+
all: check
9+
slope build
10+
11+
check: generate
12+
slope check
13+
14+
generate:
15+
# slope generate SFBits.Defs
16+
17+
sorry:
18+
rg sorry -t lean --colors 'match:fg:yellow' --colors 'line:fg:white'
19+
20+
# First-time Setup =============================================================
21+
22+
setup:
23+
lake exe cache get
24+
25+
install:
26+
make -C fmt install

‎README.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
# SFBits
2+
3+
Note: the import order goes: `import`, `open`, `namespace`, `universe`,
4+
`variable`.

‎SFBits/Overflow.lean‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
import Mathlib.Algebra.Ring.Nat
2+
import Mathlib.Order.Basic
3+
import Mathlib.Tactic
4+
5+
variable
6+
-- M is the wrapping point of the unsigned integer representation. So if we're
7+
-- dealing with uint32, then M is 1 more than the maximum representable value
8+
-- in uint32.
9+
(M : ℕ)
10+
-- Since all integer types are non-trivial (uint8, uint16, uint32, ..., but we
11+
-- never see a uint0), it is safe to assume that M is positive.
12+
(hM₀ : 0 < M)
13+
14+
-- Let (a b : uint32). This theorem tells us that we can check if there will be
15+
-- multiplcation overflow upon `a * b` by simply checking if `0 < a`, and that
16+
-- `a * b / a != b`. (note that the modulo-M operation will be the part of the
17+
-- overflow).
18+
include hM₀ in
19+
theorem UintMultplicationOverflow (a b : ℕ) :
20+
M ≤ a * b -- multiplication overflow
21+
↔ 0 < a ∧ a * b % M / a ≠ b := by
22+
rcases Nat.eq_zero_or_pos b with hb₀ | hb₀
23+
· -- b = 0
24+
subst hb₀
25+
rw [mul_zero]
26+
constructor
27+
· intro h
28+
exact False.elim (h.not_gt hM₀)
29+
· intro ⟨_, h⟩
30+
refine False.elim ?_
31+
rw [Nat.zero_mod, Nat.zero_div] at h
32+
exact false_of_ne h
33+
· -- b > 0
34+
constructor
35+
· intro hab
36+
have hab₀ : 0 < a * b := Nat.lt_of_lt_of_le hM₀ hab
37+
have ha₀ : 0 < a := Nat.pos_of_mul_pos_right hab₀
38+
have : a * b % M / a ≤ (a * b - M) / a := by
39+
refine Nat.div_le_div_right ?_
40+
rw [Nat.mod_eq_sub]
41+
refine Nat.sub_le_sub_left ?_ (a * b)
42+
refine Nat.le_mul_of_pos_right M ?_
43+
exact Nat.div_pos_iff.mpr ⟨hM₀, hab⟩
44+
refine ⟨ha₀, ?_⟩
45+
refine Nat.ne_of_lt ?_
46+
refine this.trans_lt ?_
47+
rw [Nat.div_lt_iff_lt_mul ha₀, mul_comm]
48+
exact Nat.sub_lt (Nat.mul_pos hb₀ ha₀) hM₀
49+
· intro ⟨ha₀, hne⟩
50+
refine Nat.le_of_not_lt ?_
51+
by_contra hab
52+
have : a * b % M = a * b := Nat.mod_eq_of_lt hab
53+
rw [this, Nat.mul_div_cancel_left b ha₀] at hne
54+
exact false_of_ne hne

‎lake-manifest.json‎

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
{"version": "1.1.0",
2+
"packagesDir": ".lake/packages",
3+
"packages":
4+
[{"url": "https://github.com/leanprover-community/mathlib4",
5+
"type": "git",
6+
"subDir": null,
7+
"scope": "leanprover-community",
8+
"rev": "13fd9cea576a03bec007c803ee4499e35b49dd3d",
9+
"name": "mathlib",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "master",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/leanprover-community/plausible",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "leanprover-community",
18+
"rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
19+
"name": "plausible",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "main",
22+
"inherited": true,
23+
"configFile": "lakefile.toml"},
24+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
25+
"type": "git",
26+
"subDir": null,
27+
"scope": "leanprover-community",
28+
"rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
29+
"name": "LeanSearchClient",
30+
"manifestFile": "lake-manifest.json",
31+
"inputRev": "main",
32+
"inherited": true,
33+
"configFile": "lakefile.toml"},
34+
{"url": "https://github.com/leanprover-community/import-graph",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "leanprover-community",
38+
"rev": "cff9dd30f2c161b9efd7c657cafed1f967645890",
39+
"name": "importGraph",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "main",
42+
"inherited": true,
43+
"configFile": "lakefile.toml"},
44+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
45+
"type": "git",
46+
"subDir": null,
47+
"scope": "leanprover-community",
48+
"rev": "ef8377f31b5535430b6753a974d685b0019d0681",
49+
"name": "proofwidgets",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "v0.0.84",
52+
"inherited": true,
53+
"configFile": "lakefile.lean"},
54+
{"url": "https://github.com/leanprover-community/aesop",
55+
"type": "git",
56+
"subDir": null,
57+
"scope": "leanprover-community",
58+
"rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c",
59+
"name": "aesop",
60+
"manifestFile": "lake-manifest.json",
61+
"inputRev": "master",
62+
"inherited": true,
63+
"configFile": "lakefile.toml"},
64+
{"url": "https://github.com/leanprover-community/quote4",
65+
"type": "git",
66+
"subDir": null,
67+
"scope": "leanprover-community",
68+
"rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72",
69+
"name": "Qq",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "master",
72+
"inherited": true,
73+
"configFile": "lakefile.toml"},
74+
{"url": "https://github.com/leanprover-community/batteries",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "2e16f91af2a97975e5d2fac906494cd6c17ba255",
79+
"name": "batteries",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": "main",
82+
"inherited": true,
83+
"configFile": "lakefile.toml"},
84+
{"url": "https://github.com/leanprover/lean4-cli",
85+
"type": "git",
86+
"subDir": null,
87+
"scope": "leanprover",
88+
"rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
89+
"name": "Cli",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "v4.27.0-rc1",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"}],
94+
"name": "SFBits",
95+
"lakeDir": ".lake"}

‎lakefile.lean‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
import Lake
2+
3+
open System Lake DSL
4+
5+
package SFBits where
6+
version := v!"0.1.0"
7+
keywords := #["math"]
8+
leanOptions :=
9+
#[⟨`pp.unicode.fun, true⟩,
10+
⟨`autoImplicit, false⟩,
11+
⟨`weak.linter.mathlibStandardSet, true⟩]
12+
13+
require "leanprover-community" / mathlib
14+
15+
@[default_target] lean_lib SFBits

‎lean-toolchain‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
leanprover/lean4:v4.27.0-rc1

0 commit comments

Comments
 (0)