{"action":"created","comment":{"url":"https://api.github.com/repos/FStarLang/FStar/pulls/comments/81546341","pull_request_review_id":2500485,"id":81546341,"diff_hunk":"@@ -0,0 +1,201 @@\n+module Crypto.Symmetric.Bytes\n+\n+open FStar.HyperHeap\n+open FStar.HyperStack\n+open FStar.HST\n+open FStar.UInt32\n+open FStar.Ghost\n+open Buffer.Utils\n+\n+ \n+type mem = FStar.HyperStack.mem\n+\n+type bytes = Seq.seq UInt8.t \n+type buffer = Buffer.buffer UInt8.t \n+\n+type lbytes (l:nat)  = b:bytes  {Seq.length b = l}\n+type lbuffer (l:nat) = b:buffer {Buffer.length b = l}\n+\n+val sel_bytes: h:mem -> l:UInt32.t -> buf:lbuffer(v l){Buffer.live h buf}\n+  -> GTot (lbytes (v l))\n+let sel_bytes h l buf = Buffer.as_seq h buf\n+\n+val load_bytes: l:UInt32.t -> buf:lbuffer(v l) -> Stack (lbytes(v l))\n+  (requires (fun h0 -> Buffer.live h0 buf))\n+  (ensures  (fun h0 r h1 -> h0 == h1 /\\ Buffer.live h0 buf /\\ r == sel_bytes h1 l buf))\n+let rec load_bytes l buf = \n+  assume false;//16-10-02 16-09-21 TODO \n+  if l = 0ul then Seq.createEmpty else\n+  let b = Buffer.index buf 0ul in\n+  let t = load_bytes (l -^ 1ul) (Buffer.sub buf 1ul (l -^ 1ul)) in\n+  SeqProperties.cons b t\n+\n+\n+val store_bytes: l:UInt32.t -> buf:lbuffer(v l) -> b:lbytes(v l) -> ST unit\n+  (requires (fun h0 -> Buffer.live h0 buf))\n+  (ensures (fun h0 r h1 -> Buffer.live h1 buf /\\ Buffer.modifies_1 buf h0 h1 /\\ b == sel_bytes h1 l buf\n+  ))\n+\n+val store_bytes_aux: len:UInt32.t -> buf:lbuffer(v len) -> i:UInt32.t  {i <=^ len} -> b:lbytes(v len) -> ST unit\n+  (requires (fun h0 -> Buffer.live h0 buf))\n+  (ensures (fun h0 r h1 -> Buffer.live h1 buf /\\ Buffer.modifies_1 buf h0 h1 /\\ b == sel_bytes h1 len buf\n+  ))\n+let rec store_bytes_aux len buf i b = \n+  assume false;//16-09-21 TODO \n+  if i <^ len then (\n+  Buffer.upd buf i (Seq.index b (v i));\n+  store_bytes_aux len buf (i +^ 1ul) b)\n+let store_bytes l buf b = store_bytes_aux l buf 0ul b\n+\n+\n+(* We need functions to load/store integers in byte buffers. Possibly elsewhere. *)\n+\n+open FStar.Buffer\n+open FStar.Mul // 16-10-02 avoid?\n+open FStar.Int.Cast\n+// 16-10-02 pls go to Seq.fst\n+let head (#a:Type) (b:Seq.seq a {Seq.length b >= 1}) = Seq.index b 0\n+let tail (#a:Type) (b:Seq.seq a {Seq.length b >= 1}) = Seq.slice b 1 (Seq.length b)\n+\n+(* Little endian integer value of a sequence of bytes *)\n+let rec little_endian (b:bytes) : Tot (n:nat) (decreases (Seq.length b))\n+  = if Seq.length b = 0 then 0\n+    else ( \n+      UInt8.v (head b) + pow2 8 * little_endian (tail b))\n+\n+(*\n+val lemma_little_endian: b:bytes {Seq.length b > 0} -> Lemma \n+  (little_endian b = UInt8.v (head b) + pow2 8 * little_endian (tail b))\n+\n+let lemma_little_endian b = \n+  if Seq.length b = 0 then () \n+  else assume false\n+//16-10-02 ?\n+*)\n+\n+val lemma_euclidean_division: a:nat -> b:nat -> Lemma\n+  (requires (a < pow2 8))\n+  (ensures  (a + pow2 8 * b < pow2 8 * (b + 1)))\n+let lemma_euclidean_division a b = ()\n+\n+val lemma_factorise: a:nat -> b:nat -> Lemma (a + a * b = a * (b + 1))\n+let lemma_factorise a b = ()\n+\n+#reset-options \"--initial_fuel 1 --max_fuel 1\"\n+\n+val lemma_little_endian_is_bounded: b:bytes -> Lemma\n+  (requires True)\n+  (ensures  (little_endian b < pow2 (8 * Seq.length b)))\n+  (decreases (Seq.length b))\n+let rec lemma_little_endian_is_bounded b =\n+  if Seq.length b = 0 then ()\n+  else\n+    begin\n+    let s = Seq.slice b 1 (Seq.length b) in\n+    assert(Seq.length s = Seq.length b - 1);\n+    lemma_little_endian_is_bounded s;\n+    assert(UInt8.v (Seq.index b 0) < pow2 8);\n+    assert(little_endian s < pow2 (8 * Seq.length s));\n+    assert(little_endian b < pow2 8 + pow2 8 * pow2 (8 * (Seq.length b - 1)));\n+    lemma_euclidean_division (UInt8.v (Seq.index b 0)) (little_endian s);\n+    assert(little_endian b <= pow2 8 * (little_endian s + 1));\n+    assert(little_endian b <= pow2 8 * pow2 (8 * (Seq.length b - 1)));\n+    Math.Lemmas.pow2_plus 8 (8 * (Seq.length b - 1));\n+    lemma_factorise 8 (Seq.length b - 1)\n+    end\n+ \n+#reset-options \"--initial_fuel 0 --max_fuel 0\"\n+\n+val lemma_little_endian_lt_2_128: b:bytes {Seq.length b <= 16} -> Lemma\n+  (requires (True))\n+  (ensures  (little_endian b < pow2 128))\n+  [SMTPat (little_endian b)]\n+let lemma_little_endian_lt_2_128 b =\n+  lemma_little_endian_is_bounded b;\n+  if Seq.length b = 16 then ()\n+  else Math.Lemmas.pow2_lt_compat 128 (8 * Seq.length b)\n+\n+ \n+(* loads a machine integer from a buffer of len bytes *)\n+\n+#reset-options \"--z3timeout 100\" \n+\n+val load_uint32: len:UInt32.t { v len <= 4 } -> buf:lbuffer (v len) -> ST UInt32.t\n+  (requires (fun h0 -> live h0 buf))\n+  (ensures (fun h0 n h1 -> \n+    h0 == h1 /\\ live h0 buf /\\ \n+    UInt32.v n == little_endian (sel_bytes h1 len buf)))\n+\n+let rec load_uint32 len buf = \n+  if len = 0ul then 0ul\n+  else\n+    let len = len -^ 1ul in\n+    let n = load_uint32 len (sub buf 1ul len) in\n+    let b = buf.(0ul) in \n+    FStar.UInt32(uint8_to_uint32 b +^ 256ul *^ n)\n+\n+val load_uint128: len:UInt32.t { v len <= 16 } -> buf:lbuffer (v len) -> ST UInt128.t\n+  (requires (fun h0 -> live h0 buf))\n+  (ensures (fun h0 n h1 -> \n+    h0 == h1 /\\ live h0 buf /\\ \n+    UInt128.v n == little_endian (sel_bytes h1 len buf)))\n+ \n+#reset-options \"--z3timeout 1000\" \n+\n+// 16-10-02 128-bit constants??\n+let rec load_uint128 len buf = \n+  if len = 0ul then uint64_to_uint128 0UL\n+  else\n+    let len = len -^ 1ul in\n+    let n = load_uint128 len (sub buf 1ul len) in\n+    let b = buf.(0ul) in \n+    assume false;\n+    FStar.UInt128(uint64_to_uint128 (uint8_to_uint64 b) +^ uint64_to_uint128 256UL *^ n) \n+//16-10-02 TODO not why this fails; maybe fewer lemmas on UInt128 ? ","path":"examples/low-level/crypto/Crypto.Symmetric.Bytes.fst","position":154,"original_position":154,"commit_id":"aa7d3889b3dff317e2cce02c7aaecd2206029098","original_commit_id":"aa7d3889b3dff317e2cce02c7aaecd2206029098","user":{"login":"s-zanella","id":7451757,"avatar_url":"https://avatars.githubusercontent.com/u/7451757?v=3","gravatar_id":"","url":"https://api.github.com/users/s-zanella","html_url":"https://github.com/s-zanella","followers_url":"https://api.github.com/users/s-zanella/followers","following_url":"https://api.github.com/users/s-zanella/following{/other_user}","gists_url":"https://api.github.com/users/s-zanella/gists{/gist_id}","starred_url":"https://api.github.com/users/s-zanella/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/s-zanella/subscriptions","organizations_url":"https://api.github.com/users/s-zanella/orgs","repos_url":"https://api.github.com/users/s-zanella/repos","events_url":"https://api.github.com/users/s-zanella/events{/privacy}","received_events_url":"https://api.github.com/users/s-zanella/received_events","type":"User","site_admin":false},"body":"Check why this fails\r\n","created_at":"2016-10-03T13:09:43Z","updated_at":"2016-10-03T13:31:12Z","html_url":"https://github.com/FStarLang/FStar/pull/702#discussion_r81546341","pull_request_url":"https://api.github.com/repos/FStarLang/FStar/pulls/702","_links":{"self":{"href":"https://api.github.com/repos/FStarLang/FStar/pulls/comments/81546341"},"html":{"href":"https://github.com/FStarLang/FStar/pull/702#discussion_r81546341"},"pull_request":{"href":"https://api.github.com/repos/FStarLang/FStar/pulls/702"}}},"pull_request":{"url":"https://api.github.com/repos/FStarLang/FStar/pulls/702","id":87695725,"html_url":"https://github.com/FStarLang/FStar/pull/702","diff_url":"https://github.com/FStarLang/FStar/pull/702.diff","patch_url":"https://github.com/FStarLang/FStar/pull/702.patch","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/702","number":702,"state":"open","locked":false,"title":"Feature work on AEAD","user":{"login":"s-zanella","id":7451757,"avatar_url":"https://avatars.githubusercontent.com/u/7451757?v=3","gravatar_id":"","url":"https://api.github.com/users/s-zanella","html_url":"https://github.com/s-zanella","followers_url":"https://api.github.com/users/s-zanella/followers","following_url":"https://api.github.com/users/s-zanella/following{/other_user}","gists_url":"https://api.github.com/users/s-zanella/gists{/gist_id}","starred_url":"https://api.github.com/users/s-zanella/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/s-zanella/subscriptions","organizations_url":"https://api.github.com/users/s-zanella/orgs","repos_url":"https://api.github.com/users/s-zanella/repos","events_url":"https://api.github.com/users/s-zanella/events{/privacy}","received_events_url":"https://api.github.com/users/s-zanella/received_events","type":"User","site_admin":false},"body":"","created_at":"2016-10-03T10:45:13Z","updated_at":"2016-10-03T13:31:12Z","closed_at":null,"merged_at":null,"merge_commit_sha":"5652aeabc99740f11c6ff3d64fba659fc03fdaf8","assignee":null,"assignees":[],"milestone":null,"commits_url":"https://api.github.com/repos/FStarLang/FStar/pulls/702/commits","review_comments_url":"https://api.github.com/repos/FStarLang/FStar/pulls/702/comments","review_comment_url":"https://api.github.com/repos/FStarLang/FStar/pulls/comments{/number}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/702/comments","statuses_url":"https://api.github.com/repos/FStarLang/FStar/statuses/aa7d3889b3dff317e2cce02c7aaecd2206029098","head":{"label":"FStarLang:fournet_aead","ref":"fournet_aead","sha":"aa7d3889b3dff317e2cce02c7aaecd2206029098","user":{"login":"FStarLang","id":7689927,"avatar_url":"https://avatars.githubusercontent.com/u/7689927?v=3","gravatar_id":"","url":"https://api.github.com/users/FStarLang","html_url":"https://github.com/FStarLang","followers_url":"https://api.github.com/users/FStarLang/followers","following_url":"https://api.github.com/users/FStarLang/following{/other_user}","gists_url":"https://api.github.com/users/FStarLang/gists{/gist_id}","starred_url":"https://api.github.com/users/FStarLang/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/FStarLang/subscriptions","organizations_url":"https://api.github.com/users/FStarLang/orgs","repos_url":"https://api.github.com/users/FStarLang/repos","events_url":"https://api.github.com/users/FStarLang/events{/privacy}","received_events_url":"https://api.github.com/users/FStarLang/received_events","type":"Organization","site_admin":false},"repo":{"id":18411972,"name":"FStar","full_name":"FStarLang/FStar","owner":{"login":"FStarLang","id":7689927,"avatar_url":"https://avatars.githubusercontent.com/u/7689927?v=3","gravatar_id":"","url":"https://api.github.com/users/FStarLang","html_url":"https://github.com/FStarLang","followers_url":"https://api.github.com/users/FStarLang/followers","following_url":"https://api.github.com/users/FStarLang/following{/other_user}","gists_url":"https://api.github.com/users/FStarLang/gists{/gist_id}","starred_url":"https://api.github.com/users/FStarLang/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/FStarLang/subscriptions","organizations_url":"https://api.github.com/users/FStarLang/orgs","repos_url":"https://api.github.com/users/FStarLang/repos","events_url":"https://api.github.com/users/FStarLang/events{/privacy}","received_events_url":"https://api.github.com/users/FStarLang/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/FStarLang/FStar","description":"An ML-like language with a type system for program verification","fork":false,"url":"https://api.github.com/repos/FStarLang/FStar","forks_url":"https://api.github.com/repos/FStarLang/FStar/forks","keys_url":"https://api.github.com/repos/FStarLang/FStar/keys{/key_id}","collaborators_url":"https://api.github.com/repos/FStarLang/FStar/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/FStarLang/FStar/teams","hooks_url":"https://api.github.com/repos/FStarLang/FStar/hooks","issue_events_url":"https://api.github.com/repos/FStarLang/FStar/issues/events{/number}","events_url":"https://api.github.com/repos/FStarLang/FStar/events","assignees_url":"https://api.github.com/repos/FStarLang/FStar/assignees{/user}","branches_url":"https://api.github.com/repos/FStarLang/FStar/branches{/branch}","tags_url":"https://api.github.com/repos/FStarLang/FStar/tags","blobs_url":"https://api.github.com/repos/FStarLang/FStar/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/FStarLang/FStar/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/FStarLang/FStar/git/refs{/sha}","trees_url":"https://api.github.com/repos/FStarLang/FStar/git/trees{/sha}","statuses_url":"https://api.github.com/repos/FStarLang/FStar/statuses/{sha}","languages_url":"https://api.github.com/repos/FStarLang/FStar/languages","stargazers_url":"https://api.github.com/repos/FStarLang/FStar/stargazers","contributors_url":"https://api.github.com/repos/FStarLang/FStar/contributors","subscribers_url":"https://api.github.com/repos/FStarLang/FStar/subscribers","subscription_url":"https://api.github.com/repos/FStarLang/FStar/subscription","commits_url":"https://api.github.com/repos/FStarLang/FStar/commits{/sha}","git_commits_url":"https://api.github.com/repos/FStarLang/FStar/git/commits{/sha}","comments_url":"https://api.github.com/repos/FStarLang/FStar/comments{/number}","issue_comment_url":"https://api.github.com/repos/FStarLang/FStar/issues/comments{/number}","contents_url":"https://api.github.com/repos/FStarLang/FStar/contents/{+path}","compare_url":"https://api.github.com/repos/FStarLang/FStar/compare/{base}...{head}","merges_url":"https://api.github.com/repos/FStarLang/FStar/merges","archive_url":"https://api.github.com/repos/FStarLang/FStar/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/FStarLang/FStar/downloads","issues_url":"https://api.github.com/repos/FStarLang/FStar/issues{/number}","pulls_url":"https://api.github.com/repos/FStarLang/FStar/pulls{/number}","milestones_url":"https://api.github.com/repos/FStarLang/FStar/milestones{/number}","notifications_url":"https://api.github.com/repos/FStarLang/FStar/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/FStarLang/FStar/labels{/name}","releases_url":"https://api.github.com/repos/FStarLang/FStar/releases{/id}","deployments_url":"https://api.github.com/repos/FStarLang/FStar/deployments","created_at":"2014-04-03T17:32:49Z","updated_at":"2016-09-30T20:50:31Z","pushed_at":"2016-10-03T12:54:23Z","git_url":"git://github.com/FStarLang/FStar.git","ssh_url":"git@github.com:FStarLang/FStar.git","clone_url":"https://github.com/FStarLang/FStar.git","svn_url":"https://github.com/FStarLang/FStar","homepage":"https://www.fstar-lang.org/","size":91411,"stargazers_count":628,"watchers_count":628,"language":"OCaml","has_issues":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":60,"mirror_url":null,"open_issues_count":219,"forks":60,"open_issues":219,"watchers":628,"default_branch":"master"}},"base":{"label":"FStarLang:master","ref":"master","sha":"a3b54148a9f9013a68177d83ec4fee4bcaf481a5","user":{"login":"FStarLang","id":7689927,"avatar_url":"https://avatars.githubusercontent.com/u/7689927?v=3","gravatar_id":"","url":"https://api.github.com/users/FStarLang","html_url":"https://github.com/FStarLang","followers_url":"https://api.github.com/users/FStarLang/followers","following_url":"https://api.github.com/users/FStarLang/following{/other_user}","gists_url":"https://api.github.com/users/FStarLang/gists{/gist_id}","starred_url":"https://api.github.com/users/FStarLang/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/FStarLang/subscriptions","organizations_url":"https://api.github.com/users/FStarLang/orgs","repos_url":"https://api.github.com/users/FStarLang/repos","events_url":"https://api.github.com/users/FStarLang/events{/privacy}","received_events_url":"https://api.github.com/users/FStarLang/received_events","type":"Organization","site_admin":false},"repo":{"id":18411972,"name":"FStar","full_name":"FStarLang/FStar","owner":{"login":"FStarLang","id":7689927,"avatar_url":"https://avatars.githubusercontent.com/u/7689927?v=3","gravatar_id":"","url":"https://api.github.com/users/FStarLang","html_url":"https://github.com/FStarLang","followers_url":"https://api.github.com/users/FStarLang/followers","following_url":"https://api.github.com/users/FStarLang/following{/other_user}","gists_url":"https://api.github.com/users/FStarLang/gists{/gist_id}","starred_url":"https://api.github.com/users/FStarLang/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/FStarLang/subscriptions","organizations_url":"https://api.github.com/users/FStarLang/orgs","repos_url":"https://api.github.com/users/FStarLang/repos","events_url":"https://api.github.com/users/FStarLang/events{/privacy}","received_events_url":"https://api.github.com/users/FStarLang/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/FStarLang/FStar","description":"An ML-like language with a type system for program verification","fork":false,"url":"https://api.github.com/repos/FStarLang/FStar","forks_url":"https://api.github.com/repos/FStarLang/FStar/forks","keys_url":"https://api.github.com/repos/FStarLang/FStar/keys{/key_id}","collaborators_url":"https://api.github.com/repos/FStarLang/FStar/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/FStarLang/FStar/teams","hooks_url":"https://api.github.com/repos/FStarLang/FStar/hooks","issue_events_url":"https://api.github.com/repos/FStarLang/FStar/issues/events{/number}","events_url":"https://api.github.com/repos/FStarLang/FStar/events","assignees_url":"https://api.github.com/repos/FStarLang/FStar/assignees{/user}","branches_url":"https://api.github.com/repos/FStarLang/FStar/branches{/branch}","tags_url":"https://api.github.com/repos/FStarLang/FStar/tags","blobs_url":"https://api.github.com/repos/FStarLang/FStar/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/FStarLang/FStar/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/FStarLang/FStar/git/refs{/sha}","trees_url":"https://api.github.com/repos/FStarLang/FStar/git/trees{/sha}","statuses_url":"https://api.github.com/repos/FStarLang/FStar/statuses/{sha}","languages_url":"https://api.github.com/repos/FStarLang/FStar/languages","stargazers_url":"https://api.github.com/repos/FStarLang/FStar/stargazers","contributors_url":"https://api.github.com/repos/FStarLang/FStar/contributors","subscribers_url":"https://api.github.com/repos/FStarLang/FStar/subscribers","subscription_url":"https://api.github.com/repos/FStarLang/FStar/subscription","commits_url":"https://api.github.com/repos/FStarLang/FStar/commits{/sha}","git_commits_url":"https://api.github.com/repos/FStarLang/FStar/git/commits{/sha}","comments_url":"https://api.github.com/repos/FStarLang/FStar/comments{/number}","issue_comment_url":"https://api.github.com/repos/FStarLang/FStar/issues/comments{/number}","contents_url":"https://api.github.com/repos/FStarLang/FStar/contents/{+path}","compare_url":"https://api.github.com/repos/FStarLang/FStar/compare/{base}...{head}","merges_url":"https://api.github.com/repos/FStarLang/FStar/merges","archive_url":"https://api.github.com/repos/FStarLang/FStar/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/FStarLang/FStar/downloads","issues_url":"https://api.github.com/repos/FStarLang/FStar/issues{/number}","pulls_url":"https://api.github.com/repos/FStarLang/FStar/pulls{/number}","milestones_url":"https://api.github.com/repos/FStarLang/FStar/milestones{/number}","notifications_url":"https://api.github.com/repos/FStarLang/FStar/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/FStarLang/FStar/labels{/name}","releases_url":"https://api.github.com/repos/FStarLang/FStar/releases{/id}","deployments_url":"https://api.github.com/repos/FStarLang/FStar/deployments","created_at":"2014-04-03T17:32:49Z","updated_at":"2016-09-30T20:50:31Z","pushed_at":"2016-10-03T12:54:23Z","git_url":"git://github.com/FStarLang/FStar.git","ssh_url":"git@github.com:FStarLang/FStar.git","clone_url":"https://github.com/FStarLang/FStar.git","svn_url":"https://github.com/FStarLang/FStar","homepage":"https://www.fstar-lang.org/","size":91411,"stargazers_count":628,"watchers_count":628,"language":"OCaml","has_issues":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":60,"mirror_url":null,"open_issues_count":219,"forks":60,"open_issues":219,"watchers":628,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/FStarLang/FStar/pulls/702"},"html":{"href":"https://github.com/FStarLang/FStar/pull/702"},"issue":{"href":"https://api.github.com/repos/FStarLang/FStar/issues/702"},"comments":{"href":"https://api.github.com/repos/FStarLang/FStar/issues/702/comments"},"review_comments":{"href":"https://api.github.com/repos/FStarLang/FStar/pulls/702/comments"},"review_comment":{"href":"https://api.github.com/repos/FStarLang/FStar/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/FStarLang/FStar/pulls/702/commits"},"statuses":{"href":"https://api.github.com/repos/FStarLang/FStar/statuses/aa7d3889b3dff317e2cce02c7aaecd2206029098"}}}}
{"actor":{"display_login":"s-zanella"}}