1 files changed, 64 insertions, 0 deletions
diff --git a/handwritten_support/mem_metadata.glob b/handwritten_support/mem_metadata.glob
new file mode 100644
index 0000000..c2d0ccd
--- /dev/null
+++ b/handwritten_support/mem_metadata.glob
@@ -0,0 +1,64 @@
+DIGEST 693b57d74f776ae8bd215fbfc8b03df3
+Fmem_metadata
+R15:23 Sail.Base <> <> lib
+def 52:60 <> write_ram
+binder 63:64 <> rv:1
+binder 66:66 <> e:2
+binder 68:68 <> a:3
+binder 71:72 <> wk:4
+R82:86 Sail.Values <> mword def
+R88:88 mem_metadata <> a:3 var
+binder 75:78 <> addr:5
+binder 91:94 <> size:6
+R101:105 Sail.Values <> mword def
+R109:111 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R112:115 mem_metadata <> size:6 var
+binder 97:97 <> v:7
+R127:130 Coq.Init.Datatypes <> unit ind
+binder 120:123 <> meta:8
+R135:139 Sail.Prompt_monad <> monad ind
+R141:142 mem_metadata <> rv:1 var
+R144:147 Coq.Init.Datatypes <> bool ind
+R149:149 mem_metadata <> e:2 var
+R154:162 Sail.Prompt_monad <> write_mem def
+R179:179 mem_metadata <> v:7 var
+R174:177 mem_metadata <> size:6 var
+R169:172 mem_metadata <> addr:5 var
+R167:167 mem_metadata <> a:3 var
+R164:165 mem_metadata <> wk:4 var
+def 194:201 <> read_ram
+binder 204:205 <> rv:9
+binder 207:207 <> e:10
+binder 209:209 <> a:11
+binder 212:213 <> rk:12
+R223:227 Sail.Values <> mword def
+R229:229 mem_metadata <> a:11 var
+binder 216:219 <> addr:13
+binder 232:235 <> size:14
+R249:252 Coq.Init.Datatypes <> bool ind
+binder 238:245 <> read_tag:15
+R257:265 Sail.Values <> ArithFact class
+R272:276 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R268:271 mem_metadata <> size:14 var
+binder 257:278 <> H:16
+R283:287 Sail.Prompt_monad <> monad ind
+R289:290 mem_metadata <> rv:9 var
+R309:311 Coq.Init.Datatypes <> ::type_scope:x_'*'_x not
+R293:297 Sail.Values <> mword def
+R301:303 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R304:307 mem_metadata <> size:14 var
+R312:315 Coq.Init.Datatypes <> unit ind
+R318:318 mem_metadata <> e:10 var
+R348:352 Sail.Prompt_monad <> :::x_'>>='_x not
+R325:332 Sail.Prompt_monad <> read_mem def
+R344:347 mem_metadata <> size:14 var
+R339:342 mem_metadata <> addr:13 var
+R337:337 mem_metadata <> a:11 var
+R334:335 mem_metadata <> rk:12 var
+binder 357:360 <> data:17
+R367:373 Sail.Prompt_monad <> returnm def
+R375:375 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
+R380:381 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
+R384:384 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
+R376:379 mem_metadata <> data:17 var
+R382:383 Coq.Init.Datatypes <> tt constr